Did most of the boring stuff. Now, work on the abstract domain.

1 files changed, 28 insertions, 11 deletions

diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
index 1b31ba1..44f2d39 100644
--- a/abstract/formula_printer.ml
+++ b/abstract/formula_printer.ml
@@ -1,3 +1,4 @@
+open Util
 open Ast
 open Formula
 open Ast_printer
@@ -56,15 +57,24 @@ let rec print_num_expr fmt e = match e with
     Format.fprintf fmt "%s " (string_of_unary_op op);
     print_ah fmt print_num_expr ne_prec a ne_prec e
 
+(* Enumeated expressions *)
+let print_enum_expr fmt = function
+  | EIdent id -> Format.fprintf fmt "%s" id
+  | EItem x -> Format.fprintf fmt "%s" x
+
+let str_of_enum_op = function
+  | E_EQ -> "≡"
+  | E_NE -> "≢"
+
+let print_econs fmt (op, a, b) =
+    Format.fprintf fmt "%a %s %a"
+      print_enum_expr a (str_of_enum_op op) print_enum_expr b
+
 (* 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")
-  | BBoolEq(id, v) ->
-    if v then
-      Format.fprintf fmt "%a" print_id id
-    else
-      Format.fprintf fmt "¬%a" print_id id
+  | BEnumCons c -> print_econs fmt c
   | 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);
@@ -112,26 +122,33 @@ let print_cons fmt (eq, sg) =
   Format.fprintf fmt "@[<hv 2>%a %a 0@]"
     print_num_expr eq print_cons_sg sg
 
-let rec print_conslist fmt (cons, e) =
+let rec print_conslist fmt (econs, cons, e) =
+  let c = 
+    (List.map (fun x -> Left x) econs) @ (List.map (fun y -> Right y) cons)
+  in
+  let f fmt = function
+    | Left x -> Format.fprintf fmt "@[<hv 2>%a@]" print_econs x
+    | Right x -> Format.fprintf fmt "@[<hv 2>%a@]" print_cons x
+  in
   let rec aux = function
     | [] -> false
     | [a] ->
-      Format.fprintf fmt "@[<hv 2>%a@]" print_cons a; true
+      f fmt a; true
     | p::q ->
-      Format.fprintf fmt "@[<hv 2>%a@]" print_cons p;
+      f fmt p;
       Format.fprintf fmt "@ ∧ ";
       aux q
   in
   match e with
   | CLTrue ->
     Format.fprintf fmt "@[<hv 2>(";
-    ignore (aux cons);
+    ignore (aux c);
     Format.fprintf fmt ")@]"
   | CLFalse -> 
     Format.fprintf fmt "false"
   | _ ->
     Format.fprintf fmt "@[<hv 2>(";
-    if aux cons then Format.fprintf fmt "@ ∧ ";
+    if aux c then Format.fprintf fmt "@ ∧ ";
     print_conslist_expr fmt e;
     Format.fprintf fmt ")@]"
 
@@ -140,7 +157,7 @@ and print_conslist_expr fmt = function
   | CLFalse -> Format.fprintf fmt "false"
   | CLOr(a, b) ->
     Format.fprintf fmt "@[<hv 2>(%a@ ∨ %a)@]"
-        print_conslist a
+       print_conslist a
         print_conslist b
   | CLAnd(a, b) ->
     Format.fprintf fmt "%a@ ∧ %a"