Improve CEGQI heuristics involving equality and multiple instantiations (#2254)

9 files changed, 338 insertions, 204 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 678691ef4..83098e3ba 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -57,7 +57,7 @@ class CegInstantiatorBvInverterQuery : public BvInverterQuery
 };
 
 BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn)
-    : Instantiator(qe, tn), d_tried_assertion_inst(false)
+    : Instantiator(qe, tn)
 {
   // get the global inverter utility
   // this must be global since we need to:
@@ -79,7 +79,6 @@ void BvInstantiator::reset(CegInstantiator* ci,
   d_inst_id_to_alit.clear();
   d_var_to_curr_inst_id.clear();
   d_alit_to_model_slack.clear();
-  d_tried_assertion_inst = false;
 }
 
 void BvInstantiator::processLiteral(CegInstantiator* ci,
@@ -266,8 +265,7 @@ bool BvInstantiator::useModelValue(CegInstantiator* ci,
                                    Node pv,
                                    CegInstEffort effort)
 {
-  return !d_tried_assertion_inst
-         && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort());
+  return effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort();
 }
 
 bool BvInstantiator::processAssertions(CegInstantiator* ci,
@@ -359,7 +357,6 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci,
     TermProperties pv_prop_bv;
     Trace("cegqi-bv") << "*** try " << pv << " -> " << inst_term << std::endl;
     d_var_to_curr_inst_id[pv] = inst_id;
-    d_tried_assertion_inst = true;
     ci->markSolved(alit);
     if (ci->constructInstantiationInc(
             pv, inst_term, pv_prop_bv, sf, revertOnSuccess))
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index 439309e91..35bc6c042 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -118,8 +118,6 @@ class BvInstantiator : public Instantiator
   /** the amount of slack we added for asserted literals */
   std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack;
   //--------------------------------end solved forms
-  /** whether we have tried an instantiation based on assertion in this round */
-  bool d_tried_assertion_inst;
   /** rewrite assertion for solve pv
    *
    * Returns a literal that is equivalent to lit that leads to best solved form
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index 54dc78442..3a0db0273 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -29,6 +29,14 @@ void DtInstantiator::reset(CegInstantiator* ci,
 {
 }
 
+bool DtInstantiator::hasProcessEqualTerm(CegInstantiator* ci,
+                                         SolvedForm& sf,
+                                         Node pv,
+                                         CegInstEffort effort)
+{
+  return true;
+}
+
 bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
                                        SolvedForm& sf,
                                        Node pv,
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
index 37a81b625..6cf3bdf42 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
@@ -39,6 +39,11 @@ class DtInstantiator : public Instantiator
              SolvedForm& sf,
              Node pv,
              CegInstEffort effort) override;
+  /** this instantiator implements hasProcessEqualTerm */
+  bool hasProcessEqualTerm(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort) override;
   /** process equal terms
    *
    * This tries to find an equality eqc[i] = eqc[j] such that pv can be solved
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
index 7acdab00f..9f12f8b23 100644
--- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp
@@ -34,6 +34,14 @@ void EprInstantiator::reset(CegInstantiator* ci,
   d_equal_terms.clear();
 }
 
+bool EprInstantiator::hasProcessEqualTerm(CegInstantiator* ci,
+                                          SolvedForm& sf,
+                                          Node pv,
+                                          CegInstEffort effort)
+{
+  return true;
+}
+
 bool EprInstantiator::processEqualTerm(CegInstantiator* ci,
                                        SolvedForm& sf,
                                        Node pv,
diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
index cfc937bbd..b4378e1d2 100644
--- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h
@@ -41,6 +41,11 @@ class EprInstantiator : public Instantiator
              SolvedForm& sf,
              Node pv,
              CegInstEffort effort) override;
+  /** this instantiator implements hasProcessEqualTerm */
+  bool hasProcessEqualTerm(CegInstantiator* ci,
+                           SolvedForm& sf,
+                           Node pv,
+                           CegInstEffort effort) override;
   /** process equal terms
    *
    * This adds n to the set of equal terms d_equal_terms if matching heuristics
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 4c843606b..1abd1d4e1 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -394,6 +394,18 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index)
   d_curr_iphase[v] = CEG_INST_PHASE_NONE;
 }
 
+void CegInstantiator::deactivateInstantiationVariable(Node v)
+{
+  d_curr_subs_proc.erase(v);
+  d_curr_index.erase(v);
+  d_curr_iphase.erase(v);
+}
+
+bool CegInstantiator::hasTriedInstantiation(Node v)
+{
+  return !d_curr_subs_proc[v].empty();
+}
+
 void CegInstantiator::registerTheoryIds(TypeNode tn,
                                         std::map<TypeNode, bool>& visited)
 {
@@ -454,13 +466,6 @@ void CegInstantiator::registerVariable(Node v, bool is_aux)
   registerTheoryIds(vtn, visited);
 }
 
-void CegInstantiator::deactivateInstantiationVariable(Node v)
-{
-  d_curr_subs_proc.erase( v );
-  d_curr_index.erase( v );
-  d_curr_iphase.erase(v);
-}
-
 bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
 {
   if( i==d_vars.size() ){
@@ -499,14 +504,13 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       return doAddInstantiation( sf.d_vars, sf.d_subs, lemmas );
     }
   }else{
-    //Node v = d_single_inv_map_to_prog[d_single_inv[0][i]];
-    bool is_cv = false;
+    bool is_sv = false;
     Node pv;
     if( d_stack_vars.empty() ){
       pv = d_vars[i];
     }else{
       pv = d_stack_vars.back();
-      is_cv = true;
+      is_sv = true;
       d_stack_vars.pop_back();
     }
     activateInstantiationVariable(pv, i);
@@ -520,196 +524,24 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     Assert( vinst!=NULL );
     d_active_instantiators[pv] = vinst;
     vinst->reset(this, sf, pv, d_effort);
-
-    TypeNode pvtn = pv.getType();
-    TypeNode pvtnb = pvtn.getBaseType();
-    Node pvr = pv;
-    if( d_qe->getMasterEqualityEngine()->hasTerm( pv ) ){
-      pvr = d_qe->getMasterEqualityEngine()->getRepresentative( pv );
-    }
-    Trace("cbqi-inst-debug") << "[Find instantiation for " << pv << "], rep=" << pvr << ", instantiator is " << vinst->identify() << std::endl;
-    Node pv_value;
-    if( options::cbqiModel() ){
-      pv_value = getModelValue( pv );
-      Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
-    }
-
     // if d_effort is full, we must choose at least one model value
     if ((i + 1) < d_vars.size() || d_effort != CEG_INST_EFFORT_FULL)
     {
-      //[1] easy case : pv is in the equivalence class as another term not containing pv
-      Trace("cbqi-inst-debug") << "[1] try based on equivalence class." << std::endl;
-      d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
-      std::map< Node, std::vector< Node > >::iterator it_eqc = d_curr_eqc.find( pvr );
-      if( it_eqc!=d_curr_eqc.end() ){
-        //std::vector< Node > eq_candidates;
-        Trace("cbqi-inst-debug2") << "...eqc has size " << it_eqc->second.size() << std::endl;
-        for( unsigned k=0; k<it_eqc->second.size(); k++ ){
-          Node n = it_eqc->second[k];
-          if( n!=pv ){
-            Trace("cbqi-inst-debug") << "...try based on equal term " << n << std::endl;
-            //must be an eligible term
-            if( isEligible( n ) ){
-              Node ns;
-              TermProperties pv_prop;  //coefficient of pv in the equality we solve (null is 1)
-              bool proc = false;
-              if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( pvtn, n, sf, pv_prop, false );
-                if( !ns.isNull() ){
-                  computeProgVars( ns );
-                  //substituted version must be new and cannot contain pv
-                  proc = d_prog_var[ns].find( pv )==d_prog_var[ns].end();
-                }
-              }else{
-                ns = n;
-                proc = true;
-              }
-              if( proc ){
-                if (vinst->processEqualTerm(
-                        this, sf, pv, pv_prop, ns, d_effort))
-                {
-                  return true;
-                }
-                // Do not consider more than one equal term,
-                // this helps non-monotonic strategies that may encounter
-                // duplicate instantiations.
-                break;
-              }
-            }
-          }
-        }
-        if (vinst->processEqualTerms(this, sf, pv, it_eqc->second, d_effort))
-        {
-          return true;
-        }
-      }else{
-        Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
-      }
-
-      //[2] : we can solve an equality for pv
-      /// iterate over equivalence classes to find cases where we can solve for
-      /// the variable
-      if (vinst->hasProcessEquality(this, sf, pv, d_effort))
+      // First, try to construct an instantiation term for pv based on
+      // equality and theory-specific instantiation techniques.
+      if (constructInstantiation(sf, vinst, pv))
       {
-        Trace("cbqi-inst-debug") << "[2] try based on solving equalities." << std::endl;
-        d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
-        for( unsigned k=0; k<d_curr_type_eqc[pvtnb].size(); k++ ){
-          Node r = d_curr_type_eqc[pvtnb][k];
-          std::map< Node, std::vector< Node > >::iterator it_reqc = d_curr_eqc.find( r );
-          std::vector< Node > lhs;
-          std::vector< bool > lhs_v;
-          std::vector< TermProperties > lhs_prop;
-          Assert( it_reqc!=d_curr_eqc.end() );
-          for( unsigned kk=0; kk<it_reqc->second.size(); kk++ ){
-            Node n = it_reqc->second[kk];
-            Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
-            //must be an eligible term
-            if( isEligible( n ) ){
-              Node ns;
-              TermProperties pv_prop;
-              if( !d_prog_var[n].empty() ){
-                ns = applySubstitution( pvtn, n, sf, pv_prop );
-                if( !ns.isNull() ){
-                  computeProgVars( ns );
-                }
-              }else{
-                ns = n;
-              }
-              if( !ns.isNull() ){
-                bool hasVar = d_prog_var[ns].find( pv )!=d_prog_var[ns].end();
-                Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv << " : " << hasVar << std::endl;
-                std::vector< TermProperties > term_props;
-                std::vector< Node > terms;
-                term_props.push_back( pv_prop );
-                terms.push_back( ns );
-                for( unsigned j=0; j<lhs.size(); j++ ){
-                  //if this term or the another has pv in it, try to solve for it
-                  if( hasVar || lhs_v[j] ){
-                    Trace("cbqi-inst-debug") << "... " << i << "...try based on equality " << lhs[j] << " = " << ns << std::endl;
-                    term_props.push_back( lhs_prop[j] );
-                    terms.push_back( lhs[j] );
-                    if (vinst->processEquality(
-                            this, sf, pv, term_props, terms, d_effort))
-                    {
-                      return true;
-                    }
-                    term_props.pop_back();
-                    terms.pop_back();
-                  }
-                }
-                lhs.push_back( ns );
-                lhs_v.push_back( hasVar );
-                lhs_prop.push_back( pv_prop );
-              }else{
-                Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible after substitution." << std::endl;
-              }
-            }else{
-              Trace("cbqi-inst-debug2") << "... term " << n << " is ineligible." << std::endl;
-            }
-          }
-        }
-      }
-
-      //[3] directly look at assertions
-      if (vinst->hasProcessAssertion(this, sf, pv, d_effort))
-      {
-        Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
-        d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
-        std::unordered_set< Node, NodeHashFunction > lits;
-        //unsigned rmax = Theory::theoryOf( pv )==Theory::theoryOf( pv.getType() ) ? 1 : 2;
-        for( unsigned r=0; r<2; r++ ){
-          TheoryId tid = r==0 ? Theory::theoryOf( pvtn ) : THEORY_UF;
-          Trace("cbqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
-          std::map< TheoryId, std::vector< Node > >::iterator ita = d_curr_asserts.find( tid );
-          if( ita!=d_curr_asserts.end() ){
-            for (unsigned j = 0; j<ita->second.size(); j++) {
-              Node lit = ita->second[j];
-              if( lits.find(lit)==lits.end() ){
-                lits.insert(lit);
-                Node plit;
-                if (options::cbqiRepeatLit() || !isSolvedAssertion(lit))
-                {
-                  plit =
-                      vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
-                }
-                if (!plit.isNull()) {
-                  Trace("cbqi-inst-debug2") << "  look at " << lit;
-                  if (plit != lit) {
-                    Trace("cbqi-inst-debug2") << "...processed to : " << plit;
-                  }
-                  Trace("cbqi-inst-debug2") << std::endl;
-                  // apply substitutions
-                  Node slit = applySubstitutionToLiteral(plit, sf);
-                  if( !slit.isNull() ){
-                    // check if contains pv
-                    if( hasVariable( slit, pv ) ){
-                      Trace("cbqi-inst-debug") << "...try based on literal "
-                                               << slit << "," << std::endl;
-                      Trace("cbqi-inst-debug") << "...from " << lit
-                                               << std::endl;
-                      if (vinst->processAssertion(
-                              this, sf, pv, slit, lit, d_effort))
-                      {
-                        return true;
-                      }
-                    }
-                  }
-                }
-              }
-            }
-          }
-        }
-        if (vinst->processAssertions(this, sf, pv, d_effort))
-        {
-          return true;
-        }
+        return true;
       }
     }
-
-    //[4] resort to using value in model. We do so if:
-    // - if the instantiator uses model values at this effort, or
-    // - if we are solving for a subfield of a datatype (is_cv).
-    if ((vinst->useModelValue(this, sf, pv, d_effort) || is_cv)
+    // If the above call fails, resort to using value in model. We do so if:
+    // - we have yet to try an instantiation this round (or we are trying
+    //   multiple instantiations, indicated by options::cbqiMultiInst),
+    // - the instantiator uses model values at this effort or
+    //   if we are solving for a subfield of a datatype (is_sv), and
+    // - the instantiator allows model values.
+    if ((options::cbqiMultiInst() || !hasTriedInstantiation(pv))
+        && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
 #ifdef CVC4_ASSERTIONS
@@ -742,8 +574,10 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
       }
       d_effort = prev;
     }
+
     Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
-    if( is_cv ){
+    if (is_sv)
+    {
       d_stack_vars.push_back( pv );
     }
     d_active_instantiators.erase( pv );
@@ -752,6 +586,254 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
   }
 }
 
+bool CegInstantiator::constructInstantiation(SolvedForm& sf,
+                                             Instantiator* vinst,
+                                             Node pv)
+{
+  TypeNode pvtn = pv.getType();
+  TypeNode pvtnb = pvtn.getBaseType();
+  Node pvr = pv;
+  if (d_qe->getMasterEqualityEngine()->hasTerm(pv))
+  {
+    pvr = d_qe->getMasterEqualityEngine()->getRepresentative(pv);
+  }
+  Trace("cbqi-inst-debug") << "[Find instantiation for " << pv
+                           << "], rep=" << pvr << ", instantiator is "
+                           << vinst->identify() << std::endl;
+  Node pv_value;
+  if (options::cbqiModel())
+  {
+    pv_value = getModelValue(pv);
+    Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+  }
+
+  //[1] easy case : pv is in the equivalence class as another term not
+  // containing pv
+  if (vinst->hasProcessEqualTerm(this, sf, pv, d_effort))
+  {
+    Trace("cbqi-inst-debug")
+        << "[1] try based on equivalence class." << std::endl;
+    d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
+    std::map<Node, std::vector<Node> >::iterator it_eqc = d_curr_eqc.find(pvr);
+    if (it_eqc != d_curr_eqc.end())
+    {
+      // std::vector< Node > eq_candidates;
+      Trace("cbqi-inst-debug2")
+          << "...eqc has size " << it_eqc->second.size() << std::endl;
+      for (const Node& n : it_eqc->second)
+      {
+        if (n != pv)
+        {
+          Trace("cbqi-inst-debug")
+              << "...try based on equal term " << n << std::endl;
+          // must be an eligible term
+          if (isEligible(n))
+          {
+            Node ns;
+            // coefficient of pv in the equality we solve (null is 1)
+            TermProperties pv_prop;
+            bool proc = false;
+            if (!d_prog_var[n].empty())
+            {
+              ns = applySubstitution(pvtn, n, sf, pv_prop, false);
+              if (!ns.isNull())
+              {
+                computeProgVars(ns);
+                // substituted version must be new and cannot contain pv
+                proc = d_prog_var[ns].find(pv) == d_prog_var[ns].end();
+              }
+            }
+            else
+            {
+              ns = n;
+              proc = true;
+            }
+            if (proc)
+            {
+              if (vinst->processEqualTerm(this, sf, pv, pv_prop, ns, d_effort))
+              {
+                return true;
+              }
+              else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+              {
+                return false;
+              }
+              // Do not consider more than one equal term,
+              // this helps non-monotonic strategies that may encounter
+              // duplicate instantiations.
+              break;
+            }
+          }
+        }
+      }
+      if (vinst->processEqualTerms(this, sf, pv, it_eqc->second, d_effort))
+      {
+        return true;
+      }
+      else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+      {
+        return false;
+      }
+    }
+    else
+    {
+      Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
+    }
+  }
+
+  //[2] : we can solve an equality for pv
+  /// iterate over equivalence classes to find cases where we can solve for
+  /// the variable
+  if (vinst->hasProcessEquality(this, sf, pv, d_effort))
+  {
+    Trace("cbqi-inst-debug")
+        << "[2] try based on solving equalities." << std::endl;
+    d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
+    std::vector<Node>& cteqc = d_curr_type_eqc[pvtnb];
+
+    for (const Node& r : cteqc)
+    {
+      std::map<Node, std::vector<Node> >::iterator it_reqc = d_curr_eqc.find(r);
+      std::vector<Node> lhs;
+      std::vector<bool> lhs_v;
+      std::vector<TermProperties> lhs_prop;
+      Assert(it_reqc != d_curr_eqc.end());
+      for (const Node& n : it_reqc->second)
+      {
+        Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
+        // must be an eligible term
+        if (isEligible(n))
+        {
+          Node ns;
+          TermProperties pv_prop;
+          if (!d_prog_var[n].empty())
+          {
+            ns = applySubstitution(pvtn, n, sf, pv_prop);
+            if (!ns.isNull())
+            {
+              computeProgVars(ns);
+            }
+          }
+          else
+          {
+            ns = n;
+          }
+          if (!ns.isNull())
+          {
+            bool hasVar = d_prog_var[ns].find(pv) != d_prog_var[ns].end();
+            Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv
+                                      << " : " << hasVar << std::endl;
+            std::vector<TermProperties> term_props;
+            std::vector<Node> terms;
+            term_props.push_back(pv_prop);
+            terms.push_back(ns);
+            for (unsigned j = 0, size = lhs.size(); j < size; j++)
+            {
+              // if this term or the another has pv in it, try to solve for it
+              if (hasVar || lhs_v[j])
+              {
+                Trace("cbqi-inst-debug") << "......try based on equality "
+                                         << lhs[j] << " = " << ns << std::endl;
+                term_props.push_back(lhs_prop[j]);
+                terms.push_back(lhs[j]);
+                if (vinst->processEquality(
+                        this, sf, pv, term_props, terms, d_effort))
+                {
+                  return true;
+                }
+                else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+                {
+                  return false;
+                }
+                term_props.pop_back();
+                terms.pop_back();
+              }
+            }
+            lhs.push_back(ns);
+            lhs_v.push_back(hasVar);
+            lhs_prop.push_back(pv_prop);
+          }
+          else
+          {
+            Trace("cbqi-inst-debug2")
+                << "... term " << n << " is ineligible after substitution."
+                << std::endl;
+          }
+        }
+        else
+        {
+          Trace("cbqi-inst-debug2")
+              << "... term " << n << " is ineligible." << std::endl;
+        }
+      }
+    }
+  }
+  //[3] directly look at assertions
+  if (!vinst->hasProcessAssertion(this, sf, pv, d_effort))
+  {
+    return false;
+  }
+  Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
+  d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
+  std::unordered_set<Node, NodeHashFunction> lits;
+  for (unsigned r = 0; r < 2; r++)
+  {
+    TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF;
+    Trace("cbqi-inst-debug2") << "  look at assertions of " << tid << std::endl;
+    std::map<TheoryId, std::vector<Node> >::iterator ita =
+        d_curr_asserts.find(tid);
+    if (ita != d_curr_asserts.end())
+    {
+      for (const Node& lit : ita->second)
+      {
+        if (lits.find(lit) == lits.end())
+        {
+          lits.insert(lit);
+          Node plit;
+          if (options::cbqiRepeatLit() || !isSolvedAssertion(lit))
+          {
+            plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
+          }
+          if (!plit.isNull())
+          {
+            Trace("cbqi-inst-debug2") << "  look at " << lit;
+            if (plit != lit)
+            {
+              Trace("cbqi-inst-debug2") << "...processed to : " << plit;
+            }
+            Trace("cbqi-inst-debug2") << std::endl;
+            // apply substitutions
+            Node slit = applySubstitutionToLiteral(plit, sf);
+            if (!slit.isNull())
+            {
+              // check if contains pv
+              if (hasVariable(slit, pv))
+              {
+                Trace("cbqi-inst-debug")
+                    << "...try based on literal " << slit << "," << std::endl;
+                Trace("cbqi-inst-debug") << "...from " << lit << std::endl;
+                if (vinst->processAssertion(this, sf, pv, slit, lit, d_effort))
+                {
+                  return true;
+                }
+                else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+                {
+                  return false;
+                }
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  if (vinst->processAssertions(this, sf, pv, d_effort))
+  {
+    return true;
+  }
+  return false;
+}
+
 void CegInstantiator::pushStackVariable( Node v ) {
   d_stack_vars.push_back( v );
 }
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 537d8d74f..ae191cf91 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -548,6 +548,11 @@ class CegInstantiator {
    * for the quantified formula we are processing.
    */
   void deactivateInstantiationVariable(Node v);
+  /**
+   * Have we tried an instantiation for v after the last call to
+   * activateInstantiationVariable.
+   */
+  bool hasTriedInstantiation(Node v);
   //-------------------------------end current state
 
   //---------------------------------for applying substitutions
@@ -582,12 +587,24 @@ class CegInstantiator {
   std::map<Node, Instantiator*> d_instantiator;
 
   /** construct instantiation
-   * This method constructs the current instantiation, where we
-   * are currently processing the i^th variable in d_vars.
+   *
+   * This method attempts to find a term for the i^th variable in d_vars to
+   * include in the current instantiation, given by sf.
+   *
    * It returns true if a successful call to the output channel's
    * doAddInstantiation was made.
    */
   bool constructInstantiation(SolvedForm& sf, unsigned i);
+  /** construct instantiation
+   *
+   * Helper method for the above method. This method attempts to find a term for
+   * variable pv to include in the current instantiation, given by sf based
+   * on equality and theory-specific instantiation techniques. The latter is
+   * managed by the instantiator object vinst. Prior to calling this method,
+   * the variable pv has been activated by a call to
+   * activateInstantiationVariable.
+   */
+  bool constructInstantiation(SolvedForm& sf, Instantiator* vinst, Node pv);
   /** do add instantiation
    * This method is called by the above function after we finalize the
    * variables/substitution and auxiliary lemmas.
@@ -638,6 +655,18 @@ public:
   {
   }
 
+  /** has process equal term
+   *
+   * Whether this instantiator implements processEqualTerm and
+   * processEqualTerms.
+   */
+  virtual bool hasProcessEqualTerm(CegInstantiator* ci,
+                                   SolvedForm& sf,
+                                   Node pv,
+                                   CegInstEffort effort)
+  {
+    return false;
+  }
   /** process equal term
    *
    * This method is called when the entailment:
diff --git a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
index 8e318a372..7d981597a 100644
--- a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
+++ b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --cbqi-multi-inst
+; EXPECT: unsat
 (set-info :smt-lib-version 2.6)
 (set-logic NRA)
 (set-info :status unsat)