From 5d9fa2555c67e0d6661a69ee93d384f717b6858b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 2 Aug 2018 15:29:45 -0500 Subject: [PATCH] Improve CEGQI heuristics involving equality and multiple instantiations (#2254) --- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 7 +- .../quantifiers/cegqi/ceg_bv_instantiator.h | 2 - .../quantifiers/cegqi/ceg_dt_instantiator.cpp | 8 + .../quantifiers/cegqi/ceg_dt_instantiator.h | 5 + .../cegqi/ceg_epr_instantiator.cpp | 8 + .../quantifiers/cegqi/ceg_epr_instantiator.h | 5 + .../quantifiers/cegqi/ceg_instantiator.cpp | 472 ++++++++++-------- .../quantifiers/cegqi/ceg_instantiator.h | 33 +- .../quantifiers/nra-interleave-inst.smt2 | 2 + 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 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& 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; ksecond.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 >::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; kksecond.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; jhasProcessAssertion(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; jsecond.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 >::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& cteqc = d_curr_type_eqc[pvtnb]; + + for (const Node& r : cteqc) + { + std::map >::iterator it_reqc = d_curr_eqc.find(r); + std::vector lhs; + std::vector lhs_v; + std::vector 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 term_props; + std::vector 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 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 >::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 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) -- 2.30.2