diff options
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 20 |
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 |