diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-14 17:55:23 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-02-14 17:55:23 -0600 |
commit | bf385ca69a958e0939524d8fbcf988c1fb45d131 (patch) | |
tree | 469f60484b68df6ccd00cbc68320b1b18f2e0865 /src/theory/quantifiers/cegqi | |
parent | 3c730da7c39dc5cba11bdea99191e361e505bbc8 (diff) |
Quantifiers subdirectories (#1608)
Diffstat (limited to 'src/theory/quantifiers/cegqi')
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 1337 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.h | 783 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp | 1990 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/ceg_t_instantiator.h | 331 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp | 828 | ||||
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cbqi.h | 166 |
6 files changed, 5435 insertions, 0 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp new file mode 100644 index 000000000..d7d46bb4b --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -0,0 +1,1337 @@ +/********************* */ +/*! \file ceg_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of counterexample-guided quantifier instantiation + **/ + +#include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" + +#include "options/quantifiers_options.h" +#include "smt/term_formula_removal.h" +#include "theory/arith/arith_msum.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/theory_engine.h" + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +std::ostream& operator<<(std::ostream& os, CegInstEffort e) +{ + switch (e) + { + case CEG_INST_EFFORT_NONE: os << "?"; break; + case CEG_INST_EFFORT_STANDARD: os << "STANDARD"; break; + case CEG_INST_EFFORT_STANDARD_MV: os << "STANDARD_MV"; break; + case CEG_INST_EFFORT_FULL: os << "FULL"; break; + default: Unreachable(); + } + return os; +} + +std::ostream& operator<<(std::ostream& os, CegInstPhase phase) +{ + switch (phase) + { + case CEG_INST_PHASE_NONE: os << "?"; break; + case CEG_INST_PHASE_EQC: os << "eqc"; break; + case CEG_INST_PHASE_EQUAL: os << "eq"; break; + case CEG_INST_PHASE_ASSERTION: os << "as"; break; + case CEG_INST_PHASE_MVALUE: os << "mv"; break; + default: Unreachable(); + } + return os; +} + +CegInstantiator::CegInstantiator(QuantifiersEngine* qe, + CegqiOutput* out, + bool use_vts_delta, + bool use_vts_inf) + : d_qe(qe), + d_out(out), + d_use_vts_delta(use_vts_delta), + d_use_vts_inf(use_vts_inf), + d_is_nested_quant(false), + d_effort(CEG_INST_EFFORT_NONE) +{ +} + +CegInstantiator::~CegInstantiator() { + for (std::pair<Node, Instantiator*> inst : d_instantiator) + { + delete inst.second; + } + for (std::pair<TheoryId, InstantiatorPreprocess*> instp : d_tipp) + { + delete instp.second; + } +} + +void CegInstantiator::computeProgVars( Node n ){ + if( d_prog_var.find( n )==d_prog_var.end() ){ + d_prog_var[n].clear(); + if (n.getKind() == kind::CHOICE) + { + Assert(d_prog_var.find(n[0][0]) == d_prog_var.end()); + d_prog_var[n[0][0]].clear(); + } + if (d_vars_set.find(n) != d_vars_set.end()) + { + d_prog_var[n].insert(n); + }else if( !d_out->isEligibleForInstantiation( n ) ){ + d_inelig.insert(n); + return; + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + computeProgVars( n[i] ); + if( d_inelig.find( n[i] )!=d_inelig.end() ){ + d_inelig.insert(n); + } + // all variables in child are contained in this + d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end()); + } + // selectors applied to program variables are also variables + if (n.getKind() == APPLY_SELECTOR_TOTAL + && d_prog_var[n].find(n[0]) != d_prog_var[n].end()) + { + d_prog_var[n].insert(n); + } + if (n.getKind() == kind::CHOICE) + { + d_prog_var.erase(n[0][0]); + } + } +} + +bool CegInstantiator::isEligible( Node n ) { + //compute d_subs_fv, which program variables are contained in n, and determines if eligible + computeProgVars( n ); + return d_inelig.find( n )==d_inelig.end(); +} + +bool CegInstantiator::hasVariable( Node n, Node pv ) { + computeProgVars( n ); + return d_prog_var[n].find( pv )!=d_prog_var[n].end(); +} + +void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) +{ + if( d_instantiator.find( v )==d_instantiator.end() ){ + TypeNode tn = v.getType(); + Instantiator * vinst; + if( tn.isReal() ){ + vinst = new ArithInstantiator( d_qe, tn ); + }else if( tn.isSort() ){ + Assert( options::quantEpr() ); + vinst = new EprInstantiator( d_qe, tn ); + }else if( tn.isDatatype() ){ + vinst = new DtInstantiator( d_qe, tn ); + }else if( tn.isBitVector() ){ + vinst = new BvInstantiator( d_qe, tn ); + }else if( tn.isBoolean() ){ + vinst = new ModelValueInstantiator( d_qe, tn ); + }else{ + //default + vinst = new Instantiator( d_qe, tn ); + } + d_instantiator[v] = vinst; + } + d_curr_subs_proc[v].clear(); + d_curr_index[v] = index; + d_curr_iphase[v] = CEG_INST_PHASE_NONE; +} + +void CegInstantiator::registerTheoryIds(TypeNode tn, + std::map<TypeNode, bool>& visited) +{ + if (visited.find(tn) == visited.end()) + { + visited[tn] = true; + TheoryId tid = Theory::theoryOf(tn); + registerTheoryId(tid); + if (tn.isDatatype()) + { + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for (unsigned i = 0; i < dt.getNumConstructors(); i++) + { + for (unsigned j = 0; j < dt[i].getNumArgs(); j++) + { + registerTheoryIds( + TypeNode::fromType( + ((SelectorType)dt[i][j].getType()).getRangeType()), + visited); + } + } + } + } +} + +void CegInstantiator::registerTheoryId(TheoryId tid) +{ + if (std::find(d_tids.begin(), d_tids.end(), tid) == d_tids.end()) + { + // setup any theory-specific preprocessors here + if (tid == THEORY_BV) + { + d_tipp[tid] = new BvInstantiatorPreprocess; + } + d_tids.push_back(tid); + } +} + +void CegInstantiator::registerVariable(Node v, bool is_aux) +{ + Assert(std::find(d_vars.begin(), d_vars.end(), v) == d_vars.end()); + Assert(std::find(d_aux_vars.begin(), d_aux_vars.end(), v) + == d_aux_vars.end()); + if (!is_aux) + { + d_vars.push_back(v); + d_vars_set.insert(v); + } + else + { + d_aux_vars.push_back(v); + } + TypeNode vtn = v.getType(); + Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of " + << v << std::endl; + // collect relevant theories for this variable + std::map<TypeNode, bool> visited; + 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() ){ + //solved for all variables, now construct instantiation + bool needsPostprocess = + sf.d_vars.size() > d_input_vars.size() || !d_var_order_index.empty(); + std::vector< Instantiator * > pp_inst; + std::map< Instantiator *, Node > pp_inst_to_var; + std::vector< Node > lemmas; + for( std::map< Node, Instantiator * >::iterator ita = d_active_instantiators.begin(); ita != d_active_instantiators.end(); ++ita ){ + if (ita->second->needsPostProcessInstantiationForVariable( + this, sf, ita->first, d_effort)) + { + needsPostprocess = true; + pp_inst_to_var[ ita->second ] = ita->first; + } + } + if( needsPostprocess ){ + //must make copy so that backtracking reverts sf + SolvedForm sf_tmp = sf; + bool postProcessSuccess = true; + for( std::map< Instantiator *, Node >::iterator itp = pp_inst_to_var.begin(); itp != pp_inst_to_var.end(); ++itp ){ + if (!itp->first->postProcessInstantiationForVariable( + this, sf_tmp, itp->second, d_effort, lemmas)) + { + postProcessSuccess = false; + break; + } + } + if( postProcessSuccess ){ + return doAddInstantiation( sf_tmp.d_vars, sf_tmp.d_subs, lemmas ); + }else{ + return false; + } + }else{ + 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; + Node pv; + if( d_stack_vars.empty() ){ + pv = d_vars[i]; + }else{ + pv = d_stack_vars.back(); + is_cv = true; + d_stack_vars.pop_back(); + } + activateInstantiationVariable(pv, i); + + //get the instantiator object + Instantiator * vinst = NULL; + std::map< Node, Instantiator * >::iterator itin = d_instantiator.find( pv ); + if( itin!=d_instantiator.end() ){ + vinst = itin->second; + } + 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)) + { + 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; + } + } + } + + //[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) + && vinst->allowModelValue(this, sf, pv, d_effort)) + { +#ifdef CVC4_ASSERTIONS + if( pvtn.isReal() && options::cbqiNestedQE() && !options::cbqiAll() ){ + Trace("cbqi-warn") << "Had to resort to model value." << std::endl; + Assert( false ); + } +#endif + Node mv = getModelValue( pv ); + TermProperties pv_prop_m; + Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl; + d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE; + CegInstEffort prev = d_effort; + if (d_effort < CEG_INST_EFFORT_STANDARD_MV) + { + // update the effort level to indicate we have used a model value + d_effort = CEG_INST_EFFORT_STANDARD_MV; + } + if (constructInstantiationInc(pv, mv, pv_prop_m, sf)) + { + return true; + } + d_effort = prev; + } + Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl; + if( is_cv ){ + d_stack_vars.push_back( pv ); + } + d_active_instantiators.erase( pv ); + deactivateInstantiationVariable(pv); + return false; + } +} + +void CegInstantiator::pushStackVariable( Node v ) { + d_stack_vars.push_back( v ); +} + +void CegInstantiator::popStackVariable() { + Assert( !d_stack_vars.empty() ); + d_stack_vars.pop_back(); +} + +bool CegInstantiator::constructInstantiationInc(Node pv, + Node n, + TermProperties& pv_prop, + SolvedForm& sf, + bool revertOnSuccess) +{ + Node cnode = pv_prop.getCacheNode(); + if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){ + d_curr_subs_proc[pv][n][cnode] = true; + if( Trace.isOn("cbqi-inst-debug") ){ + for( unsigned j=0; j<sf.d_subs.size(); j++ ){ + Trace("cbqi-inst-debug") << " "; + } + Trace("cbqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv] + << ") "; + Node mod_pv = pv_prop.getModifiedTerm( pv ); + Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl; + Assert( n.getType().isSubtypeOf( pv.getType() ) ); + } + //must ensure variables have been computed for n + computeProgVars( n ); + Assert( d_inelig.find( n )==d_inelig.end() ); + + //substitute into previous substitutions, when applicable + std::vector< Node > a_var; + a_var.push_back( pv ); + std::vector< Node > a_subs; + a_subs.push_back( n ); + std::vector< TermProperties > a_prop; + a_prop.push_back( pv_prop ); + std::vector< Node > a_non_basic; + if( !pv_prop.isBasic() ){ + a_non_basic.push_back( pv ); + } + bool success = true; + std::map< int, Node > prev_subs; + std::map< int, TermProperties > prev_prop; + std::map< int, Node > prev_sym_subs; + std::vector< Node > new_non_basic; + Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl; + for( unsigned j=0; j<sf.d_subs.size(); j++ ){ + Trace("cbqi-inst-debug2") << " Apply for " << sf.d_subs[j] << std::endl; + Assert( d_prog_var.find( sf.d_subs[j] )!=d_prog_var.end() ); + if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){ + prev_subs[j] = sf.d_subs[j]; + TNode tv = pv; + TNode ts = n; + TermProperties a_pv_prop; + Node new_subs = applySubstitution( sf.d_vars[j].getType(), sf.d_subs[j], a_var, a_subs, a_prop, a_non_basic, a_pv_prop, true ); + if( !new_subs.isNull() ){ + sf.d_subs[j] = new_subs; + // the substitution apply to this term resulted in a non-basic substitution relationship + if( !a_pv_prop.isBasic() ){ + // we are processing: + // sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n } + + // based on the above substitution, we have: + // x = sf.d_subs[j] { pv_prop.getModifiedTerm( pv ) -> n } + // is equivalent to + // a_pv_prop.getModifiedTerm( x ) = new_subs + + // thus we must compose substitutions: + // a_pv_prop.getModifiedTerm( sf.d_props[j].getModifiedTerm( sf.d_vars[j] ) ) = new_subs + + prev_prop[j] = sf.d_props[j]; + bool prev_basic = sf.d_props[j].isBasic(); + + // now compose the property + sf.d_props[j].composeProperty( a_pv_prop ); + + // if previously was basic, becomes non-basic + if( prev_basic && !sf.d_props[j].isBasic() ){ + Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), sf.d_vars[j] )==sf.d_non_basic.end() ); + new_non_basic.push_back( sf.d_vars[j] ); + sf.d_non_basic.push_back( sf.d_vars[j] ); + } + } + if( sf.d_subs[j]!=prev_subs[j] ){ + computeProgVars( sf.d_subs[j] ); + Assert( d_inelig.find( sf.d_subs[j] )==d_inelig.end() ); + } + Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl; + }else{ + Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl; + success = false; + break; + } + }else{ + Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl; + } + } + if( success ){ + Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl; + sf.push_back( pv, n, pv_prop ); + Trace("cbqi-inst-debug2") << "Recurse..." << std::endl; + unsigned i = d_curr_index[pv]; + success = constructInstantiation(sf, d_stack_vars.empty() ? i + 1 : i); + if (!success || revertOnSuccess) + { + Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl; + sf.pop_back( pv, n, pv_prop ); + } + } + if (success && !revertOnSuccess) + { + return true; + }else{ + Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl; + //revert substitution information + for( std::map< int, Node >::iterator it = prev_subs.begin(); it != prev_subs.end(); it++ ){ + sf.d_subs[it->first] = it->second; + } + for( std::map< int, TermProperties >::iterator it = prev_prop.begin(); it != prev_prop.end(); it++ ){ + sf.d_props[it->first] = it->second; + } + for( unsigned i=0; i<new_non_basic.size(); i++ ){ + sf.d_non_basic.pop_back(); + } + return success; + } + }else{ + //already tried this substitution + return false; + } +} + +bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) { + if (vars.size() > d_input_vars.size() || !d_var_order_index.empty()) + { + Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl; + std::map< Node, Node > subs_map; + for( unsigned i=0; i<subs.size(); i++ ){ + subs_map[vars[i]] = subs[i]; + } + subs.clear(); + for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i) + { + std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]); + Assert( it!=subs_map.end() ); + Node n = it->second; + Trace("cbqi-inst-debug") << " " << d_input_vars[i] << " -> " << n + << std::endl; + Assert(n.getType().isSubtypeOf(d_input_vars[i].getType())); + subs.push_back( n ); + } + } + if (Trace.isOn("cbqi-inst")) + { + Trace("cbqi-inst") << "Ceg Instantiator produced : " << std::endl; + for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i) + { + Node v = d_input_vars[i]; + Trace("cbqi-inst") << i << " (" << d_curr_iphase[v] << ") : " + << v << " -> " << subs[i] << std::endl; + Assert(subs[i].getType().isSubtypeOf(v.getType())); + } + } + Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl; + bool ret = d_out->doAddInstantiation( subs ); + for( unsigned i=0; i<lemmas.size(); i++ ){ + d_out->addLemma( lemmas[i] ); + } + return ret; +} + +bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){ + Assert( d_prog_var.find( n )!=d_prog_var.end() ); + if( !non_basic.empty() ){ + for (std::unordered_set<Node, NodeHashFunction>::iterator it = + d_prog_var[n].begin(); + it != d_prog_var[n].end(); + ++it) + { + if (std::find(non_basic.begin(), non_basic.end(), *it) != non_basic.end()) + { + return false; + } + } + } + return true; +} + +Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, + std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff ) { + computeProgVars( n ); + Assert( n==Rewriter::rewrite( n ) ); + bool is_basic = canApplyBasicSubstitution( n, non_basic ); + if( Trace.isOn("cegqi-si-apply-subs-debug") ){ + Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl; + for( unsigned i=0; i<subs.size(); i++ ){ + Trace("cegqi-si-apply-subs-debug") << " " << vars[i] << " -> " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl; + Assert( subs[i].getType().isSubtypeOf( vars[i].getType() ) ); + } + } + Node nret; + if( is_basic ){ + nret = n.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + }else{ + if( !tn.isInteger() ){ + //can do basic substitution instead with divisions + std::vector< Node > nvars; + std::vector< Node > nsubs; + for( unsigned i=0; i<vars.size(); i++ ){ + if( !prop[i].d_coeff.isNull() ){ + Assert( vars[i].getType().isInteger() ); + Assert( prop[i].d_coeff.isConst() ); + Node nn = NodeManager::currentNM()->mkNode( MULT, subs[i], NodeManager::currentNM()->mkConst( Rational(1)/prop[i].d_coeff.getConst<Rational>() ) ); + nn = NodeManager::currentNM()->mkNode( kind::TO_INTEGER, nn ); + nn = Rewriter::rewrite( nn ); + nsubs.push_back( nn ); + }else{ + nsubs.push_back( subs[i] ); + } + } + nret = n.substitute( vars.begin(), vars.end(), nsubs.begin(), nsubs.end() ); + }else if( try_coeff ){ + //must convert to monomial representation + std::map< Node, Node > msum; + if (ArithMSum::getMonomialSum(n, msum)) + { + std::map< Node, Node > msum_coeff; + std::map< Node, Node > msum_term; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + //check if in substitution + std::vector< Node >::iterator its = std::find( vars.begin(), vars.end(), it->first ); + if( its!=vars.end() ){ + int index = its-vars.begin(); + if( prop[index].d_coeff.isNull() ){ + //apply substitution + msum_term[it->first] = subs[index]; + }else{ + //apply substitution, multiply to ensure no divisibility conflict + msum_term[it->first] = subs[index]; + //relative coefficient + msum_coeff[it->first] = prop[index].d_coeff; + if( pv_prop.d_coeff.isNull() ){ + pv_prop.d_coeff = prop[index].d_coeff; + }else{ + pv_prop.d_coeff = NodeManager::currentNM()->mkNode( MULT, pv_prop.d_coeff, prop[index].d_coeff ); + } + } + }else{ + msum_term[it->first] = it->first; + } + } + //make sum with normalized coefficient + if( !pv_prop.d_coeff.isNull() ){ + pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff ); + Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl; + std::vector< Node > children; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + Node c_coeff; + if( !msum_coeff[it->first].isNull() ){ + c_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkConst( pv_prop.d_coeff.getConst<Rational>() / msum_coeff[it->first].getConst<Rational>() ) ); + }else{ + c_coeff = pv_prop.d_coeff; + } + if( !it->second.isNull() ){ + c_coeff = NodeManager::currentNM()->mkNode( MULT, c_coeff, it->second ); + } + Assert( !c_coeff.isNull() ); + Node c; + if( msum_term[it->first].isNull() ){ + c = c_coeff; + }else{ + c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] ); + } + children.push_back( c ); + Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl; + } + Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children ); + nretc = Rewriter::rewrite( nretc ); + //ensure that nret does not contain vars + if( !TermUtil::containsTerms( nretc, vars ) ){ + //result is ( nret / pv_prop.d_coeff ) + nret = nretc; + }else{ + Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl; + } + }else{ + //implies that we have a monomial that has a free variable + Trace("cegqi-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl; + } + }else{ + Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl; + } + } + } + if( n!=nret && !nret.isNull() ){ + nret = Rewriter::rewrite( nret ); + } + return nret; +} + +Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, + std::vector< TermProperties >& prop, std::vector< Node >& non_basic ) { + computeProgVars( lit ); + bool is_basic = canApplyBasicSubstitution( lit, non_basic ); + Node lret; + if( is_basic ){ + lret = lit.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + }else{ + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + if( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ){ + Assert( atom.getKind()!=GEQ || atom[1].isConst() ); + Node atom_lhs; + Node atom_rhs; + if( atom.getKind()==GEQ ){ + atom_lhs = atom[0]; + atom_rhs = atom[1]; + }else{ + atom_lhs = NodeManager::currentNM()->mkNode( MINUS, atom[0], atom[1] ); + atom_lhs = Rewriter::rewrite( atom_lhs ); + atom_rhs = getQuantifiersEngine()->getTermUtil()->d_zero; + } + //must be an eligible term + if( isEligible( atom_lhs ) ){ + //apply substitution to LHS of atom + TermProperties atom_lhs_prop; + atom_lhs = applySubstitution( NodeManager::currentNM()->realType(), atom_lhs, vars, subs, prop, non_basic, atom_lhs_prop ); + if( !atom_lhs.isNull() ){ + if( !atom_lhs_prop.d_coeff.isNull() ){ + atom_rhs = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, atom_lhs_prop.d_coeff, atom_rhs ) ); + } + lret = NodeManager::currentNM()->mkNode( atom.getKind(), atom_lhs, atom_rhs ); + if( !pol ){ + lret = lret.negate(); + } + } + } + }else{ + // don't know how to apply substitution to literal + } + } + if( lit!=lret && !lret.isNull() ){ + lret = Rewriter::rewrite( lret ); + } + return lret; +} + +bool CegInstantiator::check() { + if( d_qe->getTheoryEngine()->needCheck() ){ + Trace("cbqi-engine") << " CEGQI instantiator : wait until all ground theories are finished." << std::endl; + return false; + } + processAssertions(); + for( unsigned r=0; r<2; r++ ){ + d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL; + SolvedForm sf; + d_stack_vars.clear(); + d_bound_var_index.clear(); + d_solved_asserts.clear(); + //try to add an instantiation + if (constructInstantiation(sf, 0)) + { + return true; + } + } + Trace("cbqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl; + return false; +} + +void collectPresolveEqTerms( Node n, std::map< Node, std::vector< Node > >& teq ) { + if( n.getKind()==FORALL || n.getKind()==EXISTS ){ + //do nothing + }else{ + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + std::map< Node, std::vector< Node > >::iterator it = teq.find( n[i] ); + if( it!=teq.end() ){ + Node nn = n[ i==0 ? 1 : 0 ]; + if( std::find( it->second.begin(), it->second.end(), nn )==it->second.end() ){ + it->second.push_back( nn ); + Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl; + } + } + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectPresolveEqTerms( n[i], teq ); + } + } +} + +void getPresolveEqConjuncts( std::vector< Node >& vars, std::vector< Node >& terms, + std::map< Node, std::vector< Node > >& teq, Node f, std::vector< Node >& conj ) { + if( conj.size()<1000 ){ + if( terms.size()==f[0].getNumChildren() ){ + Node c = f[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); + conj.push_back( c ); + }else{ + unsigned i = terms.size(); + Node v = f[0][i]; + terms.push_back( Node::null() ); + for( unsigned j=0; j<teq[v].size(); j++ ){ + terms[i] = teq[v][j]; + getPresolveEqConjuncts( vars, terms, teq, f, conj ); + } + terms.pop_back(); + } + } +} + +void CegInstantiator::presolve( Node q ) { + //at preregister time, add proxy of obvious instantiations up front, which helps learning during preprocessing + //only if no nested quantifiers + if( !QuantifiersRewriter::containsQuantifiers( q[1] ) ){ + std::vector< Node > ps_vars; + std::map< Node, std::vector< Node > > teq; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + ps_vars.push_back( q[0][i] ); + teq[q[0][i]].clear(); + } + collectPresolveEqTerms( q[1], teq ); + std::vector< Node > terms; + std::vector< Node > conj; + getPresolveEqConjuncts( ps_vars, terms, teq, q, conj ); + + if( !conj.empty() ){ + Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj ); + Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() ); + lem = NodeManager::currentNM()->mkNode( OR, g, lem ); + Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl; + d_qe->getOutputChannel().lemma( lem, false, true ); + } + } +} + +void CegInstantiator::processAssertions() { + Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size() << ", #aux-var = " << d_aux_vars.size() << std::endl; + d_curr_asserts.clear(); + d_curr_eqc.clear(); + d_curr_type_eqc.clear(); + + // must use master equality engine to avoid value instantiations + eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine(); + //to eliminate identified illegal terms + std::map< Node, Node > aux_subs; + + //for each variable + for( unsigned i=0; i<d_vars.size(); i++ ){ + Node pv = d_vars[i]; + TypeNode pvtn = pv.getType(); + Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl; + //collect information about eqc + if( ee->hasTerm( pv ) ){ + Node pvr = ee->getRepresentative( pv ); + if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){ + Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl; + eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee ); + while( !eqc_i.isFinished() ){ + d_curr_eqc[pvr].push_back( *eqc_i ); + ++eqc_i; + } + } + } + } + //collect assertions for relevant theories + for( unsigned i=0; i<d_tids.size(); i++ ){ + TheoryId tid = d_tids[i]; + Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid ); + if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){ + Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl; + d_curr_asserts[tid].clear(); + //collect all assertions from theory + for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { + Node lit = (*it).assertion; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ + d_curr_asserts[tid].push_back( lit ); + Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; + }else{ + Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; + } + if( lit.getKind()==EQUAL ){ + std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit ); + if( itae!=d_aux_eq.end() ){ + for( std::map< Node, Node >::iterator itae2 = itae->second.begin(); itae2 != itae->second.end(); ++itae2 ){ + aux_subs[ itae2->first ] = itae2->second; + Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl; + } + } + }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){ + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){ + Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT ); + aux_subs[ atom ] = val; + Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl; + } + } + } + } + } + //collect equivalence classes that correspond to relevant theories + Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl; + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); + while( !eqcs_i.isFinished() ){ + Node r = *eqcs_i; + TypeNode rtn = r.getType(); + TheoryId tid = Theory::theoryOf( rtn ); + //if we care about the theory of this eqc + if( std::find( d_tids.begin(), d_tids.end(), tid )!=d_tids.end() ){ + if( rtn.isInteger() || rtn.isReal() ){ + rtn = rtn.getBaseType(); + } + Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl; + d_curr_type_eqc[rtn].push_back( r ); + if( d_curr_eqc.find( r )==d_curr_eqc.end() ){ + Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl; + Trace("cbqi-proc-debug") << " "; + eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); + while( !eqc_i.isFinished() ){ + Trace("cbqi-proc-debug") << *eqc_i << " "; + d_curr_eqc[r].push_back( *eqc_i ); + ++eqc_i; + } + Trace("cbqi-proc-debug") << std::endl; + } + } + ++eqcs_i; + } + //construct substitution from auxiliary variable equalities (if e.g. ITE removal was applied to CE body of quantified formula) + std::vector< Node > subs_lhs; + std::vector< Node > subs_rhs; + for( unsigned i=0; i<d_aux_vars.size(); i++ ){ + Node r = d_aux_vars[i]; + std::map< Node, Node >::iterator it = aux_subs.find( r ); + if( it!=aux_subs.end() ){ + addToAuxVarSubstitution( subs_lhs, subs_rhs, r, it->second ); + }else{ + Trace("cbqi-proc") << "....no substitution found for auxiliary variable " << r << "!!! type is " << r.getType() << std::endl; + Assert( false ); + } + } + + //apply substitutions to everything, if necessary + if( !subs_lhs.empty() ){ + Trace("cbqi-proc") << "Applying substitution : " << std::endl; + for( unsigned i=0; i<subs_lhs.size(); i++ ){ + Trace("cbqi-proc") << " " << subs_lhs[i] << " -> " << subs_rhs[i] << std::endl; + } + for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ + for( unsigned i=0; i<it->second.size(); i++ ){ + Node lit = it->second[i]; + lit = lit.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + lit = Rewriter::rewrite( lit ); + it->second[i] = lit; + } + } + for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){ + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + n = Rewriter::rewrite( n ); + it->second[i] = n; + } + } + } + + //remove unecessary assertions + for( std::map< TheoryId, std::vector< Node > >::iterator it = d_curr_asserts.begin(); it != d_curr_asserts.end(); ++it ){ + std::vector< Node > akeep; + for( unsigned i=0; i<it->second.size(); i++ ){ + Node n = it->second[i]; + //must be an eligible term + if( isEligible( n ) ){ + //must contain at least one variable + if( !d_prog_var[n].empty() ){ + Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl; + akeep.push_back( n ); + }else{ + Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl; + } + }else{ + Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl; + } + } + it->second.clear(); + it->second.insert( it->second.end(), akeep.begin(), akeep.end() ); + } + + //remove duplicate terms from eqc + for( std::map< Node, std::vector< Node > >::iterator it = d_curr_eqc.begin(); it != d_curr_eqc.end(); ++it ){ + std::vector< Node > new_eqc; + for( unsigned i=0; i<it->second.size(); i++ ){ + if( std::find( new_eqc.begin(), new_eqc.end(), it->second[i] )==new_eqc.end() ){ + new_eqc.push_back( it->second[i] ); + } + } + it->second.clear(); + it->second.insert( it->second.end(), new_eqc.begin(), new_eqc.end() ); + } +} + +void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, std::vector< Node >& subs_rhs, Node l, Node r ) { + r = r.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); + + std::vector< Node > cl; + cl.push_back( l ); + std::vector< Node > cr; + cr.push_back( r ); + for( unsigned i=0; i<subs_lhs.size(); i++ ){ + Node nr = subs_rhs[i].substitute( cl.begin(), cl.end(), cr.begin(), cr.end() ); + nr = Rewriter::rewrite( nr ); + subs_rhs[i] = nr; + } + + subs_lhs.push_back( l ); + subs_rhs.push_back( r ); +} + +Node CegInstantiator::getModelValue( Node n ) { + return d_qe->getModel()->getValue( n ); +} + +Node CegInstantiator::getBoundVariable(TypeNode tn) +{ + unsigned index = 0; + std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction>::iterator itb = + d_bound_var_index.find(tn); + if (itb != d_bound_var_index.end()) + { + index = itb->second; + } + d_bound_var_index[tn] = index + 1; + while (index >= d_bound_var[tn].size()) + { + std::stringstream ss; + ss << "x" << index; + Node x = NodeManager::currentNM()->mkBoundVar(ss.str(), tn); + d_bound_var[tn].push_back(x); + } + return d_bound_var[tn][index]; +} + +bool CegInstantiator::isSolvedAssertion(Node n) const +{ + return d_solved_asserts.find(n) != d_solved_asserts.end(); +} + +void CegInstantiator::markSolved(Node n, bool solved) +{ + if (solved) + { + d_solved_asserts.insert(n); + } + else if (isSolvedAssertion(n)) + { + d_solved_asserts.erase(n); + } +} + +void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { + if( n.getKind()==FORALL ){ + d_is_nested_quant = true; + }else if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( TermUtil::isBoolConnectiveTerm( n ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectCeAtoms( n[i], visited ); + } + }else{ + if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){ + Trace("cbqi-ce-atoms") << "CE atoms : " << n << std::endl; + d_ce_atoms.push_back( n ); + } + } + } +} + +void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { + Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl; + d_input_vars.clear(); + d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end()); + + //Assert( d_vars.empty() ); + d_vars.clear(); + registerTheoryId(THEORY_UF); + for (unsigned i = 0; i < ce_vars.size(); i++) + { + Trace("cbqi-reg") << " register input variable : " << ce_vars[i] << std::endl; + registerVariable(ce_vars[i]); + } + + // preprocess with all relevant instantiator preprocessors + Trace("cbqi-debug") << "Preprocess based on theory-specific methods..." + << std::endl; + std::vector<Node> pvars; + pvars.insert(pvars.end(), d_vars.begin(), d_vars.end()); + for (std::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp) + { + p.second->registerCounterexampleLemma(lems, pvars); + } + // must register variables generated by preprocessors + Trace("cbqi-debug") << "Register variables from theory-specific methods " + << d_input_vars.size() << " " << pvars.size() << " ..." + << std::endl; + for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i) + { + Trace("cbqi-reg") << " register theory preprocess variable : " << pvars[i] + << std::endl; + registerVariable(pvars[i]); + } + + //remove ITEs + IteSkolemMap iteSkolemMap; + d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap); + //Assert( d_aux_vars.empty() ); + d_aux_vars.clear(); + d_aux_eq.clear(); + for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { + Trace("cbqi-reg") << " register aux variable : " << i->first << std::endl; + registerVariable(i->first, true); + } + for( unsigned i=0; i<lems.size(); i++ ){ + Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl; + Node rlem = lems[i]; + rlem = Rewriter::rewrite( rlem ); + Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl; + //record the literals that imply auxiliary variables to be equal to terms + if( lems[i].getKind()==ITE && rlem.getKind()==ITE ){ + if( lems[i][1].getKind()==EQUAL && lems[i][2].getKind()==EQUAL && lems[i][1][0]==lems[i][2][0] ){ + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][1][0] )!=d_aux_vars.end() ){ + Node v = lems[i][1][0]; + for( unsigned r=1; r<=2; r++ ){ + d_aux_eq[rlem[r]][v] = lems[i][r][1]; + Trace("cbqi-debug") << " " << rlem[r] << " implies " << v << " = " << lems[i][r][1] << std::endl; + } + } + } + } + /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){ + //Boolean terms + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){ + Node v = lems[i][0]; + d_aux_eq[rlem][v] = lems[i][1]; + Trace("cbqi-debug") << " " << rlem << " implies " << v << " = " << lems[i][1] << std::endl; + } + }*/ + lems[i] = rlem; + } + + // determine variable order: must do Reals before Ints + Trace("cbqi-debug") << "Determine variable order..." << std::endl; + if (!d_vars.empty()) + { + std::map<Node, unsigned> voo; + bool doSort = false; + std::vector<Node> vars; + std::map<TypeNode, std::vector<Node> > tvars; + for (unsigned i = 0, size = d_vars.size(); i < size; i++) + { + voo[d_vars[i]] = i; + d_var_order_index.push_back(0); + TypeNode tn = d_vars[i].getType(); + if (tn.isInteger()) + { + doSort = true; + tvars[tn].push_back(d_vars[i]); + } + else + { + vars.push_back(d_vars[i]); + } + } + if (doSort) + { + Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl; + for (std::pair<const TypeNode, std::vector<Node> >& vs : tvars) + { + vars.insert(vars.end(), vs.second.begin(), vs.second.end()); + } + + Trace("cbqi-debug") << "Consider variables in this order : " << std::endl; + for (unsigned i = 0; i < vars.size(); i++) + { + d_var_order_index[voo[vars[i]]] = i; + Trace("cbqi-debug") << " " << vars[i] << " : " << vars[i].getType() + << ", index was : " << voo[vars[i]] << std::endl; + d_vars[i] = vars[i]; + } + Trace("cbqi-debug") << std::endl; + } + else + { + d_var_order_index.clear(); + } + } + + //collect atoms from all lemmas: we will only do bounds coming from original body + d_is_nested_quant = false; + std::map< Node, bool > visited; + for( unsigned i=0; i<lems.size(); i++ ){ + collectCeAtoms( lems[i], visited ); + } +} + + +Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){ + d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn); +} + +bool Instantiator::processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + CegInstEffort effort) +{ + pv_prop.d_type = 0; + return ci->constructInstantiationInc(pv, n, pv_prop, sf); +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h new file mode 100644 index 000000000..03983fe1a --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -0,0 +1,783 @@ +/********************* */ +/*! \file ceg_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H +#define __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H + +#include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +namespace arith { + class TheoryArith; +} + +namespace quantifiers { + +class CegqiOutput { +public: + virtual ~CegqiOutput() {} + virtual bool doAddInstantiation( std::vector< Node >& subs ) = 0; + virtual bool isEligibleForInstantiation( Node n ) = 0; + virtual bool addLemma( Node lem ) = 0; +}; + +class Instantiator; +class InstantiatorPreprocess; + +/** Term Properties + * + * Stores properties for a variable to solve for in counterexample-guided + * instantiation. + * + * For LIA, this includes the coefficient of the variable, and the bound type + * for the variable. + */ +class TermProperties { +public: + TermProperties() : d_type(0) {} + virtual ~TermProperties() {} + + // type of property for a term + // for arithmetic this corresponds to bound type (0:equal, 1:upper bound, -1:lower bound) + int d_type; + // for arithmetic + Node d_coeff; + // get cache node + // we consider terms + TermProperties that are unique up to their cache node + // (see constructInstantiationInc) + virtual Node getCacheNode() const { return d_coeff; } + // is non-basic + virtual bool isBasic() const { return d_coeff.isNull(); } + // get modified term + virtual Node getModifiedTerm( Node pv ) const { + if( !d_coeff.isNull() ){ + return NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, pv ); + }else{ + return pv; + } + } + // compose property, should be such that: + // p.getModifiedTerm( this.getModifiedTerm( x ) ) = this_updated.getModifiedTerm( x ) + virtual void composeProperty( TermProperties& p ){ + if( !p.d_coeff.isNull() ){ + if( d_coeff.isNull() ){ + d_coeff = p.d_coeff; + }else{ + d_coeff = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_coeff, p.d_coeff ) ); + } + } + } +}; + +/** Solved form + * This specifies a substitution: + * { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| } + */ +class SolvedForm { +public: + // list of variables + std::vector< Node > d_vars; + // list of terms that they are substituted to + std::vector< Node > d_subs; + // properties for each variable + std::vector< TermProperties > d_props; + // the variables that have non-basic information regarding how they are substituted + // an example is for linear arithmetic, we store "substitution with coefficients". + std::vector<Node> d_non_basic; + // push the substitution pv_prop.getModifiedTerm(pv) -> n + void push_back( Node pv, Node n, TermProperties& pv_prop ){ + d_vars.push_back( pv ); + d_subs.push_back( n ); + d_props.push_back( pv_prop ); + if( !pv_prop.isBasic() ){ + d_non_basic.push_back( pv ); + // update theta value + Node new_theta = getTheta(); + if( new_theta.isNull() ){ + new_theta = pv_prop.d_coeff; + }else{ + new_theta = NodeManager::currentNM()->mkNode( kind::MULT, new_theta, pv_prop.d_coeff ); + new_theta = Rewriter::rewrite( new_theta ); + } + d_theta.push_back( new_theta ); + } + } + // pop the substitution pv_prop.getModifiedTerm(pv) -> n + void pop_back( Node pv, Node n, TermProperties& pv_prop ){ + d_vars.pop_back(); + d_subs.pop_back(); + d_props.pop_back(); + if( !pv_prop.isBasic() ){ + d_non_basic.pop_back(); + // update theta value + d_theta.pop_back(); + } + } + // is this solved form empty? + bool empty() { return d_vars.empty(); } +public: + // theta values (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017) + std::vector< Node > d_theta; + // get the current value for theta (for LIA, see Section 4 of Reynolds/King/Kuncak FMSD 2017) + Node getTheta() { + if( d_theta.empty() ){ + return Node::null(); + }else{ + return d_theta[d_theta.size()-1]; + } + } +}; + +/** instantiation effort levels + * + * This effort is used to stratify the construction of + * instantiations for some theories that may result to + * using model value instantiations. + */ +enum CegInstEffort +{ + // uninitialized + CEG_INST_EFFORT_NONE, + // standard effort level + CEG_INST_EFFORT_STANDARD, + // standard effort level, but we have used model values + CEG_INST_EFFORT_STANDARD_MV, + // full effort level + CEG_INST_EFFORT_FULL +}; + +std::ostream& operator<<(std::ostream& os, CegInstEffort e); + +/** instantiation phase for variables + * + * This indicates the phase in which we constructed + * a substitution for individual variables. + */ +enum CegInstPhase +{ + // uninitialized + CEG_INST_PHASE_NONE, + // instantiation constructed during traversal of equivalence classes + CEG_INST_PHASE_EQC, + // instantiation constructed during solving equalities + CEG_INST_PHASE_EQUAL, + // instantiation constructed by looking at theory assertions + CEG_INST_PHASE_ASSERTION, + // instantiation constructed by querying model value + CEG_INST_PHASE_MVALUE, +}; + +std::ostream& operator<<(std::ostream& os, CegInstPhase phase); + +/** Ceg instantiator + * + * This class manages counterexample-guided quantifier instantiation + * for a single quantified formula. + * + * For details on counterexample-guided quantifier instantiation + * (for linear arithmetic), see Reynolds/King/Kuncak FMSD 2017. + */ +class CegInstantiator { + public: + CegInstantiator(QuantifiersEngine* qe, + CegqiOutput* out, + bool use_vts_delta = true, + bool use_vts_inf = true); + virtual ~CegInstantiator(); + /** check + * This adds instantiations based on the state of d_vars in current context + * on the output channel d_out of this class. + */ + bool check(); + /** presolve for quantified formula + * + * This initializes formulas that help static learning of the quantifier-free + * solver. It is only called if the option --cbqi-prereg-inst is used. + */ + void presolve(Node q); + /** Register the counterexample lemma + * + * lems : contains the conjuncts of the counterexample lemma of the + * quantified formula we are processing. The counterexample + * lemma is the formula { ~phi[e/x] } in Figure 1 of Reynolds + * et al. FMSD 2017. + * ce_vars : contains the variables e. Notice these are variables of + * INST_CONSTANT kind, since we do not permit bound + * variables in assertions. + * + * This method may modify the set of lemmas lems based on: + * - ITE removal, + * - Theory-specific preprocessing of instantiation lemmas. + * It may also introduce new variables to ce_vars if necessary. + */ + void registerCounterexampleLemma(std::vector<Node>& lems, + std::vector<Node>& ce_vars); + /** get the output channel of this class */ + CegqiOutput* getOutput() { return d_out; } + //------------------------------interface for instantiators + /** get quantifiers engine */ + QuantifiersEngine* getQuantifiersEngine() { return d_qe; } + /** push stack variable + * This adds a new variable to solve for in the stack + * of variables we are processing. This stack is only + * used for datatypes, where e.g. the DtInstantiator + * solving for a list x may push the stack "variables" + * head(x) and tail(x). + */ + void pushStackVariable(Node v); + /** pop stack variable */ + void popStackVariable(); + /** construct instantiation increment + * + * Adds the substitution { pv_prop.getModifiedTerm(pv) -> n } to the current + * instantiation, specified by sf. + * + * This function returns true if a call to + * QuantifiersEngine::addInstantiation(...) + * was successfully made in a recursive call. + * + * The solved form sf is reverted to its original state if + * this function returns false, or + * revertOnSuccess is true and this function returns true. + */ + bool constructInstantiationInc(Node pv, + Node n, + TermProperties& pv_prop, + SolvedForm& sf, + bool revertOnSuccess = false); + /** get the current model value of term n */ + Node getModelValue(Node n); + /** get bound variable for type + * + * This gets the next (canonical) bound variable of + * type tn. This can be used for instance when + * constructing instantiations that involve choice expressions. + */ + Node getBoundVariable(TypeNode tn); + /** has this assertion been marked as solved? */ + bool isSolvedAssertion(Node n) const; + /** marked solved */ + void markSolved(Node n, bool solved = true); + //------------------------------end interface for instantiators + + /** + * Get the number of atoms in the counterexample lemma of the quantified + * formula we are processing with this class. + */ + unsigned getNumCEAtoms() { return d_ce_atoms.size(); } + /** + * Get the i^th atom of the counterexample lemma of the quantified + * formula we are processing with this class. + */ + Node getCEAtom(unsigned i) { return d_ce_atoms[i]; } + /** is n a term that is eligible for instantiation? */ + bool isEligible(Node n); + /** does n have variable pv? */ + bool hasVariable(Node n, Node pv); + /** are we using delta for LRA virtual term substitution? */ + bool useVtsDelta() { return d_use_vts_delta; } + /** are we using infinity for LRA virtual term substitution? */ + bool useVtsInfinity() { return d_use_vts_inf; } + /** are we processing a nested quantified formula? */ + bool hasNestedQuantification() { return d_is_nested_quant; } + private: + /** quantified formula associated with this instantiator */ + QuantifiersEngine* d_qe; + /** output channel of this instantiator */ + CegqiOutput* d_out; + /** whether we are using delta for virtual term substitution + * (for quantified LRA). + */ + bool d_use_vts_delta; + /** whether we are using infinity for virtual term substitution + * (for quantified LRA). + */ + bool d_use_vts_inf; + + //-------------------------------globally cached + /** cache from nodes to the set of variables it contains + * (from the quantified formula we are instantiating). + */ + std::unordered_map<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction> + d_prog_var; + /** cache of the set of terms that we have established are + * ineligible for instantiation. + */ + std::unordered_set<Node, NodeHashFunction> d_inelig; + /** ensures n is in d_prog_var and d_inelig. */ + void computeProgVars(Node n); + //-------------------------------end globally cached + + //-------------------------------cached per round + /** current assertions per theory */ + std::map<TheoryId, std::vector<Node> > d_curr_asserts; + /** map from representatives to the terms in their equivalence class */ + std::map<Node, std::vector<Node> > d_curr_eqc; + /** map from types to representatives of that type */ + std::map<TypeNode, std::vector<Node> > d_curr_type_eqc; + /** solved asserts */ + std::unordered_set<Node, NodeHashFunction> d_solved_asserts; + /** process assertions + * This is called once at the beginning of check to + * set up all necessary information for constructing instantiations, + * such as the above data structures. + */ + void processAssertions(); + /** add to auxiliary variable substitution + * This adds the substitution l -> r to the auxiliary + * variable substitution subs_lhs -> subs_rhs, and serializes + * it (applies it to existing substitutions). + */ + void addToAuxVarSubstitution(std::vector<Node>& subs_lhs, + std::vector<Node>& subs_rhs, + Node l, + Node r); + /** cache bound variables for type returned + * by getBoundVariable(...). + */ + std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> + d_bound_var; + /** current index of bound variables for type. + * The next call to getBoundVariable(...) for + * type tn returns the d_bound_var_index[tn]^th + * element of d_bound_var[tn], or a fresh variable + * if not in bounds. + */ + std::unordered_map<TypeNode, unsigned, TypeNodeHashFunction> + d_bound_var_index; + //-------------------------------end cached per round + + //-------------------------------data per theory + /** relevant theory ids + * A list of theory ids that contain at least one + * constraint in the body of the quantified formula we + * are processing. + */ + std::vector<TheoryId> d_tids; + /** map from theory ids to instantiator preprocessors */ + std::map<TheoryId, InstantiatorPreprocess*> d_tipp; + /** registers all theory ids associated with type tn + * + * This recursively calls registerTheoryId for typeOf(tn') for + * all parameters and datatype subfields of type tn. + * visited stores the types we have already visited. + */ + void registerTheoryIds(TypeNode tn, std::map<TypeNode, bool>& visited); + /** register theory id tid + * + * This is called when the quantified formula we are processing + * with this class involves theory tid. In this case, we will + * construct instantiations based on the assertion list of this theory. + */ + void registerTheoryId(TheoryId tid); + //-------------------------------end data per theory + + //-------------------------------the variables + /** the variables we are instantiating + * + * This is a superset of the variables for the instantiations we are + * generating and sending on the output channel of this class. + */ + std::vector<Node> d_vars; + /** set form of d_vars */ + std::unordered_set<Node, NodeHashFunction> d_vars_set; + /** index of variables reported in instantiation */ + std::vector<unsigned> d_var_order_index; + /** number of input variables + * + * These are the variables, in order, for the instantiations we are generating + * and sending on the output channel of this class. + */ + std::vector<Node> d_input_vars; + /** literals to equalities for aux vars + * This stores entries of the form + * L -> ( k -> t ) + * where + * k is a variable in d_aux_vars, + * L is a literal that if asserted implies that our + * instantiation should map { k -> t }. + * For example, if a term of the form + * ite( C, t1, t2 ) + * was replaced by k, we get this (top-level) assertion: + * ite( C, k=t1, k=t2 ) + * The vector d_aux_eq contains the exact form of + * the literals in the above constraint that they would + * appear in assertions, meaning d_aux_eq may contain: + * t1=k -> ( k -> t1 ) + * t2=k -> ( k -> t2 ) + * where t1=k and t2=k are the rewritten form of + * k=t1 and k=t2 respectively. + */ + std::map<Node, std::map<Node, Node> > d_aux_eq; + /** auxiliary variables + * These variables include the result of removing ITE + * terms from the quantified formula we are processing. + * These variables must be eliminated from constraints + * as a preprocess step to check(). + */ + std::vector<Node> d_aux_vars; + /** register variable */ + void registerVariable(Node v, bool is_aux = false); + //-------------------------------the variables + + //-------------------------------quantified formula info + /** are we processing a nested quantified formula? */ + bool d_is_nested_quant; + /** the atoms of the CE lemma */ + std::vector<Node> d_ce_atoms; + /** collect atoms */ + void collectCeAtoms(Node n, std::map<Node, bool>& visited); + //-------------------------------end quantified formula info + + //-------------------------------current state + /** the current effort level of the instantiator + * This indicates the effort Instantiator objects + * will put into the terms they return. + */ + CegInstEffort d_effort; + /** for each variable, the instantiator used for that variable */ + std::map<Node, Instantiator*> d_active_instantiators; + /** map from variables to the index in the prefix of the quantified + * formula we are processing. + */ + std::map<Node, unsigned> d_curr_index; + /** map from variables to the phase in which we instantiated them */ + std::map<Node, CegInstPhase> d_curr_iphase; + /** cache of current substitutions tried between activate/deactivate */ + std::map<Node, std::map<Node, std::map<Node, bool> > > d_curr_subs_proc; + /** stack of temporary variables we are solving for, + * e.g. subfields of datatypes. + */ + std::vector<Node> d_stack_vars; + /** activate instantiation variable v at index + * + * This is called when variable (inst constant) v is activated + * for the quantified formula we are processing. + * This method initializes the instantiator class for + * that variable if necessary, where this class is + * determined by the type of v. It also initializes + * the cache of values we have tried substituting for v + * (in d_curr_subs_proc), and stores its index. + */ + void activateInstantiationVariable(Node v, unsigned index); + /** deactivate instantiation variable + * + * This is called when variable (inst constant) v is deactivated + * for the quantified formula we are processing. + */ + void deactivateInstantiationVariable(Node v); + //-------------------------------end current state + + //---------------------------------for applying substitutions + /** can use basic substitution */ + bool canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ); + /** apply substitution + * We wish to process the substitution: + * ( pv = n * sf ) + * where pv is a variable with type tn, and * denotes application of substitution. + * The return value "ret" and pv_prop is such that the above equality is equivalent to + * ( pv_prop.getModifiedTerm(pv) = ret ) + */ + Node applySubstitution( TypeNode tn, Node n, SolvedForm& sf, TermProperties& pv_prop, bool try_coeff = true ) { + return applySubstitution( tn, n, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic, pv_prop, try_coeff ); + } + /** apply substitution, with solved form expanded to subs/prop/non_basic/vars */ + Node applySubstitution( TypeNode tn, Node n, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, + std::vector< Node >& non_basic, TermProperties& pv_prop, bool try_coeff = true ); + /** apply substitution to literal lit + * The return value is equivalent to ( lit * sf ) + * where * denotes application of substitution. + */ + Node applySubstitutionToLiteral( Node lit, SolvedForm& sf ) { + return applySubstitutionToLiteral( lit, sf.d_vars, sf.d_subs, sf.d_props, sf.d_non_basic ); + } + /** apply substitution to literal lit, with solved form expanded to subs/prop/non_basic/vars */ + Node applySubstitutionToLiteral( Node lit, std::vector< Node >& vars, std::vector< Node >& subs, std::vector< TermProperties >& prop, + std::vector< Node >& non_basic ); + //---------------------------------end for applying substitutions + + /** map from variables to their instantiators */ + 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. + * It returns true if a successful call to the output channel's + * doAddInstantiation was made. + */ + bool constructInstantiation(SolvedForm& sf, unsigned i); + /** do add instantiation + * This method is called by the above function after we finalize the + * variables/substitution and auxiliary lemmas. + * It returns true if a successful call to the output channel's + * doAddInstantiation was made. + */ + bool doAddInstantiation(std::vector<Node>& vars, + std::vector<Node>& subs, + std::vector<Node>& lemmas); +}; + +/** Instantiator class + * + * This is a virtual class that is used for methods for constructing + * substitutions for individual variables in counterexample-guided + * instantiation techniques. + * + * This class contains a set of interface functions below, which are called + * based on a fixed instantiation method implemented by CegInstantiator. + * In these calls, the Instantiator in turn makes calls to methods in + * CegInstanatior (primarily constructInstantiationInc). + */ +class Instantiator { +public: + Instantiator( QuantifiersEngine * qe, TypeNode tn ); + virtual ~Instantiator(){} + /** reset + * This is called once, prior to any of the below methods are called. + * This function sets up any initial information necessary for constructing + * instantiations for pv based on the current context. + */ + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + } + + /** process equal term + * + * This method is called when the entailment: + * E |= pv_prop.getModifiedTerm(pv) = n + * holds in the current context E, and n is eligible for instantiation. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + CegInstEffort effort); + /** process equal terms + * + * This method is called after process equal term, where eqc is the list of + * eligible terms in the equivalence class of pv. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + CegInstEffort effort) + { + return false; + } + + /** whether the instantiator implements processEquality */ + virtual bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + return false; + } + /** process equality + * The input is such that term_props.size() = terms.size() = 2 + * This method is called when the entailment: + * E ^ term_props[0].getModifiedTerm(x0) = + * terms[0] ^ term_props[1].getModifiedTerm(x1) = terms[1] |= x0 = x1 + * holds in current context E for fresh variables xi, terms[i] are eligible, + * and at least one terms[i] contains pv for i = 0,1. + * Notice in the basic case, E |= terms[0] = terms[1]. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + CegInstEffort effort) + { + return false; + } + + /** whether the instantiator implements processAssertion for any literal */ + virtual bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + return false; + } + /** has process assertion + * + * This method is called when the entailment: + * E |= lit + * holds in current context E. Typically, lit belongs to the list of current + * assertions. + * + * This method is used to determine whether the instantiator implements + * processAssertion for literal lit. + * If this method returns null, then this intantiator does not handle the + * literal lit. Otherwise, this method returns a literal lit' such that: + * (1) lit' is true in the current model, + * (2) lit' implies lit. + * where typically lit' = lit. + */ + virtual Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) + { + return Node::null(); + } + /** process assertion + * This method processes the assertion slit for variable pv. + * lit : the substituted form (under sf) of a literal returned by + * hasProcessAssertion + * alit : the asserted literal, given as input to hasProcessAssertion + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) + { + return false; + } + /** process assertions + * + * Called after processAssertion is called for each literal asserted to the + * instantiator. + * + * Returns true if an instantiation was successfully added via a call to + * CegInstantiator::constructInstantiationInc. + */ + virtual bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + return false; + } + + /** do we use the model value as instantiation for pv? + * This method returns true if we use model value instantiations + * at the same effort level as those determined by this instantiator. + */ + virtual bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + return effort > CEG_INST_EFFORT_STANDARD; + } + /** do we allow the model value as instantiation for pv? */ + virtual bool allowModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + return d_closed_enum_type; + } + + /** do we need to postprocess the solved form for pv? */ + virtual bool needsPostProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + return false; + } + /** postprocess the solved form for pv + * + * This method returns true if we successfully postprocessed the solved form. + * lemmas is a set of lemmas we wish to return along with the instantiation. + */ + virtual bool postProcessInstantiationForVariable(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort, + std::vector<Node>& lemmas) + { + return true; + } + + /** Identify this module (for debugging) */ + virtual std::string identify() const { return "Default"; } + protected: + /** the type of the variable we are instantiating */ + TypeNode d_type; + /** whether d_type is a closed enumerable type */ + bool d_closed_enum_type; +}; + +class ModelValueInstantiator : public Instantiator { +public: + ModelValueInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~ModelValueInstantiator(){} + bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) + { + return true; + } + std::string identify() const { return "ModelValue"; } +}; + +/** instantiator preprocess + * + * This class implements techniques for preprocessing the counterexample lemma + * generated for counterexample-guided quantifier instantiation. + */ +class InstantiatorPreprocess +{ + public: + InstantiatorPreprocess() {} + virtual ~InstantiatorPreprocess() {} + /** register counterexample lemma + * This implements theory-specific preprocessing and registration + * of counterexample lemmas, with the same contract as + * CegInstantiation::registerCounterexampleLemma. + */ + virtual void registerCounterexampleLemma(std::vector<Node>& lems, + std::vector<Node>& ce_vars) + { + } +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp new file mode 100644 index 000000000..e6e64201e --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.cpp @@ -0,0 +1,1990 @@ +/********************* */ +/*! \file ceg_t_instantiator.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of theory-specific counterexample-guided quantifier instantiation + **/ + +#include "theory/quantifiers/cegqi/ceg_t_instantiator.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/ematching/trigger.h" + +#include "theory/arith/arith_msum.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/theory_arith_private.h" +#include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" +#include "util/random.h" + +#include <algorithm> +#include <stack> + +using namespace std; +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +struct BvLinearAttributeId {}; +using BvLinearAttribute = expr::Attribute<BvLinearAttributeId, bool>; + +Node ArithInstantiator::getModelBasedProjectionValue( CegInstantiator * ci, Node e, Node t, bool isLower, Node c, Node me, Node mt, Node theta, Node inf_coeff, Node delta_coeff ) { + Node val = t; + Trace("cegqi-arith-bound2") << "Value : " << val << std::endl; + Assert( !e.getType().isInteger() || t.getType().isInteger() ); + Assert( !e.getType().isInteger() || mt.getType().isInteger() ); + //add rho value + //get the value of c*e + Node ceValue = me; + Node new_theta = theta; + if( !c.isNull() ){ + Assert( c.getType().isInteger() ); + ceValue = NodeManager::currentNM()->mkNode( MULT, ceValue, c ); + ceValue = Rewriter::rewrite( ceValue ); + if( new_theta.isNull() ){ + new_theta = c; + }else{ + new_theta = NodeManager::currentNM()->mkNode( MULT, new_theta, c ); + new_theta = Rewriter::rewrite( new_theta ); + } + Trace("cegqi-arith-bound2") << "...c*e = " << ceValue << std::endl; + Trace("cegqi-arith-bound2") << "...theta = " << new_theta << std::endl; + } + if( !new_theta.isNull() && e.getType().isInteger() ){ + Node rho; + //if( !mt.getType().isInteger() ){ + //round up/down + //mt = NodeManager::currentNM()->mkNode( + //} + if( isLower ){ + rho = NodeManager::currentNM()->mkNode( MINUS, ceValue, mt ); + }else{ + rho = NodeManager::currentNM()->mkNode( MINUS, mt, ceValue ); + } + rho = Rewriter::rewrite( rho ); + Trace("cegqi-arith-bound2") << "...rho = " << me << " - " << mt << " = " << rho << std::endl; + Trace("cegqi-arith-bound2") << "..." << rho << " mod " << new_theta << " = "; + rho = NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, rho, new_theta ); + rho = Rewriter::rewrite( rho ); + Trace("cegqi-arith-bound2") << rho << std::endl; + Kind rk = isLower ? PLUS : MINUS; + val = NodeManager::currentNM()->mkNode( rk, val, rho ); + val = Rewriter::rewrite( val ); + Trace("cegqi-arith-bound2") << "(after rho) : " << val << std::endl; + } + if( !inf_coeff.isNull() ){ + Assert( !d_vts_sym[0].isNull() ); + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, inf_coeff, d_vts_sym[0] ) ); + val = Rewriter::rewrite( val ); + } + if( !delta_coeff.isNull() ){ + //create delta here if necessary + val = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkNode( MULT, delta_coeff, ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta() ) ); + val = Rewriter::rewrite( val ); + } + return val; +} + +//this isolates the atom into solved form +// veq_c * pv <> val + vts_coeff_delta * delta + vts_coeff_inf * inf +// ensures val is Int if pv is Int, and val does not contain vts symbols +int ArithInstantiator::solve_arith( CegInstantiator * ci, Node pv, Node atom, Node& veq_c, Node& val, Node& vts_coeff_inf, Node& vts_coeff_delta ) { + int ires = 0; + Trace("cegqi-arith-debug") << "isolate for " << pv << " in " << atom << std::endl; + std::map< Node, Node > msum; + if (ArithMSum::getMonomialSumLit(atom, msum)) + { + Trace("cegqi-arith-debug") << "got monomial sum: " << std::endl; + if( Trace.isOn("cegqi-arith-debug") ){ + ArithMSum::debugPrintMonomialSum(msum, "cegqi-arith-debug"); + } + TypeNode pvtn = pv.getType(); + //remove vts symbols from polynomial + Node vts_coeff[2]; + for( unsigned t=0; t<2; t++ ){ + if( !d_vts_sym[t].isNull() ){ + std::map< Node, Node >::iterator itminf = msum.find( d_vts_sym[t] ); + if( itminf!=msum.end() ){ + vts_coeff[t] = itminf->second; + if( vts_coeff[t].isNull() ){ + vts_coeff[t] = NodeManager::currentNM()->mkConst( Rational( 1 ) ); + } + //negate if coefficient on variable is positive + std::map< Node, Node >::iterator itv = msum.find( pv ); + if( itv!=msum.end() ){ + //multiply by the coefficient we will isolate for + if( itv->second.isNull() ){ + vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); + }else{ + if( !pvtn.isInteger() ){ + vts_coeff[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) / itv->second.getConst<Rational>() ), vts_coeff[t] ); + vts_coeff[t] = Rewriter::rewrite( vts_coeff[t] ); + }else if( itv->second.getConst<Rational>().sgn()==1 ){ + vts_coeff[t] = ArithMSum::negate(vts_coeff[t]); + } + } + } + Trace("cegqi-arith-debug") << "vts[" << t << "] coefficient is " << vts_coeff[t] << std::endl; + msum.erase( d_vts_sym[t] ); + } + } + } + + ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); + if( ires!=0 ){ + Node realPart; + if( Trace.isOn("cegqi-arith-debug") ){ + Trace("cegqi-arith-debug") << "Isolate : "; + if( !veq_c.isNull() ){ + Trace("cegqi-arith-debug") << veq_c << " * "; + } + Trace("cegqi-arith-debug") << pv << " " << atom.getKind() << " " << val << std::endl; + } + if( options::cbqiAll() ){ + // when not pure LIA/LRA, we must check whether the lhs contains pv + if( TermUtil::containsTerm( val, pv ) ){ + Trace("cegqi-arith-debug") << "fail : contains bad term" << std::endl; + return 0; + } + } + if( pvtn.isInteger() && ( ( !veq_c.isNull() && !veq_c.getType().isInteger() ) || !val.getType().isInteger() ) ){ + //redo, split integer/non-integer parts + bool useCoeff = false; + Integer coeff = ci->getQuantifiersEngine()->getTermUtil()->d_one.getConst<Rational>().getNumerator(); + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( it->first.isNull() || it->first.getType().isInteger() ){ + if( !it->second.isNull() ){ + coeff = coeff.lcm( it->second.getConst<Rational>().getDenominator() ); + useCoeff = true; + } + } + } + //multiply everything by this coefficient + Node rcoeff = NodeManager::currentNM()->mkConst( Rational( coeff ) ); + std::vector< Node > real_part; + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if( useCoeff ){ + if( it->second.isNull() ){ + msum[it->first] = rcoeff; + }else{ + msum[it->first] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, it->second, rcoeff ) ); + } + } + if( !it->first.isNull() && !it->first.getType().isInteger() ){ + real_part.push_back( msum[it->first].isNull() ? it->first : NodeManager::currentNM()->mkNode( MULT, msum[it->first], it->first ) ); + } + } + //remove delta TODO: check this + vts_coeff[1] = Node::null(); + //multiply inf + if( !vts_coeff[0].isNull() ){ + vts_coeff[0] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MULT, rcoeff, vts_coeff[0] ) ); + } + realPart = real_part.empty() ? ci->getQuantifiersEngine()->getTermUtil()->d_zero : ( real_part.size()==1 ? real_part[0] : NodeManager::currentNM()->mkNode( PLUS, real_part ) ); + Assert( ci->getOutput()->isEligibleForInstantiation( realPart ) ); + //re-isolate + Trace("cegqi-arith-debug") << "Re-isolate..." << std::endl; + ires = ArithMSum::isolate(pv, msum, veq_c, val, atom.getKind()); + Trace("cegqi-arith-debug") << "Isolate for mixed Int/Real : " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << std::endl; + Trace("cegqi-arith-debug") << " real part : " << realPart << std::endl; + if( ires!=0 ){ + int ires_use = ( msum[pv].isNull() || msum[pv].getConst<Rational>().sgn()==1 ) ? 1 : -1; + val = Rewriter::rewrite( NodeManager::currentNM()->mkNode( ires_use==-1 ? PLUS : MINUS, + NodeManager::currentNM()->mkNode( ires_use==-1 ? MINUS : PLUS, val, realPart ), + NodeManager::currentNM()->mkNode( TO_INTEGER, realPart ) ) ); //TODO: round up for upper bounds? + Trace("cegqi-arith-debug") << "result : " << val << std::endl; + Assert( val.getType().isInteger() ); + } + } + } + vts_coeff_inf = vts_coeff[0]; + vts_coeff_delta = vts_coeff[1]; + Trace("cegqi-arith-debug") << "Return " << veq_c << " * " << pv << " " << atom.getKind() << " " << val << ", vts = (" << vts_coeff_inf << ", " << vts_coeff_delta << ")" << std::endl; + }else{ + Trace("cegqi-arith-debug") << "fail : could not get monomial sum" << std::endl; + } + return ires; +} + +void ArithInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type, false, false ); + d_vts_sym[1] = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta( false, false ); + for( unsigned i=0; i<2; i++ ){ + d_mbp_bounds[i].clear(); + d_mbp_coeff[i].clear(); + for( unsigned j=0; j<2; j++ ){ + d_mbp_vts_coeff[i][j].clear(); + } + d_mbp_lit[i].clear(); + } +} + +bool ArithInstantiator::processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + CegInstEffort effort) +{ + Node eq_lhs = terms[0]; + Node eq_rhs = terms[1]; + Node lhs_coeff = term_props[0].d_coeff; + Node rhs_coeff = term_props[1].d_coeff; + //make the same coefficient + if( rhs_coeff!=lhs_coeff ){ + if( !rhs_coeff.isNull() ){ + Trace("cegqi-arith-debug") << "...mult lhs by " << rhs_coeff << std::endl; + eq_lhs = NodeManager::currentNM()->mkNode( MULT, rhs_coeff, eq_lhs ); + eq_lhs = Rewriter::rewrite( eq_lhs ); + } + if( !lhs_coeff.isNull() ){ + Trace("cegqi-arith-debug") << "...mult rhs by " << lhs_coeff << std::endl; + eq_rhs = NodeManager::currentNM()->mkNode( MULT, lhs_coeff, eq_rhs ); + eq_rhs = Rewriter::rewrite( eq_rhs ); + } + } + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Node val; + TermProperties pv_prop; + Node vts_coeff_inf; + Node vts_coeff_delta; + //isolate pv in the equality + int ires = solve_arith( ci, pv, eq, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + pv_prop.d_type = 0; + if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) + { + return true; + } + } + + return false; +} + +Node ArithInstantiator::hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) +{ + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + if (atom.getKind() == GEQ || + (atom.getKind() == EQUAL && !pol && atom[0].getType().isReal())) { + return lit; + } else { + return Node::null(); + } +} + +bool ArithInstantiator::processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) +{ + Node atom = lit.getKind()==NOT ? lit[0] : lit; + bool pol = lit.getKind()!=NOT; + //arithmetic inequalities and disequalities + Assert( atom.getKind()==GEQ || ( atom.getKind()==EQUAL && !pol && atom[0].getType().isReal() ) ); + // get model value for pv + Node pv_value = ci->getModelValue( pv ); + //cannot contain infinity? + Node vts_coeff_inf; + Node vts_coeff_delta; + Node val; + TermProperties pv_prop; + //isolate pv in the inequality + int ires = solve_arith( ci, pv, atom, pv_prop.d_coeff, val, vts_coeff_inf, vts_coeff_delta ); + if( ires!=0 ){ + //disequalities are either strict upper or lower bounds + unsigned rmax = ( atom.getKind()==GEQ || options::cbqiModel() ) ? 1 : 2; + for( unsigned r=0; r<rmax; r++ ){ + int uires = ires; + Node uval = val; + if( atom.getKind()==GEQ ){ + //push negation downwards + if( !pol ){ + uires = -ires; + if( d_type.isInteger() ){ + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + //now is strict inequality + uires = uires*2; + } + } + }else{ + bool is_upper; + if( options::cbqiModel() ){ + // disequality is a disjunction : only consider the bound in the direction of the model + //first check if there is an infinity... + if( !vts_coeff_inf.isNull() ){ + //coefficient or val won't make a difference, just compare with zero + Trace("cegqi-arith-debug") << "Disequality : check infinity polarity " << vts_coeff_inf << std::endl; + Assert( vts_coeff_inf.isConst() ); + is_upper = ( vts_coeff_inf.getConst<Rational>().sgn()==1 ); + }else{ + Node rhs_value = ci->getModelValue( val ); + Node lhs_value = pv_prop.getModifiedTerm( pv_value ); + if( !pv_prop.isBasic() ){ + lhs_value = pv_prop.getModifiedTerm( pv_value ); + lhs_value = Rewriter::rewrite( lhs_value ); + } + Trace("cegqi-arith-debug") << "Disequality : check model values " << lhs_value << " " << rhs_value << std::endl; + Assert( lhs_value!=rhs_value ); + Node cmp = NodeManager::currentNM()->mkNode( GEQ, lhs_value, rhs_value ); + cmp = Rewriter::rewrite( cmp ); + Assert( cmp.isConst() ); + is_upper = ( cmp!=ci->getQuantifiersEngine()->getTermUtil()->d_true ); + } + }else{ + is_upper = (r==0); + } + Assert( atom.getKind()==EQUAL && !pol ); + if( d_type.isInteger() ){ + uires = is_upper ? -1 : 1; + uval = NodeManager::currentNM()->mkNode( PLUS, val, NodeManager::currentNM()->mkConst( Rational( uires ) ) ); + uval = Rewriter::rewrite( uval ); + }else{ + Assert( d_type.isReal() ); + uires = is_upper ? -2 : 2; + } + } + if( Trace.isOn("cegqi-arith-bound-inf") ){ + Node pvmod = pv_prop.getModifiedTerm( pv ); + Trace("cegqi-arith-bound-inf") << "From " << lit << ", got : "; + Trace("cegqi-arith-bound-inf") << pvmod << " -> " << uval << ", styp = " << uires << std::endl; + } + //take into account delta + if( ci->useVtsDelta() && ( uires==2 || uires==-2 ) ){ + if( options::cbqiModel() ){ + Node delta_coeff = NodeManager::currentNM()->mkConst( Rational( uires > 0 ? 1 : -1 ) ); + if( vts_coeff_delta.isNull() ){ + vts_coeff_delta = delta_coeff; + }else{ + vts_coeff_delta = NodeManager::currentNM()->mkNode( PLUS, vts_coeff_delta, delta_coeff ); + vts_coeff_delta = Rewriter::rewrite( vts_coeff_delta ); + } + }else{ + Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(); + uval = NodeManager::currentNM()->mkNode( uires==2 ? PLUS : MINUS, uval, delta ); + uval = Rewriter::rewrite( uval ); + } + } + if( options::cbqiModel() ){ + //just store bounds, will choose based on tighest bound + unsigned index = uires>0 ? 0 : 1; + d_mbp_bounds[index].push_back( uval ); + d_mbp_coeff[index].push_back( pv_prop.d_coeff ); + Trace("cegqi-arith-debug") << "Store bound " << index << " " << uval << " " << pv_prop.d_coeff << " " << vts_coeff_inf << " " << vts_coeff_delta << " " << lit << std::endl; + for( unsigned t=0; t<2; t++ ){ + d_mbp_vts_coeff[index][t].push_back( t==0 ? vts_coeff_inf : vts_coeff_delta ); + } + d_mbp_lit[index].push_back( lit ); + }else{ + //try this bound + pv_prop.d_type = uires>0 ? 1 : -1; + if (ci->constructInstantiationInc(pv, uval, pv_prop, sf)) + { + return true; + } + } + } + } + + + return false; +} + +bool ArithInstantiator::processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + if (options::cbqiModel()) { + bool use_inf = ci->useVtsInfinity() && ( d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal() ); + bool upper_first = false; + if( options::cbqiMinBounds() ){ + upper_first = d_mbp_bounds[1].size()<d_mbp_bounds[0].size(); + } + int best_used[2]; + std::vector< Node > t_values[3]; + Node zero = ci->getQuantifiersEngine()->getTermUtil()->d_zero; + Node one = ci->getQuantifiersEngine()->getTermUtil()->d_one; + Node pv_value = ci->getModelValue( pv ); + //try optimal bounds + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + best_used[rr] = -1; + if( d_mbp_bounds[rr].empty() ){ + if( use_inf ){ + Trace("cegqi-arith-bound") << "No " << ( rr==0 ? "lower" : "upper" ) << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; + //no bounds, we do +- infinity + Node val = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( d_type ); + //TODO : rho value for infinity? + if( rr==0 ){ + val = NodeManager::currentNM()->mkNode( UMINUS, val ); + val = Rewriter::rewrite( val ); + } + TermProperties pv_prop_no_bound; + if (ci->constructInstantiationInc(pv, val, pv_prop_no_bound, sf)) + { + return true; + } + } + }else{ + Trace("cegqi-arith-bound") << ( rr==0 ? "Lower" : "Upper" ) << " bounds for " << pv << " (type=" << d_type << ") : " << std::endl; + int best = -1; + Node best_bound_value[3]; + for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){ + Node value[3]; + if( Trace.isOn("cegqi-arith-bound") ){ + Assert( !d_mbp_bounds[rr][j].isNull() ); + Trace("cegqi-arith-bound") << " " << j << ": " << d_mbp_bounds[rr][j]; + if( !d_mbp_vts_coeff[rr][0][j].isNull() ){ + Trace("cegqi-arith-bound") << " (+ " << d_mbp_vts_coeff[rr][0][j] << " * INF)"; + } + if( !d_mbp_vts_coeff[rr][1][j].isNull() ){ + Trace("cegqi-arith-bound") << " (+ " << d_mbp_vts_coeff[rr][1][j] << " * DELTA)"; + } + if( !d_mbp_coeff[rr][j].isNull() ){ + Trace("cegqi-arith-bound") << " (div " << d_mbp_coeff[rr][j] << ")"; + } + Trace("cegqi-arith-bound") << ", value = "; + } + t_values[rr].push_back( Node::null() ); + //check if it is better than the current best bound : lexicographic order infinite/finite/infinitesimal parts + bool new_best = true; + for( unsigned t=0; t<3; t++ ){ + //get the value + if( t==0 ){ + value[0] = d_mbp_vts_coeff[rr][0][j]; + if( !value[0].isNull() ){ + Trace("cegqi-arith-bound") << "( " << value[0] << " * INF ) + "; + }else{ + value[0] = zero; + } + }else if( t==1 ){ + Node t_value = ci->getModelValue( d_mbp_bounds[rr][j] ); + t_values[rr][j] = t_value; + value[1] = t_value; + Trace("cegqi-arith-bound") << value[1]; + }else{ + value[2] = d_mbp_vts_coeff[rr][1][j]; + if( !value[2].isNull() ){ + Trace("cegqi-arith-bound") << " + ( " << value[2] << " * DELTA )"; + }else{ + value[2] = zero; + } + } + //multiply by coefficient + if( value[t]!=zero && !d_mbp_coeff[rr][j].isNull() ){ + Assert( d_mbp_coeff[rr][j].isConst() ); + value[t] = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(1) / d_mbp_coeff[rr][j].getConst<Rational>() ), value[t] ); + value[t] = Rewriter::rewrite( value[t] ); + } + //check if new best + if( best!=-1 ){ + Assert( !value[t].isNull() && !best_bound_value[t].isNull() ); + if( value[t]!=best_bound_value[t] ){ + Kind k = rr==0 ? GEQ : LEQ; + Node cmp_bound = NodeManager::currentNM()->mkNode( k, value[t], best_bound_value[t] ); + cmp_bound = Rewriter::rewrite( cmp_bound ); + if( cmp_bound!=ci->getQuantifiersEngine()->getTermUtil()->d_true ){ + new_best = false; + break; + } + } + } + } + Trace("cegqi-arith-bound") << std::endl; + if( new_best ){ + for( unsigned t=0; t<3; t++ ){ + best_bound_value[t] = value[t]; + } + best = j; + } + } + if( best!=-1 ){ + Trace("cegqi-arith-bound") << "...best bound is " << best << " : "; + if( best_bound_value[0]!=zero ){ + Trace("cegqi-arith-bound") << "( " << best_bound_value[0] << " * INF ) + "; + } + Trace("cegqi-arith-bound") << best_bound_value[1]; + if( best_bound_value[2]!=zero ){ + Trace("cegqi-arith-bound") << " + ( " << best_bound_value[2] << " * DELTA )"; + } + Trace("cegqi-arith-bound") << std::endl; + best_used[rr] = best; + //if using cbqiMidpoint, only add the instance based on one bound if the bound is non-strict + if (!options::cbqiMidpoint() || d_type.isInteger() + || (ci->useVtsDelta() && d_mbp_vts_coeff[rr][1][best].isNull())) + { + Node val = d_mbp_bounds[rr][best]; + val = getModelBasedProjectionValue( ci, pv, val, rr==0, d_mbp_coeff[rr][best], pv_value, t_values[rr][best], sf.getTheta(), + d_mbp_vts_coeff[rr][0][best], d_mbp_vts_coeff[rr][1][best] ); + if( !val.isNull() ){ + TermProperties pv_prop_bound; + pv_prop_bound.d_coeff = d_mbp_coeff[rr][best]; + pv_prop_bound.d_type = rr==0 ? 1 : -1; + if (ci->constructInstantiationInc(pv, val, pv_prop_bound, sf)) + { + return true; + } + } + } + } + } + } + //if not using infinity, use model value of zero + if( !use_inf && d_mbp_bounds[0].empty() && d_mbp_bounds[1].empty() ){ + Node val = zero; + TermProperties pv_prop_zero; + Node theta = sf.getTheta(); + val = getModelBasedProjectionValue( ci, pv, val, true, pv_prop_zero.d_coeff, pv_value, zero, sf.getTheta(), Node::null(), Node::null() ); + if( !val.isNull() ){ + if (ci->constructInstantiationInc(pv, val, pv_prop_zero, sf)) + { + return true; + } + } + } + if( options::cbqiMidpoint() && !d_type.isInteger() ){ + Node vals[2]; + bool bothBounds = true; + Trace("cegqi-arith-bound") << "Try midpoint of bounds..." << std::endl; + for( unsigned rr=0; rr<2; rr++ ){ + int best = best_used[rr]; + if( best==-1 ){ + bothBounds = false; + }else{ + vals[rr] = d_mbp_bounds[rr][best]; + vals[rr] = getModelBasedProjectionValue( ci, pv, vals[rr], rr==0, Node::null(), pv_value, t_values[rr][best], sf.getTheta(), + d_mbp_vts_coeff[rr][0][best], Node::null() ); + } + Trace("cegqi-arith-bound") << "Bound : " << vals[rr] << std::endl; + } + Node val; + if( bothBounds ){ + Assert( !vals[0].isNull() && !vals[1].isNull() ); + if( vals[0]==vals[1] ){ + val = vals[0]; + }else{ + val = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkNode( PLUS, vals[0], vals[1] ), + NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ); + val = Rewriter::rewrite( val ); + } + }else{ + if( !vals[0].isNull() ){ + val = NodeManager::currentNM()->mkNode( PLUS, vals[0], one ); + val = Rewriter::rewrite( val ); + }else if( !vals[1].isNull() ){ + val = NodeManager::currentNM()->mkNode( MINUS, vals[1], one ); + val = Rewriter::rewrite( val ); + } + } + Trace("cegqi-arith-bound") << "Midpoint value : " << val << std::endl; + if( !val.isNull() ){ + TermProperties pv_prop_midpoint; + if (ci->constructInstantiationInc(pv, val, pv_prop_midpoint, sf)) + { + return true; + } + } + } + //generally should not make it to this point FIXME: write proper assertion + //Assert( ( ci->hasNestedQuantification() && !options::cbqiNestedQE() ) || options::cbqiAll() ); + + if( options::cbqiNopt() ){ + //try non-optimal bounds (heuristic, may help when nested quantification) ? + Trace("cegqi-arith-bound") << "Try non-optimal bounds..." << std::endl; + for( unsigned r=0; r<2; r++ ){ + int rr = upper_first ? (1-r) : r; + for( unsigned j=0; j<d_mbp_bounds[rr].size(); j++ ){ + if( (int)j!=best_used[rr] && ( !options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull() ) ){ + Node val = getModelBasedProjectionValue( ci, pv, d_mbp_bounds[rr][j], rr==0, d_mbp_coeff[rr][j], pv_value, t_values[rr][j], sf.getTheta(), + d_mbp_vts_coeff[rr][0][j], d_mbp_vts_coeff[rr][1][j] ); + if( !val.isNull() ){ + TermProperties pv_prop_nopt_bound; + pv_prop_nopt_bound.d_coeff = d_mbp_coeff[rr][j]; + pv_prop_nopt_bound.d_type = rr==0 ? 1 : -1; + if (ci->constructInstantiationInc( + pv, val, pv_prop_nopt_bound, sf)) + { + return true; + } + } + } + } + } + } + } + return false; +} + +bool ArithInstantiator::needsPostProcessInstantiationForVariable( + CegInstantiator* ci, SolvedForm& sf, Node pv, CegInstEffort effort) +{ + return std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end(); +} + +bool ArithInstantiator::postProcessInstantiationForVariable( + CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort, + std::vector<Node>& lemmas) +{ + Assert( std::find( sf.d_non_basic.begin(), sf.d_non_basic.end(), pv )!=sf.d_non_basic.end() ); + Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); + unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); + Assert( !sf.d_props[index].isBasic() ); + Node eq_lhs = sf.d_props[index].getModifiedTerm( sf.d_vars[index] ); + if( Trace.isOn("cegqi-arith-debug") ){ + Trace("cegqi-arith-debug") << "Normalize substitution for "; + Trace("cegqi-arith-debug") << eq_lhs << " = " << sf.d_subs[index] << std::endl; + } + Assert( sf.d_vars[index].getType().isInteger() ); + //must ensure that divisibility constraints are met + //solve updated rewritten equality for vars[index], if coefficient is one, then we are successful + Node eq_rhs = sf.d_subs[index]; + Node eq = eq_lhs.eqNode( eq_rhs ); + eq = Rewriter::rewrite( eq ); + Trace("cegqi-arith-debug") << "...equality is " << eq << std::endl; + std::map< Node, Node > msum; + if (ArithMSum::getMonomialSumLit(eq, msum)) + { + Node veq; + if (ArithMSum::isolate(sf.d_vars[index], msum, veq, EQUAL, true) != 0) + { + Node veq_c; + if( veq[0]!=sf.d_vars[index] ){ + Node veq_v; + if (ArithMSum::getMonomial(veq[0], veq_c, veq_v)) + { + Assert( veq_v==sf.d_vars[index] ); + } + } + sf.d_subs[index] = veq[1]; + if( !veq_c.isNull() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( INTS_DIVISION_TOTAL, veq[1], veq_c ); + Trace("cegqi-arith-debug") << "...bound type is : " << sf.d_props[index].d_type << std::endl; + //intger division rounding up if from a lower bound + if( sf.d_props[index].d_type==1 && options::cbqiRoundUpLowerLia() ){ + sf.d_subs[index] = NodeManager::currentNM()->mkNode( PLUS, sf.d_subs[index], + NodeManager::currentNM()->mkNode( ITE, + NodeManager::currentNM()->mkNode( EQUAL, + NodeManager::currentNM()->mkNode( INTS_MODULUS_TOTAL, veq[1], veq_c ), + ci->getQuantifiersEngine()->getTermUtil()->d_zero ), + ci->getQuantifiersEngine()->getTermUtil()->d_zero, ci->getQuantifiersEngine()->getTermUtil()->d_one ) + ); + } + } + Trace("cegqi-arith-debug") << "...normalize integers : " << sf.d_vars[index] << " -> " << sf.d_subs[index] << std::endl; + }else{ + Trace("cegqi-arith-debug") << "...failed to isolate." << std::endl; + return false; + } + }else{ + Trace("cegqi-arith-debug") << "...failed to get monomial sum." << std::endl; + return false; + } + return true; +} + +void DtInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ +} + +Node DtInstantiator::solve_dt( Node v, Node a, Node b, Node sa, Node sb ) { + Trace("cegqi-arith-debug2") << "Solve dt : " << v << " " << a << " " << b << " " << sa << " " << sb << std::endl; + Node ret; + if( !a.isNull() && a==v ){ + ret = sb; + }else if( !b.isNull() && b==v ){ + ret = sa; + }else if( !a.isNull() && a.getKind()==APPLY_CONSTRUCTOR ){ + if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ + if( a.getOperator()==b.getOperator() ){ + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + Node s = solve_dt( v, a[i], b[i], sa[i], sb[i] ); + if( !s.isNull() ){ + return s; + } + } + } + }else{ + unsigned cindex = Datatype::indexOf( a.getOperator().toExpr() ); + TypeNode tn = a.getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + for( unsigned i=0; i<a.getNumChildren(); i++ ){ + Node nn = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( tn.toType(), i ) ), sb ); + Node s = solve_dt( v, a[i], Node::null(), sa[i], nn ); + if( !s.isNull() ){ + return s; + } + } + } + }else if( !b.isNull() && b.getKind()==APPLY_CONSTRUCTOR ){ + return solve_dt( v, b, a, sb, sa ); + } + if( !ret.isNull() ){ + //ensure does not contain + if( TermUtil::containsTerm( ret, v ) ){ + ret = Node::null(); + } + } + return ret; +} + +bool DtInstantiator::processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + CegInstEffort effort) +{ + Trace("cegqi-dt-debug") << "try based on constructors in equivalence class." + << std::endl; + // look in equivalence class for a constructor + for( unsigned k=0; k<eqc.size(); k++ ){ + Node n = eqc[k]; + if( n.getKind()==APPLY_CONSTRUCTOR ){ + Trace("cegqi-dt-debug") << "...try based on constructor term " << n << std::endl; + std::vector< Node > children; + children.push_back( n.getOperator() ); + const Datatype& dt = ((DatatypeType)(d_type).toType()).getDatatype(); + unsigned cindex = Datatype::indexOf( n.getOperator().toExpr() ); + //now must solve for selectors applied to pv + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + Node c = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[cindex].getSelectorInternal( d_type.toType(), j ) ), pv ); + ci->pushStackVariable( c ); + children.push_back( c ); + } + Node val = NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children ); + TermProperties pv_prop_dt; + if (ci->constructInstantiationInc(pv, val, pv_prop_dt, sf)) + { + return true; + }else{ + //cleanup + for( unsigned j=0; j<dt[cindex].getNumArgs(); j++ ){ + ci->popStackVariable(); + } + break; + } + } + } + return false; +} + +bool DtInstantiator::processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + CegInstEffort effort) +{ + Node val = solve_dt( pv, terms[0], terms[1], terms[0], terms[1] ); + if( !val.isNull() ){ + TermProperties pv_prop; + if (ci->constructInstantiationInc(pv, val, pv_prop, sf)) + { + return true; + } + } + return false; +} + +void EprInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + d_equal_terms.clear(); +} + +bool EprInstantiator::processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + CegInstEffort effort) +{ + if( options::quantEprMatching() ){ + Assert( pv_prop.isBasic() ); + d_equal_terms.push_back( n ); + return false; + }else{ + pv_prop.d_type = 0; + return ci->constructInstantiationInc(pv, n, pv_prop, sf); + } +} + +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, std::vector< Node >& arg_reps, TermArgTrie * tat, unsigned index, std::map< Node, int >& match_score ) { + if( index==catom.getNumChildren() ){ + Assert( tat->hasNodeData() ); + Node gcatom = tat->getNodeData(); + Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom << std::endl; + for( unsigned i=0; i<catom.getNumChildren(); i++ ){ + if( catom[i]==pv ){ + Trace("cegqi-epr") << "...increment " << gcatom[i] << std::endl; + match_score[gcatom[i]]++; + }else{ + //recursive matching + computeMatchScore( ci, pv, catom[i], gcatom[i], match_score ); + } + } + }else{ + std::map< TNode, TermArgTrie >::iterator it = tat->d_data.find( arg_reps[index] ); + if( it!=tat->d_data.end() ){ + computeMatchScore( ci, pv, catom, arg_reps, &it->second, index+1, match_score ); + } + } +} + +void EprInstantiator::computeMatchScore( CegInstantiator * ci, Node pv, Node catom, Node eqc, std::map< Node, int >& match_score ) { + if( inst::Trigger::isAtomicTrigger( catom ) && TermUtil::containsTerm( catom, pv ) ){ + Trace("cegqi-epr") << "Find matches for " << catom << "..." << std::endl; + std::vector< Node > arg_reps; + for( unsigned j=0; j<catom.getNumChildren(); j++ ){ + arg_reps.push_back( ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( catom[j] ) ); + } + if( ci->getQuantifiersEngine()->getMasterEqualityEngine()->hasTerm( eqc ) ){ + Node rep = ci->getQuantifiersEngine()->getMasterEqualityEngine()->getRepresentative( eqc ); + Node op = ci->getQuantifiersEngine()->getTermDatabase()->getMatchOperator( catom ); + TermArgTrie * tat = ci->getQuantifiersEngine()->getTermDatabase()->getTermArgTrie( rep, op ); + Trace("cegqi-epr") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat!=NULL) << std::endl; + if( tat ){ + computeMatchScore( ci, pv, catom, arg_reps, tat, 0, match_score ); + } + } + } +} + +struct sortEqTermsMatch { + std::map< Node, int > d_match_score; + bool operator() (Node i, Node j) { + int match_score_i = d_match_score[i]; + int match_score_j = d_match_score[j]; + return match_score_i>match_score_j || ( match_score_i==match_score_j && i<j ); + } +}; + +bool EprInstantiator::processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + CegInstEffort effort) +{ + if( options::quantEprMatching() ){ + //heuristic for best matching constant + sortEqTermsMatch setm; + for( unsigned i=0; i<ci->getNumCEAtoms(); i++ ){ + Node catom = ci->getCEAtom( i ); + computeMatchScore( ci, pv, catom, catom, setm.d_match_score ); + } + //sort by match score + std::sort( d_equal_terms.begin(), d_equal_terms.end(), setm ); + TermProperties pv_prop; + pv_prop.d_type = 0; + for( unsigned i=0; i<d_equal_terms.size(); i++ ){ + if (ci->constructInstantiationInc(pv, d_equal_terms[i], pv_prop, sf)) + { + return true; + } + } + } + return false; +} + +// this class can be used to query the model value through the CegInstaniator class +class CegInstantiatorBvInverterQuery : public BvInverterQuery +{ + public: + CegInstantiatorBvInverterQuery(CegInstantiator* ci) + : BvInverterQuery(), d_ci(ci) + { + } + ~CegInstantiatorBvInverterQuery() {} + /** return the model value of n */ + Node getModelValue( Node n ) { + return d_ci->getModelValue( n ); + } + /** get bound variable of type tn */ + Node getBoundVariable(TypeNode tn) { return d_ci->getBoundVariable(tn); } + protected: + // pointer to class that is able to query model values + CegInstantiator * d_ci; +}; + +BvInstantiator::BvInstantiator(QuantifiersEngine* qe, TypeNode tn) + : Instantiator(qe, tn), d_tried_assertion_inst(false) +{ + // get the global inverter utility + // this must be global since we need to: + // * process Skolem functions properly across multiple variables within the same quantifier + // * cache Skolem variables uniformly across multiple quantified formulas + d_inverter = qe->getBvInverter(); +} + +BvInstantiator::~BvInstantiator(){ + +} +void BvInstantiator::reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + d_inst_id_counter = 0; + d_var_to_inst_id.clear(); + d_inst_id_to_term.clear(); + 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, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) +{ + Assert(d_inverter != NULL); + // find path to pv + std::vector<unsigned> path; + Node sv = d_inverter->getSolveVariable(pv.getType()); + Node pvs = ci->getModelValue(pv); + Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl; + Node slit = d_inverter->getPathToPv(lit, pv, sv, pvs, path); + if (!slit.isNull()) + { + CegInstantiatorBvInverterQuery m(ci); + unsigned iid = d_inst_id_counter; + Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl; + Node inst = d_inverter->solveBvLit(sv, slit, path, &m); + if (!inst.isNull()) + { + inst = Rewriter::rewrite(inst); + if (inst.isConst() || !ci->hasNestedQuantification()) + { + Trace("cegqi-bv") << "...solved form is " << inst << std::endl; + // store information for id and increment + d_var_to_inst_id[pv].push_back(iid); + d_inst_id_to_term[iid] = inst; + d_inst_id_to_alit[iid] = alit; + d_inst_id_counter++; + } + } + else + { + Trace("cegqi-bv") << "...failed to solve." << std::endl; + } + } +} + +Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) +{ + if (effort == CEG_INST_EFFORT_FULL) + { + // always use model values at full effort + return Node::null(); + } + Node atom = lit.getKind() == NOT ? lit[0] : lit; + bool pol = lit.getKind() != NOT; + Kind k = atom.getKind(); + if (k != EQUAL && k != BITVECTOR_ULT && k != BITVECTOR_SLT) + { + // others are unhandled + return Node::null(); + } + else if (!atom[0].getType().isBitVector()) + { + return Node::null(); + } + else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP + || (pol && k == EQUAL)) + { + return lit; + } + NodeManager* nm = NodeManager::currentNM(); + Node s = atom[0]; + Node t = atom[1]; + + Node sm = ci->getModelValue(s); + Node tm = ci->getModelValue(t); + Assert(!sm.isNull() && sm.isConst()); + Assert(!tm.isNull() && tm.isConst()); + Trace("cegqi-bv") << "Model value: " << std::endl; + Trace("cegqi-bv") << " " << s << " " << k << " " << t << " is " + << std::endl; + Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl; + + Node ret; + if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK) + { + // if using slack, we convert constraints to a positive equality based on + // the current model M, e.g.: + // (not) s ~ t ---> s = t + ( s^M - t^M ) + if (sm != tm) + { + Node slack = Rewriter::rewrite(nm->mkNode(BITVECTOR_SUB, sm, tm)); + Assert(slack.isConst()); + // remember the slack value for the asserted literal + d_alit_to_model_slack[lit] = slack; + ret = nm->mkNode(EQUAL, s, nm->mkNode(BITVECTOR_PLUS, t, slack)); + Trace("cegqi-bv") << "Slack is " << slack << std::endl; + } + else + { + ret = s.eqNode(t); + } + } else { + // turn disequality into an inequality + // e.g. s != t becomes s < t or t < s + if (k == EQUAL) + { + if (Random::getRandom().pickWithProb(0.5)) + { + std::swap(s, t); + } + pol = true; + } + // otherwise, we optimistically solve for the boundary point of an + // inequality, for example: + // for s < t, we solve s+1 = t + // for ~( s < t ), we solve s = t + // notice that this equality does not necessarily hold in the model, and + // hence the corresponding instantiation strategy is not guaranteed to be + // monotonic. + if (!pol) + { + ret = s.eqNode(t); + } else { + Node bv_one = bv::utils::mkOne(bv::utils::getSize(s)); + ret = nm->mkNode(BITVECTOR_PLUS, s, bv_one).eqNode(t); + } + } + Trace("cegqi-bv") << "Process " << lit << " as " << ret << std::endl; + return ret; +} + +bool BvInstantiator::processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) +{ + // if option enabled, use approach for word-level inversion for BV instantiation + if( options::cbqiBv() ){ + // get the best rewritten form of lit for solving for pv + // this should remove instances of non-invertible operators, and "linearize" lit with respect to pv as much as possible + Node rlit = rewriteAssertionForSolvePv(ci, pv, lit); + if( Trace.isOn("cegqi-bv") ){ + Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl; + if( lit!=rlit ){ + Trace("cegqi-bv") << "...rewritten to " << rlit << std::endl; + } + } + if (!rlit.isNull()) + { + processLiteral(ci, sf, pv, rlit, alit, effort); + } + } + return false; +} + +bool BvInstantiator::useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + return !d_tried_assertion_inst + && (effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort()); +} + +bool BvInstantiator::processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) +{ + std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction >::iterator iti = d_var_to_inst_id.find( pv ); + if( iti!=d_var_to_inst_id.end() ){ + Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv << std::endl; + // if interleaving, do not do inversion half the time + if (!options::cbqiBvInterleaveValue() || Random::getRandom().pickWithProb(0.5)) + { + bool firstVar = sf.empty(); + // get inst id list + if (Trace.isOn("cegqi-bv")) + { + Trace("cegqi-bv") << " " << iti->second.size() + << " candidate instantiations for " << pv << " : " + << std::endl; + if (firstVar) + { + Trace("cegqi-bv") << " ...this is the first variable" << std::endl; + } + } + // until we have a model-preserving selection function for BV, this must + // be heuristic (we only pick one literal) + // hence we randomize the list + // this helps robustness, since picking the same literal every time may + // lead to a stream of value instantiations, whereas with randomization + // we may find an invertible literal that leads to a useful instantiation. + std::random_shuffle(iti->second.begin(), iti->second.end()); + + if (Trace.isOn("cegqi-bv")) + { + for (unsigned j = 0, size = iti->second.size(); j < size; j++) + { + unsigned inst_id = iti->second[j]; + Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); + Node inst_term = d_inst_id_to_term[inst_id]; + Assert(d_inst_id_to_alit.find(inst_id) != d_inst_id_to_alit.end()); + Node alit = d_inst_id_to_alit[inst_id]; + + // get the slack value introduced for the asserted literal + Node curr_slack_val; + std::unordered_map<Node, Node, NodeHashFunction>::iterator itms = + d_alit_to_model_slack.find(alit); + if (itms != d_alit_to_model_slack.end()) + { + curr_slack_val = itms->second; + } + + // debug printing + Trace("cegqi-bv") << " [" << j << "] : "; + Trace("cegqi-bv") << inst_term << std::endl; + if (!curr_slack_val.isNull()) { + Trace("cegqi-bv") << " ...with slack value : " << curr_slack_val + << std::endl; + } + Trace("cegqi-bv-debug") << " ...from : " << alit << std::endl; + Trace("cegqi-bv") << std::endl; + } + } + + // Now, try all instantiation ids we want to try + // Typically we try only one, otherwise worst-case performance + // for constructing instantiations is exponential on the number of + // variables in this quantifier prefix. + bool ret = false; + bool tryMultipleInst = firstVar && options::cbqiMultiInst(); + bool revertOnSuccess = tryMultipleInst; + for (unsigned j = 0, size = iti->second.size(); j < size; j++) + { + unsigned inst_id = iti->second[j]; + Assert(d_inst_id_to_term.find(inst_id) != d_inst_id_to_term.end()); + Node inst_term = d_inst_id_to_term[inst_id]; + Node alit = d_inst_id_to_alit[inst_id]; + // try instantiation pv -> inst_term + 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)) + { + ret = true; + } + ci->markSolved(alit, false); + // we are done unless we try multiple instances + if (!tryMultipleInst) + { + break; + } + } + if (ret) + { + return true; + } + Trace("cegqi-bv") << "...failed to add instantiation for " << pv + << std::endl; + d_var_to_curr_inst_id.erase(pv); + } else { + Trace("cegqi-bv") << "...do not do instantiation for " << pv + << " (skip, based on heuristic)" << std::endl; + } + } + + return false; +} + +Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, + Node pv, + Node lit) +{ + // result of rewriting the visited term + std::stack<std::unordered_map<TNode, Node, TNodeHashFunction> > visited; + visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>()); + // whether the visited term contains pv + std::unordered_map<TNode, bool, TNodeHashFunction> visited_contains_pv; + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; + std::unordered_map<TNode, Node, TNodeHashFunction> curr_subs; + std::stack<std::stack<TNode> > visit; + TNode cur; + visit.push(std::stack<TNode>()); + visit.top().push(lit); + do { + cur = visit.top().top(); + visit.top().pop(); + it = visited.top().find(cur); + + if (it == visited.top().end()) + { + std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itc = + curr_subs.find(cur); + if (itc != curr_subs.end()) + { + visited.top()[cur] = itc->second; + } + else + { + if (cur.getKind() == CHOICE) + { + // must replace variables of choice functions + // with new variables to avoid variable + // capture when considering substitutions + // with multiple literals. + Node bv = ci->getBoundVariable(cur[0][0].getType()); + // should not have captured variables + Assert(curr_subs.find(cur[0][0]) == curr_subs.end()); + curr_subs[cur[0][0]] = bv; + // we cannot cache the results of subterms + // of this choice expression since we are + // now in the context { cur[0][0] -> bv }, + // hence we push a context here + visited.push(std::unordered_map<TNode, Node, TNodeHashFunction>()); + visit.push(std::stack<TNode>()); + } + visited.top()[cur] = Node::null(); + visit.top().push(cur); + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + visit.top().push(cur[i]); + } + } + } else if (it->second.isNull()) { + Node ret; + bool childChanged = false; + std::vector<Node> children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back(cur.getOperator()); + } + bool contains_pv = ( cur==pv ); + for (unsigned i = 0; i < cur.getNumChildren(); i++) { + it = visited.top().find(cur[i]); + Assert(it != visited.top().end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cur[i] != it->second; + children.push_back(it->second); + contains_pv = contains_pv || visited_contains_pv[cur[i]]; + } + // careful that rewrites above do not affect whether this term contains pv + visited_contains_pv[cur] = contains_pv; + + // rewrite the term + ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv); + + // return original if the above function does not produce a result + if (ret.isNull()) { + if (childChanged) { + ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); + }else{ + ret = cur; + } + } + + /* We need to update contains_pv also for rewritten nodes, since + * the normalizePv* functions rely on the information if pv occurs in a + * rewritten node or not. */ + if (ret != cur) + { + contains_pv = (ret == pv); + for (unsigned i = 0, size = ret.getNumChildren(); i < size; ++i) + { + contains_pv = contains_pv || visited_contains_pv[ret[i]]; + } + visited_contains_pv[ret] = contains_pv; + } + + // if was choice, pop context + if (cur.getKind() == CHOICE) + { + Assert(curr_subs.find(cur[0][0]) != curr_subs.end()); + curr_subs.erase(cur[0][0]); + visited.pop(); + visit.pop(); + Assert(visited.size() == visit.size()); + Assert(!visit.empty()); + } + + visited.top()[cur] = ret; + } + } while (!visit.top().empty()); + Assert(visited.size() == 1); + Assert(visited.top().find(lit) != visited.top().end()); + Assert(!visited.top().find(lit)->second.isNull()); + + Node result = visited.top()[lit]; + + if (Trace.isOn("cegqi-bv-nl")) + { + std::vector<TNode> trace_visit; + std::unordered_set<TNode, TNodeHashFunction> trace_visited; + + trace_visit.push_back(result); + do + { + cur = trace_visit.back(); + trace_visit.pop_back(); + + if (trace_visited.find(cur) == trace_visited.end()) + { + trace_visited.insert(cur); + trace_visit.insert(trace_visit.end(), cur.begin(), cur.end()); + } + else if (cur == pv) + { + Trace("cegqi-bv-nl") + << "NONLINEAR LITERAL for " << pv << " : " << lit << std::endl; + } + } while (!trace_visit.empty()); + } + + return result; +} + +/** + * Determine coefficient of pv in term n, where n has the form pv, -pv, pv * t, + * or -pv * t. Extracting the coefficient of multiplications only succeeds if + * the multiplication are normalized with normalizePvMult. + * + * If sucessful it returns + * 1 if n == pv, + * -1 if n == -pv, + * t if n == pv * t, + * -t if n == -pv * t. + * If n is not a linear term, a null node is returned. + */ +static Node getPvCoeff(TNode pv, TNode n) +{ + bool neg = false; + Node coeff; + + if (n.getKind() == BITVECTOR_NEG) + { + neg = true; + n = n[0]; + } + + if (n == pv) + { + coeff = bv::utils::mkOne(bv::utils::getSize(pv)); + } + /* All multiplications are normalized to pv * (t1 * t2). */ + else if (n.getKind() == BITVECTOR_MULT && n.getAttribute(BvLinearAttribute())) + { + Assert(n.getNumChildren() == 2); + Assert(n[0] == pv); + coeff = n[1]; + } + else /* n is in no form to extract the coefficient for pv */ + { + Trace("cegqi-bv-nl") << "Cannot extract coefficient for " << pv << " in " + << n << std::endl; + return Node::null(); + } + Assert(!coeff.isNull()); + + if (neg) return NodeManager::currentNM()->mkNode(BITVECTOR_NEG, coeff); + return coeff; +} + +/** + * Normalizes the children of a BITVECTOR_MULT w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * -pv * b * c + * + * is rewritten to + * + * pv * -(a * b * c) + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns a + * multiplication over children. + */ +static Node normalizePvMult( + TNode pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + bool neg, neg_coeff = false; + bool found_pv = false; + NodeManager* nm; + NodeBuilder<> nb(BITVECTOR_MULT); + BvLinearAttribute is_linear; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (!found_pv && nc == pv) + { + found_pv = true; + neg_coeff = neg; + continue; + } + else if (!found_pv && nc.getKind() == BITVECTOR_MULT + && nc.getAttribute(is_linear)) + { + Assert(nc.getNumChildren() == 2); + Assert(nc[0] == pv); + Assert(!contains_pv[nc[1]]); + found_pv = true; + neg_coeff = neg; + nb << nc[1]; + continue; + } + return Node::null(); /* non-linear */ + } + Assert(nb.getNumChildren() > 0); + + Node coeff = (nb.getNumChildren() == 1) ? nb[0] : nb.constructNode(); + if (neg_coeff) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + coeff = Rewriter::rewrite(coeff); + unsigned size_coeff = bv::utils::getSize(coeff); + Node zero = bv::utils::mkZero(size_coeff); + if (coeff == zero) + { + return zero; + } + Node result; + if (found_pv) + { + if (coeff == bv::utils::mkOne(size_coeff)) + { + return pv; + } + result = nm->mkNode(BITVECTOR_MULT, pv, coeff); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + } + else + { + result = coeff; + } + return result; +} + +#ifdef CVC4_ASSERTIONS +static bool isLinearPlus( + TNode n, + TNode pv, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + Node coeff; + Assert(n.getAttribute(BvLinearAttribute())); + Assert(n.getNumChildren() == 2); + if (n[0] != pv) + { + Assert(n[0].getKind() == BITVECTOR_MULT); + Assert(n[0].getNumChildren() == 2); + Assert(n[0][0] == pv); + Assert(!contains_pv[n[0][1]]); + } + Assert(!contains_pv[n[1]]); + coeff = getPvCoeff(pv, n[0]); + Assert(!coeff.isNull()); + Assert(!contains_pv[coeff]); + return true; +} +#endif + +/** + * Normalizes the children of a BITVECTOR_PLUS w.r.t. pv. contains_pv marks + * terms in which pv occurs. + * For example, + * + * a * pv + b + c * -pv + * + * is rewritten to + * + * pv * (a - c) + b + * + * Returns the normalized node if the resulting term is linear w.r.t. pv and + * a null node otherwise. If pv does not occur in children it returns an + * addition over children. + */ +static Node normalizePvPlus( + Node pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + NodeManager* nm; + NodeBuilder<> nb_c(BITVECTOR_PLUS); + NodeBuilder<> nb_l(BITVECTOR_PLUS); + BvLinearAttribute is_linear; + bool neg; + + nm = NodeManager::currentNM(); + for (TNode nc : children) + { + if (!contains_pv[nc]) + { + nb_l << nc; + continue; + } + + neg = false; + if (nc.getKind() == BITVECTOR_NEG) + { + neg = true; + nc = nc[0]; + } + + if (nc == pv + || (nc.getKind() == BITVECTOR_MULT && nc.getAttribute(is_linear))) + { + Node coeff = getPvCoeff(pv, nc); + Assert(!coeff.isNull()); + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + } + nb_c << coeff; + continue; + } + else if (nc.getKind() == BITVECTOR_PLUS && nc.getAttribute(is_linear)) + { + Assert(isLinearPlus(nc, pv, contains_pv)); + Node coeff = getPvCoeff(pv, nc[0]); + Assert(!coeff.isNull()); + Node leaf = nc[1]; + if (neg) + { + coeff = nm->mkNode(BITVECTOR_NEG, coeff); + leaf = nm->mkNode(BITVECTOR_NEG, leaf); + } + nb_c << coeff; + nb_l << leaf; + continue; + } + /* can't collect coefficients of 'pv' in 'cur' -> non-linear */ + return Node::null(); + } + Assert(nb_c.getNumChildren() > 0 || nb_l.getNumChildren() > 0); + + Node pv_mult_coeffs, result; + if (nb_c.getNumChildren() > 0) + { + Node coeffs = (nb_c.getNumChildren() == 1) ? nb_c[0] : nb_c.constructNode(); + coeffs = Rewriter::rewrite(coeffs); + result = pv_mult_coeffs = normalizePvMult(pv, {pv, coeffs}, contains_pv); + } + + if (nb_l.getNumChildren() > 0) + { + Node leafs = (nb_l.getNumChildren() == 1) ? nb_l[0] : nb_l.constructNode(); + leafs = Rewriter::rewrite(leafs); + Node zero = bv::utils::mkZero(bv::utils::getSize(pv)); + /* pv * 0 + t --> t */ + if (pv_mult_coeffs.isNull() || pv_mult_coeffs == zero) + { + result = leafs; + } + else + { + result = nm->mkNode(BITVECTOR_PLUS, pv_mult_coeffs, leafs); + contains_pv[result] = true; + result.setAttribute(is_linear, true); + } + } + Assert(!result.isNull()); + return result; +} + +/** + * Linearize an equality w.r.t. pv such that pv only occurs once. contains_pv + * marks terms in which pv occurs. + * For example, equality + * + * -pv * a + b = c + pv + * + * rewrites to + * + * pv * (-a - 1) = c - b. + */ +static Node normalizePvEqual( + Node pv, + const std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + Assert(children.size() == 2); + + NodeManager* nm = NodeManager::currentNM(); + BvLinearAttribute is_linear; + Node coeffs[2], leafs[2]; + bool neg; + TNode child; + + for (unsigned i = 0; i < 2; ++i) + { + child = children[i]; + neg = false; + if (child.getKind() == BITVECTOR_NEG) + { + neg = true; + child = child[0]; + } + if (child.getAttribute(is_linear) || child == pv) + { + if (child.getKind() == BITVECTOR_PLUS) + { + Assert(isLinearPlus(child, pv, contains_pv)); + coeffs[i] = getPvCoeff(pv, child[0]); + leafs[i] = child[1]; + } + else + { + Assert(child.getKind() == BITVECTOR_MULT || child == pv); + coeffs[i] = getPvCoeff(pv, child); + } + } + if (neg) + { + if (!coeffs[i].isNull()) + { + coeffs[i] = nm->mkNode(BITVECTOR_NEG, coeffs[i]); + } + if (!leafs[i].isNull()) + { + leafs[i] = nm->mkNode(BITVECTOR_NEG, leafs[i]); + } + } + } + + if (coeffs[0].isNull() || coeffs[1].isNull()) + { + return Node::null(); + } + + Node coeff = nm->mkNode(BITVECTOR_SUB, coeffs[0], coeffs[1]); + coeff = Rewriter::rewrite(coeff); + std::vector<Node> mult_children = {pv, coeff}; + Node lhs = normalizePvMult(pv, mult_children, contains_pv); + + Node rhs; + if (!leafs[0].isNull() && !leafs[1].isNull()) + { + rhs = nm->mkNode(BITVECTOR_SUB, leafs[1], leafs[0]); + } + else if (!leafs[0].isNull()) + { + rhs = nm->mkNode(BITVECTOR_NEG, leafs[0]); + } + else if (!leafs[1].isNull()) + { + rhs = leafs[1]; + } + else + { + rhs = bv::utils::mkZero(bv::utils::getSize(pv)); + } + rhs = Rewriter::rewrite(rhs); + + if (lhs == rhs) + { + return bv::utils::mkTrue(); + } + + Node result = lhs.eqNode(rhs); + contains_pv[result] = true; + return result; +} + +Node BvInstantiator::rewriteTermForSolvePv( + Node pv, + Node n, + std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv) +{ + NodeManager* nm = NodeManager::currentNM(); + + // [1] rewrite cases of non-invertible operators + + if (n.getKind() == EQUAL) + { + TNode lhs = children[0]; + TNode rhs = children[1]; + + /* rewrite: x * x = x -> x < 2 */ + if ((lhs == pv && rhs.getKind() == BITVECTOR_MULT && rhs[0] == pv + && rhs[1] == pv) + || (rhs == pv && lhs.getKind() == BITVECTOR_MULT && lhs[0] == pv + && lhs[1] == pv)) + { + return nm->mkNode( + BITVECTOR_ULT, + pv, + bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2)))); + } + + if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs]) + { + Node result = normalizePvEqual(pv, children, contains_pv); + if (!result.isNull()) + { + Trace("cegqi-bv-nl") + << "Normalize " << n << " to " << result << std::endl; + } + else + { + Trace("cegqi-bv-nl") + << "Nonlinear " << n.getKind() << " " << n << std::endl; + } + return result; + } + } + else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS) + { + if (options::cbqiBvLinearize() && contains_pv[n]) + { + Node result; + if (n.getKind() == BITVECTOR_MULT) + { + result = normalizePvMult(pv, children, contains_pv); + } + else + { + result = normalizePvPlus(pv, children, contains_pv); + } + if (!result.isNull()) + { + Trace("cegqi-bv-nl") + << "Normalize " << n << " to " << result << std::endl; + return result; + } + else + { + Trace("cegqi-bv-nl") + << "Nonlinear " << n.getKind() << " " << n << std::endl; + } + } + } + + // [2] try to rewrite non-linear literals -> linear literals + + return Node::null(); +} + +/** sort bv extract interval + * + * This sorts lists of bitvector extract terms where + * ((_ extract i1 i2) t) < ((_ extract j1 j2) t) + * if i1>j1 or i1=j1 and i2>j2. + */ +struct SortBvExtractInterval +{ + bool operator()(Node i, Node j) + { + Assert(i.getKind() == BITVECTOR_EXTRACT); + Assert(j.getKind() == BITVECTOR_EXTRACT); + BitVectorExtract ie = i.getOperator().getConst<BitVectorExtract>(); + BitVectorExtract je = j.getOperator().getConst<BitVectorExtract>(); + if (ie.high > je.high) + { + return true; + } + else if (ie.high == je.high) + { + Assert(ie.low != je.low); + return ie.low > je.low; + } + return false; + } +}; + +void BvInstantiatorPreprocess::registerCounterexampleLemma( + std::vector<Node>& lems, std::vector<Node>& ce_vars) +{ + // new variables + std::vector<Node> vars; + // new lemmas + std::vector<Node> new_lems; + + if (options::cbqiBvRmExtract()) + { + NodeManager* nm = NodeManager::currentNM(); + Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl; + // map from terms to bitvector extracts applied to that term + std::map<Node, std::vector<Node> > extract_map; + std::unordered_set<TNode, TNodeHashFunction> visited; + for (unsigned i = 0, size = lems.size(); i < size; i++) + { + Trace("cegqi-bv-pp-debug2") << "Register ce lemma # " << i << " : " + << lems[i] << std::endl; + collectExtracts(lems[i], extract_map, visited); + } + for (std::pair<const Node, std::vector<Node> >& es : extract_map) + { + // sort based on the extract start position + std::vector<Node>& curr_vec = es.second; + + SortBvExtractInterval sbei; + std::sort(curr_vec.begin(), curr_vec.end(), sbei); + + unsigned width = es.first.getType().getBitVectorSize(); + + // list of points b such that: + // b>0 and we must start a segment at (b-1) or b==0 + std::vector<unsigned> boundaries; + boundaries.push_back(width); + boundaries.push_back(0); + + Trace("cegqi-bv-pp") << "For term " << es.first << " : " << std::endl; + for (unsigned i = 0, size = curr_vec.size(); i < size; i++) + { + Trace("cegqi-bv-pp") << " " << i << " : " << curr_vec[i] << std::endl; + BitVectorExtract e = + curr_vec[i].getOperator().getConst<BitVectorExtract>(); + if (std::find(boundaries.begin(), boundaries.end(), e.high + 1) + == boundaries.end()) + { + boundaries.push_back(e.high + 1); + } + if (std::find(boundaries.begin(), boundaries.end(), e.low) + == boundaries.end()) + { + boundaries.push_back(e.low); + } + } + std::sort(boundaries.rbegin(), boundaries.rend()); + + // make the extract variables + std::vector<Node> children; + for (unsigned i = 1; i < boundaries.size(); i++) + { + Assert(boundaries[i - 1] > 0); + Node ex = bv::utils::mkExtract( + es.first, boundaries[i - 1] - 1, boundaries[i]); + Node var = + nm->mkSkolem("ek", + ex.getType(), + "variable to represent disjoint extract region"); + children.push_back(var); + vars.push_back(var); + } + + Node conc = nm->mkNode(kind::BITVECTOR_CONCAT, children); + Assert(conc.getType() == es.first.getType()); + Node eq_lem = conc.eqNode(es.first); + Trace("cegqi-bv-pp") << "Introduced : " << eq_lem << std::endl; + new_lems.push_back(eq_lem); + Trace("cegqi-bv-pp") << "...finished processing extracts for term " + << es.first << std::endl; + } + Trace("cegqi-bv-pp") << "-----done remove extracts" << std::endl; + } + + if (!vars.empty()) + { + // could try applying subs -> vars here + // in practice, this led to worse performance + + Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..." + << std::endl; + lems.insert(lems.end(), new_lems.begin(), new_lems.end()); + Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..." + << std::endl; + ce_vars.insert(ce_vars.end(), vars.begin(), vars.end()); + } +} + +void BvInstantiatorPreprocess::collectExtracts( + Node lem, + std::map<Node, std::vector<Node> >& extract_map, + std::unordered_set<TNode, TNodeHashFunction>& visited) +{ + std::vector<TNode> visit; + TNode cur; + visit.push_back(lem); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() != FORALL) + { + if (cur.getKind() == BITVECTOR_EXTRACT) + { + extract_map[cur[0]].push_back(cur); + } + + for (const Node& nc : cur) + { + visit.push_back(nc); + } + } + } + } while (!visit.empty()); +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/cegqi/ceg_t_instantiator.h b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h new file mode 100644 index 000000000..b9c7e2024 --- /dev/null +++ b/src/theory/quantifiers/cegqi/ceg_t_instantiator.h @@ -0,0 +1,331 @@ +/********************* */ +/*! \file ceg_t_instantiator.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief theory-specific counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__CEG_T_INSTANTIATOR_H +#define __CVC4__CEG_T_INSTANTIATOR_H + +#include "theory/quantifiers/bv_inverter.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" + +#include <unordered_set> + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** TODO (#1367) : document these classes, also move to separate files. */ + +class ArithInstantiator : public Instantiator { + public: + ArithInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~ArithInstantiator(){} + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + virtual bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override + { + return true; + } + virtual bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + CegInstEffort effort) override; + virtual bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override + { + return true; + } + virtual Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) override; + virtual bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) override; + virtual bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + virtual bool needsPostProcessInstantiationForVariable( + CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + virtual bool postProcessInstantiationForVariable( + CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort, + std::vector<Node>& lemmas) override; + virtual std::string identify() const override { return "Arith"; } + private: + Node d_vts_sym[2]; + std::vector<Node> d_mbp_bounds[2]; + std::vector<Node> d_mbp_coeff[2]; + std::vector<Node> d_mbp_vts_coeff[2][2]; + std::vector<Node> d_mbp_lit[2]; + int solve_arith(CegInstantiator* ci, + Node v, + Node atom, + Node& veq_c, + Node& val, + Node& vts_coeff_inf, + Node& vts_coeff_delta); + Node getModelBasedProjectionValue(CegInstantiator* ci, + Node e, + Node t, + bool isLower, + Node c, + Node me, + Node mt, + Node theta, + Node inf_coeff, + Node delta_coeff); +}; + +class DtInstantiator : public Instantiator { +public: + DtInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~DtInstantiator(){} + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + virtual bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + CegInstEffort effort) override; + virtual bool hasProcessEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override + { + return true; + } + virtual bool processEquality(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<TermProperties>& term_props, + std::vector<Node>& terms, + CegInstEffort effort) override; + virtual std::string identify() const override { return "Dt"; } + private: + Node solve_dt(Node v, Node a, Node b, Node sa, Node sb); +}; + +class TermArgTrie; + +class EprInstantiator : public Instantiator { + public: + EprInstantiator( QuantifiersEngine * qe, TypeNode tn ) : Instantiator( qe, tn ){} + virtual ~EprInstantiator(){} + virtual void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + virtual bool processEqualTerm(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + TermProperties& pv_prop, + Node n, + CegInstEffort effort) override; + virtual bool processEqualTerms(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + std::vector<Node>& eqc, + CegInstEffort effort) override; + virtual std::string identify() const override { return "Epr"; } + private: + std::vector<Node> d_equal_terms; + void computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + std::vector<Node>& arg_reps, + TermArgTrie* tat, + unsigned index, + std::map<Node, int>& match_score); + void computeMatchScore(CegInstantiator* ci, + Node pv, + Node catom, + Node eqc, + std::map<Node, int>& match_score); +}; + +/** Bitvector instantiator + * + * This implements an approach for counterexample-guided instantiation + * for bit-vector variables based on word-level inversions. + * It is enabled by --cbqi-bv. + */ +class BvInstantiator : public Instantiator { + public: + BvInstantiator(QuantifiersEngine* qe, TypeNode tn); + ~BvInstantiator() override; + void reset(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + bool hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override + { + return true; + } + Node hasProcessAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + CegInstEffort effort) override; + bool processAssertion(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort) override; + bool processAssertions(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + /** use model value + * + * We allow model values if we have not already tried an assertion, + * and only at levels below full if cbqiFullEffort is false. + */ + bool useModelValue(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + CegInstEffort effort) override; + std::string identify() const override { return "Bv"; } + + private: + // point to the bv inverter class + BvInverter * d_inverter; + unsigned d_inst_id_counter; + /** information about solved forms */ + std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id; + std::unordered_map< unsigned, Node > d_inst_id_to_term; + std::unordered_map<unsigned, Node> d_inst_id_to_alit; + // variable to current id we are processing + std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id; + /** the amount of slack we added for asserted literals */ + std::unordered_map<Node, Node, NodeHashFunction> d_alit_to_model_slack; + /** 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 for pv + */ + Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit); + /** rewrite term for solve pv + * This is a helper function for rewriteAssertionForSolvePv. + * If this returns non-null value ret, then this indicates + * that n should be rewritten to ret. It is called as + * a "post-rewrite", that is, after the children of n + * have been rewritten and stored in the vector children. + * + * contains_pv stores whether certain nodes contain pv. + * where we guarantee that all subterms of terms in children + * appear in the domain of contains_pv. + */ + Node rewriteTermForSolvePv( + Node pv, + Node n, + std::vector<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv); + /** process literal, called from processAssertion + * lit is the literal to solve for pv that has been rewritten according to + * internal rules here. + * alit is the asserted literal that lit is derived from. + */ + void processLiteral(CegInstantiator* ci, + SolvedForm& sf, + Node pv, + Node lit, + Node alit, + CegInstEffort effort); +}; + +/** Bitvector instantiator preprocess + * + * This class implements preprocess techniques that are helpful for + * counterexample-guided instantiation, such as introducing variables + * that refer to disjoint bit-vector extracts. + */ +class BvInstantiatorPreprocess : public InstantiatorPreprocess +{ + public: + BvInstantiatorPreprocess() {} + ~BvInstantiatorPreprocess() override {} + /** register counterexample lemma + * + * This method modifies the contents of lems based on the extract terms + * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces + * a dummy equality so that segments of terms t under extracts can be solved + * independently. + * + * For example: + * P[ ((extract 7 4) t), ((extract 3 0) t)] + * becomes: + * P[((extract 7 4) t), ((extract 3 0) t)] ^ + * t = concat( x74, x30 ) + * where x74 and x30 are fresh variables of type BV_4. + * + * Another example: + * P[ ((extract 7 3) t), ((extract 4 0) t)] + * becomes: + * P[((extract 7 4) t), ((extract 3 0) t)] ^ + * t = concat( x75, x44, x30 ) + * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4 + * respectively. + * + * Notice we leave the original conjecture alone. This is done for performance + * since the added equalities ensure we are able to construct the proper + * solved forms for variables in t and for the intermediate variables above. + */ + void registerCounterexampleLemma(std::vector<Node>& lems, + std::vector<Node>& ce_vars) override; + + private: + /** collect extracts + * + * This method collects all extract terms in lem + * and stores them in d_extract_map. + * visited is the terms we've already visited. + */ + void collectExtracts(Node lem, + std::map<Node, std::vector<Node> >& extract_map, + std::unordered_set<TNode, TNodeHashFunction>& visited); +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp new file mode 100644 index 000000000..8de3dbfcb --- /dev/null +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.cpp @@ -0,0 +1,828 @@ +/********************* */ +/*! \file inst_strategy_cbqi.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of counterexample-guided quantifier instantiation strategies + **/ +#include "theory/quantifiers/cegqi/inst_strategy_cbqi.h" + +#include "options/quantifiers_options.h" +#include "smt/term_formula_removal.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/theory_arith_private.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_epr.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/theory_engine.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::theory::arith; + +#define ARITH_INSTANTIATOR_USE_MINUS_DELTA + +InstStrategyCbqi::InstStrategyCbqi( QuantifiersEngine * qe ) + : QuantifiersModule( qe ), d_added_cbqi_lemma( qe->getUserContext() ), +d_elim_quants( qe->getSatContext() ), +d_nested_qe_waitlist_size( qe->getUserContext() ), +d_nested_qe_waitlist_proc( qe->getUserContext() ) +//, d_added_inst( qe->getUserContext() ) +{ + d_qid_count = 0; +} + +bool InstStrategyCbqi::needsCheck( Theory::Effort e ) { + return e>=Theory::EFFORT_LAST_CALL; +} + +QuantifiersModule::QEffort InstStrategyCbqi::needsModel(Theory::Effort e) +{ + for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + return QEFFORT_STANDARD; + } + } + return QEFFORT_NONE; +} + +bool InstStrategyCbqi::registerCbqiLemma( Node q ) { + if( !hasAddedCbqiLemma( q ) ){ + d_added_cbqi_lemma.insert( q ); + Trace("cbqi-debug") << "Do cbqi for " << q << std::endl; + //add cbqi lemma + //get the counterexample literal + Node ceLit = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q ); + if( !ceBody.isNull() ){ + //add counterexample lemma + Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); + //require any decision on cel to be phase=true + d_quantEngine->addRequirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + lem = Rewriter::rewrite( lem ); + Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl; + registerCounterexampleLemma( q, lem ); + + //totality lemmas for EPR + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + if( tn.isSort() ){ + if( qepr->isEPR( tn ) ){ + //add totality lemma + std::map< TypeNode, std::vector< Node > >::iterator itc = qepr->d_consts.find( tn ); + if( itc!=qepr->d_consts.end() ){ + Assert( !itc->second.empty() ); + Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ); + std::vector< Node > disj; + for( unsigned j=0; j<itc->second.size(); j++ ){ + disj.push_back( ic.eqNode( itc->second[j] ) ); + } + Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj ); + Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl; + d_quantEngine->getOutputChannel().lemma( tlem ); + }else{ + Assert( false ); + } + }else{ + Assert( !options::cbqiAll() ); + } + } + } + } + + //compute dependencies between quantified formulas + if( options::cbqiLitDepend() || options::cbqiInnermost() ){ + std::vector< Node > ics; + TermUtil::computeVarContains( q, ics ); + d_parent_quant[q].clear(); + d_children_quant[q].clear(); + std::vector< Node > dep; + for( unsigned i=0; i<ics.size(); i++ ){ + Node qi = ics[i].getAttribute(InstConstantAttribute()); + if( std::find( d_parent_quant[q].begin(), d_parent_quant[q].end(), qi )==d_parent_quant[q].end() ){ + d_parent_quant[q].push_back( qi ); + d_children_quant[qi].push_back( q ); + Assert( hasAddedCbqiLemma( qi ) ); + Node qicel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( qi ); + dep.push_back( qi ); + dep.push_back( qicel ); + } + } + if( !dep.empty() ){ + Node dep_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, ceLit, NodeManager::currentNM()->mkNode( kind::AND, dep ) ); + Trace("cbqi-lemma") << "Counterexample dependency lemma : " << dep_lemma << std::endl; + d_quantEngine->getOutputChannel().lemma( dep_lemma ); + } + } + + //must register all sub-quantifiers of counterexample lemma, register their lemmas + std::vector< Node > quants; + TermUtil::computeQuantContains( lem, quants ); + for( unsigned i=0; i<quants.size(); i++ ){ + if( doCbqi( quants[i] ) ){ + registerCbqiLemma( quants[i] ); + } + if( options::cbqiNestedQE() ){ + //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("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl; + } + } + } + } + return true; + }else{ + return false; + } +} + +void InstStrategyCbqi::reset_round( Theory::Effort effort ) { + d_cbqi_set_quant_inactive = false; + d_incomplete_check = false; + d_active_quant.clear(); + //check if any cbqi lemma has not been added yet + for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + 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("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl; + Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + bool value; + if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl; + if( !value ){ + if( d_quantEngine->getValuation().isDecision( cel ) ){ + Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl; + }else{ + Trace("cbqi") << "Inactive : " << q << std::endl; + d_quantEngine->getModel()->setQuantifierActive( q, false ); + d_cbqi_set_quant_inactive = true; + d_active_quant.erase( q ); + d_elim_quants.insert( q ); + Trace("cbqi-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("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; + d_quantEngine->getOutputChannel().lemma( dqelem ); + d_nested_qe_waitlist_proc[q] = index + 1; + } + } + } + }else{ + Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl; + } + } + } + } + + //refinement: only consider innermost active quantified formulas + if( options::cbqiInnermost() ){ + if( !d_children_quant.empty() && !d_active_quant.empty() ){ + Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl; + std::vector< Node > ninner; + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; j<itc->second.size(); j++ ){ + if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){ + Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl; + ninner.push_back( it->first ); + break; + } + } + } + } + Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl; + for( unsigned i=0; i<ninner.size(); i++ ){ + Assert( d_active_quant.find( ninner[i] )!=d_active_quant.end() ); + d_active_quant.erase( ninner[i] ); + } + Assert( !d_active_quant.empty() ); + Trace("cbqi-debug") << "...done removing." << std::endl; + } + } + + processResetInstantiationRound( effort ); +} + +void InstStrategyCbqi::check(Theory::Effort e, QEffort quant_e) +{ + if (quant_e == QEFFORT_STANDARD) + { + Assert( !d_quantEngine->inConflict() ); + double clSet = 0; + if( Trace.isOn("cbqi-engine") ){ + clSet = double(clock())/double(CLOCKS_PER_SEC); + Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; + } + unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + for( int ee=0; ee<=1; ee++ ){ + //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + // if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ + for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){ + Node q = it->first; + Trace("cbqi") << "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("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl; + Assert( false ); + } + } + if( d_quantEngine->inConflict() || d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + break; + } + } + if( Trace.isOn("cbqi-engine") ){ + if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; + } + double clSet2 = double(clock())/double(CLOCKS_PER_SEC); + Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; + } + } +} + +bool InstStrategyCbqi::checkComplete() { + if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){ + return false; + }else{ + return true; + } +} + +bool InstStrategyCbqi::checkCompleteFor( Node q ) { + std::map< Node, int >::iterator it = d_do_cbqi.find( q ); + if( it!=d_do_cbqi.end() ){ + return it->second>0; + }else{ + return false; + } +} + +Node InstStrategyCbqi::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 InstStrategyCbqi::preRegisterQuantifier( Node q ) { + if( d_quantEngine->getOwner( q )==NULL && doCbqi( q ) ){ + if( d_do_cbqi[q]==2 ){ + //take full ownership of the quantified formula + d_quantEngine->setOwner( q, this ); + + //mark all nested quantifiers with id + if( options::cbqiNestedQE() ){ + std::map< Node, Node > visited; + Node mq = getIdMarkedQuantNode( q[1], visited ); + if( mq!=q[1] ){ + //do not do cbqi + d_do_cbqi[q] = false; + //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("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl; + d_quantEngine->getOutputChannel().lemma( mlem ); + } + } + } + } +} + +void InstStrategyCbqi::registerQuantifier( Node q ) { + if( doCbqi( q ) ){ + if( registerCbqiLemma( q ) ){ + Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; + } + } +} + +Node InstStrategyCbqi::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("cbqi-nqe") << "CE quantifier elimination : " << std::endl; + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl; + //should not contain quantifiers + Assert( !QuantifiersRewriter::containsQuantifiers( 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_quantEngine->getTermUtil()->rewriteVtsSymbols( ret ); + } + Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; + Trace("cbqi-nqe") << " " << n << std::endl; + Trace("cbqi-nqe") << " " << ret << std::endl; + return ret; +} + +Node InstStrategyCbqi::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("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl; + Node nr = Rewriter::rewrite( n ); + Trace("cbqi-nqe") << " " << ceq << std::endl; + Trace("cbqi-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::cbqiInnermost() ); + } + } + } + }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 InstStrategyCbqi::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 InstStrategyCbqi::registerCounterexampleLemma( Node q, Node lem ){ + Trace("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->addLemma( lem, false ); +} + +bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()!=BOUND_VARIABLE && TermUtil::hasBoundVarAttr( n ) ){ + if( !inst::Trigger::isCbqiKind( n.getKind() ) ){ + Trace("cbqi-debug2") << "Non-cbqi kind : " << n.getKind() << " in " << n << std::endl; + return true; + }else if( n.getKind()==MULT && ( n.getNumChildren()!=2 || !n[0].isConst() ) ){ + Trace("cbqi-debug2") << "Non-linear arithmetic : " << n << std::endl; + return true; + }else if( n.getKind()==FORALL ){ + return hasNonCbqiOperator( n[1], visited ); + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( hasNonCbqiOperator( n[i], visited ) ){ + return true; + } + } + } + } + } + return false; +} + +// -1 : not cbqi sort, 0 : cbqi sort, 1 : cbqi sort regardless of quantifier body +int InstStrategyCbqi::isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited ) { + std::map< TypeNode, int >::iterator itv = visited.find( tn ); + if( itv==visited.end() ){ + visited[tn] = 0; + int ret = -1; + if( tn.isInteger() || tn.isReal() || tn.isBoolean() || tn.isBitVector() ){ + ret = 0; + }else if( tn.isDatatype() ){ + ret = 1; + const Datatype& dt = ((DatatypeType)tn.toType()).getDatatype(); + for( unsigned i=0; i<dt.getNumConstructors(); i++ ){ + for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){ + TypeNode crange = TypeNode::fromType( ((SelectorType)dt[i][j].getType()).getRangeType() ); + int cret = isCbqiSort( crange, visited ); + if( cret==-1 ){ + visited[tn] = -1; + return -1; + }else if( cret<ret ){ + ret = cret; + } + } + } + }else if( tn.isSort() ){ + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + ret = qepr->isEPR( tn ) ? 1 : -1; + } + } + visited[tn] = ret; + return ret; + }else{ + return itv->second; + } +} + +int InstStrategyCbqi::hasNonCbqiVariable( Node q ){ + int hmin = 1; + for( unsigned i=0; i<q[0].getNumChildren(); i++ ){ + TypeNode tn = q[0][i].getType(); + std::map< TypeNode, int > visited; + int handled = isCbqiSort( tn, visited ); + if( handled==-1 ){ + return -1; + }else if( handled<hmin ){ + hmin = handled; + } + } + return hmin; +} + +bool InstStrategyCbqi::doCbqi( Node q ){ + std::map< Node, int >::iterator it = d_do_cbqi.find( q ); + if( it==d_do_cbqi.end() ){ + int ret = 2; + if( !d_quantEngine->getQuantAttributes()->isQuantElim( q ) ){ + Assert( !d_quantEngine->getQuantAttributes()->isQuantElimPartial( q ) ); + //if has an instantiation pattern, don't do it + if( q.getNumChildren()==3 && options::eMatching() && options::userPatternsQuant()!=USER_PAT_MODE_IGNORE ){ + for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ + if( q[2][i].getKind()==INST_PATTERN ){ + ret = 0; + } + } + } + if( d_quantEngine->getQuantAttributes()->isSygus( q ) ){ + ret = 0; + } + if( ret!=0 ){ + //if quantifier has a non-handled variable, then do not use cbqi + //if quantifier has an APPLY_UF term, then do not use cbqi unless EPR + int ncbqiv = hasNonCbqiVariable( q ); + if( ncbqiv==0 || ncbqiv==1 ){ + std::map< Node, bool > visited; + if( hasNonCbqiOperator( q[1], visited ) ){ + if( ncbqiv==1 ){ + //all variables are fully handled, this implies this will be handlable regardless of body (e.g. for EPR) + // so, try but not exclusively + ret = 1; + }else{ + //cannot be handled + ret = 0; + } + } + }else{ + // unhandled variable type + ret = 0; + } + if( ret==0 && options::cbqiAll() ){ + //try but not exclusively + ret = 1; + } + } + } + Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; + d_do_cbqi[q] = ret; + return ret!=0; + }else{ + return it->second!=0; + } +} + +Node InstStrategyCbqi::getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ) { + if( proc.find( q )==proc.end() ){ + proc[q] = true; + //first check children + std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( q ); + if( itc!=d_children_quant.end() ){ + for( unsigned j=0; j<itc->second.size(); j++ ){ + Node d = getNextDecisionRequestProc( itc->second[j], proc ); + if( !d.isNull() ){ + return d; + } + } + } + //then check self + if( hasAddedCbqiLemma( q ) ){ + Node cel = d_quantEngine->getTermUtil()->getCounterexampleLiteral( q ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl; + return cel; + } + } + } + return Node::null(); +} + +Node InstStrategyCbqi::getNextDecisionRequest( unsigned& priority ){ + std::map< Node, bool > proc; + //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); + for( NodeSet::const_iterator it = d_added_cbqi_lemma.begin(); it != d_added_cbqi_lemma.end(); ++it ){ + Node q = *it; + Node d = getNextDecisionRequestProc( q, proc ); + if( !d.isNull() ){ + priority = 0; + return d; + } + } + return Node::null(); +} + + + +//new implementation + +bool CegqiOutputInstStrategy::doAddInstantiation( std::vector< Node >& subs ) { + return d_out->doAddInstantiation( subs ); +} + +bool CegqiOutputInstStrategy::isEligibleForInstantiation( Node n ) { + return d_out->isEligibleForInstantiation( n ); +} + +bool CegqiOutputInstStrategy::addLemma( Node lem ) { + return d_out->addLemma( lem ); +} + + +InstStrategyCegqi::InstStrategyCegqi( QuantifiersEngine * qe ) + : InstStrategyCbqi( qe ) { + d_out = new CegqiOutputInstStrategy( this ); + d_small_const = NodeManager::currentNM()->mkConst( Rational(1)/Rational(1000000) ); + d_check_vts_lemma_lc = false; +} + +InstStrategyCegqi::~InstStrategyCegqi() +{ + delete d_out; + + for(std::map< Node, CegInstantiator * >::iterator i = d_cinst.begin(), + iend = d_cinst.end(); i != iend; ++i) { + CegInstantiator * instantiator = (*i).second; + delete instantiator; + } + d_cinst.clear(); +} + +void InstStrategyCegqi::processResetInstantiationRound( Theory::Effort effort ) { + d_check_vts_lemma_lc = false; +} + +void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { + if( e==0 ){ + CegInstantiator * cinst = getInstantiator( q ); + Trace("inst-alg") << "-> Run cegqi for " << q << std::endl; + d_curr_quant = q; + if( !cinst->check() ){ + d_incomplete_check = true; + d_check_vts_lemma_lc = true; + } + d_curr_quant = Node::null(); + }else if( e==1 ){ + //minimize the free delta heuristically on demand + if( d_check_vts_lemma_lc ){ + Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl; + d_check_vts_lemma_lc = false; + d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); + d_small_const = Rewriter::rewrite( d_small_const ); + //heuristic for now, until we know how to do nested quantification + Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false ); + if( !delta.isNull() ){ + Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl; + Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const ); + d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); + } + std::vector< Node > inf; + d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false ); + for( unsigned i=0; i<inf.size(); i++ ){ + Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl; + Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) ); + d_quantEngine->getOutputChannel().lemma( inf_lem_lb ); + } + } + } +} + +bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { + Assert( !d_curr_quant.isNull() ); + //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma + if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){ + d_cbqi_set_quant_inactive = true; + d_incomplete_check = true; + d_quantEngine->getInstantiate()->recordInstantiation( + d_curr_quant, subs, false, false); + return true; + }else{ + //check if we need virtual term substitution (if used delta or infinity) + bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false ); + if (d_quantEngine->getInstantiate()->addInstantiation( + d_curr_quant, subs, false, false, used_vts)) + { + ++(d_quantEngine->d_statistics.d_instantiations_cbqi); + //d_added_inst.insert( d_curr_quant ); + return true; + }else{ + //this should never happen for monotonic selection strategies + Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl; + return false; + } + } +} + +bool InstStrategyCegqi::addLemma( Node lem ) { + return d_quantEngine->addLemma( lem ); +} + +bool InstStrategyCegqi::isEligibleForInstantiation( Node n ) { + if( n.getKind()==INST_CONSTANT || n.getKind()==SKOLEM ){ + if( n.getAttribute(VirtualTermSkolemAttribute()) ){ + // virtual terms are allowed + return true; + }else{ + TypeNode tn = n.getType(); + if( tn.isSort() ){ + QuantEPR * qepr = d_quantEngine->getQuantEPR(); + if( qepr!=NULL ){ + //legal if in the finite set of constants of type tn + if( qepr->isEPRConstant( tn, n ) ){ + return true; + } + } + } + //only legal if current quantified formula contains n + return TermUtil::containsTerm( d_curr_quant, n ); + } + }else{ + return true; + } +} + +CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { + std::map< Node, CegInstantiator * >::iterator it = d_cinst.find( q ); + if( it==d_cinst.end() ){ + CegInstantiator * cinst = new CegInstantiator( d_quantEngine, d_out, true, true ); + d_cinst[q] = cinst; + return cinst; + }else{ + return it->second; + } +} + +void InstStrategyCegqi::registerQuantifier( Node q ) { + if( doCbqi( q ) ){ + // get the instantiator + if( options::cbqiPreRegInst() ){ + getInstantiator( q ); + } + // register the cbqi lemma + if( registerCbqiLemma( q ) ){ + Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl; + } + } +} + +void InstStrategyCegqi::registerCounterexampleLemma( Node q, Node lem ) { + //must register with the instantiator + //must explicitly remove ITEs so that we record dependencies + std::vector< Node > ce_vars; + for( unsigned i=0; i<d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ); i++ ){ + ce_vars.push_back( d_quantEngine->getTermUtil()->getInstantiationConstant( q, i ) ); + } + std::vector< Node > lems; + lems.push_back( lem ); + CegInstantiator * cinst = getInstantiator( q ); + cinst->registerCounterexampleLemma( lems, ce_vars ); + for( unsigned i=0; i<lems.size(); i++ ){ + Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i] << std::endl; + d_quantEngine->addLemma( lems[i], false ); + } +} + +void InstStrategyCegqi::presolve() { + if( options::cbqiPreRegInst() ){ + for( std::map< Node, CegInstantiator * >::iterator it = d_cinst.begin(); it != d_cinst.end(); ++it ){ + Trace("cbqi-presolve") << "Presolve " << it->first << std::endl; + it->second->presolve( it->first ); + } + } +} + diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h new file mode 100644 index 000000000..3443d2c4d --- /dev/null +++ b/src/theory/quantifiers/cegqi/inst_strategy_cbqi.h @@ -0,0 +1,166 @@ +/********************* */ +/*! \file inst_strategy_cbqi.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief counterexample-guided quantifier instantiation + **/ + + +#include "cvc4_private.h" + +#ifndef __CVC4__INST_STRATEGY_CBQI_H +#define __CVC4__INST_STRATEGY_CBQI_H + +#include "theory/arith/arithvar.h" +#include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/ematching/instantiation_engine.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { + +namespace arith { + class TheoryArith; +} + +namespace quantifiers { + +class InstStrategyCbqi : public QuantifiersModule { + typedef context::CDHashSet<Node, NodeHashFunction> NodeSet; + typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; + + protected: + bool d_cbqi_set_quant_inactive; + 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; + std::map< Node, bool > d_active_quant; + /** whether we have instantiated quantified formulas */ + //NodeSet d_added_inst; + /** whether to do cbqi for this quantified formula 0 : no, 2 : yes, 1 : yes but not exclusively, -1 : heuristically */ + std::map< Node, int > d_do_cbqi; + /** register ce lemma */ + bool registerCbqiLemma( Node q ); + virtual 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(); } + /** helper functions */ + int hasNonCbqiVariable( Node q ); + bool hasNonCbqiOperator( Node n, std::map< Node, bool >& visited ); + int isCbqiSort( TypeNode tn, std::map< TypeNode, int >& visited ); + /** get next decision request with dependency checking */ + Node getNextDecisionRequestProc( Node q, std::map< Node, bool >& proc ); + /** process functions */ + virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; + virtual void process( Node q, Theory::Effort effort, int e ) = 0; + + protected: + //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; + + public: + //do nested quantifier elimination + Node doNestedQE( Node q, std::vector< Node >& inst_terms, Node lem, bool doVts ); + + public: + InstStrategyCbqi( QuantifiersEngine * qe ); + + /** whether to do CBQI for quantifier q */ + bool doCbqi( Node q ); + /** process functions */ + bool needsCheck( Theory::Effort e ); + QEffort needsModel(Theory::Effort e); + void reset_round( Theory::Effort e ); + void check(Theory::Effort e, QEffort quant_e); + bool checkComplete(); + bool checkCompleteFor( Node q ); + void preRegisterQuantifier( Node q ); + void registerQuantifier( Node q ); + /** get next decision request */ + Node getNextDecisionRequest( unsigned& priority ); +}; + +//generalized counterexample guided quantifier instantiation + +class InstStrategyCegqi; + +class CegqiOutputInstStrategy : public CegqiOutput { +public: + CegqiOutputInstStrategy( InstStrategyCegqi * out ) : d_out( out ){} + InstStrategyCegqi * d_out; + bool doAddInstantiation( std::vector< Node >& subs ); + bool isEligibleForInstantiation( Node n ); + bool addLemma( Node lem ); +}; + +class InstStrategyCegqi : public InstStrategyCbqi { + protected: + CegqiOutputInstStrategy * d_out; + std::map< Node, CegInstantiator * > d_cinst; + Node d_small_const; + Node d_curr_quant; + bool d_check_vts_lemma_lc; + /** process functions */ + void processResetInstantiationRound(Theory::Effort effort) override; + void process(Node f, Theory::Effort effort, int e) override; + /** register ce lemma */ + void registerCounterexampleLemma(Node q, Node lem) override; + + public: + InstStrategyCegqi( QuantifiersEngine * qe ); + ~InstStrategyCegqi() override; + + bool doAddInstantiation( std::vector< Node >& subs ); + bool isEligibleForInstantiation( Node n ); + bool addLemma( Node lem ); + /** identify */ + std::string identify() const override { return std::string("Cegqi"); } + + //get instantiator for quantifier + CegInstantiator * getInstantiator( Node q ); + //register quantifier + void registerQuantifier(Node q) override; + //presolve + void presolve() override; +}; + +} +} +} + +#endif |