diff options
| author | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-18 17:53:11 +0200 |
|---|---|---|
| committer | Alex Auvolat <alex.auvolat@ansys.com> | 2014-06-18 17:53:11 +0200 |
| commit | 5a4165f55002876033c718303f86e9e1b7417745 (patch) | |
| tree | aa17967d9b952b3df9a6b6fce215997ea2c9f7e5 /abstract/formula.ml | |
| parent | 96753a375e814be6bde6c41cfdfa4b4cc06bd28e (diff) | |
| download | scade-analyzer-5a4165f55002876033c718303f86e9e1b7417745.tar.gz scade-analyzer-5a4165f55002876033c718303f86e9e1b7417745.zip | |
Nice view of guarantees ; add half test, proved.
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index 44495c4..f3c1df1 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -50,15 +50,18 @@ and eliminate_not_negate = function | BBoolEq(id, v) -> BBoolEq(id, not v) | BNot e -> eliminate_not e | BRel(r, a, b) -> - let r' = match r with - | AST_EQ -> AST_NE - | AST_NE -> AST_EQ - | AST_LT -> AST_GE - | AST_LE -> AST_GT - | AST_GT -> AST_LE - | AST_GE -> AST_LT - in - BRel(r', a, b) + if r = AST_EQ then + BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b)) + else + let r' = match r with + | AST_EQ -> AST_NE + | AST_NE -> AST_EQ + | AST_LT -> AST_GE + | AST_LE -> AST_GT + | AST_GT -> AST_LE + | AST_GE -> AST_LT + in + BRel(r', a, b) | BAnd(a, b) -> BOr(eliminate_not_negate a, eliminate_not_negate b) | BOr(a, b) -> |