From e18d0c3d8d7bb072ea686599a8d03d15ea73e7f0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 19 Dec 2022 10:59:28 +0100
Subject: [PATCH] [Quant] Use smart substitution also for delayed instantiation
---
colibri2/theories/quantifier/trigger.ml | 19 +++++++++++--------
1 file changed, 11 insertions(+), 8 deletions(-)
diff --git a/colibri2/theories/quantifier/trigger.ml b/colibri2/theories/quantifier/trigger.ml
index 84094540e..62eb03ac2 100644
--- a/colibri2/theories/quantifier/trigger.ml
+++ b/colibri2/theories/quantifier/trigger.ml
@@ -336,13 +336,21 @@ let debug_new_instantiation =
Debug.register_info_flag ~desc:"Handling of quantifiers"
"quantifiers.instantiations"
+let mode_option =
+ Options.register ~pp:Fmt.bool "Quant.old"
+ Cmdliner.Arg.(
+ value & flag & info [ "quant-old" ] ~doc:"Use quant old heuristic")
+
let instantiate_aux d tri subst =
SubstTrie.set tri.substs subst Instantiated;
let form = Ground.ClosedQuantifier.sem tri.form in
Debug.incr nb_instantiation;
- let subst = Ground.Subst.distinct_union subst form.subst in
- let n = Ground.convert ~subst d form.body in
- (* let n = Subst.convert ~subst_old:form.subst ~subst_new:subst d form.body in *)
+ let n =
+ if Options.get d mode_option then
+ let subst = Ground.Subst.distinct_union subst form.subst in
+ Ground.convert ~subst d form.body
+ else Subst.convert ~subst_old:form.subst ~subst_new:subst d None form.body
+ in
if
Colibri2_stdlib.Debug.test_flag Colibri2_stdlib.Debug.stats
&& not (Egraph.is_equal d n (Ground.ClosedQuantifier.node tri.form))
@@ -391,11 +399,6 @@ end
let () = Events.register (module Delayed_instantiation)
-let mode_option =
- Options.register ~pp:Fmt.bool "Quant.old"
- Cmdliner.Arg.(
- value & flag & info [ "quant-old" ] ~doc:"Use quant old heuristic")
-
let no_eager_instantiation =
Options.register ~pp:Fmt.bool "Quant.no_eager_instantiation"
Cmdliner.Arg.(
--
GitLab