First implementation of resetting transitions.

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)