From 5ac14cee1bdb9f2ccc40ad6eb1841b5c2ed584d1 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 18 Jun 2014 11:34:36 +0200 Subject: Pretty printing. --- abstract/formula.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'abstract/formula.ml') 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 -- cgit v1.2.3