From a5adf6de89b24573c7fe6b101a92359d5e15a2d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 15 Jul 2022 12:05:25 +0200
Subject: [PATCH] [Quant] batch more invertedpath execution
---
.../theories/quantifier/quantifier.ml | 21 +++++++++----------
1 file changed, 10 insertions(+), 11 deletions(-)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index 90bf57f10..a67cc165f 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -84,7 +84,7 @@ let add_trigger d t =
Trigger.instantiate_many d t substs
module Find_new_event = struct
- let two d n (info : Info.t) n' (info' : Info.t) =
+ let two d n (info : Info.t) n' (info' : Info.t) acc =
Debug.dprintf8 debug "Find_new_event %a %a %a %a" Node.pp n Info.pp info
Node.pp n' Info.pp info';
let symmetric f acc na a nb b =
@@ -163,14 +163,13 @@ module Find_new_event = struct
in
symmetric aux acc n info n' info'
in
- let acc = [] in
let acc = InvertedPath.HPP.fold do_pp InvertedPath.pp_ips d acc in
let acc = InvertedPath.HPC.fold do_pc InvertedPath.pc_ips d acc in
let acc = InvertedPath.HPT.fold do_pt InvertedPath.pt_ips d acc in
let acc = InvertedPath.HPN.fold do_pn InvertedPath.pn_ips d acc in
acc
- let one d n (info : Info.t) =
+ let one d n (info : Info.t) acc =
Debug.dprintf4 debug "Find_new_event %a %a" Node.pp n Info.pp info;
let do_pp pp ip acc =
let aux acc _ info1 =
@@ -241,14 +240,13 @@ module Find_new_event = struct
in
aux acc n info
in
- let acc = [] in
let acc = InvertedPath.HPP.fold do_pp InvertedPath.pp_ips d acc in
let acc = InvertedPath.HPC.fold do_pc InvertedPath.pc_ips d acc in
let acc = InvertedPath.HPT.fold do_pt InvertedPath.pt_ips d acc in
let acc = InvertedPath.HPN.fold do_pn InvertedPath.pn_ips d acc in
acc
- let one_pt d n info ty =
+ let one_pt d n info ty acc =
Debug.dprintf4 debug "Find_new_event pt %a %a" Node.pp n Info.pp info;
let do_pt { PT.parent = f_pos; ty = vty } ip acc =
let aux acc n info1 =
@@ -266,12 +264,12 @@ module Find_new_event = struct
in
aux acc n info
in
- let acc = [] in
let acc = InvertedPath.HPT.fold do_pt InvertedPath.pt_ips d acc in
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)
@@ -362,7 +360,7 @@ let () =
Egraph.set_dom d Info.dom cl0 info;
Egraph.set_dom d Info.dom cl1 info;
Debug.add_time_during stats_time (fun () ->
- let ips = Find_new_event.two d cl0 info0 cl1 info1 in
+ let ips = Find_new_event.two d cl0 info0 cl1 info1 [] in
Delayed_find_new_event.enqueue d repr ips)
end)
@@ -449,13 +447,14 @@ 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)
+ process_inverted_path 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' *)
- process_inverted_path d repr (Find_new_event.one_pt d repr info' g.ty);
- process_inverted_path d repr (Find_new_event.one d repr info);
- process_inverted_path d repr (Find_new_event.two d repr info repr 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
in
let add_pc pos n =
merge_info n
--
GitLab