diff options
Diffstat (limited to 'abstract/formula.ml')
| -rw-r--r-- | abstract/formula.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index cb7a4c4..01f6655 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -7,13 +7,15 @@ open Ast_util (* Numerical part *) +(* bool on numerical operators : is it float ? *) + type num_expr = (* constants *) | NIntConst of int | NRealConst of float (* operators *) - | NBinary of binary_op * num_expr * num_expr - | NUnary of unary_op * num_expr + | NBinary of binary_op * num_expr * num_expr * bool + | NUnary of unary_op * num_expr * bool (* identifier *) | NIdent of id @@ -40,7 +42,7 @@ type bool_expr = (* constants *) | BConst of bool (* operators from numeric values to boolean values *) - | BRel of binary_rel_op * num_expr * num_expr + | BRel of binary_rel_op * num_expr * num_expr * bool (* operators on enumerated types *) | BEnumCons of enum_cons (* boolean operators *) @@ -78,9 +80,9 @@ and eliminate_not_negate = function | BConst x -> BConst(not x) | BEnumCons(op, a, b) -> BEnumCons((if op = E_EQ then E_NE else E_EQ), a, b) | BNot e -> eliminate_not e - | BRel(r, a, b) -> + | BRel(r, a, b, is_real) -> if r = AST_EQ then - BOr(BRel(AST_LT, a, b), BRel(AST_GT, a, b)) + BOr(BRel(AST_LT, a, b, is_real), BRel(AST_GT, a, b, is_real)) else let r' = match r with | AST_EQ -> AST_NE @@ -90,7 +92,7 @@ and eliminate_not_negate = function | AST_GT -> AST_LE | AST_GE -> AST_LT in - BRel(r', a, b) + BRel(r', a, b, is_real) | BAnd(a, b) -> BOr(eliminate_not_negate a, eliminate_not_negate b) | BOr(a, b) -> @@ -112,7 +114,7 @@ and conslist_bool_expr = let rec conslist_of_f = function | BNot e -> conslist_of_f (eliminate_not_negate e) - | BRel (op, a, b) -> + | BRel (op, a, b, is_real) -> let x, y, op = match op with | AST_EQ -> a, b, CONS_EQ | AST_NE -> a, b, CONS_NE @@ -121,9 +123,9 @@ let rec conslist_of_f = function | AST_LT -> b, a, CONS_GT | AST_LE -> b, a, CONS_GE in - let cons = if y = NIntConst 0 + let cons = if y = NIntConst 0 || y = NRealConst 0. then (x, op) - else (NBinary(AST_MINUS, x, y), op) + else (NBinary(AST_MINUS, x, y, is_real), op) in [], [cons], CLTrue | BConst x -> [], [], if x then CLTrue else CLFalse |