Initialize the environment of a more efficient handling of watcher

src/lib/cp.mlw

@@ -96,11 +96,14 @@ module Type
      use map.Map
      use set.Fset as S
      use mach.array.Array63 as Array
+     use list.List
 
      type env 'a 'b = {
        domi : Var.Hbi.t 'a; (* domain *)
        domb : Var.Hbb.t 'b;
        mutable dirty : bool;
+       mutable mi: list Var.ti;
+       mutable mb: list Var.tb;
      }
 
      let function get_int e b
@@ -254,7 +257,6 @@ module Engine
      type interp = Type.interp DomI.value DomB.value
      type model = Type.model DomI.value DomB.value
 
-
      scope Prob
         type t = list Constraint.t
 
@@ -268,6 +270,59 @@ module Engine
             end
      end
 
+     scope Watcher
+       type t = {
+            wb: Var.Hb.t (list Constraint.t);
+            wi: Var.Hi.t (list Constraint.t);
+            ghost prob: list Constraint.t;
+       }
+       invariant { forall x. Var.Hb.mem x wb -> forall c. LMem.mem c (Var.Hb.get wb x) -> LMem.mem c prob }
+       invariant { forall x. Var.Hi.mem x wi -> forall c. LMem.mem c (Var.Hi.get wi x) -> LMem.mem c prob }
+       by
+        { wb = Var.Hb.create 0 Nil S.empty; wi = Var.Hi.create 0 Nil S.empty; prob = Nil }
+
+       let rec init wb wi (prob: list Constraint.t)
+              requires { S.subset (Prob.vars prob).Var.sb (Var.Hb.defined wb) }
+              requires { S.subset (Prob.vars prob).Var.si (Var.Hi.defined wi) }
+              requires { forall x. Var.Hb.mem x wb -> (Var.Hb.get wb x) = Nil }
+              requires { forall x. Var.Hi.mem x wi -> (Var.Hi.get wi x) = Nil }
+              ensures { forall x. Var.Hb.mem x wb -> forall c. LMem.mem c (Var.Hb.get wb x) -> LMem.mem c prob }
+              ensures { forall x. Var.Hi.mem x wi -> forall c. LMem.mem c (Var.Hi.get wi x) -> LMem.mem c prob }
+              variant { prob }
+       =
+         match prob with
+         | Nil -> ()
+         | Cons c l ->
+           init wb wi l;
+           let si = Var.Si.create () in
+           Constraint.compute_vars_ti  c si;
+           let iteri = Var.Si.Iterator.create si in
+           while not (Var.Si.Iterator.is_empty iteri) do
+               invariant { forall x. Var.Hi.mem x wi -> forall c. LMem.mem c (Var.Hi.get wi x) -> LMem.mem c prob }
+               variant { S.cardinal iteri.Var.Si.todo }
+               let vi = Var.Si.Iterator.next iteri in
+               Var.Hi.set wi vi (Cons c (Var.Hi.find wi vi));
+           done;
+
+           let sb = Var.Sb.create () in
+           Constraint.compute_vars_tb  c sb;
+           let iterb = Var.Sb.Iterator.create sb in
+           while not (Var.Sb.Iterator.is_empty iterb) do
+               invariant { forall x. Var.Hb.mem x wb -> forall c. LMem.mem c (Var.Hb.get wb x) -> LMem.mem c prob }
+               variant { S.cardinal iterb.Var.Sb.todo }
+               let vb = Var.Sb.Iterator.next iterb in
+               Var.Hb.set wb vb (Cons c (Var.Hb.find wb vb));
+           done;
+         end
+
+       let create e (prob: list Constraint.t) =
+           requires { Var.subset (Prob.vars prob) (defined e) }
+           let wi = Var.Hi.create (Var.Hbi.max_tags e.domi) Nil (defined e).Var.si in
+           let wb = Var.Hb.create (Var.Hbb.max_tags e.domb) Nil (defined e).Var.sb in
+           init wb wi prob;
+           { wb = wb; wi = wi; prob = prob }
+     end
+
      predicate is_true_in (m:interp) (e:env) =
         (forall v:Var.ti. Var.Hbi.mem v e.domi -> DomI.is_true_in (m.i v) (Var.Hbi.contents e.domi v)) /\
         (forall v:Var.tb. Var.Hbb.mem v e.domb -> DomB.is_true_in (m.b v) (Var.Hbb.contents e.domb v))
@@ -739,6 +794,8 @@ module Engine
                domi = domi;
                domb = domb;
                dirty = false;
+               mi = Nil;
+               mb = Nil;
            }
            in
            assert { forall m:interp. (forall v. DomB.is_true_in (m.b v) topb) -> (forall v. DomI.is_true_in (m.i v) topi) -> is_true_in m e };