Did most of the boring stuff. Now, work on the abstract domain.

1 files changed, 15 insertions, 6 deletions

diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
index ddc34ab..a7f5455 100644
--- a/abstract/abs_domain.ml
+++ b/abstract/abs_domain.ml
@@ -2,6 +2,7 @@ open Ast
 open Formula
 open Num_domain
 open Typing
+open Util
 
 module type ENVIRONMENT_DOMAIN = sig
     type t
@@ -43,6 +44,14 @@ end
 
 module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
 
+    type enum_valuation = (string * string) list
+
+    module VMapKey = struct
+      type t = enum_valuation VarMap.t
+      let compare = VarMap.compare (fun a b -> Pervasives.compare (List.sort Pervasives.compare a) (List.sort Pervasives.compare b))
+    end
+    module VMap = Mapext.Make(VMapKey)
+
     type t = ND.t
     type itv = ND.itv
 
@@ -65,16 +74,16 @@ module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
     let subset = ND.subset
     let eq = ND.eq
 
-    let rec apply_cl x (cons, rest) = match rest with
+    let rec apply_cl x (econs, cons, rest) = match rest with
         | CLTrue ->
           ND.apply_ncl x cons
         | CLFalse -> vbottom x
         | CLAnd(a, b) ->
-          let y = apply_cl x (cons, a) in
-          apply_cl y (cons, b)
-        | CLOr((ca, ra), (cb, rb)) ->
-          let y = apply_cl x (cons@ca, ra) in
-          let z = apply_cl x (cons@cb, rb) in
+          let y = apply_cl x (econs, cons, a) in
+          apply_cl y (econs, cons, b)
+        | CLOr((eca, ca, ra), (ecb, cb, rb)) ->
+          let y = apply_cl x (econs@eca, cons@ca, ra) in
+          let z = apply_cl x (econs@ecb, cons@cb, rb) in
           join y z
 
     let apply_f x f = apply_cl x (conslist_of_f f)