From 38e9700aa8a6d86388e9f3e83bde6af96028cdef Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 21 Sep 2022 09:32:54 +0200
Subject: [PATCH] [Quant] move around debug flag and timers
---
colibri2/theories/quantifier/InvertedPath.ml | 6 +++++-
colibri2/theories/quantifier/InvertedPath.mli | 1 -
colibri2/theories/quantifier/common.ml | 2 +-
colibri2/theories/quantifier/quantifier.ml | 5 ++++-
colibri2/theories/quantifier/trigger.ml | 9 +++++++++
5 files changed, 19 insertions(+), 4 deletions(-)
diff --git a/colibri2/theories/quantifier/InvertedPath.ml b/colibri2/theories/quantifier/InvertedPath.ml
index ecac633da..545568482 100644
--- a/colibri2/theories/quantifier/InvertedPath.ml
+++ b/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)
diff --git a/colibri2/theories/quantifier/InvertedPath.mli b/colibri2/theories/quantifier/InvertedPath.mli
index ebe6d6a28..8d802226a 100644
--- a/colibri2/theories/quantifier/InvertedPath.mli
+++ b/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
diff --git a/colibri2/theories/quantifier/common.ml b/colibri2/theories/quantifier/common.ml
index a5b985dcc..0d34608b1 100644
--- a/colibri2/theories/quantifier/common.ml
+++ b/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"
diff --git a/colibri2/theories/quantifier/quantifier.ml b/colibri2/theories/quantifier/quantifier.ml
index c07d92463..3562b3712 100644
--- a/colibri2/theories/quantifier/quantifier.ml
+++ b/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
diff --git a/colibri2/theories/quantifier/trigger.ml b/colibri2/theories/quantifier/trigger.ml
index 7a8305445..82f77593a 100644
--- a/colibri2/theories/quantifier/trigger.ml
+++ b/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"
--
GitLab