Merge branch 'refactor'

7 files changed, 357 insertions, 182 deletions

diff --git a/Makefile b/Makefile
index 07daf1d..3955694 100644
--- a/Makefile
+++ b/Makefile
@@ -19,6 +19,7 @@ SRC= 	main.ml \
 		abstract/num_domain.ml \
 		abstract/enum_domain.ml \
 		abstract/enum_domain_edd.ml \
+		abstract/abs_domain.ml \
 		\
 		abstract/formula.ml \
 		abstract/formula_printer.ml \
diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
new file mode 100644
index 0000000..ce58c3b
--- /dev/null
+++ b/abstract/abs_domain.ml
@@ -0,0 +1,221 @@
+open Ast
+open Formula
+
+open Num_domain
+open Enum_domain
+
+open Varenv
+
+module type ENVIRONMENT_DOMAIN = sig
+    type t
+    type itv
+
+    (* constructors *)
+    val top           : varenv -> t
+    val bottom        : varenv -> t
+    val is_top        : t -> bool
+    val is_bot        : t -> bool
+
+    (* variable management *)
+    val varenv        : t -> varenv
+
+    val forgetvar     : t -> id -> t
+    val forgetvars    : t -> id list -> t
+    val nproject      : t -> id -> itv    (* numerical project *)
+    val eproject      : t -> id -> item list
+
+    (* set-theoretic operations *)
+    val join          : t -> t -> t
+    val meet          : t -> t -> t
+    val widen         : t -> t -> t
+
+    val subset        : t -> t -> bool
+    val eq            : t -> t -> bool
+
+    (* abstract operations *)
+    val apply_ec      : t -> enum_cons -> t
+    val apply_ecl     : t -> enum_cons list -> t
+    val apply_nc      : t -> num_cons -> t
+    val apply_ncl     : t -> num_cons list -> t
+    val eassign       : t -> (id * id) list -> t
+    val nassign       : t -> (id * num_expr) list -> t
+
+    (* pretty-printing *)
+    val print         : Format.formatter -> t -> unit
+    val print_vars    : Format.formatter -> t -> id list -> unit
+    val print_itv     : Format.formatter -> itv -> unit
+
+end
+
+module NumDomainOnly(ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN =
+struct
+
+    type t = varenv * ND.t
+    type itv = ND.itv
+
+    let top ve = (ve, ND.top ve.nvars)
+    let bottom ve = (ve, ND.top ve.nvars)
+    let is_top (_, x) = ND.is_top x
+    let is_bot (_, x) = ND.is_bot x
+
+    let varenv (ve, x) = ve
+
+    let forgetvar (ve, x) id =
+      if List.exists (fun (i, _) -> i = id) ve.nvars
+        then (ve, ND.forgetvar x id)
+        else (ve, x)
+    let forgetvars (ve, x) ids =
+      (ve, List.fold_left ND.forgetvar x
+        (List.filter (fun id -> List.exists (fun (i, _) -> i = id) ve.nvars) ids))
+    let nproject (_, x) id = ND.project x id
+    let eproject (ve, _) id = List.assoc id ve.evars
+
+    let join (ve, a) (_, b) = (ve, ND.join a b)
+    let meet (ve, a) (_, b) = (ve, ND.meet a b)
+    let widen (ve, a) (_, b) = (ve, ND.widen a b)
+
+    let subset (_, a) (_, b) = ND.subset a b
+    let eq (_, a) (_, b) = ND.eq a b
+
+    let apply_ec x _ = x
+    let apply_ecl x _ = x
+    let apply_nc (ve, x) c = (ve, ND.apply_cons x c)
+    let apply_ncl (ve, x) cl = (ve, ND.apply_cl x cl)
+    let eassign x _ = x
+    let nassign (ve, x) ex = (ve, ND.assign x ex)
+
+    let print fmt (_, x) = ND.print fmt x
+    let print_vars fmt (ve, x) ids =
+      ND.print_vars fmt x
+        (List.filter
+          (fun id -> List.exists (fun (i, _) -> i = id) ve.nvars) ids)
+    let print_itv = ND.print_itv
+
+end
+
+module NumEnumDomain
+  (ED : ENUM_ENVIRONMENT_DOMAIN)(ND : NUMERICAL_ENVIRONMENT_DOMAIN)
+  : ENVIRONMENT_DOMAIN
+= struct
+
+  type t =
+    | V of varenv * ED.t * ND.t
+    | Bot of varenv
+  type itv = ND.itv
+
+  let strict = function
+    | V(ve, enum, num) as x ->
+      if ND.is_bot num || ED.is_bot enum
+        then Bot ve
+        else x
+    | b -> b
+  let strict_apply f x = match x with
+    | V(ve, enum, num) ->
+      begin
+        try strict (f (ve, enum, num))
+        with Enum_domain.Bot -> Bot ve
+      end
+    | Bot ve -> Bot ve
+
+  let top ve = V(ve, ED.top ve.evars, ND.top ve.nvars)
+  let bottom ve = Bot ve
+  let is_top x = match strict x with
+    | Bot _ -> false
+    | V(_, enum, num) -> ED.is_top enum && ND.is_top num
+  let is_bot x = match strict x with
+    | Bot _ -> true
+    | _ -> false
+
+  let varenv = function
+    | Bot x -> x
+    | V(ve, _, _) -> ve
+
+  let forgetvar x id =
+    strict_apply (fun (ve, enum, num) ->
+        if List.exists (fun (id2, _) -> id2 = id) ve.evars
+          then V(ve, ED.forgetvar enum id, num)
+          else V(ve, enum, ND.forgetvar num id))
+      x
+
+  let forgetvars x ids = 
+    strict_apply (fun (ve, enum, num) ->
+        let efv, nfv = List.fold_left
+          (fun (efv, nfv) id ->
+            if List.exists (fun (id2, _) -> id2 = id) ve.evars
+              then id::efv, nfv
+              else efv, id::nfv)
+          ([], []) ids
+        in
+          V(ve, ED.forgetvars enum efv, List.fold_left ND.forgetvar num nfv))
+      x
+
+  let nproject x id = match x with
+    | V(ve, enum, num) ->
+        ND.project num id
+    | Bot ve -> ND.project (ND.bottom ve.nvars) id
+  let eproject x id = match x with
+    | V(ve, enum, num) ->
+        ED.project enum id
+    | Bot ve -> []
+
+  let join x y = match strict x, strict y with
+    | Bot _, a | a, Bot _ -> a
+    | V(ve, enum, num), V(_, enum', num') ->
+      V(ve, ED.join enum enum', ND.join num num')
+
+  let meet x y = match strict x, strict y with
+    | Bot ve, a | a, Bot ve -> Bot ve
+    | V(ve, enum, num), V(_, enum', num') ->
+      try
+        strict (V(ve, ED.meet enum enum', ND.meet num num'))
+      with Enum_domain.Bot -> Bot ve
+
+  let widen x y = match strict x, strict y with
+    | Bot _, a | a, Bot _ -> a
+    | V(ve, enum, num), V(_, enum', num') ->
+      V(ve, ED.join enum enum', ND.widen num num')
+
+  let subset x y = match strict x, strict y with
+    | Bot _, a -> true
+    | V(_, _, _), Bot _ -> false
+    | V(_, enum, num), V(_, enum', num') ->
+      ED.subset enum enum' && ND.subset num num'
+
+  let eq x y = match strict x, strict y with
+    | Bot _, Bot _ -> true
+    | V(_, enum, num), V(_, enum', num') ->
+      ED.eq enum enum' && ND.eq num num'
+    | _ -> false
+
+  let apply_ec x f =
+    strict_apply
+      (fun (ve, enum, num) -> V(ve, ED.apply_cl enum [f], num))
+      x
+  let apply_ecl x f =
+    strict_apply (fun (ve, enum, num) -> V(ve, ED.apply_cl enum f, num)) x
+  let apply_nc x f =
+    strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.apply_cons num f)) x
+  let apply_ncl x f =
+    strict_apply (fun (ve, enum, num) -> V(ve, enum, ND.apply_cl num f)) x
+  let eassign x ass =
+    strict_apply (fun  (ve, enum, num) -> V(ve, ED.assign enum ass, num)) x
+  let nassign x ass =
+    strict_apply (fun  (ve, enum, num) -> V(ve, enum, ND.assign num ass)) x
+
+  let print_itv = ND.print_itv
+  let print fmt x = match strict x with
+    | Bot _ -> Format.fprintf fmt "⊥"
+    | V(_, enum, num) ->
+      Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
+  let print_vars fmt x vars = match strict x with
+    | Bot _ -> Format.fprintf fmt "⊥"
+    | V(ve, enum, num) ->
+      let nvars = List.filter
+        (fun v -> List.exists (fun (x, _) -> x = v) ve.nvars)
+        vars
+      in
+      Format.fprintf fmt "@[<hov 1>(%a,@ " ED.print enum;
+      ND.print_vars fmt num nvars;
+      Format.printf ")@]" 
+
+end
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index bbd8d19..0f6bbbf 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -5,20 +5,17 @@ open Typing
 open Cmdline
 
 open Util
-open Num_domain
-open Enum_domain
+open Abs_domain
 
 open Varenv
 
-module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN)
+module I (D0 : ENVIRONMENT_DOMAIN)
 : sig
 
     val do_prog : cmdline_opt -> rooted_prog -> unit
 
 end = struct
 
-    type abs_v = ED.t * ND.t
-
     (*
       Abstract analysis based on dynamic partitionning of the state space.
       Idea : use somme conditions appearing in the text of the program as
@@ -32,7 +29,7 @@ end = struct
         id              : int;
         depth           : int;
 
-        mutable def     : abs_v;
+        mutable def     : D0.t;
         is_init         : bool;
 
         mutable f       : bool_expr;
@@ -40,7 +37,7 @@ end = struct
 
         (* For chaotic iteration fixpoint *)
         mutable in_c    : int;
-        mutable v       : abs_v;
+        mutable v       : D0.t;
 
         mutable out_t   : int list;
         mutable in_t    : int list;
@@ -69,86 +66,32 @@ end = struct
        ************************** *)
 
     (*
-      top : env -> abs_v
-      bottom : env -> abs_v
-    *)
-    let top e = (ED.top e.ve.evars, ND.top e.ve.nvars)
-    let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars)
-    let is_bot (e, n) = ED.is_bot e || ND.is_bot n
-
-    let print_v fmt (enum, num) =
-      if is_bot (enum, num) then
-        Format.fprintf fmt "⊥"
-      else
-        Format.fprintf fmt "@[<hov 1>(%a,@ %a)@]" ED.print enum ND.print num
-
-    (*
-      join : abs_v -> abs_v -> abs_v
-      widen : abs_v -> abs_v -> abs_v
-      meet : abs_v -> abs_v -> abs_v
-    *)
-    let join a b =
-      if is_bot a then b
-      else if is_bot b then a
-      else (ED.join (fst a) (fst b), ND.join (snd a) (snd b))
-
-    let widen a b =
-      if is_bot a then b
-      else if is_bot b then a
-      else (ED.join (fst a) (fst b), ND.widen (snd a) (snd b))
-
-    let meet (e1, n1) (e2, n2) =
-      if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1
-      else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2
-      else
-        try (ED.meet e1 e2 , ND.meet n1 n2)
-        with Bot -> ED.vtop e1, ND.vbottom n1
-
-    (*
-      eq_v : abs_v -> abs_v -> bool
-      subset_v : abs_v -> abs_v -> bool
+      apply_cl : D0.t -> conslist -> D0.t
     *)
-    let eq_v (a, b) (c, d) =
-        (is_bot (a, b) && is_bot (c, d)) 
-          || (ED.eq a c && ND.eq b d)
-
-    let subset_v (a, b) (c, d) =
-      (is_bot (a, b)) ||
-        (not (is_bot (c, d)) && ED.subset a c && ND.subset b d)
-
-    (*
-      apply_cl : abs_v -> conslist -> abs_v
-    *)
-    let rec apply_cl (enum, num) (ec, nc, r) =
+    let rec apply_cl v (ec, nc, r) =
         begin match r with
         | CLTrue ->
-          begin
-            try (ED.apply_cl enum ec, ND.apply_cl num nc)
-            with Bot -> ED.vtop enum, ND.vbottom num
-          end
+          D0.apply_ncl (D0.apply_ecl v ec) nc
         | CLFalse ->
-          (ED.vtop enum, ND.vbottom num)
+          D0.bottom (D0.varenv v)
         | CLAnd(a, b) ->
-          let enum, num = apply_cl (enum, num) (ec, nc, a) in
-          let enum, num = apply_cl (enum, num) ([], nc, b) in
-          enum, num
+          let v = apply_cl v (ec, nc, a) in
+          let v = apply_cl v ([], nc, b) in
+          v
         | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
-          let a = apply_cl (enum, num) (ec@eca, nc@nca, ra) in 
-          let b = apply_cl (enum, num) (ec@ecb, nc@ncb, rb) in 
-          join a b
+          let a = apply_cl v (ec@eca, nc@nca, ra) in 
+          let b = apply_cl v (ec@ecb, nc@ncb, rb) in 
+          D0.join a b
         end
 
     (*
-      apply_cl_all_cases : abs_v -> conslist -> abs_v list
+      apply_cl_all_cases : D0.t -> conslist -> D0.t list
     *)
     let rec apply_cl_all_cases v (ec, nc, r) =
         match r with
         | CLTrue ->
-          let v =
-            try ED.apply_cl (fst v) ec, ND.apply_cl (snd v) nc
-            with Bot -> ED.vtop (fst v), ND.vbottom (snd v)
-          in
-          if is_bot v then [] else [v]
+          let v = D0.apply_ncl (D0.apply_ecl v ec) nc in
+          if D0.is_bot v then [] else [v]
         | CLFalse ->
           []
         | CLAnd(a, b) ->
@@ -158,7 +101,7 @@ end = struct
         | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
           let la = apply_cl_all_cases v (ec@eca, nc@nca, ra) in 
           let lb = apply_cl_all_cases v (ec@ecb, nc@ncb, rb) in 
-          lb@(List.filter (fun a -> not (List.exists (fun b -> eq_v a b) lb)) la)
+          lb@(List.filter (fun a -> not (List.exists (fun b -> D0.eq a b) lb)) la)
 
 
     (* ***************************
@@ -237,14 +180,14 @@ end = struct
             {
               id;
               depth = 0;
-              def = apply_cl (top env) (conslist_of_f cf);
+              def = apply_cl (D0.top env.ve) (conslist_of_f cf);
               is_init;
 
               f = cf;
               cl = conslist_of_f cf;
 
               in_c = 0;
-              v = bottom env;
+              v = D0.bottom env.ve;
 
               out_t = [];
               in_t = [];
@@ -281,41 +224,29 @@ end = struct
       set_target_case : env -> edd_v -> bool_expr -> edd_v
       cycle : env -> edd_v -> conslist -> edd_v
     *)
-    let pass_cycle env (enum, num) =
+    let pass_cycle env v =
         let assign_e, assign_n = List.fold_left
           (fun (ae, an) (a, b, t) -> match t with
             | TEnum _ -> (a, b)::ae, an
             | TInt | TReal -> ae, (a, NIdent b)::an)
           ([], []) env.cycle in
 
-        let enum = ED.assign enum assign_e in
-        let num = ND.assign num assign_n in
+        let v = D0.eassign v assign_e in
+        let v = D0.nassign v assign_n in
 
-        let ef, nf = List.fold_left
-            (fun (ef, nf) (var, t) -> match t with
-              | TEnum _ -> var::ef, nf
-              | TReal | TInt -> ef, var::nf)
-            ([], []) env.forget in
+        D0.forgetvars v (List.map fst env.forget)
 
-        (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
-
-    let unpass_cycle env (enum, num) =
+    let unpass_cycle env v =
         let assign_e, assign_n = List.fold_left
           (fun (ae, an) (a, b, t) -> match t with
             | TEnum _ -> (b, a)::ae, an
             | TInt | TReal -> ae, (b, NIdent a)::an)
           ([], []) env.ve.cycle in
 
-        let enum = ED.assign enum assign_e in
-        let num = ND.assign num assign_n in
-
-        let ef, nf = List.fold_left
-            (fun (ef, nf) (var, t) -> match t with
-              | TEnum _ -> var::ef, nf
-              | TReal | TInt -> ef, var::nf)
-            ([], []) env.ve.forget_inv in
+        let v = D0.eassign v assign_e in
+        let v = D0.nassign v assign_n in
 
-        (ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf)
+        D0.forgetvars v (List.map fst env.ve.forget_inv)
 
     (*
       print_locs : env -> unit
@@ -324,7 +255,7 @@ end = struct
     let print_locs_defs e =
         Hashtbl.iter
           (fun id loc ->
-            Format.printf "q%d: @[<v 2>%a@]@." id print_v loc.def;
+            Format.printf "q%d: @[<v 2>%a@]@." id D0.print loc.def;
             )
           e.loc
 
@@ -332,9 +263,9 @@ end = struct
         Hashtbl.iter
           (fun id loc ->
             Format.printf "@.";
-            Format.printf "q%d (depth = %d):@.  D: @[<v 2>%a@]@." id loc.depth print_v loc.def;
+            Format.printf "q%d (depth = %d):@.  D: @[<v 2>%a@]@." id loc.depth D0.print loc.def;
             (*Format.printf "  F: (%a)@." Formula_printer.print_expr loc.f;*)
-            Format.printf "  V: %a@." print_v loc.v;
+            Format.printf "  V: %a@." D0.print loc.v;
             Format.printf " -> @[<hov>[%a]@]@."
               (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
             )
@@ -385,10 +316,10 @@ end = struct
             loc.in_t <- [];
             loc.in_c <- 0;
             if loc.is_init then begin
-              loc.v <- apply_cl (top e) loc.cl;
+              loc.v <- apply_cl (D0.top e.ve) loc.cl;
               delta := q::!delta
             end else
-              loc.v <- bottom e)
+              loc.v <- D0.bottom e.ve)
           e.loc;
 
         (*print_locs_defs e;*)
@@ -404,14 +335,14 @@ end = struct
 
           let start = loc.v in
           let f i =
-            (*Format.printf "I: %a@." print_v i;*)
-            let i' = meet i (unpass_cycle e loc.def) in
-            (*Format.printf "I': %a@." print_v i';*)
-            let j = join start
+            (*Format.printf "I: %a@." D0.print i;*)
+            let i' = D0.meet i (unpass_cycle e loc.def) in
+            (*Format.printf "I': %a@." D0.print i';*)
+            let j = D0.join start
               (apply_cl
-                (meet (pass_cycle e.ve i') loc.def)
+                (D0.meet (pass_cycle e.ve i') loc.def)
                 loc.cl) in
-            (*Format.printf "J: %a@." print_v j;*)
+            (*Format.printf "J: %a@." D0.print j;*)
             j
           in
 
@@ -419,11 +350,11 @@ end = struct
             let fi = f i in
             let j = 
                 if n < e.opt.widen_delay then
-                  join i fi
+                  D0.join i fi
                 else
-                  widen i fi
+                  D0.widen i fi
             in
-            if eq_v i j
+            if D0.eq i j
               then i
               else iter (n+1) j
           in
@@ -432,27 +363,27 @@ end = struct
           let u = pass_cycle e.ve z in
 
           if e.opt.verbose_ci then
-            Format.printf "Fixpoint: %a@. mem fp: %a@." print_v z print_v u;
+            Format.printf "Fixpoint: %a@. mem fp: %a@." D0.print z D0.print u;
 
           loc.v <- z;
 
           Hashtbl.iter
             (fun t loc2 ->
-                let v = meet u loc2.def in
+                let v = D0.meet u loc2.def in
                 let w = apply_cl v loc2.cl in
-                (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
-                if not (is_bot w) then begin
+                (*Format.printf "u: %a@.v: %a@. w: %a@." D0.print u D0.print v D0.print w;*)
+                if not (D0.is_bot w) then begin
                   if e.opt.verbose_ci then
-                    Format.printf "%d -> %d with:@.  %a@." s t print_v w;
+                    Format.printf "%d -> %d with:@.  %a@." s t D0.print w;
                   if not (List.mem s loc2.in_t)
                     then loc2.in_t <- s::loc2.in_t;
                   if not (List.mem t loc.out_t)
                     then loc.out_t <- t::loc.out_t;
-                  if not (subset_v w loc2.v) then begin
+                  if not (D0.subset w loc2.v) then begin
                     if loc2.in_c < e.opt.widen_delay then
-                      loc2.v <- join loc2.v w
+                      loc2.v <- D0.join loc2.v w
                     else
-                      loc2.v <- widen loc2.v w;
+                      loc2.v <- D0.widen loc2.v w;
                     loc2.in_c <- loc2.in_c + 1;
                     if not (List.mem t !delta)
                       then delta := t::!delta
@@ -467,7 +398,7 @@ end = struct
         let useless = ref [] in
         Hashtbl.iter
           (fun i loc ->
-            if is_bot loc.v then begin
+            if D0.is_bot loc.v then begin
               Format.printf "Useless location detected: q%d@." i;
               useless := i::!useless
             end)
@@ -479,7 +410,7 @@ end = struct
           (fun _ loc ->
             let verif, violate = List.partition
               (fun (_, f, _) ->
-                is_bot (apply_cl loc.v (conslist_of_f f)))
+                D0.is_bot (apply_cl loc.v (conslist_of_f f)))
               e.guarantees
             in
             loc.verif_g <- List.map (fun (a, b, c) -> a) verif;
@@ -511,12 +442,12 @@ end = struct
                   try
                     let cond, _ = List.find
                       (fun (c, _) ->
-                        is_bot (apply_cl loc.v (conslist_of_f c))
-                        || is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
+                        D0.is_bot (apply_cl loc.v (conslist_of_f c))
+                        || D0.is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
                       (ternary_conds loc.f)
                     in
                     let tr =
-                      if is_bot (apply_cl loc.v (conslist_of_f cond))
+                      if D0.is_bot (apply_cl loc.v (conslist_of_f cond))
                       then BNot cond
                       else cond
                     in
@@ -538,13 +469,13 @@ end = struct
                 let cs = ternary_conds loc.f in
                 List.iter
                   (fun (c, exprs) ->
-                    let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in
-                    let cases_f = apply_cl_all_cases (top e) (conslist_of_f (BNot c)) in
+                    let cases_t = apply_cl_all_cases (D0.top e.ve) (conslist_of_f c) in
+                    let cases_f = apply_cl_all_cases (D0.top e.ve) (conslist_of_f (BNot c)) in
                     let cases = List.mapi (fun i c -> i, c) (cases_t @ cases_f) in
                     if
                       List.length 
                         (List.filter
-                          (fun (_, case) -> not (is_bot (meet loc.v case)))
+                          (fun (_, case) -> not (D0.is_bot (D0.meet loc.v case)))
                           cases)
                         >= 2
                     then
@@ -554,10 +485,10 @@ end = struct
                           (fun qi ->
                             let loci = Hashtbl.find e.loc qi in
                             let v = apply_cl
-                              (meet (pass_cycle e.ve loci.v) loc.def)
+                              (D0.meet (pass_cycle e.ve loci.v) loc.def)
                               loc.cl in
                             List.map
-                              (fun (ci, case) -> qi, ci, not (is_bot (meet v case)))
+                              (fun (ci, case) -> qi, ci, not (D0.is_bot (D0.meet v case)))
                               cases)
                           loc.in_t
                       in
@@ -565,14 +496,14 @@ end = struct
                       let out_tc =
                         List.flatten @@ List.map
                           (fun (ci, case) ->
-                            let v = meet loc.v case in
+                            let v = D0.meet loc.v case in
                             List.map
                               (fun qo ->
                                   let loco = Hashtbl.find e.loc qo in
                                   let w = apply_cl
-                                    (meet (pass_cycle e.ve v) loco.def)
+                                    (D0.meet (pass_cycle e.ve v) loco.def)
                                     loco.cl
-                                  in qo, ci, not (is_bot w))
+                                  in qo, ci, not (D0.is_bot w))
                               loc.out_t)
                           cases
                       in
@@ -672,13 +603,13 @@ end = struct
               Format.printf "@.Found no more possible refinement.@.@."
             | Some (score, q, c, cases_t, cases_f) ->
               Format.printf "@.Refine q%d : @[<v 2>[ %a ]@]@." q
-                (print_list print_v ", ") (cases_t@cases_f);
+                (print_list D0.print ", ") (cases_t@cases_f);
 
               let loc = Hashtbl.find e.loc q in
               Hashtbl.remove e.loc loc.id;
 
               let handle_case cc case =
-                  if not (is_bot (meet loc.v case)) then
+                  if not (D0.is_bot (D0.meet loc.v case)) then
                     let ff = simplify_k [cc] loc.f in
                     let ff = simplify_k (get_root_true ff) ff in
                   
@@ -686,7 +617,7 @@ end = struct
                       { loc with
                         id = (incr e.counter; !(e.counter));
                         depth = loc.depth + 1;
-                        def = meet loc.def case;
+                        def = D0.meet loc.def case;
                         f = ff;
                         cl = conslist_of_f ff } in
                     Hashtbl.add e.loc loc2.id loc2
@@ -727,15 +658,15 @@ end = struct
         if List.exists (fun (p, _, _) -> p) e.ve.all_vars then begin
           let final =
             Hashtbl.fold
-              (fun _ loc v -> join v loc.v)
-              e.loc (bottom e) in
+              (fun _ loc v -> D0.join v loc.v)
+              e.loc (D0.bottom e.ve) in
 
           Format.printf "Probes: @[<v 0>";
           List.iter (fun (p, id, ty) ->
             if p then match ty with
             | TInt | TReal ->
               Format.printf "%a ∊ %a@ " Formula_printer.print_id id
-                ND.print_itv (ND.project (snd final) id)
+                D0.print_itv (D0.nproject final id)
             | TEnum _ -> Format.printf "%a : enum variable@ "
                 Formula_printer.print_id id)
             e.ve.all_vars;
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index cdf3c7e..074987f 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -5,7 +5,7 @@ open Typing
 open Cmdline
 
 open Util
-open Num_domain
+open Abs_domain
 
 open Varenv
 
@@ -14,7 +14,7 @@ exception Top
 
 exception Found_int of int
 
-module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
+module I (D0 : ENVIRONMENT_DOMAIN) : sig
 
     val do_prog : cmdline_opt -> rooted_prog -> unit
 
@@ -56,7 +56,7 @@ end = struct
     type edd_v = {
         ve            : varenv;
         root          : edd;
-        leaves        : (int, ND.t) Hashtbl.t;
+        leaves        : (int, D0.t) Hashtbl.t;
     }
 
     (*
@@ -120,10 +120,10 @@ end = struct
         let leaves = Hashtbl.create 12 in
         let lc = ref 0 in
         let get_leaf st x = 
-          if ND.is_top x then DTop else
-          if ND.is_bot x then DBot else
+          if D0.is_top x then DTop else
+          if D0.is_bot x then DBot else
             try
-              Hashtbl.iter (fun i v -> if ND.eq v x then raise (Found_int i)) leaves;
+              Hashtbl.iter (fun i v -> if D0.eq v x then raise (Found_int i)) leaves;
               incr lc;
               Hashtbl.add leaves !lc x;
               DVal (!lc, st)
@@ -205,7 +205,7 @@ end = struct
 
         for id = 0 to !max_v do
           try let v = Hashtbl.find v.leaves id in
-            Format.fprintf fmt "v%d: %a@." id ND.print v
+            Format.fprintf fmt "v%d: %a@." id D0.print v
           with Not_found -> ()
         done
 
@@ -324,7 +324,7 @@ end = struct
               dq vb kl
 
             | DVal (u, _), DVal (v, _) ->
-              let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+              let x = D0.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
               get_leaf x
             | DVal(u, _), DBot ->
               get_leaf (Hashtbl.find a.leaves u)
@@ -365,7 +365,7 @@ end = struct
               dq vb kl
 
             | DVal (u, _) , DVal (v, _) ->
-              let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+              let x = D0.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
               get_leaf x
             | DVal(u, _), DTop ->
               get_leaf (Hashtbl.find a.leaves u)
@@ -380,10 +380,10 @@ end = struct
 
 
     (*
-      edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v
+      edd_leaf_apply : edd_v -> (D0.t -> D0.t) -> edd_v
       edd_apply_ncl : edd_v -> num_cons list -> edd_v
     *)
-    let edd_num_apply v nfun =
+    let edd_leaf_apply v nfun =
         let ve = v.ve in
 
         let leaves, get_leaf = get_leaf_fun () in
@@ -393,7 +393,7 @@ end = struct
         let f f_rec n =
           match n with
           | DBot -> DBot
-          | DTop -> get_leaf (nfun (ND.top ve.nvars))
+          | DTop -> get_leaf (nfun (D0.top ve))
           | DVal (i, _) -> get_leaf (nfun (Hashtbl.find v.leaves i))
           | DChoice(n, var, l) ->
             let l = List.map (fun (k, v) -> k, f_rec v) l in
@@ -402,7 +402,7 @@ end = struct
         { leaves; ve; root = memo f v.root }
 
     let edd_apply_ncl v ncl =
-        edd_num_apply v (fun n -> ND.apply_cl n ncl)
+        edd_leaf_apply v (fun n -> D0.apply_ncl n ncl)
 
     (*
       edd_apply_ecl : edd_v -> enum_cons list -> edd_v
@@ -418,13 +418,15 @@ end = struct
         in
         let cons_edd = cl_k ec in
         edd_meet v cons_edd
-        (*List.fold_left (fun v c -> edd_meet v (edd_of_cons v.ve c)) v ec*)
 
     (*
       edd_apply_cl : edd_v -> conslist -> edd_v
     *)
     let rec edd_apply_cl v (ec, nc, r) =
-        let v = edd_apply_ecl v ec in
+        let v = edd_leaf_apply
+              (edd_apply_ecl v ec)
+              (fun k -> D0.apply_ecl k ec)
+        in
         match r with
         | CLTrue ->
           edd_apply_ncl v nc
@@ -465,7 +467,7 @@ end = struct
           | DBot, DBot -> true
           | DTop, DTop -> true
           | DVal (i, _), DVal (j, _) ->
-            ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+            D0.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
           | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
                 la lb
@@ -484,11 +486,11 @@ end = struct
           | _, DTop -> true
           | DTop, DBot -> false
 
-          | DVal(i, _), DBot -> ND.is_bot (Hashtbl.find a.leaves i)
-          | DTop, DVal(i, _) -> ND.is_top (Hashtbl.find b.leaves i)
+          | DVal(i, _), DBot -> D0.is_bot (Hashtbl.find a.leaves i)
+          | DTop, DVal(i, _) -> D0.is_top (Hashtbl.find b.leaves i)
 
           | DVal(i, _), DVal(j, _) ->
-            ND.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+            D0.subset (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
 
           | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
@@ -530,8 +532,10 @@ end = struct
                 if cn = [] then
                   if fn = [] then DBot
                   else
-                    let x = list_fold_op ND.join
-                        (List.map (Hashtbl.find v.leaves) fn)
+                    let x = list_fold_op D0.join
+                        (List.map
+                          (fun i -> D0.forgetvars (Hashtbl.find v.leaves i) vars)
+                          fn)
                     in get_leaf x
                 else
                   let _, dv, cl = List.hd cn in
@@ -665,7 +669,7 @@ end = struct
             let widen = 
               if edd_eq p1 p2 then true else false
             in
-            let x = (if widen then ND.widen else ND.join)
+            let x = (if widen then D0.widen else D0.join)
                  (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
             get_leaf x
 
@@ -711,7 +715,7 @@ end = struct
             let p1, p2 = edd_extract_path a u, edd_extract_path b v in
             let d1, d2 = Hashtbl.find a.leaves u, Hashtbl.find b.leaves v in
             let widen = edd_eq p1 p2 && i1 >= env.opt.widen_delay in
-            let x = (if widen then ND.widen else ND.join) d1 d2 in
+            let x = (if widen then D0.widen else D0.join) d1 d2 in
             get_leaf (s1, i1 + 1) x
 
           | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
@@ -754,7 +758,7 @@ end = struct
           ([], []) env.cycle in
 
         let v = edd_eassign v assign_e in
-        let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
+        let v = edd_leaf_apply v (fun nv -> D0.nassign nv assign_n) in
 
         let ef, nf = List.fold_left
             (fun (ef, nf) (var, t) -> match t with
@@ -763,7 +767,7 @@ end = struct
             ([], []) env.forget in
 
         let v = edd_forget_vars v ef in
-        edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+        edd_leaf_apply v (fun nv -> D0.forgetvars nv nf)
 
     let unpass_cycle env v =
         let assign_e, assign_n = List.fold_left
@@ -773,7 +777,7 @@ end = struct
           ([], []) env.ve.cycle in
 
         let v = edd_eassign v assign_e in
-        let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
+        let v = edd_leaf_apply v (fun nv -> D0.nassign nv assign_n) in
 
         let ef, nf = List.fold_left
             (fun (ef, nf) (var, t) -> match t with
@@ -782,7 +786,7 @@ end = struct
             ([], []) env.ve.forget_inv in
 
         let v = edd_forget_vars v ef in
-        edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+        edd_leaf_apply v (fun nv -> D0.forgetvars nv nf)
 
 
 
@@ -988,8 +992,8 @@ end = struct
                 | TEnum _ -> id::l)
               [] e.ve.all_vars) in
           let final_flat = match final_flat.root with
-            | DTop -> ND.top e.ve.nvars
-            | DBot -> ND.bottom e.ve.nvars
+            | DTop -> D0.top e.ve
+            | DBot -> D0.bottom e.ve
             | DVal(i, _) -> Hashtbl.find final_flat.leaves i
             | DChoice _ -> assert false
           in
@@ -999,9 +1003,13 @@ end = struct
             if p then match ty with
             | TInt | TReal ->
               Format.printf "%a ∊ %a@ " Formula_printer.print_id id
-                ND.print_itv (ND.project final_flat id)
-            | TEnum _ -> Format.printf "%a : enum variable@ "
-                Formula_printer.print_id id)
+                D0.print_itv (D0.nproject final_flat id)
+            | TEnum _ ->
+              (* not precise : does not take into account info from decision graph *)
+              Format.printf "%a ∊ @[<hov 2>[%a]@]@ "
+                Formula_printer.print_id id
+                (print_list Format.pp_print_string ", ")
+                (D0.eproject final_flat id))
             e.ve.all_vars;
           Format.printf "@]@."
         end
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index 68b04f5..b035cc0 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -26,6 +26,7 @@ module type ENUM_ENVIRONMENT_DOMAIN = sig
     val bottom        : (id * item list) list -> t
     val vtop          : t -> t  (* top with same vars *)
     val is_bot        : t -> bool
+    val is_top        : t -> bool
 
     (* variable management *)
     val vars          : t -> (id * item list) list
@@ -67,6 +68,7 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
     let vtop x = { x with value = VarMap.empty }
     let bottom vars = raise Bot  (* we don't represent Bot *)
     let is_bot x = false
+    let is_top x = VarMap.is_empty x.value
 
     let vars x = x.vars
 
@@ -197,6 +199,11 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
     let vtop x = { x with value = VarMap.empty }
     let bottom vars = raise Bot  (* we don't represent Bot *)
     let is_bot x = false
+    let is_top x =
+      VarMap.for_all
+        (fun k v -> List.for_all (fun vv -> List.mem vv v)
+            (List.assoc k x.vars))
+        x.value
 
     let vars x = x.vars
 
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index 3e03d59..ed13798 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -150,8 +150,10 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
 
     (*
       is_bot : t -> bool
+      is_top : t -> bool
     *)
     let is_bot x = (x.root = DBot)
+    let is_top x = (x.root = DTop)
 
     (*
       vars : t -> (id * item list) list
diff --git a/main.ml b/main.ml
index f130b6c..0dc0408 100644
--- a/main.ml
+++ b/main.ml
@@ -8,6 +8,8 @@ open Num_domain
 open Nonrelational
 open Apron_domain
 
+open Abs_domain
+
 open Enum_domain_edd
 open Abs_interp_dynpart
 
@@ -16,23 +18,26 @@ module Interpret = Interpret.I
 module ItvND = Apron_domain.ND_Box   (* Nonrelational.ND(Intervals_domain.VD) *)
 module PolyND = Apron_domain.ND_Poly
 module OctND = Apron_domain.ND_Oct
+module ItvOND = NumDomainOnly(ItvND)
+module PolyOND = NumDomainOnly(PolyND)
+module OctOND = NumDomainOnly(OctND)
+module ItvEND = NumEnumDomain(Enum_domain.MultiValuation)(ItvND)
+module PolyEND = NumEnumDomain(Enum_domain.MultiValuation)(PolyND)
+module ItvENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(ItvND)
+module PolyENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(PolyND)
 
 module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
 module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(PolyND)
 module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(OctND)
 
-module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
-module AI_Poly_EDD = Abs_interp_edd.I(PolyND)
-module AI_Oct_EDD = Abs_interp_edd.I(OctND)
-
-module AI_S_Itv_DP = Abs_interp_dynpart.I
-      (Enum_domain.MultiValuation)(ItvND)
-module AI_S_Rel_DP = Abs_interp_dynpart.I
-      (Enum_domain.MultiValuation)(PolyND)
-module AI_EDD_Itv_DP = Abs_interp_dynpart.I
-      (Enum_domain_edd.EDD)(ItvND)
-module AI_EDD_Rel_DP = Abs_interp_dynpart.I
-      (Enum_domain_edd.EDD)(PolyND)
+module AI_Itv_EDD = Abs_interp_edd.I(ItvOND)
+module AI_Poly_EDD = Abs_interp_edd.I(PolyOND)
+module AI_Oct_EDD = Abs_interp_edd.I(OctOND)
+
+module AI_S_Itv_DP = Abs_interp_dynpart.I(ItvEND)
+module AI_S_Rel_DP = Abs_interp_dynpart.I(PolyEND)
+module AI_EDD_Itv_DP = Abs_interp_dynpart.I(ItvENDEdd)
+module AI_EDD_Rel_DP = Abs_interp_dynpart.I(PolyENDEdd)
 
 (* command line options *)
 let times = ref false