[Egraph] One delayed by environment

  simpler but perhaps less checks

src_colibri2/core/egraph.ml

@@ -106,19 +106,19 @@ module Def = struct
       (** Environment not saved during backtrack point, they should use !{Context} *)
       unsaved_envs: Env.Unsaved.VectorH.t;
       history : saved Context.history;
-      mutable current_delayed  : delayed_t; (** For assert-check *)
+      delayed  : delayed_t;
     }
 
   (** delayed_t is used *)
   and delayed_t = {
-    env : t;
+    env: t;
     todo_immediate_dem : action_immediate_dem Queue.t;
     todo_merge_dom : action_merge_dom Queue.t;
     mutable todo_delayed_merge : (Node.t * Node.t * bool) option;
     todo_merge : action_merge Queue.t;
     todo_ext_action : action_ext Queue.t;
-    sched_daemon : Events.Wait.daemon_key -> unit;
-    sched_decision : choice -> unit;
+    mutable sched_daemon : Events.Wait.daemon_key -> unit;
+    mutable sched_decision : choice -> unit;
   }
 
   and action_immediate_dem =
@@ -143,6 +143,20 @@ module Def = struct
     prio: int;
   }
 
+  let nothing_todo t =
+    Queue.is_empty t.todo_immediate_dem
+    && Queue.is_empty t.todo_merge_dom
+    && Option.is_none t.todo_delayed_merge
+    && Queue.is_empty t.todo_merge
+    && Queue.is_empty t.todo_ext_action
+
+  let emptied delayed =
+    Queue.clear delayed.todo_immediate_dem;
+    Queue.clear delayed.todo_merge_dom ;
+    delayed.todo_delayed_merge <- None ;
+    Queue.clear delayed.todo_merge ;
+    Queue.clear delayed.todo_ext_action
+
 end
 
 open Def
@@ -173,26 +187,12 @@ module Wait : Events.Wait.S with type delayed = delayed_t and type delayed_ro =
 module VDom = DomKind.Make(struct type delayed = delayed_t end)
 include VDom
 
-let mk_dumb_delayed () = { env = Obj.magic 0;
-                           todo_immediate_dem = Queue.create ();
-                           todo_merge_dom = Queue.create ();
-                           todo_delayed_merge = None;
-                           todo_merge = Queue.create ();
-                           todo_ext_action = Queue.create ();
-                           sched_daemon   = (fun _ -> (assert false : unit));
-                           (* should never be called *)
-                           sched_decision = (fun _ -> (assert false : unit));
-                         }
-
-let dumb_delayed = mk_dumb_delayed ()
-let unsat_delayed = mk_dumb_delayed ()
-
 module Hidden = Context.Make(struct
     type saved = Def.saved
     type t = Def.t
 
     let save (t:t) : saved =
-      assert (Equal.physical t.current_delayed dumb_delayed); {
+      assert (Def.nothing_todo t.delayed); {
         saved_repr = t.repr;
         saved_rang = t.rang;
         saved_event_repr = t.event_repr;
@@ -217,7 +217,7 @@ module Hidden = Context.Make(struct
       VDomTable.move ~from:s.saved_dom ~to_:t.dom;
       VSemTable.move ~from:s.saved_sem ~to_:t.sem;
       Env.Saved.VectorH.move ~from:s.saved_envs ~to_:t.envs;
-      t.current_delayed <- dumb_delayed
+      Def.emptied t.delayed
 
     let get_history t = t.history
   end)
@@ -442,7 +442,7 @@ module Delayed = struct
 
   let context t = Hidden.creator t.env.history
 
-  let is_current_env t = Equal.physical t.env.current_delayed t
+  let is_current_env t = Equal.physical t.env.delayed t
 
   let find t node =
     assert (is_current_env t);
@@ -850,13 +850,6 @@ module Delayed = struct
     | None -> ()
     | Some runable -> Wait.new_pending_daemon delayed dem runable
 
-  and nothing_todo t =
-    Queue.is_empty t.todo_immediate_dem
-    && Queue.is_empty t.todo_merge_dom
-    && Equal.physical t.todo_delayed_merge None
-    && Queue.is_empty t.todo_merge
-    && Queue.is_empty t.todo_ext_action
-
   and do_pending t =
     draw_graph t.env;
     if not (Queue.is_empty t.todo_immediate_dem) then
@@ -902,7 +895,7 @@ module Delayed = struct
           Debug.dprintf0 debug "[Egraph] Nothing to do"
 
   and flush_internal d =
-    assert (Equal.physical d.env.current_delayed 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
@@ -930,7 +923,7 @@ module Delayed = struct
       add_pending_merge t node1_0 node2_0
 
   let check d _node =
-    assert (Equal.physical d.env.current_delayed d)
+    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@]"
@@ -966,7 +959,7 @@ module Delayed = struct
     t.sched_daemon (Events.Wait.DaemonKey(dem,v))
 
   let contradiction d =
-    d.env.current_delayed <- unsat_delayed;
+    Def.emptied d.env.delayed;
     raise Contradiction
 
   (** {2 API for attaching event} *)
@@ -1056,78 +1049,59 @@ include Delayed
 
 module Backtrackable = struct
 
-  let check_disabled_delayed t =
-    Equal.physical t.current_delayed dumb_delayed
-    || Equal.physical t.current_delayed unsat_delayed
-
   type delayed = t
   type t = Hidden.hidden
 
   let new_t context =
-    Hidden.hide {
-    repr = Node.M.empty;
-    rang = Node.M.empty;
-    event_repr = Node.M.empty;
-    event_any_repr = [];
-    event_value = Node.M.empty;
-    event_reg = Node.M.empty;
-    event_any_reg = [];
-    dom = VDomTable.create 5;
-    sem = VSemTable.create 5;
-    value = { reg_events = ValueKind.M.empty;
-              values = Node.M.empty;
-              events = ValueKind.M.empty;
-            };
-    envs = Env.Saved.VectorH.create 5;
-    unsaved_envs = Env.Unsaved.VectorH.create 5;
-    current_delayed = dumb_delayed;
-    history = Hidden.create context;
-  }
+    let rec t = {
+      repr = Node.M.empty;
+      rang = Node.M.empty;
+      event_repr = Node.M.empty;
+      event_any_repr = [];
+      event_value = Node.M.empty;
+      event_reg = Node.M.empty;
+      event_any_reg = [];
+      dom = VDomTable.create 5;
+      sem = VSemTable.create 5;
+      value = { reg_events = ValueKind.M.empty;
+                values = Node.M.empty;
+                events = ValueKind.M.empty;
+              };
+      envs = Env.Saved.VectorH.create 5;
+      unsaved_envs = Env.Unsaved.VectorH.create 5;
+      delayed;
+      history = Hidden.create context;
+    }
+    and delayed =  { env = t;
+           todo_immediate_dem = Queue.create ();
+           todo_merge_dom = Queue.create ();
+           todo_delayed_merge = None;
+           todo_merge = Queue.create ();
+           todo_ext_action = Queue.create ();
+                     sched_daemon = (fun _ -> ()) ;
+                     sched_decision = (fun _ -> ());
+         } in
+    Hidden.hide t
+
+  let set_sched ~sched_daemon ~sched_decision t =
+    let t = Hidden.rw t in
+    t.delayed.sched_daemon <- sched_daemon;
+    t.delayed.sched_decision <- sched_decision
 
-  (* let new_handle t =
-   *   assert (Equal.physical t.current_delayed dumb_delayed);
-   *   {
-   *     repr  = t.repr;
-   *     rang  = t.rang;
-   *     event_repr = t.event_repr;
-   *     event_value = t.event_value;
-   *     event_reg = t.event_reg;
-   *     event_any_reg = t.event_any_reg;
-   *     dom = VDomTable.copy t.dom;
-   *     sem = VSemTable.copy t.sem;
-   *     value = VValueTable.copy t.value;
-   *     envs = Env.Saved.VectorH.copy t.envs;
-   *     trail = Trail.new_handle t.trail;
-   *     current_delayed = t.current_delayed;
-   *   } *)
+  let get_delayed t = (Hidden.rw t).delayed
 
   let context t =
     let t = Hidden.ro t in
     Hidden.creator t.history
 
-  let new_delayed ~sched_daemon ~sched_decision t =
-    let t = Hidden.rw t in
-    assert (Equal.physical t.current_delayed dumb_delayed);
-    let d =  { env = t;
-               todo_immediate_dem = Queue.create ();
-               todo_merge_dom = Queue.create ();
-               todo_delayed_merge = None;
-               todo_merge = Queue.create ();
-               todo_ext_action = Queue.create ();
-               sched_daemon; sched_decision;
-             } in
-    t.current_delayed <- d;
-    d
-
   let delayed_stop d =
-    assert (Equal.physical d.env.current_delayed d);
-    assert (Delayed.nothing_todo d);
-    d.env.current_delayed <- dumb_delayed
+    assert (Equal.physical d.env.delayed d);
+    assert (Def.nothing_todo d)
 
   let flush d =
-    assert (Equal.physical d.env.current_delayed d);
+    assert (Equal.physical d.env.delayed d);
     Delayed.do_pending d;
-    assert (Delayed.nothing_todo d)
+    assert (Def.nothing_todo d)
 
   let run_daemon d dem =
     Queue.push (ExtDem dem) d.todo_ext_action
@@ -1138,7 +1112,6 @@ module Backtrackable = struct
 
   let is_equal t node1 node2 =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     let node1,node2 = Shuffle.shuffle2 (node1,node2) in
     Debug.dprintf4 debug "[Egraph] @[is_equal %a %a@]"
       Node.pp node1 Node.pp node2;
@@ -1147,7 +1120,6 @@ module Backtrackable = struct
 
   let find t node =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     T.find t node
 
   let get_dom t dom node =
@@ -1156,32 +1128,26 @@ module Backtrackable = struct
 
   let get_value t node =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     T.get_value t node
 
   let get_env t env =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     T.get_env t env
 
   let set_env t env v =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     T.set_env t env v
 
   let get_unsaved_env t env =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     T.get_unsaved_env t env
 
   let is_repr t node =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     T.is_repr t node
 
   let find_def t node =
     let t = Hidden.rw t in
-    assert (check_disabled_delayed t);
     T.find_def t node
 
   let get_getter t =

src_colibri2/core/egraph.mli

@@ -163,15 +163,16 @@ module Backtrackable: sig
   type delayed = t
   include Getter
 
-  val new_t    : Context.creator -> t
+  val new_t    :
+    Context.creator -> t
 
-  val new_delayed :
+  val set_sched:
     sched_daemon:(Events.Wait.daemon_key -> unit) ->
     sched_decision:(choice -> unit) ->
+    t -> unit
+
+  val get_delayed:
     t -> delayed
-  (** The solver shouldn't be used anymore before
-      calling flush. (flushd doesn't count)
-  *)
 
   val run_daemon: delayed -> Events.Wait.daemon_key -> unit
   (** schedule the run of a deamon *)

src_colibri2/solver/scheduler.ml

@@ -43,7 +43,6 @@ let stats_con = Debug.register_stats_int ~name:"Scheduler.conflict" ~init:0
 let stats_step = Debug.register_stats_int ~name:"Scheduler.step" ~init:0
 let stats_fix_model = Debug.register_stats_int ~name:"Scheduler.fix_model" ~init:0
 
-exception NeedStopDelayed
 exception Contradiction
 
 module Att = struct
@@ -85,7 +84,6 @@ type t =
     fixing_model : Events.Wait.daemon_key list Context.Ref.t;
     mutable prev_scheduler_state : bp option;
             solver_state      : Egraph.Backtrackable.t;
-    mutable delayed           : Egraph.t option;
     (* global *)
     decprio : Att.db;
     var_inc  : float ref;
@@ -114,19 +112,41 @@ let print_level fmt t =
 
 let new_solver () =
   let context = Context.create () in
-  { choices = Prio.empty;
-    daemons = Context.TimeWheel.create (Context.creator context);
-    lasteffort = Context.TimeWheel.create (Context.creator context);
-    fixing_model = Context.Ref.create (Context.creator context) [];
-    prev_scheduler_state = None;
-    solver_state = Egraph.Backtrackable.new_t (Context.creator context);
-    context;
-    delayed    = None;
-    decprio = Node.H.create 100;
-    var_inc = ref 1.;
-    level = 0;
-    solve_step = Context.Ref.create (Context.creator context) (Propagate);
-  }
+  let daemon_count = ref (-1) in
+  let dec_count = ref (-1) in
+  let t =
+    { choices = Prio.empty;
+      daemons = Context.TimeWheel.create (Context.creator context);
+      lasteffort = Context.TimeWheel.create (Context.creator context);
+      fixing_model = Context.Ref.create (Context.creator context) [];
+      prev_scheduler_state = None;
+      solver_state = Egraph.Backtrackable.new_t (Context.creator context);
+      context;
+      decprio = Node.H.create 100;
+      var_inc = ref 1.;
+      level = 0;
+      solve_step = Context.Ref.create (Context.creator context) (Propagate);
+    }
+  in
+  let sched_daemon att =
+    incr daemon_count;
+    Debug.dprintf0 debug "[Scheduler] New waiting daemon";
+    match Egraph.Wait.get_priority att with
+    | Immediate -> assert false (* absurd *)
+    | Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
+    | LastEffort offset ->
+      Context.TimeWheel.add t.lasteffort att offset
+    | FixingModel ->
+      Context.Ref.set t.fixing_model (att :: (Context.Ref.get t.fixing_model))
+  and sched_decision dec =
+    incr dec_count;
+    Debug.dprintf1 debug "[Scheduler] New possible decisions prio:%i"
+      !dec_count;
+    t.choices <- Prio.insert t.decprio (Att.Decision (!dec_count,dec))
+        t.choices in
+  Egraph.Backtrackable.set_sched ~sched_daemon ~sched_decision t.solver_state;
+  t
+
 
 let push kind t =
   if Debug.test_flag debug_dotgui then
@@ -155,29 +175,6 @@ let pop_to t prev =
   Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a"
     print_level t
 
-let new_delayed =
-  let daemon_count = ref (-1) in
-  let dec_count = ref (-1) in
-  fun t ->
-    let sched_daemon att =
-      incr daemon_count;
-      Debug.dprintf0 debug "[Scheduler] New waiting daemon";
-      match Egraph.Wait.get_priority att with
-    | Immediate -> assert false (* absurd *)
-    | Delayed_by offset -> Context.TimeWheel.add t.daemons att offset
-    | LastEffort offset ->
-      Context.TimeWheel.add t.lasteffort att offset
-    | FixingModel ->
-      Context.Ref.set t.fixing_model (att :: (Context.Ref.get t.fixing_model))
-    in
-    let sched_decision dec =
-      incr dec_count;
-      Debug.dprintf1 debug "[Scheduler] New possible decisions prio:%i"
-        !dec_count;
-      t.choices <- Prio.insert t.decprio (Att.Decision (!dec_count,dec))
-          t.choices in
-    Egraph.Backtrackable.new_delayed ~sched_daemon ~sched_decision t.solver_state
-
 (*
   let rec apply_learnt llearnt t d =
     match llearnt with
@@ -247,12 +244,12 @@ let rec conflict_analysis t =
   rewind ()
 
 and try_run_dec:
-  t -> Egraph.t -> Prio.t -> Egraph.choice -> Egraph.t = fun t d prio choice ->
+  t -> Prio.t -> Egraph.choice -> unit = fun t prio choice ->
   (** First we verify its the decision is at this point needed *)
+  let d = Egraph.Backtrackable.get_delayed t.solver_state in
   match choice.choice d with
   | Egraph.DecNo | Egraph.DecTodo [] ->
-    t.choices <- prio;
-    d (** d can be precised by choose_decision *)
+    t.choices <- prio
   | Egraph.DecTodo (todo::todos) ->
     (** We remove the decision it is replaced by the todos,
         we can change the interface of choice and in that case
@@ -264,10 +261,8 @@ and try_run_dec:
 
 and make_choice t todo todos =
   ignore (push (Choices todos) t);
-  let d = new_delayed t in
   try
-    todo d;
-    d
+    todo (Egraph.Backtrackable.get_delayed t.solver_state)
   with Egraph.Contradiction ->
     conflict_analysis t
 
@@ -285,139 +280,136 @@ and make_choice t todo todos =
  *     end
  *   | Some (Att.Decision (_,_)) | None -> () *)
 
-let [@inline always] protect_against_contradiction t d f g =
-  match f d with
+let [@inline always] protect_against_contradiction t f g =
+  match f () with
   | exception Egraph.Contradiction ->
     Debug.dprintf0 debug "[Scheduler] Contradiction";
-    Some (conflict_analysis t)
-  | r -> g d r
+    conflict_analysis t;
+    true
+  | r -> g r
 
-let run_one_step_propagation ~nodec t d =
+let run_one_step_propagation ~nodec t =
   Debug.incr stats_step;
   match Context.TimeWheel.next t.daemons with
   | Some att -> begin
       Debug.incr stats_propa;
-      protect_against_contradiction t d (fun d ->
+      protect_against_contradiction t (fun () ->
+          let d = Egraph.Backtrackable.get_delayed t.solver_state in
           Egraph.Backtrackable.run_daemon d att
-        ) (fun d () -> Some d)
+        ) (fun () -> true)
     end
-  | None when nodec -> None
+  | None when nodec -> false
   | None ->
     match Context.TimeWheel.next_at_same_time t.lasteffort with
     | Some att -> begin
         Debug.dprintf1 debug "[Scheduler] LastEffort mode remaining: %t"
           (fun fmt -> Fmt.int fmt (Context.TimeWheel.size_at_current_time t.lasteffort));
         Debug.incr stats_lasteffort;
-        protect_against_contradiction t d (fun d ->
+        protect_against_contradiction t (fun () ->
+            let d = Egraph.Backtrackable.get_delayed t.solver_state in
             Egraph.Backtrackable.run_daemon d att
-          ) (fun d () -> Some d)
+          ) (fun () -> true)
       end
     | None ->
       match Prio.extract_min t.choices with
       | Att.Decision (_,chogen), prio ->
         Debug.dprintf0 debug "[Scheduler] decision";
-        Some (try_run_dec t d prio chogen)
+        try_run_dec t prio chogen;
+        true
       | exception Leftistheap.Empty ->
         Debug.dprintf1 debug "[Scheduler] LastEffort: %i" (Context.TimeWheel.size t.lasteffort);
         match Context.TimeWheel.next t.lasteffort with
         | Some att -> begin
             Debug.incr stats_lasteffort;
-        protect_against_contradiction t d (fun d ->
-              Egraph.Backtrackable.run_daemon d att
-          ) (fun d () -> Some d)
+            protect_against_contradiction t (fun () ->
+                let d = Egraph.Backtrackable.get_delayed t.solver_state in
+                Egraph.Backtrackable.run_daemon d att
+          ) (fun () -> true)
           end
         | None ->
-          None
+          false
 
-let run_one_step_fix_model t d =
+let run_one_step_fix_model t =
   Debug.incr stats_fix_model;
   match Context.Ref.get t.fixing_model with
   | att::l -> begin
       Context.Ref.set t.fixing_model l;
-      protect_against_contradiction t d (fun d ->
+      protect_against_contradiction t (fun () ->
+          let d = Egraph.Backtrackable.get_delayed t.solver_state in
           Egraph.Backtrackable.run_daemon d att
-        ) (fun d () -> Some d)
+        ) (fun () -> true)
     end
   | [] ->
-    protect_against_contradiction t d (fun d ->
+    protect_against_contradiction t (fun () ->
+        let d = Egraph.Backtrackable.get_delayed t.solver_state in
         Interp.Fix_model.next_dec d
-      ) (fun d seq ->
+      ) (fun seq ->
         match Base.Sequence.next seq with
-        | None -> None
+        | None -> false
         | Some (todo,todos) ->
+          let d = Egraph.Backtrackable.get_delayed t.solver_state in
           Egraph.Backtrackable.delayed_stop d;
-          Some (make_choice t todo todos)
+          make_choice t todo todos;
+          true
       )
 
-let run_one_step ~nodec t d =
+let run_one_step ~nodec t =
   match Context.Ref.get t.solve_step with
   | Propagate -> begin
-    match run_one_step_propagation ~nodec t d with
-      | Some _ as s -> s
-      | None when nodec -> None
-      | None ->
+    match run_one_step_propagation ~nodec t with
+      | true -> true
+      | false when nodec -> false
+      | false ->
         Debug.dprintf0 debug "[Scheduler] FixModel";
         Context.Ref.set t.solve_step FixModel;
-        Some d
+        true
   end
-  | FixModel -> run_one_step_fix_model t d
+  | FixModel -> run_one_step_fix_model t
 
-let rec flush t d =
+let rec flush t =
   try
-    Egraph.Backtrackable.flush d; d
+    let d = Egraph.Backtrackable.get_delayed t.solver_state in
+    Egraph.Backtrackable.flush d
   with Egraph.Contradiction ->
     Debug.dprintf0 debug "[Scheduler] Contradiction";
-    let d = conflict_analysis t in
-    flush t d
+    conflict_analysis t;
+    flush t
 
 exception ReachStepLimit
 
-let rec run_inf_step ?limit ~nodec t d =
+let rec run_inf_step ?limit ~nodec t =
   (match limit with | Some n when n <= 0 -> raise ReachStepLimit | _ -> ());
-  let d = flush t d in
-  match run_one_step ~nodec t d with
-  | Some d ->
-    run_inf_step ?limit:(Opt.map pred limit) ~nodec t d
-  | None ->
+  flush t;
+  match run_one_step ~nodec t with
+  | 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
 
 let run_inf_step ?limit ?(nodec=false) t =
-  if t.delayed <> None then raise NeedStopDelayed;
-  let d = new_delayed t in
   try
-    run_inf_step ?limit  ~nodec t d;
+    run_inf_step ?limit  ~nodec t;
     Debug.dprintf0 debug_pushpop "[Scheduler] sat";
   with (Contradiction as e) ->
     Debug.dprintf0 debug_pushpop "[Scheduler] unsat";
     raise e
 
-let get_delayed t =
-  match t.delayed with
-  | Some d -> d
-  | None   ->
-    let d = new_delayed t in
-    t.delayed <- Some d;
-    d
-
-let stop t d =
-  let d = flush t d in
-  Egraph.Backtrackable.delayed_stop d;
-  t.delayed <- None
+let stop t =
+  flush t;
+  let d = Egraph.Backtrackable.get_delayed t.solver_state in
+  Egraph.Backtrackable.delayed_stop d
 
 let stop_delayed t =
-  match t.delayed with
-  | None -> ()
-  | Some d ->
-    let d = flush t d in
-    stop t d
+    stop t
 
 let init_theories ~theories t =
   try
-    let d = get_delayed t in
+    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;
-    let d = flush t d in
-    stop t d
+    flush t;
+    stop t
   with Egraph.Contradiction ->
     Debug.dprintf0 debug
       "[Scheduler] Contradiction during theory initialization";
@@ -426,10 +418,10 @@ let init_theories ~theories t =
 
 let add_assertion t f =
   try
-    let d = get_delayed t in
+    let d = Egraph.Backtrackable.get_delayed t.solver_state in
     f d;
-    let d = flush t d in
-    stop t d
+    flush t;
+    stop t
   with Egraph.Contradiction ->
     Debug.dprintf0 debug
       "[Scheduler] Contradiction during assertion";
@@ -439,7 +431,7 @@ let check_sat ?limit t =
   try
     stop_delayed t;
     run_inf_step ?limit t;
-    `Sat (get_delayed t)
+    `Sat (Egraph.Backtrackable.get_delayed t.solver_state)
   with Contradiction ->
     `Unsat
 
@@ -449,7 +441,8 @@ let run_exn ?nodec ?limit ~theories f =
   add_assertion t f;
   stop_delayed t;
   run_inf_step ~nodec:(nodec=Some ()) ?limit t;
-  get_delayed t
+  let d = Egraph.Backtrackable.get_delayed t.solver_state in
+  d
 
 let run ?nodec ?limit ~theories f =
   try

src_colibri2/tests/tests_lib.ml

@@ -56,11 +56,6 @@ let new_solver () =
     context;
   }
 
-let new_delayed t =
-  let sched_daemon dem = Queue.push dem t.wakeup_daemons in
-  let sched_decision _ = () in
-  Egraph.Backtrackable.new_delayed ~sched_daemon ~sched_decision t.solver_state
-
 exception ReachStepLimit
 exception Contradiction