summaryrefslogtreecommitdiff
path: root/abstract/formula_printer.ml
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-18 15:31:03 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-18 15:31:03 +0200
commit43487d3baf695875482454ade1bdbc1403bfaaf6 (patch)
tree3718a44913fc1544d7ddfbe5fdb5d909e162ca9b /abstract/formula_printer.ml
parent0caa1ebe947646459295c6a66da6bf19f399c21e (diff)
downloadscade-analyzer-43487d3baf695875482454ade1bdbc1403bfaaf6.tar.gz
scade-analyzer-43487d3baf695875482454ade1bdbc1403bfaaf6.zip
Add gilbreath suite ; booleans are not represented in a good way.
Diffstat (limited to 'abstract/formula_printer.ml')
-rw-r--r--abstract/formula_printer.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 53a9b6a..1b31ba1 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -60,6 +60,11 @@ let rec print_num_expr fmt e = match e with
let rec print_bool_expr fmt e = match e with
| BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
+ | BBoolEq(id, v) ->
+ if v then
+ Format.fprintf fmt "%a" print_id id
+ else
+ Format.fprintf fmt "¬%a" print_id id
| BRel(op, a, b) ->
print_ch fmt print_num_expr ne_prec a be_prec e;
Format.fprintf fmt "@ %s " (string_of_binary_rel op);