diff options
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index 9c0ff71..0045489 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -50,20 +50,26 @@ type 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 - | BNot (BConst true), _ | _, BNot (BConst true) -> BConst false - | BConst true, b -> b - | a, BConst true -> a - | a, b -> BAnd(a, b) +let is_false = function + | BConst false | BNot(BConst true) -> true + | _ -> false +let is_true = function + | BConst true | BNot(BConst false) -> true + | _ -> false + +let f_and a b = + if is_false a || is_false b then BConst false + else if is_true a then b + else if is_true b then a + else BAnd(a, b) let f_and_list = List.fold_left f_and (BConst true) -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) +let f_or a b = + if is_true a || is_true b then BConst true + else if is_false a then b + else if is_false b then a + else BOr(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) |