Clean up & comment a bit.

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)))
+