diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-18 11:34:36 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-18 11:34:36 +0200 |
| commit | 5ac14cee1bdb9f2ccc40ad6eb1841b5c2ed584d1 (patch) | |
| tree | c03d6741f565f1ed5a5b27efb2c96a8d9a098581 /abstract/formula.ml | |
| parent | f04de3faad13a3904836dd1bd8c334b6634d60a4 (diff) | |
| download | scade-analyzer-5ac14cee1bdb9f2ccc40ad6eb1841b5c2ed584d1.tar.gz scade-analyzer-5ac14cee1bdb9f2ccc40ad6eb1841b5c2ed584d1.zip | |
Pretty printing.
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index 2c83b32..262bccb 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -69,13 +69,17 @@ and conslist_bool_expr = let rec conslist_of_f = function | BNot e -> conslist_of_f (eliminate_not_negate e) | BRel (op, a, b) -> - let cons = match op with - | AST_EQ -> NBinary(AST_MINUS, a, b), CONS_EQ - | AST_NE -> NBinary(AST_MINUS, a, b), CONS_NE - | AST_GT -> NBinary(AST_MINUS, a, b), CONS_GT - | AST_GE -> NBinary(AST_MINUS, a, b), CONS_GE - | AST_LT -> NBinary(AST_MINUS, b, a), CONS_GT - | AST_LE -> NBinary(AST_MINUS, b, a), CONS_GE + let x, y, op = match op with + | AST_EQ -> a, b, CONS_EQ + | AST_NE -> a, b, CONS_NE + | AST_GT -> a, b, CONS_GT + | AST_GE -> a, b, CONS_GE + | AST_LT -> b, a, CONS_GT + | AST_LE -> b, a, CONS_GE + in + let cons = if y = NIntConst 0 + then (x, op) + else (NBinary(AST_MINUS, x, y), op) in [cons], CLTrue | BConst x -> [], if x then CLTrue else CLFalse |