1 files changed, 108 insertions, 25 deletions

diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 7e626f0..994c82a 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -1,6 +1,15 @@
+open Ast
 open Formula
 open Ast_printer
 
+let string_of_binary_rel = function
+  | AST_EQ -> "="
+  | AST_NE -> "≠"
+  | AST_LT -> "<"
+  | AST_LE -> "≤"
+  | AST_GT -> ">"
+  | AST_GE -> "≥"
+
 let ne_prec = function
   | NUnary(op, _) -> unary_precedence
   | NBinary(op, _, _) -> binary_op_precedence op
@@ -13,44 +22,118 @@ let be_prec = function
   | BNot _ -> unary_precedence
   | _ -> 100
 
+let is_or = function
+  | BOr _ -> true
+  | _ -> false
+let is_and = function
+  | BAnd _ -> true
+  | _ -> false
+
 
-let print_lh fmt pf fa a fe e =
+let print_ch fmt pf fa a fe e =
   if fa a < fe e
-    then Format.fprintf fmt "@[<2>(%a)@]" pf a
-    else Format.fprintf fmt "%a" pf a
-let print_rh fmt pf fb b fe e =
-  if fb b < fe e
-    then Format.fprintf fmt "@[<2>(%a)@]" pf b
-    else Format.fprintf fmt "%a" pf b
+    then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
+    else Format.fprintf fmt "@[<hv 2>%a@]" pf a
+let print_ah fmt pf fa a fe e =
+  if fa a <= fe e
+    then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
+    else Format.fprintf fmt "@[<hv 2>%a@]" pf a
 
 let rec print_num_expr fmt e = match e with
   | NIntConst i -> Format.fprintf fmt "%d" i
   | NRealConst f -> Format.fprintf fmt "%f" f
-  | NIdent id -> Format.fprintf fmt "%s" id
+  | NIdent id ->
+    let re = Str.regexp "/" in
+    Format.fprintf fmt "%s" (Str.global_replace re "·" id)
   | NBinary(op, a, b) ->
-    print_lh fmt print_num_expr ne_prec a ne_prec e;
-    Format.fprintf fmt "@ %s@ " (string_of_binary_op op);
-    print_rh fmt print_num_expr ne_prec b ne_prec e
+    print_ch fmt print_num_expr ne_prec a ne_prec e;
+    Format.fprintf fmt "@ %s " (string_of_binary_op op);
+    print_ah fmt print_num_expr ne_prec b ne_prec e
   | NUnary(op, a) ->
-    Format.pp_print_string fmt (string_of_unary_op op);
-    print_rh fmt print_num_expr ne_prec a ne_prec e
+    Format.fprintf fmt "%s " (string_of_unary_op op);
+    print_ah fmt print_num_expr ne_prec a ne_prec e
+
+(* Print boolean form of formula *)
 
 let rec print_bool_expr fmt e = match e with
   | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
   | BRel(op, a, b) ->
-    print_lh fmt print_num_expr ne_prec a be_prec e;
-    Format.fprintf fmt "@ %s@ " (string_of_binary_rel op);
-    print_rh fmt print_num_expr ne_prec b be_prec e
+    print_ch fmt print_num_expr ne_prec a be_prec e;
+    Format.fprintf fmt "@ %s " (string_of_binary_rel op);
+    print_ch fmt print_num_expr ne_prec b be_prec e
   | BAnd (a, b) ->
-    print_lh fmt print_bool_expr be_prec a be_prec e;
-    Format.fprintf fmt "@ /\\@ ";
-    print_rh fmt print_bool_expr be_prec b be_prec e
+
+    if is_and a then
+      Format.fprintf fmt "%a" print_bool_expr a
+    else
+      if be_prec a < be_prec e || is_or a
+        then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr a
+        else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr a;
+    Format.fprintf fmt "@ ∧ ";
+    if is_and b then
+        Format.fprintf fmt "%a" print_bool_expr b
+    else
+      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_lh fmt print_bool_expr be_prec a be_prec e;
-    Format.fprintf fmt "@ \\/@ ";
-    print_rh fmt print_bool_expr be_prec b be_prec e
+    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
   | BNot (a) ->
-    Format.pp_print_string fmt "!";
-    print_rh fmt print_bool_expr be_prec a be_prec e
+    Format.pp_print_string fmt "¬";
+    print_ch fmt print_bool_expr be_prec a be_prec e
+
+let print_expr fmt e =
+  Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr e
+
+
+(* Print constraint list form of formula *)
+
+let print_cons fmt (eq, sg) =
+  let sg_str = match sg with
+  | CONS_EQ -> "="
+  | CONS_NE -> "≠"
+  | CONS_GT -> ">"
+  | CONS_GE -> "≥"
+  in
+  Format.fprintf fmt "@[<hv 2>%a %s 0@]"
+    print_num_expr eq sg_str
+
+let rec print_conslist fmt (cons, e) =
+  let rec aux = function
+    | [] -> false
+    | [a] ->
+      Format.fprintf fmt "@[<hv 2>%a@]" print_cons a; true
+    | p::q ->
+      Format.fprintf fmt "@[<hv 2>%a@]" print_cons p;
+      Format.fprintf fmt "@ ∧ ";
+      aux q
+  in
+  match e with
+  | CLTrue ->
+    Format.fprintf fmt "@[<hv 2>(";
+    ignore (aux cons);
+    Format.fprintf fmt ")@]"
+  | CLFalse -> 
+    Format.fprintf fmt "false"
+  | _ ->
+    Format.fprintf fmt "@[<hv 2>(";
+    if aux cons then Format.fprintf fmt "@ ∧ ";
+    print_conslist_expr fmt e;
+    Format.fprintf fmt ")@]"
+
+and print_conslist_expr fmt = function
+  | CLTrue -> Format.fprintf fmt "true"
+  | CLFalse -> Format.fprintf fmt "false"
+  | CLOr(a, b) ->
+    Format.fprintf fmt "@[<hv 2>(%a@ ∨ %a)@]"
+        print_conslist a
+        print_conslist b
+  | CLAnd(a, b) ->
+    Format.fprintf fmt "%a@ ∧ %a"
+        print_conslist_expr a
+        print_conslist_expr b
+
 
-let print_expr = print_bool_expr