Enable new implementation of CEGQI based on nested quantifier elimination (#5477)

This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.

The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.

Fixes #5365, fixes #5279, fixes #4849, fixes #4433.

This PR also required fixes related to how quantifier elimination is computed.

1 files changed, 24 insertions, 4 deletions

diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index 38fd57790..59e9dfc9e 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/quant_elim_solver.h"
 
+#include "expr/subs.h"
 #include "smt/smt_solver.h"
 #include "theory/quantifiers/extended_rewrite.h"
 #include "theory/rewriter.h"
@@ -33,7 +34,7 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
                                                Node q,
                                                bool doFull)
 {
-  Trace("smt-qe") << "Do quantifier elimination " << q << std::endl;
+  Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl;
   if (q.getKind() != EXISTS && q.getKind() != FORALL)
   {
     throw ModalException(
@@ -73,6 +74,10 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
       // failed, return original
       return q;
     }
+    // must use original quantified formula to compute QE, which ensures that
+    // e.g. term formula removal is not run on the body. Notice that we assume
+    // that the (single) quantified formula is preprocessed, rewritten
+    // version of the input quantified formula q.
     std::vector<Node> inst_qs;
     te->getInstantiatedQuantifiedFormulas(inst_qs);
     Assert(inst_qs.size() <= 1);
@@ -81,9 +86,24 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     {
       Node topq = inst_qs[0];
       Assert(topq.getKind() == FORALL);
-      Trace("smt-qe") << "Get qe for " << topq << std::endl;
-      ret = te->getInstantiatedConjunction(topq);
-      Trace("smt-qe") << "Returned : " << ret << std::endl;
+      Trace("smt-qe") << "Get qe based on preprocessed quantified formula "
+                      << topq << std::endl;
+      std::vector<std::vector<Node>> insts;
+      te->getInstantiationTermVectors(topq, insts);
+      std::vector<Node> vars(ne[0].begin(), ne[0].end());
+      std::vector<Node> conjs;
+      // apply the instantiation on the original body
+      for (const std::vector<Node>& inst : insts)
+      {
+        // note we do not convert to witness form here, since we could be
+        // an internal subsolver
+        Subs s;
+        s.add(vars, inst);
+        Node c = s.apply(ne[1].negate());
+        conjs.push_back(c);
+      }
+      ret = nm->mkAnd(conjs);
+      Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
       if (q.getKind() == EXISTS)
       {
         ret = Rewriter::rewrite(ret.negate());