From c82709e30fa68fa842b1a0a148f0a674c99ab0eb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 15 Jul 2022 14:38:59 +0200
Subject: [PATCH] [Quant] Regroup all the InverteedPath execution
---
src_colibri2/theories/quantifier/quantifier.ml | 14 +++-----------
1 file changed, 3 insertions(+), 11 deletions(-)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index a67cc165f..051f997cd 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -268,15 +268,6 @@ module Find_new_event = struct
acc
end
-let process_inverted_path d n acc =
- let acc = List.sort_uniq InvertedPath.compare acc in
- let acc =
- List.fold_left
- (fun acc ip -> InvertedPath.exec d acc Pattern.init n ip)
- Trigger.M.empty acc
- in
- Trigger.M.iter (fun tri substs -> Trigger.instantiate_many d tri substs) acc
-
module Delayed_find_new_event : sig
val enqueue : _ Egraph.t -> Node.t -> InvertedPath.t list -> unit
end = struct
@@ -447,14 +438,15 @@ let add_info_on_ground_terms d thg =
match Egraph.get_dom d Info.dom repr with
| None ->
Egraph.set_dom d Info.dom repr info;
- process_inverted_path d repr (Find_new_event.one d repr info [])
+ Delayed_find_new_event.enqueue d repr
+ (Find_new_event.one d repr info [])
| Some info' ->
Egraph.set_dom d Info.dom repr (Info.merge d ~repr ~other info info');
(* The type is added (during registration) after the parents found in info' *)
Find_new_event.one_pt d repr info' g.ty []
|> Find_new_event.one d repr info
|> Find_new_event.two d repr info repr info'
- |> process_inverted_path d repr
+ |> Delayed_find_new_event.enqueue d repr
in
let add_pc pos n =
merge_info n
--
GitLab