Regroup delayed inverted path

src_colibri2/theories/quantifier/InvertedPath.ml

@@ -45,15 +45,31 @@ type t' = {
 }
 (** All the alternative path to continue in parallel *)
 
-and t = t' Context.Ref.t [@@deriving show]
+and t = { id : int; r : t' Context.Ref.t } [@@deriving show]
 
-let create creator =
-  Context.Ref.create creator
+include (
+  Popop_stdlib.MakeMSH (struct
+    type nonrec t = t
+
+    let tag t = t.id
+    let pp = pp
+  end) :
+    Popop_stdlib.Datatype with type t := t)
+
+let create =
+  let get_counter, incr_counter = Util.get_counter () in
+  fun creator ->
+    incr_counter ();
     {
-      matches = Pattern.M.empty;
-      any_matches = Pattern.M.empty;
-      triggers = [];
-      ups = F_Pos.M.empty;
+      id = get_counter ();
+      r =
+        Context.Ref.create creator
+          {
+            matches = Pattern.M.empty;
+            any_matches = Pattern.M.empty;
+            triggers = [];
+            ups = F_Pos.M.empty;
+          };
     }
 
 let stat = Debug.register_stats_int "InvertedPath.exec"
@@ -66,7 +82,7 @@ let rec exec d acc substs n ip =
   (* pp ip; *)
   if Ground.Subst.S.is_empty substs then acc
   else
-    let ip = Context.Ref.get ip in
+    let ip = Context.Ref.get ip.r in
     let acc =
       List.fold_left
         (fun acc tr ->
@@ -139,35 +155,35 @@ let pt_ips = HPT.create Fmt.nop "Quantifier.pt" (fun c _ -> create c)
 let pn_ips = HPN.create Fmt.nop "Quantifier.pn" (fun c _ -> create c)
 
 let add_trigger pat ip =
-  Context.Ref.set ip
+  Context.Ref.set ip.r
   @@
-  let ip = Context.Ref.get ip in
+  let ip = Context.Ref.get ip.r in
   { ip with triggers = pat :: ip.triggers }
 
 let add_match pat ipr =
-  let ip = Context.Ref.get ipr in
+  let ip = Context.Ref.get ipr.r in
   match Pattern.M.find_opt pat ip.matches with
   | Some ip' -> ip'
   | None ->
-      let ip' = create (Context.Ref.creator ipr) in
-      Context.Ref.set ipr
+      let ip' = create (Context.Ref.creator ipr.r) in
+      Context.Ref.set ipr.r
       @@ { ip with matches = Pattern.M.add pat ip' ip.matches };
       ip'
 
 let add_any_match pat ipr =
-  let ip = Context.Ref.get ipr in
+  let ip = Context.Ref.get ipr.r in
   match Pattern.M.find_opt pat ip.any_matches with
   | Some ip' -> ip'
   | None ->
-      let ip' = create (Context.Ref.creator ipr) in
-      Context.Ref.set ipr
+      let ip' = create (Context.Ref.creator ipr.r) in
+      Context.Ref.set ipr.r
       @@ { ip with any_matches = Pattern.M.add pat ip' ip.any_matches };
       ip'
 
 let add_up f_pos tytl tl ipr =
-  let ip = Context.Ref.get ipr in
-  let ip' = create (Context.Ref.creator ipr) in
-  Context.Ref.set ipr
+  let ip = Context.Ref.get ipr.r in
+  let ip' = create (Context.Ref.creator ipr.r) in
+  Context.Ref.set ipr.r
   @@ {
        ip with
        ups =

src_colibri2/theories/quantifier/InvertedPath.mli

@@ -23,7 +23,7 @@ type t
    of triggers. It allows to know which nodes merge can create new substitutions
    for a pattern and how to find them. Cf Efficient E-matching + modifications *)
 
-val pp : t Fmt.t
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
 
 val exec :
   _ Egraph.t ->

src_colibri2/theories/quantifier/quantifier.ml

@@ -279,24 +279,61 @@ let process_inverted_path d n acc =
   in
   Trigger.M.iter (fun tri substs -> Trigger.instantiate_many d tri substs) acc
 
-module Delayed_find_new_event = struct
-  let key =
-    Events.Dem.create
-      (module struct
-        type t = Node.t * InvertedPath.t list
+module Delayed_find_new_event : sig
+  val enqueue : _ Egraph.t -> Node.t -> InvertedPath.t list -> unit
+end = struct
+  module Delayed_find_new_event = struct
+    let key =
+      Events.Dem.create
+        (module struct
+          type t = unit
 
-        let name = "Quantifier.new_event"
-      end)
+          let name = "Quantifier.new_event"
+        end)
 
-  let delay = Events.Delayed_by 10
+    let delay = Events.Delayed_by 15
 
-  type runable = Node.t * InvertedPath.t list [@@deriving show]
+    type runable = unit
 
-  let print_runable = pp_runable
-  let run d (n, ips) = process_inverted_path d n ips
-end
+    let print_runable = Unit.pp
+
+    let scheduled =
+      Datastructure.Ref.create Fmt.nop "Quant.delayed_find_new_event"
+        Node.M.empty
+
+    let run d () =
+      let run () =
+        let m = Datastructure.Ref.get scheduled d in
+        Datastructure.Ref.set scheduled d Node.M.empty;
+        let triggers =
+          Node.M.fold_left
+            (fun acc n ips ->
+              InvertedPath.S.fold_left
+                (fun acc ip -> InvertedPath.exec d acc Pattern.init n ip)
+                acc ips)
+            Trigger.M.empty m
+        in
+        Trigger.M.iter
+          (fun tri substs -> Trigger.instantiate_many d tri substs)
+          triggers
+      in
+      Debug.add_time_during stats_time run
+  end
 
-let () = Events.register (module Delayed_find_new_event)
+  let () = Events.register (module Delayed_find_new_event)
+
+  let enqueue d n l =
+    if not (Base.List.is_empty l) then (
+      let m = Datastructure.Ref.get Delayed_find_new_event.scheduled d in
+      if Node.M.is_empty m then
+        Events.new_pending_daemon d Delayed_find_new_event.key ();
+      let m =
+        Node.M.add_change InvertedPath.S.of_list
+          (fun l v -> List.fold_right InvertedPath.S.add l v)
+          n l m
+      in
+      Datastructure.Ref.set Delayed_find_new_event.scheduled d m)
+end
 
 let () =
   Dom.register
@@ -324,9 +361,9 @@ let () =
             let info = Info.merge d ~other ~repr info0 info1 in
             Egraph.set_dom d Info.dom cl0 info;
             Egraph.set_dom d Info.dom cl1 info;
-            let ips = Find_new_event.two d cl0 info0 cl1 info1 in
-            if not (Base.List.is_empty ips) then
-              Events.new_pending_daemon d Delayed_find_new_event.key (repr, ips)
+            Debug.add_time_during stats_time (fun () ->
+                let ips = Find_new_event.two d cl0 info0 cl1 info1 in
+                Delayed_find_new_event.enqueue d repr ips)
     end)
 
 let skolemize d (e : Ground.ClosedQuantifier.s) =
@@ -440,9 +477,10 @@ let th_register d =
   (* let delay = Events.Delayed_by 10 in *)
   Daemon.attach_reg_sem d Ground.ClosedQuantifier.key quantifier_registered;
   Ground.register_converter d (fun d g ->
-      if application_useless d g then
-        Debug.dprintf2 debug "[Info] %a is redundant" Ground.pp g
-      else add_info_on_ground_terms d g);
+      Debug.add_time_during stats_time (fun () ->
+          if application_useless d g then
+            Debug.dprintf2 debug "[Info] %a is redundant" Ground.pp g
+          else add_info_on_ground_terms d g));
   Interp.Register.check_closed_quantifier d (fun d g ->
       let n = Ground.ClosedQuantifier.node g in
       let unknown =