[Quant] move around debug flag and timers

colibri2/theories/quantifier/InvertedPath.ml

@@ -80,7 +80,6 @@ let rec exec d ((triggers, callbacks) as acc) substs n ip =
   Debug.dprintf5 debug_full "[Quant] Exec: %a, %a[%i]" Node.pp n
     Ground.Subst.S.pp substs
     (Ground.Subst.S.cardinal substs);
-  Debug.incr stat;
   (* pp ip; *)
   if Ground.Subst.S.is_empty substs then acc
   else
@@ -149,6 +148,11 @@ let rec exec d ((triggers, callbacks) as acc) substs n ip =
     in
     acc
 
+let exec d acc n ip =
+  Debug.dprintf3 debug "[Quant] IP Exec %i: %a" ip.id Node.pp n;
+  Debug.incr stat;
+  exec d acc Pattern.init n ip
+
 module HPC = Datastructure.Memo (PC)
 module HPP = Datastructure.Memo (PP)
 module HPT = Datastructure.Memo (PT)

colibri2/theories/quantifier/InvertedPath.mli

@@ -28,7 +28,6 @@ include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
 val exec :
   _ Egraph.t ->
   Ground.Subst.S.t Trigger.M.t * Ground.Subst.S.t Callback.M.t ->
-  Ground.Subst.S.t ->
   Node.t ->
   t ->
   Ground.Subst.S.t Trigger.M.t * Ground.Subst.S.t Callback.M.t

colibri2/theories/quantifier/common.ml

@@ -23,7 +23,7 @@ let debug =
 
 let debug_instantiation =
   Debug.register_info_flag ~desc:"Handling of quantifiers"
-    "quantifiers.instantiations"
+    "quantifiers.debug_instantiations"
 
 let debug_full =
   Debug.register_flag ~desc:"Handling of quantifiers full" "quantifiers.full"

colibri2/theories/quantifier/quantifier.ml

@@ -259,6 +259,9 @@ end = struct
       Datastructure.Ref.create Fmt.nop "Quant.delayed_find_new_event"
         Node.M.empty
 
+    let stats_time =
+      Debug.register_stats_time "Quantifier.time_delayed_find_new_event"
+
     let run d () =
       let run () =
         let m = Datastructure.Ref.get scheduled d in
@@ -267,7 +270,7 @@ end = struct
           Node.M.fold_left
             (fun acc n ips ->
               InvertedPath.S.fold_left
-                (fun acc ip -> InvertedPath.exec d acc Pattern.init n ip)
+                (fun acc ip -> InvertedPath.exec d acc n ip)
                 acc ips)
             (Trigger.M.empty, Callback.M.empty)
             m

colibri2/theories/quantifier/trigger.ml

@@ -332,6 +332,10 @@ let register_pattern d (pat : Pattern.t) t =
 let add_trigger d t = register_pattern d t.pat (Trigger t)
 let add_callback d c = register_pattern d (Callback.pattern c) (Callback c)
 
+let debug_new_instantiation =
+  Debug.register_info_flag ~desc:"Handling of quantifiers"
+    "quantifiers.instantiations"
+
 let instantiate_aux d tri subst =
   SubstTrie.set tri.substs subst Instantiated;
   let form = Ground.ClosedQuantifier.sem tri.form in
@@ -344,6 +348,8 @@ let instantiate_aux d tri subst =
     && not (Egraph.is_equal d n (Ground.ClosedQuantifier.node tri.form))
     (* not (Egraph.is_registered d n) *)
   then Debug.incr nb_new_instantiation;
+  Debug.dprintf4 debug_new_instantiation "[Quant] Instantiate %a with %a"
+    Ground.ClosedQuantifier.pp tri.form Ground.Subst.pp subst;
   Egraph.register d n;
   Egraph.merge d n (Ground.ClosedQuantifier.node tri.form)
 
@@ -452,6 +458,9 @@ let instantiate' d tri subst =
               Colibri2_stdlib.Debug.test_flag Colibri2_stdlib.Debug.stats
               && not (Egraph.is_registered d n)
             then Debug.incr nb_new_instantiation;
+            Debug.dprintf6 debug_new_instantiation
+              "[Quant] Instantiate %a with %a and %a" Ground.ClosedQuantifier.pp
+              tri.form Ground.Subst.pp subst Ground.Subst.pp form.subst;
             Egraph.register d n;
             Egraph.merge d n (Ground.ClosedQuantifier.node tri.form);
             Debug.dprintf0 debug "[Quant]   Done"