Write transformation of program into logical formula.

1 files changed, 78 insertions, 0 deletions

diff --git a/abstract/formula.ml b/abstract/formula.ml
index 389000c..2c83b32 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -22,3 +22,81 @@ type bool_expr =
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
+
+
+(* Write all formula without using the NOT operator *)
+
+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)
+  | x -> x
+and eliminate_not_negate = function
+  | BConst x -> BConst(not x)
+  | BNot e -> eliminate_not e
+  | BRel(r, a, b) ->
+    let r' = match r with
+    | AST_EQ -> AST_NE
+    | AST_NE -> AST_EQ
+    | AST_LT -> AST_GE
+    | AST_LE -> AST_GT
+    | AST_GT -> AST_LE
+    | AST_GE -> AST_LT
+    in
+    BRel(r', a, b)
+  | BAnd(a, b) ->
+    BOr(eliminate_not_negate a, eliminate_not_negate b)
+  | BOr(a, b) ->
+    BAnd(eliminate_not_negate a, eliminate_not_negate b)
+
+(*
+  In big ANDs, try to separate levels of /\ and levels of \/
+  We also use this step to simplify trues and falses that may be present.
+*)
+
+type cons_op =
+  | CONS_EQ | CONS_NE
+  | CONS_GT | CONS_GE
+type cons = num_expr * cons_op  (* always imply right member = 0 *)
+
+type conslist = cons list * conslist_bool_expr
+and conslist_bool_expr =
+  | CLTrue
+  | CLFalse
+  | CLAnd of conslist_bool_expr * conslist_bool_expr
+  | CLOr of conslist * conslist
+
+let rec conslist_of_f = function
+  | BNot e -> conslist_of_f (eliminate_not_negate e)
+  | BRel (op, a, b) ->
+    let cons = match op with
+      | AST_EQ -> NBinary(AST_MINUS, a, b), CONS_EQ
+      | AST_NE -> NBinary(AST_MINUS, a, b), CONS_NE
+      | AST_GT -> NBinary(AST_MINUS, a, b), CONS_GT
+      | AST_GE -> NBinary(AST_MINUS, a, b), CONS_GE
+      | AST_LT -> NBinary(AST_MINUS, b, a), CONS_GT
+      | AST_LE -> NBinary(AST_MINUS, b, a), CONS_GE
+    in [cons], CLTrue
+  | BConst x ->
+    [], if x then CLTrue else CLFalse
+  | 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))
+    end
+  | BAnd(a, b) ->
+    let ca, ra = conslist_of_f a in
+    let cb, rb = conslist_of_f b in
+    let cons = ca @ cb in
+    begin match ra, rb with
+      | CLFalse, _ | _, CLFalse -> [], CLFalse
+      | CLTrue, _ -> cons, rb
+      | ra, CLTrue -> cons, ra
+      | _, _ -> cons, CLAnd(ra, rb)
+    end
+