[Simplex] Fix redundant run

src_colibri2/theories/LRA/simplex.ml

@@ -24,9 +24,6 @@ open Base
 
 let comparisons = Datastructure.Push.create Node.pp "LRA.simplex.comparisons"
 
-let scheduled =
-  Datastructure.Ref.create Base.Bool.pp "LRA.simplex.scheduled" false
-
 let debug =
   Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "simplex"
 
@@ -377,7 +374,6 @@ let update_domains d env =
 let simplex (d : Egraph.wt) =
   Debug.dprintf0 debug "[Simplex]";
   Debug.incr stats_run;
-  Datastructure.Ref.set scheduled d false;
   let eqs, vars =
     Datastructure.Push.fold comparisons d ~f:(make_equations d)
       ~init:(Polynome.H.create 10, Node.S.empty)
@@ -443,33 +439,53 @@ let simplex (d : Egraph.wt) =
 
 let simplex d = Debug.add_time_during stats_time (fun () -> simplex d)
 
-module DaemonSimplex = struct
-  let key =
-    Events.Dem.create
-      (module struct
-        type t = unit
+module DaemonSimplex : sig
+  val enqueue : _ Egraph.t -> _ -> Events.enqueue
+  val enqueue' : _ Egraph.t -> unit
+end = struct
+  module DaemonSimplex = struct
+    let key =
+      Events.Dem.create
+        (module struct
+          type t = unit
 
-        let name = "LRA.simplex"
-      end)
+          let name = "LRA.simplex"
+        end)
 
-  let enqueue d _ =
-    if Datastructure.Ref.get scheduled d then (
-      Debug.dprintf0 debug "[Scheduler] Simplex? No";
-      Events.EnqAlready)
-    else (
-      Debug.dprintf0 debug "[Scheduler] Simplex? Yes";
-      Datastructure.Ref.set scheduled d true;
-      Events.EnqRun (key, (), None))
+    let scheduled =
+      Datastructure.Ref.create Base.Bool.pp "LRA.simplex.scheduled" false
 
-  let delay = Events.Delayed_by 64
+    let enqueue_aux d =
+      if Datastructure.Ref.get scheduled d then (
+        Debug.dprintf0 debug "[Scheduler] Simplex? No";
+        false)
+      else (
+        Debug.dprintf0 debug "[Scheduler] Simplex? Yes";
+        Datastructure.Ref.set scheduled d true;
+        true)
 
-  type runable = unit
+    let enqueue d _ =
+      if enqueue_aux d then Events.EnqRun (key, (), None) else Events.EnqAlready
 
-  let print_runable = Unit.pp
-  let run d () = simplex d
-end
+    let delay = Events.Delayed_by 64
+
+    type runable = unit
+
+    let print_runable = Unit.pp
 
-let () = Events.register (module DaemonSimplex)
+    let run d () =
+      Debug.dprintf0 debug "[Scheduler] Simplex? Run";
+      Datastructure.Ref.set scheduled d false;
+      simplex d
+  end
+
+  let () = Events.register (module DaemonSimplex)
+  let enqueue = DaemonSimplex.enqueue
+
+  let enqueue' d =
+    if DaemonSimplex.enqueue_aux d then
+      Events.new_pending_daemon d DaemonSimplex.key ()
+end
 
 let ord_inv = function
   | Expr.Lt -> Expr.Gt
@@ -543,7 +559,7 @@ let converter d (f : Ground.t) =
         Events.attach_dom d n Dom_interval.dom DaemonSimplex.enqueue;
 
         Datastructure.Push.push comparisons d n;
-        Events.new_pending_daemon d DaemonSimplex.key ())
+        DaemonSimplex.enqueue' d)
   | _ -> ()
 
 let init env = Ground.register_converter env converter