[Solver] the user of the solver makes itself the flush

src/arith.ml

@@ -203,7 +203,7 @@ module Th = struct
     let normalize d t =
       let t' = Cl.M.fold
         (fun x _ p ->
-          let x' = Delayed.normalize d x in
+          let x' = Delayed.propagate d x in
           match Delayed.get_sem d sem x' with
           | None when Cl.equal x x' -> p
           | None   -> subst_cl p x x'
@@ -270,7 +270,7 @@ let mult_cst t cst cl =
       ev)
     ~wakeup:(fun d ~own v ev ->
       let change_one p x =
-        let x' = Delayed.normalize d x in
+        let x' = Delayed.propagate d x in
         match Delayed.get_sem d sem x' with
         | None when Cl.equal x x' -> p
         | None   -> Th.subst_cl p x x'
@@ -321,5 +321,5 @@ let mult_cst t cst cl =
 
 
   let propagate env =
-    Solver.if_propagate_sem env sem
+    Solver.Delayed.if_propagate_sem env sem
     ( fun ~attach_daemon v -> attach_daemon daemon v )

src/arith.mli

@@ -34,4 +34,4 @@ val mult_cst : env -> Q.t -> Cl.t -> Cl.t
 
 val mult : env -> Cl.t -> Cl.t -> Cl.t
 
-val propagate : env -> unit
+val propagate : Delayed.t -> unit

src/bool.ml

@@ -140,7 +140,7 @@ module Th = struct
   let bcp d l absorbent =
     try
       let res = IArray.fold (fun acc cl ->
-        let cl = Delayed.normalize d cl in
+        let cl = Delayed.propagate d cl in
         match Delayed.get_dom d dom cl, acc with
         | Some b, _ when b = absorbent -> raise (TopKnown absorbent)
         | Some _, _ -> acc
@@ -161,7 +161,7 @@ module Th = struct
     Debug.dprintf debug "[Bool] @[norm_dom %a %a@]@."
       Cl.print own (print Cl.print) v;
     let set_dom b cl =
-      let cl = Delayed.normalize d cl in
+      let cl = Delayed.propagate d cl in
       Delayed.set_dom_merge d dom cl b in
     let top_dom = Delayed.get_dom d dom own in
     match top_dom, v with
@@ -171,7 +171,7 @@ module Th = struct
     | Some false, Or  cls -> IArray.iter (set_dom false) cls; AliveStopped
     | None  , True -> Delayed.set_dom d dom own true; AliveStopped
     | None  , Not cl ->
-      begin let cl = Delayed.normalize d cl in
+      begin let cl = Delayed.propagate d cl in
       match Delayed.get_dom d dom cl with
       | Some b -> Delayed.set_dom d dom own (not b); AliveStopped
       | None   -> AliveReattached
@@ -192,8 +192,8 @@ module Th = struct
     begin match s with
     | True           -> ()
     | And t1 | Or t1 ->
-      IArray.iter (fun cl -> ignore (Delayed.normalize d cl)) t1
-    | Not t1 -> ignore (Delayed.normalize d t1)
+      IArray.iter (fun cl -> ignore (Delayed.propagate d cl)) t1
+    | Not t1 -> ignore (Delayed.propagate d t1)
     end;
     NormalizeToSem s
 
@@ -227,10 +227,10 @@ let daemon = register_daemon sem
     Th.norm_dom d own v)
 
 let propagate env =
-  Solver.if_propagate_sem env sem
+  Solver.Delayed.if_propagate_sem env sem
     (fun ~attach_daemon v -> attach_daemon daemon v);
-  let strue = Solver.index env sem True in
-  ignore (Solver.propagate env strue)
+  let strue = Solver.Delayed.index env sem True in
+  ignore (Solver.Delayed.propagate env strue)
 
 
 let _true env = Solver.index env sem True

src/bool.mli

@@ -38,4 +38,4 @@ val is_false : Solver.t -> Cl.t -> bool
     current constraints or due to incompletness *)
 val is_unknown : Solver.t -> Cl.t -> bool
 
-val propagate: Solver.t -> unit
+val propagate: Delayed.t -> unit

src/inputlang/altergo/popop_of_altergo.ml

@@ -58,17 +58,21 @@ let rec add_lexpr_axiom _true env t =
     let f = Uninterp.cst env s in
     let l = List.map (fun e -> add_lexpr_term env e) l in
     let cl = Uninterp.appl env f l in
-    let cl = Solver.propagate env cl in
-    Solver.merge env cl _true
+    let d  = Solver.new_delayed env in
+    let cl = Solver.Delayed.propagate d cl in
+    Solver.Delayed.merge d cl _true;
+    Solver.flush d
   | PPinfix (t1,PPand,t2) ->
     add_lexpr_axiom _true env t1;
     add_lexpr_axiom _true env t2
   | PPinfix (t1,PPeq,t2) ->
     let cl1 = add_lexpr_term env t1 in
-    let cl1 = Solver.propagate env cl1 in
     let cl2 = add_lexpr_term env t2 in
-    let cl2 = Solver.propagate env cl2 in
-    Solver.merge env cl1 cl2
+    let d  = Solver.new_delayed env in
+    let cl1 = Solver.Delayed.propagate d cl1 in
+    let cl2 = Solver.Delayed.propagate d cl2 in
+    Solver.Delayed.merge d cl1 cl2;
+    Solver.flush d
   | _ -> raise (Not_supported (Loc.extract t.pp_loc))
 
 
@@ -78,7 +82,9 @@ let rec add_lexpr_goal _true env t =
     let f = Uninterp.cst env s in
     let l = List.map (fun e -> add_lexpr_term env e) l in
     let cl = Uninterp.appl env f l in
-    let cl = Solver.propagate env cl in
+    let d  = Solver.new_delayed env in
+    let cl = Solver.Delayed.propagate d cl in
+    Solver.flush d;
     Solver.is_equal env cl _true
   | PPinfix (t1,PPand,t2) ->
     let b1 = add_lexpr_goal _true env t1 in
@@ -90,9 +96,11 @@ let rec add_lexpr_goal _true env t =
     b2
   | PPinfix (t1,PPeq,t2) ->
     let cl1 = add_lexpr_term env t1 in
-    let cl1 = Solver.propagate env cl1 in
     let cl2 = add_lexpr_term env t2 in
-    let cl2 = Solver.propagate env cl2 in
+    let d  = Solver.new_delayed env in
+    let cl1 = Solver.Delayed.propagate d cl1 in
+    let cl2 = Solver.Delayed.propagate d cl2 in
+    Solver.flush d;
     Solver.is_equal env cl1 cl2
   | PPforall (_,_,_,e) | PPforall_named (_,_,_,e) -> add_lexpr_goal _true env e
   | _ -> raise (Not_supported (Loc.extract t.pp_loc))
@@ -107,8 +115,10 @@ let rec add_decl _true env = function
 
 let check_goal l =
   let env = Solver.new_t () in
-  Uninterp.propagate env;
-  Arith.propagate env;
+  let d  = Solver.new_delayed env in
+  Uninterp.propagate d;
+  Arith.propagate d;
+  Solver.flush d;
   let _true = uninterp_true env in
   add_decl _true env l
 

src/solver.ml

@@ -223,11 +223,13 @@ type t = {
   mutable attached_daemons : exi_sem attached_daemon Tad.M.t;
   mutable wakeup_daemons   : Tad.t list;
           (** To treat in the reverse order *)
+  mutable current_delayed  : delayed_t; (** For assert-check *)
 }
 
+(** delayed_t is used *)
 and delayed_t = {
   env : t;
-  todo : action Queue.t; (** currently delayed_t is not copied *)
+  todo : action Queue.t;
 }
 
 and action =
@@ -246,6 +248,11 @@ and 'a attached_daemon = {
   wakeup : Events'.data Events'.events;
 }
 
+type decision = {
+  action : action;
+  nbr    : Z.t;
+}
+
 let new_attached_daemon_c = ref (-1)
 let new_attached_daemon (type a) (dem : (a,delayed_t) Events'.dem) (vsem : a) =
   { dem; vsem;
@@ -254,6 +261,8 @@ let new_attached_daemon (type a) (dem : (a,delayed_t) Events'.dem) (vsem : a) =
 
 let exi_sem : 'a attached_daemon -> exi_sem attached_daemon = Obj.magic
 
+let dumb_delayed = { env = Obj.magic 0; todo = Queue.create () }
+
 let new_t () = {
   repr = Cl.M.empty;
   event = Cl.M.empty;
@@ -261,19 +270,21 @@ let new_t () = {
   sem = Simple_vector.create 5;
   attached_daemons = Tad.M.empty;
   wakeup_daemons = [];
-}
+  current_delayed = dumb_delayed;
+  }
 
-let new_handler t = {
+let new_handler t =
+  assert (t.current_delayed == dumb_delayed);
+  {
   repr  = t.repr;
   event = t.event;
   dom = Simple_vector.copy t.dom;
   sem = Simple_vector.copy t.sem;
   attached_daemons = t.attached_daemons;
   wakeup_daemons = t.wakeup_daemons;
+  current_delayed = t.current_delayed;
 }
 
-let delayed_of_t t = { env = t; todo = Queue.create () }
-
 (** {2 Dom and Sem} *)
 module type Dom = Dom' with type delayed := delayed_t
 module type Sem = Sem' with type delayed := delayed_t
@@ -564,13 +575,14 @@ let rec find t cl =
   let cl' = Cl.M.find_exn NotNormalized cl t.repr in
   if Cl.equal cl cl' then cl else find t cl'
 
-
 (** {2 Delayed} *)
 
 module Delayed = struct
   type t = delayed_t
 
-  let find t cl = find t.env cl
+  let find t cl =
+    assert (t.env.current_delayed == t);
+    find t.env cl
 
   let is_repr t cl = Cl.equal (Cl.M.find cl t.env.repr) cl
 
@@ -598,10 +610,15 @@ module Delayed = struct
     Queue.add (SetDom (merge,dom,cl,v)) t.todo
 
 
-  let get_dom t dom cl = get_dom t.env dom cl
-  let get_sem t sem cl = get_sem t.env sem cl
-
-  let index t sem s = index t.env sem s
+  let get_dom t dom cl =
+    assert (t.env.current_delayed == t);
+    get_dom t.env dom cl
+  let get_sem t sem cl =
+    assert (t.env.current_delayed == t);
+    get_sem t.env sem cl
+  let index t sem s =
+    assert (t.env.current_delayed == t);
+    index t.env sem s
 
   let wakeup_event t events cl =
     match events with
@@ -670,6 +687,7 @@ module Delayed = struct
 
   let attach_daemon (type a) t (dem : (a,delayed_t) Events.dem)
       (v : a) =
+    assert (t.env.current_delayed == t);
     let open Events in
     let cl_own = match is_sem_present t dem.dsem v with
       | None -> invalid_arg "Solver.attach_daemon this semantic value \
@@ -688,8 +706,9 @@ module Delayed = struct
     List.iter (fun f -> f ~attach_daemon s) events
 
 
-  let normalize t cl =
-    Debug.dprintf debug "[Solver] normalize %a@." Cl.print cl;
+  let propagate t cl =
+    assert (t.env.current_delayed == t);
+    Debug.dprintf debug "[Solver] propagate %a@." Cl.print cl;
     try
       find t cl
     with NotNormalized ->
@@ -737,7 +756,7 @@ module Delayed = struct
     | None -> ()
     | Some cl' ->
       (** come from invtable, can be just indexed *)
-      let cl' = normalize t cl' in
+      let cl' = propagate t cl' in
       add_pending_merge t cl cl'
 
 
@@ -910,14 +929,21 @@ module Delayed = struct
     end
 
   let merge t cl1 cl2 =
+    assert (t.env.current_delayed == t);
     let cl1,cl2 = Shuffle.shufflep (cl1,cl2) in
     let cl1 = find t cl1 in
     let cl2 = find t cl2 in
     if not (Cl.equal cl1 cl2) then add_pending_merge t cl1 cl2
 
-  let set_sem = add_pending_set_sem
-  let set_dom d dom cl v = add_pending_set_dom false d dom cl v
-  let set_dom_merge d dom cl v = add_pending_set_dom true d dom cl v
+  let set_sem  d sem cl v =
+    assert (d.env.current_delayed == d);
+    add_pending_set_sem d sem cl v
+  let set_dom d dom cl v =
+    assert (d.env.current_delayed == d);
+    add_pending_set_dom false d dom cl v
+  let set_dom_merge d dom cl v =
+    assert (d.env.current_delayed == d);
+    add_pending_set_dom true d dom cl v
 
   let rec do_pending_act t act =
     draw_graph t.env;
@@ -963,17 +989,20 @@ module Delayed = struct
   (*   end in *)
   (*   Simple_vector.set t.env.sem (sem :> int) (module SemTable') *)
 
-  let if_propagate_sem t sem f = if_propagate_sem t.env sem f
+  let if_propagate_sem t sem f =
+    assert (t.env.current_delayed == t);
+    if_propagate_sem t.env sem f
 end
 
 
 
+
+let delayed_of_t t = { env = t; todo = Queue.create () }
+
 let rec flush_daemons t =
   let todo = List.rev (t.wakeup_daemons) in
   if todo <> [] then
-    let delayed = delayed_of_t t in
-    t.wakeup_daemons <- [];
-    let iter tad =
+    let iter delayed tad =
       let att = Tad.M.find tad t.attached_daemons in
       let own = is_sem_present t att.dem.Events.dsem att.vsem in
       match own with
@@ -1000,59 +1029,54 @@ let rec flush_daemons t =
             can perhaps first apply what the daemon does first, then
             readd it to watch list then apply the others pending actions?
         *)
-        Delayed.do_pending delayed in
-    List.iter iter todo;
+        Delayed.do_pending delayed;
+    in
+    let delayed = delayed_of_t t in
+    t.current_delayed <- delayed;
+    t.wakeup_daemons <- [];
+    List.iter (iter delayed) todo;
+    t.current_delayed <- dumb_delayed;
     flush_daemons t
 
 
-let propagate t cl =
-  Debug.dprintf debug "[Solver] @[propagate %a@]@."
-    Cl.print cl;
-  let delayed = delayed_of_t t in
-  let cl = Delayed.normalize delayed cl in
-  Delayed.do_pending delayed;
-  flush_daemons t;
-  draw_graph t;
-  Cl.M.find_exn Impossible cl t.repr
+let new_delayed t =
+  assert (t.current_delayed == dumb_delayed);
+  let d = delayed_of_t t in
+  t.current_delayed <- d;
+  d
 
-let merge t cl1 cl2 =
-  let cl1,cl2 = Shuffle.shufflep (cl1,cl2) in
-  Debug.dprintf debug "[Solver] @[merge %a %a@]@."
-    Cl.print cl1 Cl.print cl2;
-  let delayed = delayed_of_t t in
-  let cl1 = Delayed.find delayed cl1 in
-  let cl2 = Delayed.find delayed cl2 in
-  Delayed.merge_pending delayed cl1 cl2;
-  Delayed.do_pending delayed;
-  flush_daemons t;
-  draw_graph t
 
+let flush d =
+  assert (d.env.current_delayed == d);
+  Delayed.do_pending d;
+  d.env.current_delayed <- dumb_delayed;
+  flush_daemons d.env
 
 let is_equal t cl1 cl2 =
+  assert (t.current_delayed == dumb_delayed);
   let cl1,cl2 = Shuffle.shufflep (cl1,cl2) in
   Debug.dprintf debug "[Solver] @[is_equal %a %a@]@."
     Cl.print cl1 Cl.print cl2;
-  let delayed = delayed_of_t t in
-  let cl1 = Delayed.find delayed cl1 in
-  let cl2 = Delayed.find delayed cl2 in
+  let cl1 = find t cl1 in
+  let cl2 = find t cl2 in
   Cl.equal cl1 cl2
 
+let find t cl =
+  assert (t.current_delayed == dumb_delayed);
+  find t cl
+
+let index t sem v =
+  assert (t.current_delayed == dumb_delayed);
+  index t sem v
+
+let get_sem t sem cl =
+  assert (t.current_delayed == dumb_delayed);
+  get_sem t sem cl
+
+let get_dom t dom cl =
+  assert (t.current_delayed == dumb_delayed);
+  get_dom t dom cl
 
-let set_sem t sem cl v =
-  Debug.dprintf debug "[Solver] @[set_sem %a@]@." Cl.print cl;
-  let delayed = delayed_of_t t in
-  Delayed.set_sem delayed sem cl v;
-  Delayed.do_pending delayed;
-  flush_daemons t;
-  draw_graph t
-
-let set_dom t dom cl v =
-  Debug.dprintf debug "[Solver] @[set_dom %a@]@." Cl.print cl;
-  let delayed = delayed_of_t t in
-  Delayed.set_dom delayed dom cl v;
-  Delayed.do_pending delayed;
-  flush_daemons t;
-  draw_graph t
 
 
 type alive = Events.alive = AliveReattached | AliveStopped

src/solver.mli

@@ -39,17 +39,28 @@ type 'a dom
 type 'a dem
 (** kind of daemon for semantic value of type 'a *)
 
+(* type action *)
+
+(* type decision = { *)
+(*   action : action; *)
+(*   nbr    : Z.t; *)
+(* } *)
+
 module Delayed : sig
   type t
-  (** Immediate information *)
-  val get_sem  : t -> 'a sem -> Cl.t -> 'a option
-  val get_dom  : t -> 'a dom -> Cl.t -> 'a option
-  val index    : t -> 'a sem -> 'a -> Cl.t
-  val normalize: t -> Cl.t -> Cl.t
+  (** {3 Immediate information} *)
+  val propagate : t -> Cl.t -> Cl.t
+  (** Add a new class to propagate *)
+
+  (** {4 The classes must have been marked has propagated} *)
+  val get_sem   : t -> 'a sem -> Cl.t -> 'a option
+  val get_dom   : t -> 'a dom -> Cl.t -> 'a option
+  val index     : t -> 'a sem -> 'a -> Cl.t
+  val find      : t -> Cl.t -> Cl.t
 
   val is_sem_present : t -> 'a sem -> 'a -> Cl.t option
 
-  (** Delayed modifications *)
+  (** {3 Delayed modifications} *)
   val set_dom  : t -> 'a dom -> Cl.t -> 'a -> unit
   val set_dom_merge  : t -> 'a dom -> Cl.t -> 'a -> unit
   (** merge the current domain with the provided one *)
@@ -151,18 +162,36 @@ val register_daemon:
 type t
 
 val new_t    : unit -> t
-val index    : t -> 'a sem -> 'a -> Cl.t
-val propagate: t -> Cl.t -> Cl.t
-val merge    : t -> Cl.t -> Cl.t -> unit
-val is_equal : t -> Cl.t -> Cl.t -> bool
-val get_sem  : t -> 'a sem -> Cl.t -> 'a option
-val get_dom  : t -> 'a dom -> Cl.t -> 'a option
-val set_dom  : t -> 'a dom -> Cl.t -> 'a -> unit
-val set_sem  : t -> 'a sem -> Cl.t -> 'a -> unit
-val find     : t -> Cl.t -> Cl.t
-
-val if_propagate_sem :
-  t -> 'a sem -> (attach_daemon:('a dem -> 'a -> unit) -> 'a -> unit) -> unit
+
+val new_delayed :
+(*
+  decisions:(decision -> unit) ->
+  daemons  :(attached_daemons -> unit) ->
+*)
+  t -> Delayed.t
+(** The argument shouldn't be used anymore before
+    calling flush
+*)
+
+val flush : Delayed.t -> unit
+(** Apply all the modifications and consequences. The argument
+    shouldn't be used anymore *)
+(*
+(** Apply all the modifications and direct consequences (no daemon
+    wakeup) *)
+
+val run_daemons: Delayed.t -> attached_daemons -> unit
+val make_decisions : Delayed.t -> attached_daemons -> unit
+
+*)
+
+val get_sem   : t -> 'a sem -> Cl.t -> 'a option
+val get_dom   : t -> 'a dom -> Cl.t -> 'a option
+val index     : t -> 'a sem -> 'a -> Cl.t
+val find      : t -> Cl.t -> Cl.t
+val is_equal  : t -> Cl.t -> Cl.t -> bool
+
+
 
 (** {2 Implementation Specifics } *)
 (** Because this module is implemented with persistent datastructure *)

src/uninterp.ml

@@ -76,14 +76,14 @@ module Th = struct
     let solve  _d _ _ = NoMerge
 
     let norm d s =
-      Delayed.normalize d (Delayed.index d sem s)
+      Delayed.propagate d (Delayed.index d sem s)
 
     let normalize d s =
       match s with
       | Cst _    ->
         NormalizeToSem s
       | App(f,g) ->
-        let s' = (App(Delayed.normalize d f, Delayed.normalize d g)) in
+        let s' = (App(Delayed.propagate d f, Delayed.propagate d g)) in
           Debug.dprintf debug "[Uninterp] @[normalize %a to %a@]@."
             (print Cl.print) s (print Cl.print) s';
         NormalizeToSem s'
@@ -135,12 +135,12 @@ module Registered = RegisterSem(Th)
           | Cst _ -> assert false
           | App(f,g) ->
             assert (Cl.equal cl f);
-            App(Delayed.normalize d f, g) in
+            App(Delayed.propagate d f, g) in
         let dog d cl = function
           | Cst _ -> assert false
           | App(f,g) ->
             assert (Cl.equal cl g);
-            App(f, Delayed.normalize d g) in
+            App(f, Delayed.propagate d g) in
         Events.add ev (Events.cl_change dof f);
         Events.add ev (Events.cl_change dog g);
         ev)
@@ -151,7 +151,7 @@ module Registered = RegisterSem(Th)
       (* match v with *)
       (* | Cst _ -> assert false *)
       (* | App(f,g) -> *)
-      (*   App(Delayed.normalize d f, Delayed.normalize d g) *)
+      (*   App(Delayed.propagate d f, Delayed.propagate d g) *)
       AliveStopped)
 
   (* let rec add_daemon d arg s = *)
@@ -169,7 +169,7 @@ module Registered = RegisterSem(Th)
   (*     assert ( *)
   (*       if not ( Cl.equal t1 f || Cl.equal t1 g) then raise SubstNoLeaves *)
   (*       else true); *)
-  (*     let replace arg = Delayed.normalize d arg in *)
+  (*     let replace arg = Delayed.propagate d arg in *)
   (*     let f = replace f in *)
   (*     let g = replace g in *)
   (*     let s = App (f,g) in *)
@@ -178,5 +178,5 @@ module Registered = RegisterSem(Th)
   (*     Delayed.set_sem d sem cl3 s *)
 
   let propagate env =
-    Solver.if_propagate_sem env sem
+    Solver.Delayed.if_propagate_sem env sem
       ( fun ~attach_daemon v -> attach_daemon daemon v)

src/uninterp.mli

@@ -49,4 +49,4 @@ val fun5 :
   (Solver.t -> Cl.t -> Cl.t -> Cl.t -> Cl.t -> Cl.t -> Cl.t)
 
 
-val propagate : Solver.t -> unit
+val propagate : Solver.Delayed.t -> unit

tests/tests_arith.ml

 open OUnit
 
 open Solver
+open Tests_lib
 
 let new_env () =
   let t  = new_t () in
-  Uninterp.propagate t;
-  Arith.propagate t;
+  let d = new_delayed t in
+  Uninterp.propagate d;
+  Arith.propagate d;
+  Solver.flush d;
   t
 
 
-let propagate env cl = ignore (Solver.propagate env cl)
-let equal = Solver.merge
-
 let solve1 () =
   let env = new_env () in
   let a  = Uninterp.cst env "a" in
@@ -20,7 +20,7 @@ let solve1 () =
   let a1 = Arith.add env a _1 in
   let b1 = Arith.add env b _1 in
   propagate env a1; propagate env b1;
-  equal env a1 b1;
+  merge env a1 b1;
   assert_bool "" (is_equal env a b)
 
 let solve2 () =
@@ -35,7 +35,7 @@ let solve2 () =
   let b2 = Arith.add env b _2 in
   propagate env a1; propagate env b1;
   propagate env a2; propagate env b2;
-  equal env a1 b1;
+  merge env a1 b1;
   assert_bool "" (is_equal env a2 b2)
 
 let solve3 () =
@@ -50,7 +50,7 @@ let solve3 () =
   let b2 = Arith.add env b _2 in
   propagate env a1; propagate env b1;
   propagate env a2; propagate env b2;
-  equal env a2 b1;
+  merge env a2 b1;
   assert_bool "" (is_equal env a1 b)
 
 let solve4 () =
@@ -65,8 +65,8 @@ let solve4 () =
   propagate env a;
   propagate env a2;
   propagate env _2;
-  equal env a2 b1;
-  equal env a _2;
+  merge env a2 b1;
+  merge env a _2;
   assert_bool "" (not (is_equal env b _2));
   let _3 = Arith.cst env (Q.of_int 3) in
   propagate env _3;
@@ -90,8 +90,8 @@ let solve5 () =
   let t2' = Arith.cst env (Q.of_int 2) in
   let t2' = Arith.add env t2' b in
   propagate env t2';
-  equal env t1 t1';
-  equal env t2 t2';
+  merge env t1 t1';
+  merge env t2 t2';
   let t3' = Arith.cst env (Q.of_int (-3)) in
   propagate env t3';
   assert_bool "" (is_equal env c t3')
@@ -115,8 +115,8 @@ let solve6 () =
   propagate env t2';
   propagate env t3;
   propagate env t3';
-  equal env t1 t1';
-  equal env t2 t2';
+  merge env t1 t1';
+  merge env t2 t2';
   assert_bool "" (is_equal env t3 t3')
 
 

tests/tests_arith_uninterp.ml

 open OUnit
 
 open Solver
+open Tests_lib
 
 let new_env () =
   let t  = new_t () in
-  Uninterp.propagate t;
-  Arith.propagate t;
+  let d = new_delayed t in
+  Uninterp.propagate d;
+  Arith.propagate d;
+  Solver.flush d;
   t
 
-
-let propagate env cl = ignore (Solver.propagate env cl)
-let equal = Solver.merge
-
 let solve6 () =
   let env = new_env () in
   let a  = Uninterp.cst env "a" in
@@ -31,8 +30,8 @@ let solve6 () =
   propagate env t1';
   propagate env t2;
   propagate env t2';
-  equal env t1 t1';
-  equal env t2 t2';
+  merge env t1 t1';
+  merge env t2 t2';
   assert_bool "" (is_equal env t3 t3')
 
 

tests/tests_bool.ml

 open OUnit
 
 open Solver
+open Tests_lib
+
 
 let new_env () =
   let t  = new_t () in
-  Uninterp.propagate t;
-  Bool.propagate t;
+  let d = new_delayed t in
+  Uninterp.propagate d;
+  Bool.propagate d;
+  Solver.flush d;
   t
 
-
-let propagate env cl = ignore (Solver.propagate env cl)
-let equal = Solver.merge
-
 let true_is_true () =
   let env = new_env () in
   assert_bool "" (Bool.is_true env (Bool._true env));

tests/tests_lib.ml

@@ -21,3 +21,14 @@ let test_split s =
 
     ) l
   end
+
+
+let propagate env cl =
+  let d = Solver.new_delayed env in
+  ignore (Solver.Delayed.propagate d cl);
+  Solver.flush d
+
+let merge env cl1 cl2 =
+  let d = Solver.new_delayed env in
+  Solver.Delayed.merge d cl1 cl2;
+  Solver.flush d

tests/tests_uf.ml

 open OUnit
 
 open Solver
+open Tests_lib
 
 
 let new_env () =
   let t  = new_t () in
-  Uninterp.propagate t;
-  Arith.propagate t;
+  let d = new_delayed t in
+  Uninterp.propagate d;
+  Solver.flush d;
   t
 
-
-let propagate env cl = ignore (Solver.propagate env cl)
-let equal = Solver.merge
-
 let empty () =
   let env = new_env () in
   let a  = Uninterp.cst env "a" in
@@ -25,7 +23,7 @@ let tauto () =
   let a  = Uninterp.cst env "a" in
   let b  = Uninterp.cst env "b" in
   propagate env a; propagate env b;
-  equal env a b;
+  merge env a b;
   assert_bool "a = b => a = b"
   (is_equal env a b)
 
@@ -35,7 +33,7 @@ let trans () =
   let b  = Uninterp.cst env "b" in
   let c  = Uninterp.cst env "c" in
   propagate env a; propagate env b; propagate env c;
-  equal env a b; equal env b c;
+  merge env a b; merge env b c;
   assert_bool "a = b => b = c => a = c" (is_equal env a c);
   assert_bool "a = b => b = c => a = b" (is_equal env a b);
   assert_bool "a = b => b = c => b = c" (is_equal env b c)
@@ -46,7 +44,7 @@ let noteq () =
   let b  = Uninterp.cst env "b" in
   let c  = Uninterp.cst env "c" in
   propagate env a; propagate env b; propagate env c;
-  equal env b c;
+  merge env b c;
   assert_bool "b = c => a != c" (not (is_equal env a c))
 
 let basic = "Basic" >::: ["empty" >:: empty; "tauto" >:: tauto;
@@ -76,7 +74,7 @@ let congru () =
   let fa = f env a in
   let fb = f env b in
   propagate env fa; propagate env fb;
-  equal env a b;
+  merge env a b;
   assert_bool "a = b => f(a) = f(b)"
     (is_equal env fa fb)
 
@@ -88,7 +86,7 @@ let _2level () =
   let ffa = f env (f env a) in
   let ffb = f env (f env b) in
   propagate env ffa; propagate env ffb;
-  equal env a b;
+  merge env a b;
   assert_bool "a = b => f(f(a)) = f(f(b))"
   (is_equal env ffa ffb)
 
@@ -100,14 +98,13 @@ let _2level' () =
   let ffa = f env (f env a) in
   let ffb = f env (f env b) in
   propagate env a; propagate env b;
-  equal env a b;
+  merge env a b;
   propagate env ffa; propagate env ffb;
   assert_bool "a = b => f(f(a)) = f(f(b))" (is_equal env ffa ffb)
 
 
 let bigger () =
-  let env = new_t () in
-  Uninterp.propagate env;
+  let env = new_env () in
   let f = Uninterp.fun1 env "f" in
   let a = Uninterp.cst env "a" in
   let rec bf n = if n < 1 then a else (f env (bf(n-1))) in
@@ -115,10 +112,10 @@ let bigger () =
   let fffa = bf 3 in
   let fffffa = bf 5 in
   propagate env fa; propagate env fffa; propagate env fffffa;
-  equal env a fffa;
+  merge env a fffa;
   assert_bool "a = f(f(f(a))) => f(a) != a"
     (not (is_equal env fa a));
-  equal env fffffa a;
+  merge env fffffa a;
   assert_bool "a = f(f(f(a))) => f(f(f(f(f(a))))) = a => f(a) = a"
     (is_equal env fa a)
 
@@ -147,7 +144,7 @@ let congru () =
   let gab = g env a b in
   let gaa = g env a a in
   propagate env gab; propagate env gaa;
-  equal env a b;
+  merge env a b;
   assert_bool "a = b => g(a,b) = g(a,a)"
     (is_equal env gab gaa)
 
@@ -159,7 +156,7 @@ let notcongru () =
   let gab = g env a b in
   let gaa = g env a a in
   propagate env a; propagate env gab; propagate env gaa;
-  equal env a gab;
+  merge env a gab;
   assert_bool "a = g(a,b) => g(a,b) != g(a,a)"
     (not (is_equal env gab gaa))
 
@@ -171,7 +168,7 @@ let _2level () =
   let gab = g env a b in
   let ggabb = g env gab b in
   propagate env a; propagate env gab;
-  equal env gab a;
+  merge env gab a;
   propagate env ggabb;
   assert_bool "g(a,b) = a => g(g(a,b),b) = a"
     (is_equal env ggabb a)
@@ -179,10 +176,10 @@ let _2level () =
 let congru2 = "congru 2 args" >::: ["refl" >:: refl; "congru" >:: congru;
                                     "2level" >:: _2level;]
 
-let equal env x y =
+let merge env x y =
   propagate env x;
   propagate env y;
-  equal env x y
+  merge env x y
 
 
 let is_equal env x y =
@@ -194,16 +191,15 @@ let is_equal env x y =
 let altergo1 =
   "h(x)=x and g(a,x)=a ->  g(g(a,h(x)),x)=a" >::
     fun () ->
-      let env = new_t () in
-      Uninterp.propagate env;
+      let env = new_env () in
       let h = Uninterp.fun1 env "h" in
       let g = Uninterp.fun2 env "g" in
       let x = Uninterp.cst env "x" in
       let a = Uninterp.cst env "a" in
       let hx = h env x in
-      equal env hx x;
+      merge env hx x;
       let gax = g env a x in
-      equal env gax a;
+      merge env gax a;
       let hx = h env x in
       let gahx = g env a hx in
       let ggahxx = g env gahx x in
@@ -213,8 +209,7 @@ let altergo2 =
   "f(f(f(a)))=a and f(f(f(f(f(a)))))=a and g(x,y)=x -> \
    h(g(g(x,y),y),a)=h(x,f(a))" >::
     fun () ->
-      let env = new_t () in
-      Uninterp.propagate env;
+      let env = new_env () in
       let f = Uninterp.fun1 env "f" in
       let h = Uninterp.fun2 env "h" in
       let g = Uninterp.fun2 env "g" in
@@ -223,11 +218,11 @@ let altergo2 =
       let a = Uninterp.cst env "a" in
       let rec bf n = if n < 1 then a else f env (bf (n-1)) in
       let fffa = bf 3 in
-      equal env fffa a;
+      merge env fffa a;
       let fffffa = bf 5 in
-      equal env fffffa a;
+      merge env fffffa a;
       let gxy = g env x y in
-      equal env gxy x;
+      merge env gxy x;
       let ggxyy = g env gxy y in
       let hggxyya = h env ggxyy a in
       let fa = f env a in