1 files changed, 40 insertions, 24 deletions

diff --git a/abstract/formula.ml b/abstract/formula.ml
index a598750..ce83935 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -1,4 +1,6 @@
 open Ast
+open Util
+open Ast_util
 
 (* AST for logical formulas *)
 
@@ -23,12 +25,24 @@ type num_cons = num_expr * num_cons_op  (* always imply right member = 0 *)
 
 (* Logical part *)
 
+
+(* Enumerated types *)
+type enum_expr =
+  | EIdent of id
+  | EItem of string
+
+type enum_op =
+  | E_EQ | E_NE
+
+type enum_cons = enum_op * enum_expr * enum_expr
+
 type bool_expr =
   (* constants *)
   | BConst of bool
   (* operators from numeric values to boolean values *)
   | BRel of binary_rel_op * num_expr * num_expr
-  | BBoolEq of id * bool
+  (* operators on enumerated types *)
+  | BEnumCons of enum_cons
   (* boolean operators *)
   | BAnd of bool_expr * bool_expr
   | BOr of bool_expr * bool_expr
@@ -46,6 +60,10 @@ let f_or a b = match a, b with
   | a, BConst false -> a
   | a, b -> BOr(a, b)
 
+let f_e_eq a b = match a, b with
+  | EItem u, EItem v -> BConst (u = v)
+  | _ -> BEnumCons(E_EQ, a, b)
+
 
 (* Write all formula without using the NOT operator *)
 
@@ -56,7 +74,7 @@ let rec eliminate_not = function
   | x -> x
 and eliminate_not_negate = function
   | BConst x -> BConst(not x)
-  | BBoolEq(id, v) -> BBoolEq(id, not v)
+  | BEnumCons(op, a, b) -> BEnumCons((if op = E_EQ then E_NE else E_EQ), a, b)
   | BNot e -> eliminate_not e
   | BRel(r, a, b) ->
     if r = AST_EQ then
@@ -83,7 +101,7 @@ and eliminate_not_negate = function
   We also use this step to simplify trues and falses that may be present.
 *)
 
-type conslist = num_cons list * conslist_bool_expr
+type conslist = enum_cons list * num_cons list * conslist_bool_expr
 and conslist_bool_expr =
   | CLTrue
   | CLFalse
@@ -104,32 +122,30 @@ let rec conslist_of_f = function
     let cons = if y = NIntConst 0
       then (x, op)
       else (NBinary(AST_MINUS, x, y), op)
-    in [cons], CLTrue
+    in [], [cons], CLTrue
   | BConst x ->
-    [], if x then CLTrue else CLFalse
-  | BBoolEq(id, v) ->
-    if v then
-      [NBinary(AST_MINUS, NIdent id, NIntConst 1), CONS_EQ], CLTrue
-    else
-      [NIdent id, CONS_EQ], CLTrue
+    [], [], if x then CLTrue else CLFalse
+  | BEnumCons e ->
+    [e], [], CLTrue
   | BOr(a, b) ->
-    let ca, ra = conslist_of_f a in
-    let cb, rb = conslist_of_f b in
-    begin match ca, ra, cb, rb with
-      | _, CLFalse, _, _ -> cb, rb
-      | _, _, _, CLFalse -> ca, ra
-      | [], CLTrue, _, _ -> [], CLTrue
-      | _, _, [], CLTrue -> [], CLTrue
-      | _ -> [], CLOr((ca, ra), (cb, rb))
+    let eca, ca, ra = conslist_of_f a in
+    let ecb, cb, rb = conslist_of_f b in
+    begin match eca, ca, ra, ecb, cb, rb with
+      | _, _, CLFalse, _, _, _ -> ecb, cb, rb
+      | _, _, _, _, _, CLFalse -> eca, ca, ra
+      | [], [], CLTrue, _, _, _ -> [], [], CLTrue
+      | _, _, _, [], [], CLTrue -> [], [], CLTrue
+      | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb))
     end
   | BAnd(a, b) ->
-    let ca, ra = conslist_of_f a in
-    let cb, rb = conslist_of_f b in
+    let eca, ca, ra = conslist_of_f a in
+    let ecb, cb, rb = conslist_of_f b in
     let cons = ca @ cb in
+    let econs = eca @ ecb in
     begin match ra, rb with
-      | CLFalse, _ | _, CLFalse -> [], CLFalse
-      | CLTrue, _ -> cons, rb
-      | ra, CLTrue -> cons, ra
-      | _, _ -> cons, CLAnd(ra, rb)
+      | CLFalse, _ | _, CLFalse -> [], [], CLFalse
+      | CLTrue, _ -> econs, cons, rb
+      | _, CLTrue -> econs, cons, ra
+      | _, _ -> econs, cons, CLAnd(ra, rb)
     end