[Scheduler] Cleanup after simplification of Egraph

src_colibri2/core/egraph.ml

@@ -442,46 +442,34 @@ module Delayed = struct
 
   let context t = Hidden.creator t.env.history
 
-  let is_current_env t = Equal.physical t.env.delayed t
-
   let find t node =
-    assert (is_current_env t);
     find t.env node
 
   let find_def t node =
-    assert (is_current_env t);
     find_def t.env node
 
   let is_repr t node =
-    assert (is_current_env t);
     is_repr t.env node
 
   let is_equal t node1 node2 =
-    assert (is_current_env t);
     is_equal t.env node1 node2
 
   let get_dom t dom node =
-    assert (is_current_env t);
     get_dom t.env dom node
 
   let get_value t node =
-    assert (is_current_env t);
     get_value t.env node
 
   let get_env t env =
-    assert (is_current_env t);
     get_env t.env env
 
   let set_env t env v =
-    assert (is_current_env t);
     set_env t.env env v
 
   let get_unsaved_env t env =
-    assert (is_current_env t);
     get_unsaved_env t.env env
 
   let is_registered t node =
-    assert (is_current_env t);
     is_registered t.env node
 
   let set_value_direct t node0 new_v =
@@ -517,7 +505,6 @@ module Delayed = struct
     Queue.add (Merge (node,node')) t.todo_merge
 
   let register t node =
-    assert (is_current_env t);
     if not (is_registered t node) then begin
       Debug.incr stats_register;
       if Debug.test_flag debug_few then begin
@@ -895,7 +882,6 @@ module Delayed = struct
           Debug.dprintf0 debug "[Egraph] Nothing to do"
 
   and flush_internal d =
-    assert (Equal.physical d.env.delayed d);
     Debug.dprintf0 debug "[Egraph] @[flush delayed@]";
     try
       if not (Queue.is_empty d.todo_ext_action) then
@@ -916,40 +902,32 @@ module Delayed = struct
   (** {2 API} *)
 
   let merge t node1_0 node2_0 =
-    assert (is_current_env t);
     if not (Node.equal
               (find t node1_0)
               (find t node2_0)) then
       add_pending_merge t node1_0 node2_0
 
-  let check d _node =
-    assert (Equal.physical d.env.delayed d)
-
   let set_thterm  d node thterm =
     Debug.dprintf4 debug "[Egraph] @[add_pending_set_thterm for %a and %a@]"
       Node.pp node ThTerm.pp thterm;
-    check d node;
     set_sem_pending d node thterm
 
   let set_value d node nodevalue =
     Debug.dprintf4 debug_few
       "[Egraph] @[set_value for %a with %a@]"
       Node.pp node Value.pp nodevalue;
-    check d node;
     set_value_pending d node nodevalue
 
   let set_dom d dom node v =
     Debug.dprintf4 debug_few
       "[Egraph] @[set_dom for %a with %a@]"
       Node.pp node (print_dom dom) v;
-    check d node;
     set_dom_pending d dom node (Some v)
 
   let unset_dom d dom node =
     Debug.dprintf2 debug
       "[Egraph] @[unset_dom for %a@]"
       Node.pp node;
-    check d node;
     set_dom_pending d dom node None
 
   let register_decision t chogen =
@@ -1094,12 +1072,12 @@ module Backtrackable = struct
     let t = Hidden.ro t in
     Hidden.creator t.history
 
-  let delayed_stop d =
-    assert (Equal.physical d.env.delayed d);
+  let delayed_stop t =
+    let d = (Hidden.rw t).delayed in
     assert (Def.nothing_todo d)
 
-  let flush d =
-    assert (Equal.physical d.env.delayed d);
+  let flush t =
+    let d = (Hidden.rw t).delayed in
     Delayed.do_pending d;
     assert (Def.nothing_todo d)
 
@@ -1191,8 +1169,6 @@ module type Ro = sig
   (** {3 Immediate information} *)
   val register : t -> Node.t -> unit
 
-  val is_current_env: t -> bool
-
   (** {3 Attach Event} *)
   (** todo rename events and attachment *)
 

src_colibri2/core/egraph.mli

@@ -66,8 +66,6 @@ module type Ro = sig
   val register : t -> Node.t -> unit
   (** Add a new node to register *)
 
-  val is_current_env: t -> bool
-
   (** {3 Attach Event} *)
   (** todo rename events and attachment *)
 
@@ -177,15 +175,11 @@ module Backtrackable: sig
   val run_daemon: delayed -> Events.Wait.daemon_key -> unit
   (** schedule the run of a deamon *)
 
-  val delayed_stop: delayed -> unit
-  (** Apply all the modifications and direct consequences.
-      The argument shouldn't be used anymore *)
-
-  val flush: delayed -> unit
-  (** Apply all the modifications and direct consequences.
-      The argument can be used after that *)
-
+  val delayed_stop: t -> unit
+  (** Check that not work need to be done. *)
 
+  val flush: t -> unit
+  (** Apply all the modifications and direct consequences. *)
 
   (* val make_decisions : delayed -> attached_daemons -> unit *)
 

src_colibri2/core/interp.ml

@@ -294,7 +294,6 @@ module Fix_model = struct
               | Some _ -> aux nextnode
               | None ->
                   Debug.dprintf2 debug "FixModel %a has no value" Node.pp n;
-                  assert (Egraph.is_current_env d);
                   let seq = node d n in
                   let seq =
                     seq |> spy_sequence "got"

src_colibri2/solver/scheduler.ml

@@ -256,7 +256,7 @@ and try_run_dec:
         we want to keep the decision in the current branch *)
     t.choices <- prio;
     Debug.incr stats_dec;
-    Egraph.Backtrackable.delayed_stop d;
+    Egraph.Backtrackable.delayed_stop t.solver_state;
     make_choice t todo (Base.Sequence.of_list todos)
 
 and make_choice t todo todos =
@@ -347,8 +347,7 @@ let run_one_step_fix_model t =
         match Base.Sequence.next seq with
         | None -> false
         | Some (todo,todos) ->
-          let d = Egraph.Backtrackable.get_delayed t.solver_state in
-          Egraph.Backtrackable.delayed_stop d;
+          Egraph.Backtrackable.delayed_stop t.solver_state;
           make_choice t todo todos;
           true
       )
@@ -368,8 +367,7 @@ let run_one_step ~nodec t =
 
 let rec flush t =
   try
-    let d = Egraph.Backtrackable.get_delayed t.solver_state in
-    Egraph.Backtrackable.flush d
+    Egraph.Backtrackable.flush t.solver_state
   with Egraph.Contradiction ->
     Debug.dprintf0 debug "[Scheduler] Contradiction";
     conflict_analysis t;
@@ -384,8 +382,7 @@ let rec run_inf_step ?limit ~nodec t =
   | true ->
     run_inf_step ?limit:(Opt.map pred limit) ~nodec t
   | false ->
-    let d = Egraph.Backtrackable.get_delayed t.solver_state in
-    Egraph.Backtrackable.delayed_stop d
+    Egraph.Backtrackable.delayed_stop t.solver_state
 
 let run_inf_step ?limit ?(nodec=false) t =
   try
@@ -395,21 +392,11 @@ let run_inf_step ?limit ?(nodec=false) t =
     Debug.dprintf0 debug_pushpop "[Scheduler] unsat";
     raise e
 
-let stop t =
-  flush t;
-  let d = Egraph.Backtrackable.get_delayed t.solver_state in
-  Egraph.Backtrackable.delayed_stop d
-
-let stop_delayed t =
-    stop t
-
 let init_theories ~theories t =
   try
     let d = Egraph.Backtrackable.get_delayed t.solver_state in
     List.iter (fun f -> f d) (Ground.init::Interp.init::theories);
-    Egraph.Backtrackable.flush d;
-    flush t;
-    stop t
+    Egraph.Backtrackable.flush t.solver_state
   with Egraph.Contradiction ->
     Debug.dprintf0 debug
       "[Scheduler] Contradiction during theory initialization";
@@ -420,8 +407,7 @@ let add_assertion t f =
   try
     let d = Egraph.Backtrackable.get_delayed t.solver_state in
     f d;
-    flush t;
-    stop t
+    flush t
   with Egraph.Contradiction ->
     Debug.dprintf0 debug
       "[Scheduler] Contradiction during assertion";
@@ -429,7 +415,7 @@ let add_assertion t f =
 
 let check_sat ?limit t =
   try
-    stop_delayed t;
+    flush t;
     run_inf_step ?limit t;
     `Sat (Egraph.Backtrackable.get_delayed t.solver_state)
   with Contradiction ->
@@ -439,7 +425,7 @@ let run_exn ?nodec ?limit ~theories f =
   let t = new_solver () in
   init_theories ~theories t;
   add_assertion t f;
-  stop_delayed t;
+  flush t;
   run_inf_step ~nodec:(nodec=Some ()) ?limit t;
   let d = Egraph.Backtrackable.get_delayed t.solver_state in
   d

src_colibri2/tests/tests_lib.ml

@@ -32,11 +32,11 @@ let (&:) s l = s >::: (List.map (fun f -> OUnit2.test_case f) l)
 
 let register d cl =
   Egraph.register d cl;
-  Egraph.Backtrackable.flush d
+  Egraph.flush_internal d
 
 let merge d cl1 cl2 =
   Egraph.merge d cl1 cl2;
-  Egraph.Backtrackable.flush d
+  Egraph.flush_internal d
 
 let is_equal = Egraph.is_equal