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.

15 files changed, 195 insertions, 388 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
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 488a25316..59666f6fd 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -630,20 +630,6 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
         && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
-#ifdef CVC4_ASSERTIONS
-      // the instantiation strategy for quantified linear integer/real
-      // arithmetic with arbitrary quantifier nesting is "monotonic" as a
-      // consequence of Lemmas 5, 9 and Theorem 4 of Reynolds et al, "Solving
-      // Quantified Linear Arithmetic by Counterexample Guided Instantiation",
-      // FMSD 2017. We throw an assertion failure if we detect a case where the
-      // strategy was not monotonic.
-      if (options::cegqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
-          && d_qe->getLogicInfo().isLinear())
-      {
-        Trace("cegqi-warn") << "Had to resort to model value." << std::endl;
-        Assert(false);
-      }
-#endif
       Node mv = getModelValue( pv );
       TermProperties pv_prop_m;
       Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 561817aa8..1a67a2b16 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -56,20 +56,20 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe)
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
       d_added_cbqi_lemma(qe->getUserContext()),
-      d_elim_quants(qe->getSatContext()),
       d_vtsCache(new VtsTermCache(qe)),
-      d_bv_invert(nullptr),
-      d_nested_qe_waitlist_size(qe->getUserContext()),
-      d_nested_qe_waitlist_proc(qe->getUserContext())
+      d_bv_invert(nullptr)
 {
-  d_qid_count = 0;
   d_small_const =
       NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
   d_check_vts_lemma_lc = false;
   if (options::cegqiBv())
   {
     // if doing instantiation for BV, need the inverter class
-    d_bv_invert.reset(new quantifiers::BvInverter);
+    d_bv_invert.reset(new BvInverter);
+  }
+  if (options::cegqiNestedQE())
+  {
+    d_nestedQe.reset(new NestedQe(qe->getUserContext()));
   }
 }
 
@@ -177,16 +177,6 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         if( doCbqi( quants[i] ) ){
           registerCbqiLemma( quants[i] );
         }
-        if( options::cegqiNestedQE() ){
-          //record these as counterexample quantifiers
-          QAttributes qa;
-          QuantAttributes::computeQuantAttributes( quants[i], qa );
-          if( !qa.d_qid_num.isNull() ){
-            d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
-            d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
-            Trace("cegqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
-          }
-        }
       }
     }
     // The decision strategy for this quantified formula ensures that its
@@ -226,7 +216,6 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
     Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
     //it is not active if it corresponds to a rewrite rule: we will process in rewrite engine
     if( doCbqi( q ) ){
-      Assert(hasAddedCbqiLemma(q));
       if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
         d_active_quant[q] = true;
         Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
@@ -242,20 +231,6 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
               d_quantEngine->getModel()->setQuantifierActive( q, false );
               d_cbqi_set_quant_inactive = true;
               d_active_quant.erase( q );
-              d_elim_quants.insert( q );
-              Trace("cegqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
-              //process from waitlist
-              while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
-                int index = d_nested_qe_waitlist_proc[q];
-                Assert(index >= 0);
-                Assert(index < (int)d_nested_qe_waitlist[q].size());
-                Node nq = d_nested_qe_waitlist[q][index];
-                Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
-                Node dqelem = nq.eqNode( nqeqn ); 
-                Trace("cegqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
-                d_quantEngine->getOutputChannel().lemma( dqelem );
-                d_nested_qe_waitlist_proc[q] = index + 1;
-              }
             }
           }
         }else{
@@ -312,14 +287,10 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
       for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
         Node q = it->first;
         Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
-        if( d_nested_qe.find( q )==d_nested_qe.end() ){
-          process( q, e, ee );
-          if( d_quantEngine->inConflict() ){
-            break;
-          }
-        }else{
-          Trace("cegqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
-          Assert(false);
+        process(q, e, ee);
+        if (d_quantEngine->inConflict())
+        {
+          break;
         }
       }
       if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
@@ -355,55 +326,6 @@ bool InstStrategyCegqi::checkCompleteFor(Node q)
   }
 }
 
-Node InstStrategyCegqi::getIdMarkedQuantNode(Node n,
-                                             std::map<Node, Node>& visited)
-{
-  std::map< Node, Node >::iterator it = visited.find( n );
-  if( it==visited.end() ){
-    Node ret = n;
-    if( n.getKind()==FORALL ){
-      QAttributes qa;
-      QuantAttributes::computeQuantAttributes( n, qa );
-      if( qa.d_qid_num.isNull() ){
-        std::vector< Node > rc;
-        rc.push_back( n[0] );
-        rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
-        Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
-        QuantIdNumAttribute ida;
-        avar.setAttribute(ida,d_qid_count);
-        d_qid_count++;
-        std::vector< Node > iplc;
-        iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
-        if( n.getNumChildren()==3 ){
-          for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
-            iplc.push_back( n[2][i] );
-          }
-        }
-        rc.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
-        ret = NodeManager::currentNM()->mkNode( FORALL, rc );
-      }
-    }else if( n.getNumChildren()>0 ){
-      std::vector< Node > children;
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( n.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = getIdMarkedQuantNode( n[i], visited );
-        childChanged = childChanged || nc!=n[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return it->second;
-  }
-}
-
 void InstStrategyCegqi::checkOwnership(Node q)
 {
   if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){
@@ -417,34 +339,13 @@ void InstStrategyCegqi::checkOwnership(Node q)
 
 void InstStrategyCegqi::preRegisterQuantifier(Node q)
 {
-  // mark all nested quantifiers with id
-  if (options::cegqiNestedQE())
+  if (doCbqi(q))
   {
-    if( d_quantEngine->getOwner(q)==this )
+    if (processNestedQe(q, true))
     {
-      std::map<Node, Node> visited;
-      Node mq = getIdMarkedQuantNode(q[1], visited);
-      if (mq != q[1])
-      {
-        // do not do cbqi, we are reducing this quantified formula to a marked
-        // one
-        d_do_cbqi[q] = CEG_UNHANDLED;
-        // instead do reduction
-        std::vector<Node> qqc;
-        qqc.push_back(q[0]);
-        qqc.push_back(mq);
-        if (q.getNumChildren() == 3)
-        {
-          qqc.push_back(q[2]);
-        }
-        Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc);
-        Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq);
-        Trace("cegqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
-        d_quantEngine->addLemma(mlem);
-      }
+      // will process using nested quantifier elimination
+      return;
     }
-  }
-  if( doCbqi( q ) ){
     // get the instantiator
     if (options::cegqiPreRegInst())
     {
@@ -470,10 +371,6 @@ TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
     inst = d_vtsCache->rewriteVtsSymbols(inst);
     Trace("quant-vts-debug") << "...got " << inst << std::endl;
   }
-  if (options::cegqiNestedQE())
-  {
-    inst = doNestedQE(q, terms, inst, doVts);
-  }
   if (prevInst != inst)
   {
     // not proof producing yet
@@ -487,110 +384,6 @@ InstantiationRewriter* InstStrategyCegqi::getInstRewriter() const
   return d_irew.get();
 }
 
-Node InstStrategyCegqi::doNestedQENode(
-    Node q, Node ceq, Node n, std::vector<Node>& inst_terms, bool doVts)
-{
-  // there is a nested quantified formula (forall y. nq[y,x]) such that 
-  //    q is (forall y. nq[y,t]) for ground terms t,
-  //    ceq is (forall y. nq[y,e]) for CE variables e.
-  // we call this function when we know (forall y. nq[y,e]) is equivalent to quantifier-free formula C[e].
-  // in this case, q is equivalent to the quantifier-free formula C[t].
-  if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
-    d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
-    Trace("cegqi-nqe") << "CE quantifier elimination : " << std::endl;
-    Trace("cegqi-nqe") << "  " << ceq << std::endl; 
-    Trace("cegqi-nqe") << "  " << d_nested_qe[ceq] << std::endl;
-    //should not contain quantifiers
-    Assert(!expr::hasClosure(d_nested_qe[ceq]));
-  }
-  Assert(d_quantEngine->getTermUtil()->d_inst_constants[q].size()
-         == inst_terms.size());
-  //replace inst constants with instantiation
-  Node ret = d_nested_qe[ceq].substitute( d_quantEngine->getTermUtil()->d_inst_constants[q].begin(),
-                                          d_quantEngine->getTermUtil()->d_inst_constants[q].end(),
-                                          inst_terms.begin(), inst_terms.end() );
-  if( doVts ){
-    //do virtual term substitution
-    ret = Rewriter::rewrite( ret );
-    ret = d_vtsCache->rewriteVtsSymbols(ret);
-  }
-  Trace("cegqi-nqe") << "Nested quantifier elimination: " << std::endl;
-  Trace("cegqi-nqe") << "  " << n << std::endl; 
-  Trace("cegqi-nqe") << "  " << ret << std::endl;
-  return ret;
-}
-
-Node InstStrategyCegqi::doNestedQERec(Node q,
-                                      Node n,
-                                      std::map<Node, Node>& visited,
-                                      std::vector<Node>& inst_terms,
-                                      bool doVts)
-{
-  if( visited.find( n )==visited.end() ){
-    Node ret = n;
-    if( n.getKind()==FORALL ){
-      QAttributes qa;
-      QuantAttributes::computeQuantAttributes( n, qa );
-      if( !qa.d_qid_num.isNull() ){
-        //if it has an id, check whether we have done quantifier elimination for this id
-        std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
-        if( it!=d_id_to_ce_quant.end() ){
-          Node ceq = it->second;
-          bool doNestedQe = d_elim_quants.contains( ceq );
-          if( doNestedQe ){
-            ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
-          }else{
-            Trace("cegqi-nqe") << "Add to nested qe waitlist : " << std::endl;
-            Node nr = Rewriter::rewrite( n );
-            Trace("cegqi-nqe") << "  " << ceq << std::endl;
-            Trace("cegqi-nqe") << "  " << nr << std::endl;
-            int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
-            d_nested_qe_waitlist_size[ceq] = wlsize;
-            if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
-              d_nested_qe_waitlist[ceq][wlsize] = nr;
-            }else{
-              d_nested_qe_waitlist[ceq].push_back( nr );
-            }
-            d_nested_qe_info[nr].d_q = q;
-            d_nested_qe_info[nr].d_inst_terms.clear();
-            d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
-            d_nested_qe_info[nr].d_doVts = doVts;
-            //TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
-            Assert(!options::cegqiInnermost());
-          }
-        } 
-      } 
-    }else if( n.getNumChildren()>0 ){
-      std::vector< Node > children;
-      if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
-        children.push_back( n.getOperator() );
-      }
-      bool childChanged = false;
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Node nc = doNestedQERec( q, n[i], visited, inst_terms, doVts );
-        childChanged = childChanged || nc!=n[i];
-        children.push_back( nc );
-      }
-      if( childChanged ){
-        ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
-      }
-    }
-    visited[n] = ret;
-    return ret;
-  }else{
-    return n;
-  }  
-}
-
-Node InstStrategyCegqi::doNestedQE(Node q,
-                                   std::vector<Node>& inst_terms,
-                                   Node lem,
-                                   bool doVts)
-{
-  std::map< Node, Node > visited;
-  return doNestedQERec( q, lem, visited, inst_terms, doVts );
-}
-
 void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
 {
   // must register with the instantiator
@@ -631,6 +424,13 @@ bool InstStrategyCegqi::doCbqi(Node q)
 }
 
 void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
+  // If we are doing nested quantifier elimination, check if q was already
+  // processed.
+  if (processNestedQe(q, false))
+  {
+    // don't need to process this, since it has been reduced
+    return;
+  }
   if( e==0 ){
     CegInstantiator * cinst = getInstantiator( q );
     Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
@@ -743,6 +543,33 @@ void InstStrategyCegqi::presolve() {
   }
 }
 
+bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
+{
+  if (d_nestedQe != nullptr)
+  {
+    if (isPreregister)
+    {
+      // If at preregister, we are done if we have nested quantification.
+      // We will process nested quantification.
+      return NestedQe::hasNestedQuantification(q);
+    }
+    // if not a preregister, we process, which may trigger quantifier
+    // elimination in subsolvers.
+    std::vector<Node> lems;
+    if (d_nestedQe->process(q, lems))
+    {
+      // add lemmas to process
+      for (const Node& lem : lems)
+      {
+        d_quantEngine->addLemma(lem);
+      }
+      // don't need to process this, since it has been reduced
+      return true;
+    }
+  }
+  return false;
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 0a3472968..2ca232699 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -21,6 +21,7 @@
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/cegqi/nested_qe.h"
 #include "theory/quantifiers/cegqi/vts_term_cache.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
@@ -143,8 +144,6 @@ class InstStrategyCegqi : public QuantifiersModule
   bool d_incomplete_check;
   /** whether we have added cbqi lemma */
   NodeSet d_added_cbqi_lemma;
-  /** whether we have added cbqi lemma */
-  NodeSet d_elim_quants;
   /** parent guards */
   std::map< Node, std::vector< Node > > d_parent_quant;
   std::map< Node, std::vector< Node > > d_children_quant;
@@ -193,6 +192,14 @@ class InstStrategyCegqi : public QuantifiersModule
   void registerCounterexampleLemma(Node q, Node lem);
   /** has added cbqi lemma */
   bool hasAddedCbqiLemma( Node q ) { return d_added_cbqi_lemma.find( q )!=d_added_cbqi_lemma.end(); }
+  /**
+   * Return true if q can be processed with nested quantifier elimination.
+   * This may add a lemma on the output channel of quantifiers engine if so.
+   *
+   * @param q The quantified formula to process
+   * @param isPreregister Whether this method is being called at preregister.
+   */
+  bool processNestedQe(Node q, bool isPreregister);
   /** process functions */
   void process(Node q, Theory::Effort effort, int e);
   /**
@@ -204,44 +211,10 @@ class InstStrategyCegqi : public QuantifiersModule
   Node getCounterexampleLiteral(Node q);
   /** map from universal quantifiers to their counterexample literals */
   std::map<Node, Node> d_ce_lit;
-
-  //for identification
-  uint64_t d_qid_count;
-  //nested qe map
-  std::map< Node, Node > d_nested_qe;
-  //mark ids on quantifiers 
-  Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
-  // id to ce quant
-  std::map< Node, Node > d_id_to_ce_quant;
-  std::map< Node, Node > d_ce_quant_to_id;
-  //do nested quantifier elimination recursive
-  Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
-  Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );
-  //elimination information (for delayed elimination)
-  class NestedQEInfo {
-  public:
-    NestedQEInfo() : d_doVts(false){}
-    ~NestedQEInfo(){}
-    Node d_q;
-    std::vector< Node > d_inst_terms;
-    bool d_doVts;
-  };
-  std::map< Node, NestedQEInfo > d_nested_qe_info;
-  NodeIntMap d_nested_qe_waitlist_size;
-  NodeIntMap d_nested_qe_waitlist_proc;
-  std::map< Node, std::vector< Node > > d_nested_qe_waitlist;
-
-  /** Do nested quantifier elimination.
-   *
-   * This rewrites the quantified formulas in inst based on nested quantifier
-   * elimination. In this method, inst is the instantiation of quantified
-   * formula q for the vector terms. The flag doVts indicates whether we must
-   * apply virtual term substitution (if terms contains virtual terms).
-   */
-  Node doNestedQE(Node q, std::vector<Node>& terms, Node inst, bool doVts);
+  /** The nested quantifier elimination utility */
+  std::unique_ptr<NestedQe> d_nestedQe;
 };
 
-
 }
 }
 }
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 759fa026b..aaf7cb4bc 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -256,6 +256,32 @@ void InstMatchTrie::getExplanationForInstLemmas(
   }
 }
 
+void InstMatchTrie::getInstantiations(
+    Node q, std::vector<std::vector<Node>>& insts) const
+{
+  std::vector<Node> terms;
+  getInstantiations(q, insts, terms);
+}
+
+void InstMatchTrie::getInstantiations(Node q,
+                                      std::vector<std::vector<Node>>& insts,
+                                      std::vector<Node>& terms) const
+{
+  if (terms.size() == q[0].getNumChildren())
+  {
+    insts.push_back(terms);
+  }
+  else
+  {
+    for (const std::pair<const Node, InstMatchTrie>& d : d_data)
+    {
+      terms.push_back(d.first);
+      d.second.getInstantiations(q, insts, terms);
+      terms.pop_back();
+    }
+  }
+}
+
 CDInstMatchTrie::~CDInstMatchTrie()
 {
   for (std::pair<const Node, CDInstMatchTrie*>& d : d_data)
@@ -517,6 +543,36 @@ void CDInstMatchTrie::getExplanationForInstLemmas(
   }
 }
 
+void CDInstMatchTrie::getInstantiations(
+    Node q, std::vector<std::vector<Node>>& insts) const
+{
+  std::vector<Node> terms;
+  getInstantiations(q, insts, terms);
+}
+
+void CDInstMatchTrie::getInstantiations(Node q,
+                                        std::vector<std::vector<Node>>& insts,
+                                        std::vector<Node>& terms) const
+{
+  if (!d_valid.get())
+  {
+    // do nothing
+  }
+  else if (terms.size() == q[0].getNumChildren())
+  {
+    insts.push_back(terms);
+  }
+  else
+  {
+    for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data)
+    {
+      terms.push_back(d.first);
+      d.second->getInstantiations(q, insts, terms);
+      terms.pop_back();
+    }
+  }
+}
+
 } /* CVC4::theory::inst namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index 67a942c57..a63954838 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -125,6 +125,10 @@ class InstMatchTrie
                        Node lem,
                        ImtIndexOrder* imtio = NULL,
                        unsigned index = 0);
+  /**
+   * Adds the instantiations for q into insts.
+   */
+  void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
 
   /** get instantiations
    *
@@ -174,6 +178,10 @@ class InstMatchTrie
   std::map<Node, InstMatchTrie> d_data;
 
  private:
+  /** Helper for getInstantiations.*/
+  void getInstantiations(Node q,
+                         std::vector<std::vector<Node>>& insts,
+                         std::vector<Node>& terms) const;
   /** helper for print
    * terms accumulates the path we are on in the trie.
    */
@@ -293,6 +301,10 @@ class CDInstMatchTrie
                        std::vector<Node>& m,
                        Node lem,
                        unsigned index = 0);
+  /**
+   * Adds the instantiations for q into insts.
+   */
+  void getInstantiations(Node q, std::vector<std::vector<Node>>& insts) const;
 
   /** get instantiations
    *
@@ -338,6 +350,10 @@ class CDInstMatchTrie
   }
 
  private:
+  /** Helper for getInstantiations.*/
+  void getInstantiations(Node q,
+                         std::vector<std::vector<Node>>& insts,
+                         std::vector<Node>& terms) const;
   /** the data */
   std::map<Node, CDInstMatchTrie*> d_data;
   /** is valid */
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 8549b1eae..fb622452e 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -714,14 +714,39 @@ bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas)
 void Instantiate::getInstantiationTermVectors(
     Node q, std::vector<std::vector<Node> >& tvecs)
 {
-  std::vector<Node> lemmas;
-  getInstantiations(q, lemmas);
-  std::map<Node, Node> quant;
-  std::map<Node, std::vector<Node> > tvec;
-  getExplanationForInstLemmas(lemmas, quant, tvec);
-  for (std::pair<const Node, std::vector<Node> >& t : tvec)
+  // if track instantiations is true, we use the instantiation + explanation
+  // methods for doing minimization based on unsat cores.
+  if (options::trackInstLemmas())
+  {
+    std::vector<Node> lemmas;
+    getInstantiations(q, lemmas);
+    std::map<Node, Node> quant;
+    std::map<Node, std::vector<Node> > tvec;
+    getExplanationForInstLemmas(lemmas, quant, tvec);
+    for (std::pair<const Node, std::vector<Node> >& t : tvec)
+    {
+      tvecs.push_back(t.second);
+    }
+    return;
+  }
+
+  if (options::incrementalSolving())
+  {
+    std::map<Node, inst::CDInstMatchTrie*>::const_iterator it =
+        d_c_inst_match_trie.find(q);
+    if (it != d_c_inst_match_trie.end())
+    {
+      it->second->getInstantiations(q, tvecs);
+    }
+  }
+  else
   {
-    tvecs.push_back(t.second);
+    std::map<Node, inst::InstMatchTrie>::const_iterator it =
+        d_inst_match_trie.find(q);
+    if (it != d_inst_match_trie.end())
+    {
+      it->second.getInstantiations(q, tvecs);
+    }
   }
 }
 
@@ -730,14 +755,14 @@ void Instantiate::getInstantiationTermVectors(
 {
   if (options::incrementalSolving())
   {
-    for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie)
+    for (const auto& t : d_c_inst_match_trie)
     {
       getInstantiationTermVectors(t.first, insts[t.first]);
     }
   }
   else
   {
-    for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie)
+    for (const auto& t : d_inst_match_trie)
     {
       getInstantiationTermVectors(t.first, insts[t.first]);
     }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index ac7d6efc7..e9e15ef3b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -241,6 +241,8 @@ bool CegSingleInv::solve()
     Node body = siq[1];
     for (unsigned i = 0, ninsts = d_inst.size(); i < ninsts; i++)
     {
+      // note we do not convert to witness form here, since we could be
+      // an internal subsolver
       std::vector<Node>& inst = d_inst[i];
       Trace("sygus-si") << "  Instantiation: " << inst << std::endl;
       // instantiation should have same arity since we are not allowed to
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 7f0b46c99..297f11690 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1013,10 +1013,6 @@ void QuantifiersEngine::flushLemmas(){
   }
 }
 
-bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) {
-  return d_instantiate->getUnsatCoreLemmas(active_lemmas);
-}
-
 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
   d_instantiate->getInstantiationTermVectors(q, tvecs);
 }
@@ -1025,14 +1021,6 @@ void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector
   d_instantiate->getInstantiationTermVectors(insts);
 }
 
-void QuantifiersEngine::getExplanationForInstLemmas(
-    const std::vector<Node>& lems,
-    std::map<Node, Node>& quant,
-    std::map<Node, std::vector<Node> >& tvec)
-{
-  d_instantiate->getExplanationForInstLemmas(lems, quant, tvec);
-}
-
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
   bool printed = false;
   // print the skolemizations
@@ -1066,18 +1054,6 @@ void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >&
   d_instantiate->getInstantiatedQuantifiedFormulas(qs);
 }
 
-void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
-  d_instantiate->getInstantiations(insts);
-}
-
-void QuantifiersEngine::getInstantiations( Node q, std::vector< Node >& insts  ) {
-  d_instantiate->getInstantiations(q, insts);
-}
-
-Node QuantifiersEngine::getInstantiatedConjunction( Node q ) {
-  return d_instantiate->getInstantiatedConjunction(q);
-}
-
 QuantifiersEngine::Statistics::Statistics()
     : d_time("theory::QuantifiersEngine::time"),
       d_qcf_time("theory::QuantifiersEngine::time_qcf"),
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index e266e2058..8dcaf668f 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -278,22 +278,11 @@ public:
  void printSynthSolution(std::ostream& out);
  /** get list of quantified formulas that were instantiated */
  void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
- /** get instantiations */
- void getInstantiations(Node q, std::vector<Node>& insts);
- void getInstantiations(std::map<Node, std::vector<Node> >& insts);
  /** get instantiation term vectors */
  void getInstantiationTermVectors(Node q,
                                   std::vector<std::vector<Node> >& tvecs);
  void getInstantiationTermVectors(
      std::map<Node, std::vector<std::vector<Node> > >& insts);
- /** get instantiated conjunction */
- Node getInstantiatedConjunction(Node q);
- /** get unsat core lemmas */
- bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas);
- /** get explanation for instantiation lemmas */
- void getExplanationForInstLemmas(const std::vector<Node>& lems,
-                                  std::map<Node, Node>& quant,
-                                  std::map<Node, std::vector<Node> >& tvec);
 
  /** get synth solutions
   *
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index d54538049..dc59cbbf5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1215,14 +1215,6 @@ void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs )
   }
 }
 
-void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
-  if( d_quantEngine ){
-    d_quantEngine->getInstantiations( q, insts );
-  }else{
-    Assert(false);
-  }
-}
-
 void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
   if( d_quantEngine ){
     d_quantEngine->getInstantiationTermVectors( q, tvecs );
@@ -1231,14 +1223,6 @@ void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector
   }
 }
 
-void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
-  if( d_quantEngine ){
-    d_quantEngine->getInstantiations( insts );
-  }else{
-    Assert(false);
-  }
-}
-
 void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
   if( d_quantEngine ){
     d_quantEngine->getInstantiationTermVectors( insts );
@@ -1247,15 +1231,6 @@ void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std
   }
 }
 
-Node TheoryEngine::getInstantiatedConjunction( Node q ) {
-  if( d_quantEngine ){
-    return d_quantEngine->getInstantiatedConjunction( q );
-  }else{
-    Assert(false);
-    return Node::null();
-  }
-}
-
 TrustNode TheoryEngine::getExplanation(TNode node)
 {
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index ee3611a53..1412d7464 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -686,23 +686,14 @@ class TheoryEngine {
 
   /**
    * Get instantiation methods
-   *   first inputs forall x.q[x] and returns ( q[a], ..., q[z] )
-   *   second inputs forall x.q[x] and returns ( a, ..., z )
-   *   third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] )
+   *   the first given forall x.q[x] returns ( a, ..., z )
+   *   the second returns mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] )
    * , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
    */
-  void getInstantiations( Node q, std::vector< Node >& insts );
   void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
-  void getInstantiations( std::map< Node, std::vector< Node > >& insts );
   void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
 
   /**
-   * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q.
-   *   Can be used for quantifier elimination when satisfiable and q[t1] ^ ... ^ q[tn] |= q
-   */
-  Node getInstantiatedConjunction( Node q );
-
-  /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */