Implement simple tracking of instantiation lemmas (#6077)

We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.

This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.

Fixes #5899.

2 files changed, 403 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c7d97d0fd..1a773de0a 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1776,6 +1776,7 @@ set(regress_1_tests
   regress1/quantifiers/issue5507-qe.smt2
   regress1/quantifiers/issue5658-qe.smt2
   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
+  regress1/quantifiers/issue5899-qe.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
diff --git a/test/regress/regress1/quantifiers/issue5899-qe.smt2 b/test/regress/regress1/quantifiers/issue5899-qe.smt2
new file mode 100644
index 000000000..963eaabcd
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5899-qe.smt2
@@ -0,0 +1,402 @@
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+
+
+(set-logic LIRA)
+(define-fun
+ __node_init_HH_4
+ ((HH.usr.x@0 Bool)
+  (HH.usr.y@0 Bool)
+  (HH.res.init_flag@0 Bool))
+ Bool
+ (and
+  (= HH.usr.y@0 HH.usr.x@0)
+  HH.res.init_flag@0))
+;; Success 
+
+(define-fun
+ __node_trans_HH_4
+ ((HH.usr.x@1 Bool)
+  (HH.usr.y@1 Bool)
+  (HH.res.init_flag@1 Bool)
+  (HH.usr.x@0 Bool)
+  (HH.usr.y@0 Bool)
+  (HH.res.init_flag@0 Bool))
+ Bool
+ (and
+  (= HH.usr.y@1 (or HH.usr.x@1 HH.usr.y@0))
+  (not HH.res.init_flag@1)))
+;; Success 
+
+(define-fun
+ __node_init_FTH_4
+ ((FTH.usr.x@0 Bool)
+  (FTH.usr.r@0 Bool)
+  (FTH.res.init_flag@0 Bool)
+  (FTH.res.abs_0@0 Bool)
+  (FTH.res.inst_1@0 Bool))
+ Bool
+ (and
+  (= FTH.usr.r@0 FTH.usr.x@0)
+  (__node_init_HH_4
+   FTH.usr.x@0
+   FTH.res.abs_0@0
+   FTH.res.inst_1@0)
+  FTH.res.init_flag@0))
+;; Success 
+
+(define-fun
+ __node_trans_FTH_4
+ ((FTH.usr.x@1 Bool)
+  (FTH.usr.r@1 Bool)
+  (FTH.res.init_flag@1 Bool)
+  (FTH.res.abs_0@1 Bool)
+  (FTH.res.inst_1@1 Bool)
+  (FTH.usr.x@0 Bool)
+  (FTH.usr.r@0 Bool)
+  (FTH.res.init_flag@0 Bool)
+  (FTH.res.abs_0@0 Bool)
+  (FTH.res.inst_1@0 Bool))
+ Bool
+ (and
+  (=
+   FTH.usr.r@1
+   (and (not FTH.res.abs_0@0) FTH.usr.x@1))
+  (__node_trans_HH_4
+   FTH.usr.x@1
+   FTH.res.abs_0@1
+   FTH.res.inst_1@1
+   FTH.usr.x@0
+   FTH.res.abs_0@0
+   FTH.res.inst_1@0)
+  (not FTH.res.init_flag@1)))
+;; Success 
+
+(declare-fun %f137@0 () Bool)
+;; Success 
+
+(declare-fun %f144@0 () Bool)
+;; Success 
+
+(declare-fun %f145@0 () Real)
+;; Success 
+
+(declare-fun %f146@0 () Real)
+;; Success 
+
+(declare-fun %f147@0 () Int)
+;; Success 
+
+(declare-fun %f148@0 () Real)
+;; Success 
+
+(declare-fun %f149@0 () Real)
+;; Success 
+
+(declare-fun %f136@0 () Bool)
+;; Success 
+
+(declare-fun %f150@0 () Bool)
+;; Success 
+
+(declare-fun %f151@0 () Bool)
+;; Success 
+
+(declare-fun %f152@0 () Bool)
+;; Success 
+
+(declare-fun %f154@0 () Bool)
+;; Success 
+
+(declare-fun %f155@0 () Bool)
+;; Success 
+
+(declare-fun %f156@0 () Bool)
+;; Success 
+
+(declare-fun %f157@0 () Bool)
+;; Success 
+
+(declare-fun %f158@0 () Bool)
+;; Success 
+
+(declare-fun %f275@0 () Bool)
+;; Success 
+
+(declare-fun %f274@0 () Bool)
+;; Success 
+
+(declare-fun %f273@0 () Bool)
+;; Success 
+
+(declare-fun %f272@0 () Bool)
+;; Success 
+
+(declare-fun %f271@0 () Bool)
+;; Success 
+
+(declare-fun %f137@1 () Bool)
+;; Success 
+
+(declare-fun %f144@1 () Bool)
+;; Success 
+
+(declare-fun %f145@1 () Real)
+;; Success 
+
+(declare-fun %f146@1 () Real)
+;; Success 
+
+(declare-fun %f147@1 () Int)
+;; Success 
+
+(declare-fun %f148@1 () Real)
+;; Success 
+
+(declare-fun %f149@1 () Real)
+;; Success 
+
+(declare-fun %f136@1 () Bool)
+;; Success 
+
+(declare-fun %f150@1 () Bool)
+;; Success 
+
+(declare-fun %f151@1 () Bool)
+;; Success 
+
+(declare-fun %f152@1 () Bool)
+;; Success 
+
+(declare-fun %f154@1 () Bool)
+;; Success 
+
+(declare-fun %f155@1 () Bool)
+;; Success 
+
+(declare-fun %f156@1 () Bool)
+;; Success 
+
+(declare-fun %f157@1 () Bool)
+;; Success 
+
+(declare-fun %f158@1 () Bool)
+;; Success 
+
+(declare-fun %f275@1 () Bool)
+;; Success 
+
+(declare-fun %f274@1 () Bool)
+;; Success 
+
+(declare-fun %f273@1 () Bool)
+;; Success 
+
+(declare-fun %f272@1 () Bool)
+;; Success 
+
+(declare-fun %f271@1 () Bool)
+;; Success
+
+(get-qe
+ (exists
+ ((X1 Bool)
+  (X2 Bool)
+  (X3 Bool)
+  (X4 Bool)
+  (X5 Bool)
+  (X6 Bool)
+  (X7 Bool)
+  (X8 Bool)
+  (X9 Bool)
+  (X10 Bool)
+  (X11 Bool)
+  (X12 Bool)
+  (X13 Bool)
+  (X14 Bool)
+  (X15 Real)
+  (X16 Real)
+  (X17 Int)
+  (X18 Real)
+  (X19 Real)
+  (X20 Bool)
+  (X21 Bool))
+  (not
+   (or
+    (and
+     (or X21 (not X20))
+     (or
+      (and
+       (not %f150@0)
+       (or
+        (__node_trans_FTH_4
+         false
+         false
+         false
+         true
+         false
+         false
+         %f154@0
+         %f274@0
+         %f273@0
+         %f272@0)
+        (__node_trans_FTH_4
+         false
+         false
+         false
+         false
+         false
+         false
+         %f154@0
+         %f274@0
+         %f273@0
+         %f272@0))
+       (or
+        (__node_trans_HH_4 false true false false %f151@0 %f275@0)
+        (__node_trans_HH_4 false false false false %f151@0 %f275@0))
+       (or
+        (__node_trans_HH_4 false true false %f156@0 %f157@0 %f271@0)
+        (__node_trans_HH_4
+         false
+         false
+         false
+         %f156@0
+         %f157@0
+         %f271@0)))
+      (and
+       %f150@0
+       (__node_trans_HH_4 true true false %f156@0 %f157@0 %f271@0)
+       (or
+        (__node_trans_FTH_4
+         false
+         false
+         false
+         true
+         false
+         true
+         %f154@0
+         %f274@0
+         %f273@0
+         %f272@0)
+        (__node_trans_FTH_4
+         false
+         false
+         false
+         false
+         false
+         true
+         %f154@0
+         %f274@0
+         %f273@0
+         %f272@0))
+       (or
+        (__node_trans_HH_4 false true false true %f151@0 %f275@0)
+        (__node_trans_HH_4 false false false true %f151@0 %f275@0)))))
+    (and
+     X20
+     (not X21)
+     (or
+      (and
+       (not %f150@0)
+       (__node_trans_HH_4 true true false false %f151@0 %f275@0)
+       (or
+        (and
+         (__node_trans_HH_4
+          false
+          true
+          false
+          %f156@0
+          %f157@0
+          %f271@0)
+         (or
+          (__node_trans_FTH_4
+           true
+           false
+           false
+           true
+           false
+           false
+           %f154@0
+           %f274@0
+           %f273@0
+           %f272@0)
+          (and
+           (= %f148@0 X19)
+           (= %f149@0 X18)
+           (__node_trans_FTH_4
+            true
+            true
+            false
+            true
+            false
+            false
+            %f154@0
+            %f274@0
+            %f273@0
+            %f272@0))))
+        (and
+         (__node_trans_HH_4
+          false
+          false
+          false
+          %f156@0
+          %f157@0
+          %f271@0)
+         (or
+          (__node_trans_FTH_4
+           true
+           true
+           false
+           true
+           false
+           false
+           %f154@0
+           %f274@0
+           %f273@0
+           %f272@0)
+          (__node_trans_FTH_4
+           true
+           false
+           false
+           true
+           false
+           false
+           %f154@0
+           %f274@0
+           %f273@0
+           %f272@0)))))
+      (and
+       %f150@0
+       (__node_trans_HH_4 true true false %f156@0 %f157@0 %f271@0)
+       (__node_trans_HH_4 true true false true %f151@0 %f275@0)
+       (or
+        (__node_trans_FTH_4
+         true
+         false
+         false
+         true
+         false
+         true
+         %f154@0
+         %f274@0
+         %f273@0
+         %f272@0)
+        (and
+         (= %f148@0 X19)
+         (= %f149@0 X18)
+         (__node_trans_FTH_4
+          true
+          true
+          false
+          true
+          false
+          true
+          %f154@0
+          %f274@0
+          %f273@0
+          %f272@0))))))))))
+
+(exit)
+;; NoResponse 
+