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.

4 files changed, 26 insertions, 35 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());
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 0c2d06f1d..aaff29479 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -838,10 +838,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     options::cegqi.set(false);
   }
   // Do we need to track instantiations?
-  // Needed for sygus due to single invocation techniques.
-  if (options::cegqiNestedQE()
-      || (options::unsatCores() && !options::trackInstLemmas.wasSetByUser())
-      || is_sygus)
+  if (options::unsatCores() && !options::trackInstLemmas.wasSetByUser())
   {
     options::trackInstLemmas.set(true);
   }
@@ -1188,13 +1185,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
       // only supported in pure arithmetic or pure BV
       options::cegqiNestedQE.set(false);
     }
-    // prenexing
-    if (options::cegqiNestedQE())
-    {
-      // only complete with prenex = normal
-      options::prenexQuant.set(options::PrenexQuantMode::NORMAL);
-    }
-    else if (options::globalNegate())
+    if (options::globalNegate())
     {
       if (!options::prenexQuant.wasSetByUser())
       {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 27bcdc036..2a0cde015 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1560,14 +1560,6 @@ void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
   te->getInstantiatedQuantifiedFormulas(qs);
 }
 
-void SmtEngine::getInstantiations(Node q, std::vector<Node>& insts)
-{
-  SmtScope smts(this);
-  TheoryEngine* te = getTheoryEngine();
-  Assert(te != nullptr);
-  te->getInstantiations(q, insts);
-}
-
 void SmtEngine::getInstantiationTermVectors(
     Node q, std::vector<std::vector<Node>>& tvecs)
 {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 6c721b9b0..1c83fa61f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -652,18 +652,6 @@ class CVC4_PUBLIC SmtEngine
   void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
 
   /**
-   * Get instantiations for quantified formula q.
-   *
-   * If q was a quantified formula that was instantiated on the last call to
-   * check-sat (i.e. q is returned as part of the vector in the method
-   * getInstantiatedQuantifiedFormulas above), then the list of instantiations
-   * of that formula that were generated are added to insts.
-   *
-   * In particular, if q is of the form forall x. P(x), then insts is a list
-   * of formulas of the form P(t1), ..., P(tn).
-   */
-  void getInstantiations(Node q, std::vector<Node>& insts);
-  /**
    * Get instantiation term vectors for quantified formula q.
    *
    * This method is similar to above, but in the example above, we return the