Experiment on dynamic partitionning (guarantee initial partition).

1 files changed, 35 insertions, 42 deletions

diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 23df612..2ff950a 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -228,48 +228,41 @@ end = struct
           loc = Hashtbl.create 2; counter = ref 2; } in
 
         (* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *)
-        let rstc = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in
-        let rstf = simplify_k [rstc] f in
-        let rstf = simplify_k (get_root_true rstf) rstf in
-        let nrstc = BEnumCons(E_NE, "L/must_reset", EItem bool_true) in
-        let nrstf = simplify_k [nrstc] f in
-        let nrstf = simplify_k (get_root_true nrstf) nrstf in
-        Hashtbl.add env.loc 0
-          {
-            id = 0;
-            depth = 0;
-            def = apply_cl (top env) (conslist_of_f rstc);
-            is_init = true;
-
-            f = rstf;
-            cl = conslist_of_f rstf;
-
-            in_c = 0;
-            v = bottom env;
-
-            out_t = [];
-            in_t = [];
-            verif_g = [];
-            violate_g = [];
-          };
-        Hashtbl.add env.loc 1
-          {
-            id = 1;
-            depth = 0;
-            def = apply_cl (top env) (conslist_of_f nrstc);
-            is_init = false;
-
-            f = nrstf;
-            cl = conslist_of_f nrstf;
-
-            in_c = 0;
-            v = bottom env;
-
-            out_t = [];
-            in_t = [];
-            verif_g = [];
-            violate_g = [];
-          };
+        let id = let i = ref 0 in fun () -> (incr i; !i) in
+        let add_loc is_init conds =
+          let cf = simplify_k conds f in
+          let cf = simplify_k (get_root_true cf) cf in
+          let id = id() in
+          Hashtbl.add env.loc id
+            {
+              id;
+              depth = 0;
+              def = apply_cl (top env) (conslist_of_f cf);
+              is_init;
+
+              f = cf;
+              cl = conslist_of_f cf;
+
+              in_c = 0;
+              v = bottom env;
+
+              out_t = [];
+              in_t = [];
+              verif_g = [];
+              violate_g = [];
+            };
+        in
+
+        add_loc true [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)];
+
+        let rec div_g conds = function
+          | [] -> add_loc false conds
+          | (_, _, v)::r ->
+            add_loc false ((BEnumCons(E_NE, v, EItem bool_true))::conds);
+            div_g ((BEnumCons(E_EQ, v, EItem bool_true))::conds) r
+        in
+          div_g [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] env.guarantees;
+
         env