summaryrefslogtreecommitdiff
path: root/abstract/formula_printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'abstract/formula_printer.ml')
-rw-r--r--abstract/formula_printer.ml8
1 files changed, 7 insertions, 1 deletions
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 9c6c403..a5359a8 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -17,6 +17,7 @@ let ne_prec = function
| _ -> 100
let be_prec = function
+ | BTernary _ -> 10
| BRel(op, _, _, _) -> binary_rel_precedence op
| BAnd _ -> binary_bool_precedence AST_AND
| BOr _ -> binary_bool_precedence AST_OR
@@ -97,11 +98,16 @@ let rec print_bool_expr fmt e = match e with
if be_prec b < be_prec e || is_or b
then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr b
else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr b
-
| BOr (a, b) ->
print_ch fmt print_bool_expr be_prec a be_prec e;
Format.fprintf fmt "@ ∨ ";
print_ch fmt print_bool_expr be_prec b be_prec e
+ | BTernary(c, a, b) ->
+ print_ah fmt print_bool_expr be_prec c be_prec e;
+ Format.fprintf fmt "@ ? ";
+ print_ah fmt print_bool_expr be_prec a be_prec e;
+ Format.fprintf fmt "@ : ";
+ print_ah fmt print_bool_expr be_prec b be_prec e;
| BNot (a) ->
Format.pp_print_string fmt "¬";
print_ch fmt print_bool_expr be_prec a be_prec e