diff options
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index f2a3bd1..650f8f4 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -76,8 +76,9 @@ let f_or a b = let f_ternary c a b = if is_true c then a else if is_false c then b - else - BTernary(c, a, b) + else if is_true a && is_false b then c + else if is_true b && is_false a then BNot c + else BTernary(c, 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) @@ -263,3 +264,15 @@ let rec formula_replace_evars repls e = | x -> x + +(* + extract names of variables referenced in formula +*) + +let rec refd_evars_of_f = function + | BAnd (a, b) | BOr(a, b) -> refd_evars_of_f a @ refd_evars_of_f b + | BNot a -> refd_evars_of_f a + | BTernary(a, b, c) -> refd_evars_of_f a @ refd_evars_of_f b @ refd_evars_of_f c + | BEnumCons(_, e, EItem _) -> [e] + | BEnumCons(_, e, EIdent f) -> [e; f] + | _ -> [] |