Add ternaries, simplifications. BIG BUG FOUND (init/reset translation)

1 files changed, 68 insertions, 0 deletions

diff --git a/abstract/formula.ml b/abstract/formula.ml
index 0045489..1882c85 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -48,6 +48,8 @@ type bool_expr =
   (* boolean operators *)
   | BAnd of bool_expr * bool_expr
   | BOr of bool_expr * bool_expr
+  | BTernary of bool_expr * bool_expr * bool_expr
+      (* (A and B) or ((not A) and C) *)
   | BNot of bool_expr
 
 let is_false = function
@@ -71,6 +73,11 @@ let f_or a b =
   else if is_false b then a
   else BOr(a, b)
 
+let f_ternary c a b =
+  if is_true c then a
+  else if is_false c then b
+  else BTernary(c, a, b)
+
 let f_e_op op a b = match a, b with
   | EItem i, EItem j -> BConst (if op = E_EQ then i = j else i <> j)
   | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v)
@@ -82,6 +89,8 @@ let rec eliminate_not = function
   | BNot e -> eliminate_not_negate e
   | BAnd(a, b) -> BAnd(eliminate_not a, eliminate_not b)
   | BOr(a, b) -> BOr(eliminate_not a, eliminate_not b)
+  | BTernary(c, a, b) ->
+    BTernary(eliminate_not c, eliminate_not a, eliminate_not b)
   | x -> x
 and eliminate_not_negate = function
   | BConst x -> BConst(not x)
@@ -100,6 +109,7 @@ and eliminate_not_negate = function
       | AST_GE -> AST_LT
       in
       BRel(r', a, b, is_real)
+  | BTernary _ -> assert false
   | BAnd(a, b) ->
     BOr(eliminate_not_negate a, eliminate_not_negate b)
   | BOr(a, b) ->
@@ -159,4 +169,62 @@ let rec conslist_of_f = function
       | _, CLTrue -> econs, cons, ra
       | _, _ -> econs, cons, CLAnd(ra, rb)
     end
+  | BTernary(c, a, b) ->
+    conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b)))
+
 
+
+(*
+  Simplify formula considering something is true
+*)
+
+let rec get_root_true = function
+  | BAnd(a, b) ->
+    get_root_true a @ get_root_true b
+  | BEnumCons e -> [BEnumCons e]
+  | BRel (a, b, c, d) -> [BRel (a, b, c, d)]
+  | _ -> []
+
+let rec simplify true_eqs e =
+  if List.exists
+      (fun f ->
+        try eliminate_not e = eliminate_not f with _ -> false)
+      true_eqs
+    then BConst true
+  else if List.exists
+      (fun f ->
+        match e, f with
+        | BEnumCons(E_EQ, a, EItem v), BEnumCons(E_EQ, b, EItem w)
+          when a = b && v <> w -> true
+        | _ -> try eliminate_not e = eliminate_not_negate f with _ -> false)
+      true_eqs
+    then BConst false
+  else
+    match e with
+    | BAnd(a, b) ->
+      f_and
+        (simplify true_eqs a)
+        (simplify true_eqs b)
+    | BOr(a, b) ->
+      f_or
+        (simplify true_eqs a)
+        (simplify true_eqs b)
+    | BTernary(c, a, b) ->
+      let c, a, b =
+        simplify true_eqs c,
+        simplify true_eqs a,
+        simplify true_eqs b in
+      begin match c with
+      | BConst true -> a
+      | BConst false -> b
+      | _ -> BTernary(c, a, b)
+      end
+    | BNot(n) ->
+      begin match simplify true_eqs n with
+      | BConst e -> BConst (not e)
+      | x -> BNot x
+      end
+    | v -> v
+    
+let rec simplify_k true_eqs e =
+  List.fold_left f_and (simplify true_eqs e) true_eqs