diff options
Diffstat (limited to 'abstract/formula.ml')
-rw-r--r-- | abstract/formula.ml | 165 |
1 files changed, 103 insertions, 62 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml index 650f8f4..4102891 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -4,6 +4,21 @@ open Ast_util (* AST for logical formulas *) +(* + Two representations are used for the formulas : + - Formula tree, representing the boolean formula directly + as would be expected + - "conslist", where all the numerical and enumerate constraints + considered in a tree of ANDs are regrouped in a big list. + The second form is used when applying a formula to an abstract value, + whereas the first form is the one generated by the program transformation + procedure and is the one we prefer to show the user because it is more + easily understandable. +*) + +(* ------------------------------------ *) +(* First representation *) +(* ------------------------------------ *) (* Numerical part *) @@ -27,7 +42,6 @@ type num_cons = num_expr * num_cons_op (* always imply right member = 0 *) (* Logical part *) - (* Enumerated types *) type enum_expr = | EIdent of id @@ -52,6 +66,11 @@ type bool_expr = (* (A and B) or ((not A) and C) *) | BNot of bool_expr +(* + Helper functions to construct formula trees and automatically + simplifying some tautologies/contradictions +*) + let is_false = function | BConst false | BNot(BConst true) -> true | _ -> false @@ -85,7 +104,10 @@ let f_e_op op a b = match a, b with | EIdent x, v | v, EIdent x -> BEnumCons(op, x, v) let f_e_eq = f_e_op E_EQ -(* Write all formula without using the NOT operator *) +(* + Transformation functions so that all the logical formula are written + without using the NOT operator +*) let rec eliminate_not = function | BNot e -> eliminate_not_negate e @@ -117,68 +139,19 @@ and eliminate_not_negate = function BOr(eliminate_not_negate a, eliminate_not_negate b) | BOr(a, b) -> BAnd(eliminate_not_negate a, eliminate_not_negate b) + +(* ------------------------------------ *) +(* Simplification functions on the *) +(* first representation *) +(* ------------------------------------ *) (* - 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 conslist = enum_cons list * num_cons list * conslist_bool_expr -and conslist_bool_expr = - | CLTrue - | CLFalse - | CLAnd of conslist_bool_expr * conslist_bool_expr - | CLOr of conslist * conslist - -let rec conslist_of_f = function - | BNot e -> conslist_of_f (eliminate_not_negate e) - | 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 - | 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 || y = NRealConst 0. - then (x, op) - else (NBinary(AST_MINUS, x, y, is_real), op) - in [], [cons], CLTrue - | BConst x -> - [], [], if x then CLTrue else CLFalse - | BEnumCons e -> - [e], [], CLTrue - | BOr(a, b) -> - let eca, ca, ra = conslist_of_f a in - let ecb, cb, rb = conslist_of_f b in - begin match eca, ca, ra, ecb, cb, rb with - | _, _, CLFalse, _, _, _ -> ecb, cb, rb - | _, _, _, _, _, CLFalse -> eca, ca, ra - | [], [], CLTrue, _, _, _ -> [], [], CLTrue - | _, _, _, [], [], CLTrue -> [], [], CLTrue - | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb)) - end - | BAnd(a, b) -> - let eca, ca, ra = conslist_of_f a in - let ecb, cb, rb = conslist_of_f b in - let cons = ca @ cb in - let econs = eca @ ecb in - begin match ra, rb with - | CLFalse, _ | _, CLFalse -> [], [], CLFalse - | CLTrue, _ -> econs, cons, rb - | _, CLTrue -> econs, cons, ra - | _, _ -> econs, cons, CLAnd(ra, rb) - end - | BTernary(c, a, b) -> - conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b))) - - - -(* - Simplify formula considering something is true + Extract enumerated and numeric constants that + are always true in the formula (ie do not appear + under an OR or a ternary). + (not mathematically exact : only a subset is returned) *) let rec get_root_true = function @@ -188,6 +161,13 @@ let rec get_root_true = function | BRel (a, b, c, d) -> [BRel (a, b, c, d)] | _ -> [] +(* + Simplify formula considering something is true + (only does some clearly visible simplifications ; + later simplifications are implicitly done when + abstract-interpreting the formula) +*) + let rec simplify true_eqs e = if List.exists (fun f -> @@ -228,7 +208,6 @@ let rec simplify_k true_eqs e = List.fold_left f_and (simplify true_eqs e) true_eqs - (* Simplify a formula replacing a variable with another *) @@ -266,7 +245,7 @@ let rec formula_replace_evars repls e = (* - extract names of variables referenced in formula + Extract names of enumerated variables referenced in formula *) let rec refd_evars_of_f = function @@ -276,3 +255,65 @@ let rec refd_evars_of_f = function | BEnumCons(_, e, EItem _) -> [e] | BEnumCons(_, e, EIdent f) -> [e; f] | _ -> [] + + + +(* ------------------------------------ *) +(* Second representation *) +(* ------------------------------------ *) + +(* + 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 conslist = enum_cons list * num_cons list * conslist_bool_expr +and conslist_bool_expr = + | CLTrue + | CLFalse + | CLAnd of conslist_bool_expr * conslist_bool_expr + | CLOr of conslist * conslist + +let rec conslist_of_f = function + | BNot e -> conslist_of_f (eliminate_not_negate e) + | 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 + | 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 || y = NRealConst 0. + then (x, op) + else (NBinary(AST_MINUS, x, y, is_real), op) + in [], [cons], CLTrue + | BConst x -> + [], [], if x then CLTrue else CLFalse + | BEnumCons e -> + [e], [], CLTrue + | BOr(a, b) -> + let eca, ca, ra = conslist_of_f a in + let ecb, cb, rb = conslist_of_f b in + begin match eca, ca, ra, ecb, cb, rb with + | _, _, CLFalse, _, _, _ -> ecb, cb, rb + | _, _, _, _, _, CLFalse -> eca, ca, ra + | [], [], CLTrue, _, _, _ -> [], [], CLTrue + | _, _, _, [], [], CLTrue -> [], [], CLTrue + | _ -> [], [], CLOr((eca, ca, ra), (ecb, cb, rb)) + end + | BAnd(a, b) -> + let eca, ca, ra = conslist_of_f a in + let ecb, cb, rb = conslist_of_f b in + let cons = ca @ cb in + let econs = eca @ ecb in + begin match ra, rb with + | CLFalse, _ | _, CLFalse -> [], [], CLFalse + | CLTrue, _ -> econs, cons, rb + | _, CLTrue -> econs, cons, ra + | _, _ -> econs, cons, CLAnd(ra, rb) + end + | BTernary(c, a, b) -> + conslist_of_f (BOr (BAnd(c, a), BAnd(BNot(c), b))) + |