Add gilbreath suite ; booleans are not represented in a good way.

1 files changed, 20 insertions, 0 deletions

diff --git a/abstract/formula.ml b/abstract/formula.ml
index 262bccb..44495c4 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -12,17 +12,31 @@ type num_expr =
   (* identifier *)
   | NIdent of id
 
+
 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
   (* boolean operators *)
   | BAnd of bool_expr * bool_expr
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
 
+let f_and a b = match a, b with
+  | BConst false, _ | _, BConst false -> BConst false
+  | BConst true, b -> b
+  | a, BConst true -> a
+  | a, b -> BAnd(a, b)
+
+let f_or a b = match a, b with
+  | BConst true, _ | _, BConst true -> BConst true
+  | BConst false, b -> b
+  | a, BConst false -> a
+  | a, b -> BOr(a, b)
+
 
 (* Write all formula without using the NOT operator *)
 
@@ -33,6 +47,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)
   | BNot e -> eliminate_not e
   | BRel(r, a, b) ->
     let r' = match r with
@@ -83,6 +98,11 @@ let rec conslist_of_f = function
     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
   | BOr(a, b) ->
     let ca, ra = conslist_of_f a in
     let cb, rb = conslist_of_f b in