diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-19 10:51:59 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-19 10:51:59 +0200 |
| commit | 8286c7c23a47c166aa87337a3146cdf3b278b144 (patch) | |
| tree | 8126efa61eb9af62d1c4e97b504e78d5e9c772df /abstract/formula.ml | |
| parent | a2da1268c4a9af6755723698b7b6ba669aa7fd46 (diff) | |
| download | scade-analyzer-8286c7c23a47c166aa87337a3146cdf3b278b144.tar.gz scade-analyzer-8286c7c23a47c166aa87337a3146cdf3b278b144.zip | |
Isolate numerical part of domain. Next: isolate numerical part of equations.
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index f3c1df1..a598750 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -2,6 +2,9 @@ open Ast (* AST for logical formulas *) + +(* Numerical part *) + type num_expr = (* constants *) | NIntConst of int @@ -12,6 +15,13 @@ type num_expr = (* identifier *) | NIdent of id +type num_cons_op = + | CONS_EQ | CONS_NE + | CONS_GT | CONS_GE +type num_cons = num_expr * num_cons_op (* always imply right member = 0 *) + + +(* Logical part *) type bool_expr = (* constants *) @@ -24,7 +34,6 @@ 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 -> BConst false | BConst true, b -> b @@ -67,17 +76,14 @@ and eliminate_not_negate = function | BOr(a, b) -> BAnd(eliminate_not_negate a, eliminate_not_negate b) + + (* In big ANDs, try to separate levels of /\ and levels of \/ We also use this step to simplify trues and falses that may be present. *) -type cons_op = - | CONS_EQ | CONS_NE - | CONS_GT | CONS_GE -type cons = num_expr * cons_op (* always imply right member = 0 *) - -type conslist = cons list * conslist_bool_expr +type conslist = num_cons list * conslist_bool_expr and conslist_bool_expr = | CLTrue | CLFalse |