diff options
Diffstat (limited to 'src/theory/quantifiers')
30 files changed, 2390 insertions, 610 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index c418d0fb1..0a6df7df5 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/ambqi_builder.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -165,7 +166,8 @@ bool AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, return true; }else{ if( depth==q[0].getNumChildren() ){ - if( qe->addInstantiation( q, terms, true ) ){ + if (qe->getInstantiate()->addInstantiation(q, terms, true)) + { Trace("ambqi-inst-debug") << "-> Added instantiation." << std::endl; inst++; return true; diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 712112615..699a93286 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -12,9 +12,10 @@ ** \brief Implementation of theory uf candidate generator class **/ -#include "options/quantifiers_options.h" #include "theory/quantifiers/candidate_generator.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -302,7 +303,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { if( d_firstTime ){ //must return something d_firstTime = false; - return d_qe->getTermForType(d_match_pattern_type); + return d_qe->getInstantiate()->getTermForType(d_match_pattern_type); } return Node::null(); } diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index bc6817560..378b26eef 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -21,6 +21,7 @@ #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database_sygus.h" @@ -108,7 +109,8 @@ void CegConjecture::assign( Node q ) { } Trace("cegqi") << "Base quantified formula is : " << d_embed_quant << std::endl; //construct base instantiation - d_base_inst = Rewriter::rewrite( d_qe->getInstantiation( d_embed_quant, vars, d_candidates ) ); + d_base_inst = Rewriter::rewrite(d_qe->getInstantiate()->getInstantiation( + d_embed_quant, vars, d_candidates)); Trace("cegqi") << "Base instantiation is : " << d_base_inst << std::endl; // register this term with sygus database and other utilities that impact @@ -224,7 +226,8 @@ void CegConjecture::doBasicCheck(std::vector< Node >& lems) { getCandidateList( clist, true ); Assert( clist.size()==d_quant[0].getNumChildren() ); getModelValues( clist, model_terms ); - if( d_qe->addInstantiation( d_quant, model_terms ) ){ + if (d_qe->getInstantiate()->addInstantiation(d_quant, model_terms)) + { //record the instantiation recordInstantiation( model_terms ); }else{ diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h index 8e63e8909..33fc7303f 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.h +++ b/src/theory/quantifiers/ce_guided_single_inv.h @@ -20,6 +20,7 @@ #include "context/cdchunk_list.h" #include "context/cdhashmap.h" #include "theory/quantifiers/ce_guided_single_inv_sol.h" +#include "theory/quantifiers/inst_match_trie.h" #include "theory/quantifiers/inst_strategy_cbqi.h" #include "theory/quantifiers/single_inv_partition.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index e79f3456b..86878b9ca 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -15,8 +15,9 @@ #include "theory/quantifiers/equality_query.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/equality_infer.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 4277ab366..15b96d2a0 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -12,9 +12,10 @@ ** \brief Implementation of full model check class **/ +#include "theory/quantifiers/full_model_check.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -694,7 +695,8 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i }else{ //just add the instance d_triedLemmas++; - if( d_qe->addInstantiation( f, inst, true ) ){ + if (d_qe->getInstantiate()->addInstantiation(f, inst, true)) + { Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; d_addedLemmas++; if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ @@ -845,7 +847,8 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No if (ev!=d_true) { Trace("fmc-exh-debug") << ", add!"; //add as instantiation - if( d_qe->addInstantiation( f, inst, true ) ){ + if (d_qe->getInstantiate()->addInstantiation(f, inst, true)) + { Trace("fmc-exh-debug") << " ...success."; addedLemmas++; if( d_qe->inConflict() || options::fmfOneInstPerRound() ){ diff --git a/src/theory/quantifiers/ho_trigger.cpp b/src/theory/quantifiers/ho_trigger.cpp index b0ac02a25..0386c0cf0 100644 --- a/src/theory/quantifiers/ho_trigger.cpp +++ b/src/theory/quantifiers/ho_trigger.cpp @@ -15,6 +15,7 @@ #include <stack> #include "theory/quantifiers/ho_trigger.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -325,7 +326,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) else { // do not run higher-order matching - return d_quantEngine->addInstantiation(d_f, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_f, m); } } @@ -336,7 +337,7 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m, unsigned var_index) if (var_index == d_ho_var_list.size()) { // we now have an instantiation to try - return d_quantEngine->addInstantiation(d_f, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_f, m); } else { diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index e24b8f96a..da16010cd 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -13,41 +13,42 @@ **/ #include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/term_database.h" + +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; - namespace CVC4 { namespace theory { namespace inst { -InstMatch::InstMatch( TNode f ) { - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - d_vals.push_back( Node::null() ); - } +InstMatch::InstMatch(TNode q) +{ + d_vals.resize(q[0].getNumChildren()); + Assert(!d_vals.empty()); + // resize must initialize with null nodes + Assert(d_vals[0].isNull()); } InstMatch::InstMatch( InstMatch* m ) { d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() ); } -bool InstMatch::add( InstMatch& m ){ - for( unsigned i=0; i<d_vals.size(); i++ ){ +void InstMatch::add(InstMatch& m) +{ + for (unsigned i = 0, size = d_vals.size(); i < size; i++) + { if( d_vals[i].isNull() ){ d_vals[i] = m.d_vals[i]; } } - return true; } bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){ - for( unsigned i=0; i<m.d_vals.size(); i++ ){ + Assert(d_vals.size() == m.d_vals.size()); + for (unsigned i = 0, size = d_vals.size(); i < size; i++) + { if( !m.d_vals[i].isNull() ){ if( d_vals[i].isNull() ){ d_vals[i] = m.d_vals[i]; @@ -63,7 +64,8 @@ bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){ } void InstMatch::debugPrint( const char* c ){ - for( unsigned i=0; i<d_vals.size(); i++ ){ + for (unsigned i = 0, size = d_vals.size(); i < size; i++) + { if( !d_vals[i].isNull() ){ Debug( c ) << " " << i << " -> " << d_vals[i] << std::endl; } @@ -71,8 +73,10 @@ void InstMatch::debugPrint( const char* c ){ } bool InstMatch::isComplete() { - for( unsigned i=0; i<d_vals.size(); i++ ){ - if( d_vals[i].isNull() ){ + for (Node& v : d_vals) + { + if (v.isNull()) + { return false; } } @@ -80,58 +84,37 @@ bool InstMatch::isComplete() { } bool InstMatch::empty() { - for( unsigned i=0; i<d_vals.size(); i++ ){ - if( !d_vals[i].isNull() ){ + for (Node& v : d_vals) + { + if (!v.isNull()) + { return false; } } return true; } -void InstMatch::makeRepresentative( QuantifiersEngine* qe ){ - for( unsigned i=0; i<d_vals.size(); i++ ){ - if( !d_vals[i].isNull() ){ - if( qe->getEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){ - d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] ); - } - } - } -} - -void InstMatch::applyRewrite(){ - for( unsigned i=0; i<d_vals.size(); i++ ){ - if( !d_vals[i].isNull() ){ - d_vals[i] = Rewriter::rewrite( d_vals[i] ); - } - } -} - void InstMatch::clear() { for( unsigned i=0; i<d_vals.size(); i++ ){ d_vals[i] = Node::null(); } } -/** get value */ - -Node InstMatch::get( int i ) { - return d_vals[i]; -} - -void InstMatch::getTerms( Node f, std::vector< Node >& inst ){ - for( size_t i=0; i<f[0].getNumChildren(); i++ ){ - inst.push_back( d_vals[i] ); - } +Node InstMatch::get(int i) const { return d_vals[i]; } +void InstMatch::getInst(std::vector<Node>& inst) const +{ + inst.insert(inst.end(), d_vals.begin(), d_vals.end()); } void InstMatch::setValue( int i, TNode n ) { d_vals[i] = n; } - -bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) { +bool InstMatch::set(EqualityQuery* q, int i, TNode n) +{ Assert( i>=0 ); if( !d_vals[i].isNull() ){ - if( qe->getEqualityQuery()->areEqual( d_vals[i], n ) ){ + if (q->areEqual(d_vals[i], n)) + { return true; }else{ return false; @@ -142,341 +125,6 @@ bool InstMatch::set( QuantifiersEngine* qe, int i, TNode n ) { } } -bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq, - ImtIndexOrder* imtio, bool onlyExist, int index ) { - if( index==(int)f[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){ - return false; - }else{ - int i_index = imtio ? imtio->d_order[index] : index; - Node n = m[i_index]; - std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); - if( it!=d_data.end() ){ - bool ret = it->second.addInstMatch( qe, f, m, modEq, imtio, onlyExist, index+1 ); - if( !onlyExist || !ret ){ - return ret; - } - } - if( modEq ){ - //check modulo equality if any other instantiation match exists - if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), - qe->getEqualityQuery()->getEngine() ); - while( !eqc.isFinished() ){ - Node en = (*eqc); - if( en!=n ){ - std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en ); - if( itc!=d_data.end() ){ - if( itc->second.addInstMatch( qe, f, m, modEq, imtio, true, index+1 ) ){ - return false; - } - } - } - ++eqc; - } - } - } - if( !onlyExist ){ - d_data[n].addInstMatch( qe, f, m, modEq, imtio, false, index+1 ); - } - return true; - } -} - -bool InstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, ImtIndexOrder* imtio, int index ) { - Assert( index<(int)q[0].getNumChildren() ); - Assert( !imtio || index<(int)imtio->d_order.size() ); - int i_index = imtio ? imtio->d_order[index] : index; - Node n = m[i_index]; - std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); - if( it!=d_data.end() ){ - if( (index+1)==(int)q[0].getNumChildren() || ( imtio && (index+1)==(int)imtio->d_order.size() ) ){ - d_data.erase( n ); - return true; - }else{ - return it->second.removeInstMatch( qe, q, m, imtio, index+1 ); - } - }else{ - return false; - } -} - -bool InstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio, int index ){ - if( index==(int)q[0].getNumChildren() || ( imtio && index==(int)imtio->d_order.size() ) ){ - setInstLemma( lem ); - return true; - }else{ - int i_index = imtio ? imtio->d_order[index] : index; - std::map< Node, InstMatchTrie >::iterator it = d_data.find( m[i_index] ); - if( it!=d_data.end() ){ - return it->second.recordInstLemma( q, m, lem, imtio, index+1 ); - }else{ - return false; - } - } -} - -void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const { - if( terms.size()==q[0].getNumChildren() ){ - bool print; - if( useActive ){ - if( hasInstLemma() ){ - Node lem = getInstLemma(); - print = std::find( active.begin(), active.end(), lem )!=active.end(); - }else{ - print = false; - } - }else{ - print = true; - } - if( print ){ - if( firstTime ){ - out << "(instantiation " << q << std::endl; - firstTime = false; - } - out << " ( "; - for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ){ out << ", ";} - out << terms[i]; - } - out << " )" << std::endl; - } - }else{ - for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ - terms.push_back( it->first ); - it->second.print( out, q, terms, firstTime, useActive, active ); - terms.pop_back(); - } - } -} - -void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const { - if( terms.size()==q[0].getNumChildren() ){ - if( useActive ){ - if( hasInstLemma() ){ - Node lem = getInstLemma(); - if( std::find( active.begin(), active.end(), lem )!=active.end() ){ - insts.push_back( lem ); - } - } - }else{ - if( hasInstLemma() ){ - insts.push_back( getInstLemma() ); - }else{ - insts.push_back( qe->getInstantiation( q, terms, true ) ); - } - } - }else{ - for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ - terms.push_back( it->first ); - it->second.getInstantiations( insts, q, terms, qe, useActive, active ); - terms.pop_back(); - } - } -} - -void InstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { - if( terms.size()==q[0].getNumChildren() ){ - if( hasInstLemma() ){ - Node lem = getInstLemma(); - if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){ - quant[lem] = q; - tvec[lem].clear(); - tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() ); - } - } - }else{ - for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ - terms.push_back( it->first ); - it->second.getExplanationForInstLemmas( q, terms, lems, quant, tvec ); - terms.pop_back(); - } - } -} - -CDInstMatchTrie::~CDInstMatchTrie() { - for(std::map< Node, CDInstMatchTrie* >::iterator i = d_data.begin(), - iend = d_data.end(); i != iend; ++i) { - CDInstMatchTrie* current = (*i).second; - delete current; - } - d_data.clear(); -} - - -bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, - context::Context* c, bool modEq, int index, bool onlyExist ){ - bool reset = false; - if( !d_valid.get() ){ - if( onlyExist ){ - return true; - }else{ - d_valid.set( true ); - reset = true; - } - } - if( index==(int)f[0].getNumChildren() ){ - return reset; - }else{ - Node n = m[ index ]; - std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); - if( it!=d_data.end() ){ - bool ret = it->second->addInstMatch( qe, f, m, c, modEq, index+1, onlyExist ); - if( !onlyExist || !ret ){ - return reset || ret; - } - } - if( modEq ){ - //check modulo equality if any other instantiation match exists - if( !n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){ - eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ), - qe->getEqualityQuery()->getEngine() ); - while( !eqc.isFinished() ){ - Node en = (*eqc); - if( en!=n ){ - std::map< Node, CDInstMatchTrie* >::iterator itc = d_data.find( en ); - if( itc!=d_data.end() ){ - if( itc->second->addInstMatch( qe, f, m, c, modEq, index+1, true ) ){ - return false; - } - } - } - ++eqc; - } - } - } - - if( !onlyExist ){ - // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); - CDInstMatchTrie* imt = new CDInstMatchTrie( c ); - Assert(d_data.find(n) == d_data.end()); - d_data[n] = imt; - imt->addInstMatch( qe, f, m, c, modEq, index+1, false ); - } - return true; - } -} - -bool CDInstMatchTrie::removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index ) { - if( index==(int)q[0].getNumChildren() ){ - if( d_valid.get() ){ - d_valid.set( false ); - return true; - }else{ - return false; - } - }else{ - std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] ); - if( it!=d_data.end() ){ - return it->second->removeInstMatch( qe, q, m, index+1 ); - }else{ - return false; - } - } -} - -bool CDInstMatchTrie::recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index ) { - if( index==(int)q[0].getNumChildren() ){ - if( d_valid.get() ){ - setInstLemma( lem ); - return true; - }else{ - return false; - } - }else{ - std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( m[index] ); - if( it!=d_data.end() ){ - return it->second->recordInstLemma( q, m, lem, index+1 ); - }else{ - return false; - } - } -} - -void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const{ - if( d_valid.get() ){ - if( terms.size()==q[0].getNumChildren() ){ - bool print; - if( useActive ){ - if( hasInstLemma() ){ - Node lem = getInstLemma(); - print = std::find( active.begin(), active.end(), lem )!=active.end(); - }else{ - print = false; - } - }else{ - print = true; - } - if( print ){ - if( firstTime ){ - out << "(instantiation " << q << std::endl; - firstTime = false; - } - out << " ( "; - for( unsigned i=0; i<terms.size(); i++ ){ - if( i>0 ) out << " "; - out << terms[i]; - } - out << " )" << std::endl; - } - }else{ - for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ - terms.push_back( it->first ); - it->second->print( out, q, terms, firstTime, useActive, active ); - terms.pop_back(); - } - } - } -} - -void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const{ - if( d_valid.get() ){ - if( terms.size()==q[0].getNumChildren() ){ - if( useActive ){ - if( hasInstLemma() ){ - Node lem = getInstLemma(); - if( std::find( active.begin(), active.end(), lem )!=active.end() ){ - insts.push_back( lem ); - } - } - }else{ - if( hasInstLemma() ){ - insts.push_back( getInstLemma() ); - }else{ - insts.push_back( qe->getInstantiation( q, terms, true ) ); - } - } - }else{ - for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ - terms.push_back( it->first ); - it->second->getInstantiations( insts, q, terms, qe, useActive, active ); - terms.pop_back(); - } - } - } -} - - -void CDInstMatchTrie::getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { - if( d_valid.get() ){ - if( terms.size()==q[0].getNumChildren() ){ - if( hasInstLemma() ){ - Node lem; - if( std::find( lems.begin(), lems.end(), lem )!=lems.end() ){ - quant[lem] = q; - tvec[lem].clear(); - tvec[lem].insert( tvec[lem].end(), terms.begin(), terms.end() ); - } - } - }else{ - for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ - terms.push_back( it->first ); - it->second->getExplanationForInstLemmas( q, terms, lems, quant, tvec ); - terms.pop_back(); - } - } - } -} - }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 8597755c9..ce438861c 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -17,45 +17,54 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H -#include <map> +#include <vector> -#include "context/cdlist.h" -#include "context/cdo.h" #include "expr/node.h" namespace CVC4 { namespace theory { -class QuantifiersEngine; class EqualityQuery; namespace inst { -/** basic class defining an instantiation */ +/** Inst match + * + * This is the basic class specifying an instantiation. Its domain size (the + * size of d_vals) is the number of bound variables of the quantified formula + * that is passed to its constructor. + * + * The values of d_vals may be null, which indicate that the field has + * yet to be initialized. + */ class InstMatch { public: - /* map from variable to ground terms */ - std::vector< Node > d_vals; -public: InstMatch(){} - explicit InstMatch( TNode f ); + explicit InstMatch(TNode q); InstMatch( InstMatch* m ); - - /** fill all unfilled values with m */ - bool add( InstMatch& m ); - /** if compatible, fill all unfilled values with m and return true - return false otherwise */ + /* map from variable to ground terms */ + std::vector<Node> d_vals; + /** add match m + * + * This adds the initialized fields of m to this match for each field that is + * not already initialized in this match. + */ + void add(InstMatch& m); + /** merge with match m + * + * This method returns true if the merge was successful, that is, all jointly + * initialized fields of this class and m are equivalent modulo the equalities + * given by q. + */ bool merge( EqualityQuery* q, InstMatch& m ); - /** debug print method */ - void debugPrint( const char* c ); - /** is complete? */ + /** is this complete, i.e. are all fields non-null? */ bool isComplete(); - /** make representative */ - void makeRepresentative( QuantifiersEngine* qe ); - /** empty */ + /** is this empty, i.e. are all fields the null node? */ bool empty(); - /** clear */ + /** clear the instantiation, i.e. set all fields to the null node */ void clear(); + /** debug print method */ + void debugPrint(const char* c); /** to stream */ inline void toStream(std::ostream& out) const { out << "INST_MATCH( "; @@ -69,166 +78,25 @@ public: } out << " )"; } - /** apply rewrite */ - void applyRewrite(); - /** get */ - Node get( int i ); - void getTerms( Node f, std::vector< Node >& inst ); - /** set */ + /** get the i^th term in the instantiation */ + Node get(int i) const; + /** append the terms of this instantiation to inst */ + void getInst(std::vector<Node>& inst) const; + /** set/overwrites the i^th field in the instantiation with n */ void setValue( int i, TNode n ); - bool set( QuantifiersEngine* qe, int i, TNode n ); -};/* class InstMatch */ + /** set the i^th term in the instantiation to n + * + * This method returns true if the i^th field was previously uninitialized, + * or is equivalent to n modulo the equalities given by q. + */ + bool set(EqualityQuery* q, int i, TNode n); +}; inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) { m.toStream(out); return out; } -/** trie for InstMatch objects */ -class InstMatchTrie { -public: - class ImtIndexOrder { - public: - std::vector< int > d_order; - };/* class InstMatchTrie ImtIndexOrder */ - /** the data */ - std::map< Node, InstMatchTrie > d_data; -private: - void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const; - void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const; - void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const; -private: - void setInstLemma( Node n ){ - d_data.clear(); - d_data[n].clear(); - } - bool hasInstLemma() const { return !d_data.empty(); } - Node getInstLemma() const { return d_data.begin()->first; } -public: - InstMatchTrie(){} - ~InstMatchTrie(){} -public: - /** return true if m exists in this trie - modEq is if we check modulo equality - modInst is if we return true if m is an instance of a match that exists - */ - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, int index = 0 ) { - return !addInstMatch( qe, f, m, modEq, imtio, true, index ); - } - bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, int index = 0 ) { - return !addInstMatch( qe, f, m, modEq, imtio, true, index ); - } - /** add match m for quantifier f, take into account equalities if modEq = true, - if imtio is non-null, this is the order to add to trie - return true if successful - */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ){ - return addInstMatch( qe, f, m.d_vals, modEq, imtio, onlyExist, index ); - } - bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); - bool removeInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, ImtIndexOrder* imtio = NULL, int index = 0 ); - bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, ImtIndexOrder* imtio = NULL, int index = 0 ); - void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{ - std::vector< TNode > terms; - print( out, q, terms, firstTime, useActive, active ); - } - void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) { - std::vector< Node > terms; - getInstantiations( insts, q, terms, qe, useActive, active ); - } - void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { - std::vector< Node > terms; - getExplanationForInstLemmas( q, terms, lems, quant, tvec ); - } - void clear() { d_data.clear(); } -};/* class InstMatchTrie */ - -/** trie for InstMatch objects */ -class CDInstMatchTrie { -private: - /** the data */ - std::map< Node, CDInstMatchTrie* > d_data; - /** is valid */ - context::CDO< bool > d_valid; -private: - void print( std::ostream& out, Node q, std::vector< TNode >& terms, bool& firstTime, bool useActive, std::vector< Node >& active ) const; - void getInstantiations( std::vector< Node >& insts, Node q, std::vector< Node >& terms, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) const; - void getExplanationForInstLemmas( Node q, std::vector< Node >& terms, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const; -private: - void setInstLemma( Node n ){ - d_data.clear(); - d_data[n] = NULL; - } - bool hasInstLemma() const { return !d_data.empty(); } - Node getInstLemma() const { return d_data.begin()->first; } -public: - CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} - ~CDInstMatchTrie(); - - /** return true if m exists in this trie - modEq is if we check modulo equality - modInst is if we return true if m is an instance of a match that exists - */ - bool existsInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, - int index = 0 ) { - return !addInstMatch( qe, q, m, c, modEq, index, true ); - } - bool existsInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, - int index = 0 ) { - return !addInstMatch( qe, q, m, c, modEq, index, true ); - } - /** add match m for quantifier f, take into account equalities if modEq = true, - if imtio is non-null, this is the order to add to trie - return true if successful - */ - bool addInstMatch( QuantifiersEngine* qe, Node q, InstMatch& m, context::Context* c, bool modEq = false, - int index = 0, bool onlyExist = false ) { - return addInstMatch( qe, q, m.d_vals, c, modEq, index, onlyExist ); - } - bool addInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, context::Context* c, bool modEq = false, - int index = 0, bool onlyExist = false ); - bool removeInstMatch( QuantifiersEngine* qe, Node q, std::vector< Node >& m, int index = 0 ); - bool recordInstLemma( Node q, std::vector< Node >& m, Node lem, int index = 0 ); - void print( std::ostream& out, Node q, bool& firstTime, bool useActive, std::vector< Node >& active ) const{ - std::vector< TNode > terms; - print( out, q, terms, firstTime, useActive, active ); - } - void getInstantiations( std::vector< Node >& insts, Node q, QuantifiersEngine * qe, bool useActive, std::vector< Node >& active ) { - std::vector< Node > terms; - getInstantiations( insts, q, terms, qe, useActive, active ); - } - void getExplanationForInstLemmas( Node q, std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) const { - std::vector< Node > terms; - getExplanationForInstLemmas( q, terms, lems, quant, tvec ); - } -};/* class CDInstMatchTrie */ - - -class InstMatchTrieOrdered{ -private: - InstMatchTrie::ImtIndexOrder* d_imtio; - InstMatchTrie d_imt; -public: - InstMatchTrieOrdered( InstMatchTrie::ImtIndexOrder* imtio ) : d_imtio( imtio ){} - ~InstMatchTrieOrdered(){} - /** get ordering */ - InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; } - /** get trie */ - InstMatchTrie* getTrie() { return &d_imt; } -public: - /** add match m, return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ - return d_imt.addInstMatch( qe, f, m, modEq, d_imtio ); - } - bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ - return d_imt.existsInstMatch( qe, f, m, modEq, d_imtio ); - } -};/* class InstMatchTrieOrdered */ - }/* CVC4::theory::inst namespace */ typedef CVC4::theory::inst::InstMatch InstMatch; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index a8942326c..5cdb2a64b 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -15,9 +15,10 @@ #include "theory/quantifiers/inst_match_generator.h" #include "expr/datatype.h" -#include "options/quantifiers_options.h" #include "options/datatypes_options.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" @@ -238,7 +239,8 @@ int InstMatchGenerator::getMatch( if( d_children_types[i]==0 ){ Trace("matching-debug2") << "Setting " << d_var_num[i] << " to " << t[i] << "..." << std::endl; bool addToPrev = m.get( d_var_num[i] ).isNull(); - if( !m.set( qe, d_var_num[i], t[i] ) ){ + if (!m.set(q, d_var_num[i], t[i])) + { //match is in conflict Trace("matching-fail") << "Match fail: " << m.get(d_var_num[i]) << " and " << t[i] << std::endl; success = false; @@ -260,7 +262,8 @@ int InstMatchGenerator::getMatch( //for variable matching if( d_match_pattern.getKind()==INST_CONSTANT ){ bool addToPrev = m.get( d_var_num[0] ).isNull(); - if( !m.set( qe, d_var_num[0], t ) ){ + if (!m.set(q, d_var_num[0], t)) + { success = false; }else{ if( addToPrev ){ @@ -296,7 +299,8 @@ int InstMatchGenerator::getMatch( } if( !t_match.isNull() ){ bool addToPrev = m.get( v ).isNull(); - if( !m.set( qe, v, t_match ) ){ + if (!m.set(q, v, t_match)) + { success = false; }else if( addToPrev ){ prev.push_back( v ); @@ -572,7 +576,8 @@ int VarMatchGeneratorBooleanTerm::getNextMatch(Node q, Node s = NodeManager::currentNM()->mkConst(qe->getEqualityQuery()->areEqual( d_eq_class, d_pattern )); d_eq_class = Node::null(); d_rm_prev = m.get( d_var_num[0] ).isNull(); - if( !m.set( qe, d_var_num[0], s ) ){ + if (!m.set(qe->getEqualityQuery(), d_var_num[0], s)) + { return -1; }else{ ret_val = continueNextMatch(q, m, qe, tparent); @@ -608,7 +613,8 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, d_eq_class = Node::null(); //if( s.getType().isSubtypeOf( d_var_type ) ){ d_rm_prev = m.get( d_var_num[0] ).isNull(); - if( !m.set( qe, d_var_num[0], s ) ){ + if (!m.set(qe->getEqualityQuery(), d_var_num[0], s)) + { return -1; }else{ ret_val = continueNextMatch(q, m, qe, tparent); @@ -1087,7 +1093,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, } // we do not need the trigger parent for simple triggers (no post-processing // required) - if (qe->addInstantiation(d_quant, m)) + if (qe->getInstantiate()->addInstantiation(d_quant, m)) { addedLemmas++; Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl; diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index a74035076..e36ee2b58 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -17,8 +17,8 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H -#include "theory/quantifiers/inst_match.h" #include <map> +#include "theory/quantifiers/inst_match_trie.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp new file mode 100644 index 000000000..12844eacb --- /dev/null +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -0,0 +1,527 @@ +/********************* */ +/*! \file inst_match.cpp + ** \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 Implementation of inst match class + **/ + +#include "theory/quantifiers/inst_match_trie.h" + +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" + +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace inst { + +bool InstMatchTrie::addInstMatch(QuantifiersEngine* qe, + Node f, + std::vector<Node>& m, + bool modEq, + ImtIndexOrder* imtio, + bool onlyExist, + unsigned index) +{ + if (index == f[0].getNumChildren() + || (imtio && index == imtio->d_order.size())) + { + return false; + } + unsigned i_index = imtio ? imtio->d_order[index] : index; + Node n = m[i_index]; + std::map<Node, InstMatchTrie>::iterator it = d_data.find(n); + if (it != d_data.end()) + { + bool ret = + it->second.addInstMatch(qe, f, m, modEq, imtio, onlyExist, index + 1); + if (!onlyExist || !ret) + { + return ret; + } + } + if (modEq) + { + // check modulo equality if any other instantiation match exists + if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n)) + { + eq::EqClassIterator eqc( + qe->getEqualityQuery()->getEngine()->getRepresentative(n), + qe->getEqualityQuery()->getEngine()); + while (!eqc.isFinished()) + { + Node en = (*eqc); + if (en != n) + { + std::map<Node, InstMatchTrie>::iterator itc = d_data.find(en); + if (itc != d_data.end()) + { + if (itc->second.addInstMatch( + qe, f, m, modEq, imtio, true, index + 1)) + { + return false; + } + } + } + ++eqc; + } + } + } + if (!onlyExist) + { + d_data[n].addInstMatch(qe, f, m, modEq, imtio, false, index + 1); + } + return true; +} + +bool InstMatchTrie::removeInstMatch(Node q, + std::vector<Node>& m, + ImtIndexOrder* imtio, + unsigned index) +{ + Assert(index < q[0].getNumChildren()); + Assert(!imtio || index < imtio->d_order.size()); + unsigned i_index = imtio ? imtio->d_order[index] : index; + Node n = m[i_index]; + std::map<Node, InstMatchTrie>::iterator it = d_data.find(n); + if (it != d_data.end()) + { + if ((index + 1) == q[0].getNumChildren() + || (imtio && (index + 1) == imtio->d_order.size())) + { + d_data.erase(n); + return true; + } + return it->second.removeInstMatch(q, m, imtio, index + 1); + } + return false; +} + +bool InstMatchTrie::recordInstLemma(Node q, + std::vector<Node>& m, + Node lem, + ImtIndexOrder* imtio, + unsigned index) +{ + if (index == q[0].getNumChildren() + || (imtio && index == imtio->d_order.size())) + { + setInstLemma(lem); + return true; + } + unsigned i_index = imtio ? imtio->d_order[index] : index; + std::map<Node, InstMatchTrie>::iterator it = d_data.find(m[i_index]); + if (it != d_data.end()) + { + return it->second.recordInstLemma(q, m, lem, imtio, index + 1); + } + return false; +} + +void InstMatchTrie::print(std::ostream& out, + Node q, + std::vector<TNode>& terms, + bool& firstTime, + bool useActive, + std::vector<Node>& active) const +{ + if (terms.size() == q[0].getNumChildren()) + { + bool print; + if (useActive) + { + if (hasInstLemma()) + { + Node lem = getInstLemma(); + print = std::find(active.begin(), active.end(), lem) != active.end(); + } + else + { + print = false; + } + } + else + { + print = true; + } + if (print) + { + if (firstTime) + { + out << "(instantiation " << q << std::endl; + firstTime = false; + } + out << " ( "; + for (unsigned i = 0, size = terms.size(); i < size; i++) + { + if (i > 0) + { + out << ", "; + } + out << terms[i]; + } + out << " )" << std::endl; + } + } + else + { + for (const std::pair<const Node, InstMatchTrie>& d : d_data) + { + terms.push_back(d.first); + d.second.print(out, q, terms, firstTime, useActive, active); + terms.pop_back(); + } + } +} + +void InstMatchTrie::getInstantiations(std::vector<Node>& insts, + Node q, + std::vector<Node>& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector<Node>& active) const +{ + if (terms.size() == q[0].getNumChildren()) + { + if (useActive) + { + if (hasInstLemma()) + { + Node lem = getInstLemma(); + if (std::find(active.begin(), active.end(), lem) != active.end()) + { + insts.push_back(lem); + } + } + } + else + { + if (hasInstLemma()) + { + insts.push_back(getInstLemma()); + } + else + { + insts.push_back(qe->getInstantiate()->getInstantiation(q, terms, true)); + } + } + } + else + { + for (const std::pair<const Node, InstMatchTrie>& d : d_data) + { + terms.push_back(d.first); + d.second.getInstantiations(insts, q, terms, qe, useActive, active); + terms.pop_back(); + } + } +} + +void InstMatchTrie::getExplanationForInstLemmas( + Node q, + std::vector<Node>& terms, + const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec) const +{ + if (terms.size() == q[0].getNumChildren()) + { + if (hasInstLemma()) + { + Node lem = getInstLemma(); + if (std::find(lems.begin(), lems.end(), lem) != lems.end()) + { + quant[lem] = q; + tvec[lem].clear(); + tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end()); + } + } + } + else + { + for (const std::pair<const Node, InstMatchTrie>& d : d_data) + { + terms.push_back(d.first); + d.second.getExplanationForInstLemmas(q, terms, lems, quant, tvec); + terms.pop_back(); + } + } +} + +CDInstMatchTrie::~CDInstMatchTrie() +{ + for (std::pair<const Node, CDInstMatchTrie*>& d : d_data) + { + CDInstMatchTrie* current = d.second; + delete current; + } + d_data.clear(); +} + +bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, + Node f, + std::vector<Node>& m, + context::Context* c, + bool modEq, + unsigned index, + bool onlyExist) +{ + bool reset = false; + if (!d_valid.get()) + { + if (onlyExist) + { + return true; + } + else + { + d_valid.set(true); + reset = true; + } + } + if (index == f[0].getNumChildren()) + { + return reset; + } + Node n = m[index]; + std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(n); + if (it != d_data.end()) + { + bool ret = + it->second->addInstMatch(qe, f, m, c, modEq, index + 1, onlyExist); + if (!onlyExist || !ret) + { + return reset || ret; + } + } + if (modEq) + { + // check modulo equality if any other instantiation match exists + if (!n.isNull() && qe->getEqualityQuery()->getEngine()->hasTerm(n)) + { + eq::EqClassIterator eqc( + qe->getEqualityQuery()->getEngine()->getRepresentative(n), + qe->getEqualityQuery()->getEngine()); + while (!eqc.isFinished()) + { + Node en = (*eqc); + if (en != n) + { + std::map<Node, CDInstMatchTrie*>::iterator itc = d_data.find(en); + if (itc != d_data.end()) + { + if (itc->second->addInstMatch(qe, f, m, c, modEq, index + 1, true)) + { + return false; + } + } + } + ++eqc; + } + } + } + + if (!onlyExist) + { + // std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + CDInstMatchTrie* imt = new CDInstMatchTrie(c); + Assert(d_data.find(n) == d_data.end()); + d_data[n] = imt; + imt->addInstMatch(qe, f, m, c, modEq, index + 1, false); + } + return true; +} + +bool CDInstMatchTrie::removeInstMatch(Node q, + std::vector<Node>& m, + unsigned index) +{ + if (index == q[0].getNumChildren()) + { + if (d_valid.get()) + { + d_valid.set(false); + return true; + } + return false; + } + std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]); + if (it != d_data.end()) + { + return it->second->removeInstMatch(q, m, index + 1); + } + return false; +} + +bool CDInstMatchTrie::recordInstLemma(Node q, + std::vector<Node>& m, + Node lem, + unsigned index) +{ + if (index == q[0].getNumChildren()) + { + if (d_valid.get()) + { + setInstLemma(lem); + return true; + } + return false; + } + std::map<Node, CDInstMatchTrie*>::iterator it = d_data.find(m[index]); + if (it != d_data.end()) + { + return it->second->recordInstLemma(q, m, lem, index + 1); + } + return false; +} + +void CDInstMatchTrie::print(std::ostream& out, + Node q, + std::vector<TNode>& terms, + bool& firstTime, + bool useActive, + std::vector<Node>& active) const +{ + if (d_valid.get()) + { + if (terms.size() == q[0].getNumChildren()) + { + bool print; + if (useActive) + { + if (hasInstLemma()) + { + Node lem = getInstLemma(); + print = std::find(active.begin(), active.end(), lem) != active.end(); + } + else + { + print = false; + } + } + else + { + print = true; + } + if (print) + { + if (firstTime) + { + out << "(instantiation " << q << std::endl; + firstTime = false; + } + out << " ( "; + for (unsigned i = 0; i < terms.size(); i++) + { + if (i > 0) out << " "; + out << terms[i]; + } + out << " )" << std::endl; + } + } + else + { + for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data) + { + terms.push_back(d.first); + d.second->print(out, q, terms, firstTime, useActive, active); + terms.pop_back(); + } + } + } +} + +void CDInstMatchTrie::getInstantiations(std::vector<Node>& insts, + Node q, + std::vector<Node>& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector<Node>& active) const +{ + if (d_valid.get()) + { + if (terms.size() == q[0].getNumChildren()) + { + if (useActive) + { + if (hasInstLemma()) + { + Node lem = getInstLemma(); + if (std::find(active.begin(), active.end(), lem) != active.end()) + { + insts.push_back(lem); + } + } + } + else + { + if (hasInstLemma()) + { + insts.push_back(getInstLemma()); + } + else + { + insts.push_back( + qe->getInstantiate()->getInstantiation(q, terms, true)); + } + } + } + else + { + for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data) + { + terms.push_back(d.first); + d.second->getInstantiations(insts, q, terms, qe, useActive, active); + terms.pop_back(); + } + } + } +} + +void CDInstMatchTrie::getExplanationForInstLemmas( + Node q, + std::vector<Node>& terms, + const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec) const +{ + if (d_valid.get()) + { + if (terms.size() == q[0].getNumChildren()) + { + if (hasInstLemma()) + { + Node lem; + if (std::find(lems.begin(), lems.end(), lem) != lems.end()) + { + quant[lem] = q; + tvec[lem].clear(); + tvec[lem].insert(tvec[lem].end(), terms.begin(), terms.end()); + } + } + } + else + { + for (const std::pair<const Node, CDInstMatchTrie*>& d : d_data) + { + terms.push_back(d.first); + d.second->getExplanationForInstLemmas(q, terms, lems, quant, tvec); + terms.pop_back(); + } + } + } +} + +} /* CVC4::theory::inst namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h new file mode 100644 index 000000000..e33bf5997 --- /dev/null +++ b/src/theory/quantifiers/inst_match_trie.h @@ -0,0 +1,439 @@ +/********************* */ +/*! \file inst_match.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Francois Bobot + ** 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 inst match class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H +#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H + +#include <map> + +#include "context/cdlist.h" +#include "context/cdo.h" +#include "expr/node.h" +#include "theory/quantifiers/inst_match.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; +class EqualityQuery; + +namespace inst { + +/** trie for InstMatch objects + * + * This class is used for storing instantiations of a quantified formula q. + * It is a trie data structure for which entries can be added and removed. + * This class has interfaces for adding instantiations that are either + * represented by std::vectors or InstMatch objects (see inst_match.h). + */ +class InstMatchTrie +{ + public: + /** index ordering */ + class ImtIndexOrder + { + public: + std::vector<unsigned> d_order; + }; + + public: + InstMatchTrie() {} + ~InstMatchTrie() {} + /** exists inst match + * + * This method considers the entry given by m, starting at the given index. + * The domain of m is the bound variables of quantified formula q. + * It returns true if (the suffix) of m exists in this trie. + * If modEq is true, we check for duplication modulo equality the current + * equalities in the active equality engine of qe. + */ + bool existsInstMatch(QuantifiersEngine* qe, + Node q, + InstMatch& m, + bool modEq = false, + ImtIndexOrder* imtio = NULL, + unsigned index = 0) + { + return !addInstMatch(qe, q, m, modEq, imtio, true, index); + } + /** exists inst match, vector version */ + bool existsInstMatch(QuantifiersEngine* qe, + Node q, + std::vector<Node>& m, + bool modEq = false, + ImtIndexOrder* imtio = NULL, + unsigned index = 0) + { + return !addInstMatch(qe, q, m, modEq, imtio, true, index); + } + /** add inst match + * + * This method adds (the suffix of) m starting at the given index to this + * trie, and returns true if and only if m did not already occur in this trie. + * The domain of m is the bound variables of quantified formula q. + * If modEq is true, we check for duplication modulo equality the current + * equalities in the active equality engine of qe. + */ + bool addInstMatch(QuantifiersEngine* qe, + Node q, + InstMatch& m, + bool modEq = false, + ImtIndexOrder* imtio = NULL, + bool onlyExist = false, + unsigned index = 0) + { + return addInstMatch(qe, q, m.d_vals, modEq, imtio, onlyExist, index); + } + /** add inst match, vector version */ + bool addInstMatch(QuantifiersEngine* qe, + Node f, + std::vector<Node>& m, + bool modEq = false, + ImtIndexOrder* imtio = NULL, + bool onlyExist = false, + unsigned index = 0); + /** remove inst match + * + * This removes (the suffix of) m starting at the given index from this trie. + * It returns true if and only if this entry existed in this trie. + * The domain of m is the bound variables of quantified formula q. + */ + bool removeInstMatch(Node f, + std::vector<Node>& m, + ImtIndexOrder* imtio = NULL, + unsigned index = 0); + /** record instantiation lemma + * + * This records that the instantiation lemma lem corresponds to the entry + * given by (the suffix of) m starting at the given index. + */ + bool recordInstLemma(Node q, + std::vector<Node>& m, + Node lem, + ImtIndexOrder* imtio = NULL, + unsigned index = 0); + + /** get instantiations + * + * This gets the set of instantiation lemmas that were recorded in this trie + * via calls to recordInstLemma. If useActive is true, we only add + * instantiations that occur in active. + */ + void getInstantiations(std::vector<Node>& insts, + Node q, + QuantifiersEngine* qe, + bool useActive, + std::vector<Node>& active) + { + std::vector<Node> terms; + getInstantiations(insts, q, terms, qe, useActive, active); + } + /** get explanation for inst lemmas + * + * This gets the explanation for the instantiation lemmas in lems for + * quantified formula q, for which this trie stores instantiation matches for. + * For each instantiation lemma lem recording in this trie via calls to + * recordInstLemma, we map lem to q in map quant, and lem to its corresponding + * vector of terms in tvec. + */ + void getExplanationForInstLemmas( + Node q, + const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec) const + { + std::vector<Node> terms; + getExplanationForInstLemmas(q, terms, lems, quant, tvec); + } + + /** clear the data of this class */ + void clear() { d_data.clear(); } + /** print this class */ + void print(std::ostream& out, + Node q, + bool& firstTime, + bool useActive, + std::vector<Node>& active) const + { + std::vector<TNode> terms; + print(out, q, terms, firstTime, useActive, active); + } + /** the data */ + std::map<Node, InstMatchTrie> d_data; + + private: + /** helper for print + * terms accumulates the path we are on in the trie. + */ + void print(std::ostream& out, + Node q, + std::vector<TNode>& terms, + bool& firstTime, + bool useActive, + std::vector<Node>& active) const; + /** helper for get instantiations + * terms accumulates the path we are on in the trie. + */ + void getInstantiations(std::vector<Node>& insts, + Node q, + std::vector<Node>& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector<Node>& active) const; + /** helper for get explantaion for inst lemmas + * terms accumulates the path we are on in the trie. + */ + void getExplanationForInstLemmas( + Node q, + std::vector<Node>& terms, + const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec) const; + /** set instantiation lemma at this node in the trie */ + void setInstLemma(Node n) + { + d_data.clear(); + d_data[n].clear(); + } + /** does this node of the trie store an instantiation lemma? */ + bool hasInstLemma() const { return !d_data.empty(); } + /** get the instantiation lemma stored in this node of the trie */ + Node getInstLemma() const { return d_data.begin()->first; } +}; + +/** trie for InstMatch objects + * + * This is a context-dependent version of the above class. + */ +class CDInstMatchTrie +{ + public: + CDInstMatchTrie(context::Context* c) : d_valid(c, false) {} + ~CDInstMatchTrie(); + + /** exists inst match + * + * This method considers the entry given by m, starting at the given index. + * The domain of m is the bound variables of quantified formula q. + * It returns true if (the suffix) of m exists in this trie. + * If modEq is true, we check for duplication modulo equality the current + * equalities in the active equality engine of qe. + * It additionally takes a context c, for which the entry is valid in. + */ + bool existsInstMatch(QuantifiersEngine* qe, + Node q, + InstMatch& m, + context::Context* c, + bool modEq = false, + unsigned index = 0) + { + return !addInstMatch(qe, q, m, c, modEq, index, true); + } + /** exists inst match, vector version */ + bool existsInstMatch(QuantifiersEngine* qe, + Node q, + std::vector<Node>& m, + context::Context* c, + bool modEq = false, + unsigned index = 0) + { + return !addInstMatch(qe, q, m, c, modEq, index, true); + } + /** add inst match + * + * This method adds (the suffix of) m starting at the given index to this + * trie, and returns true if and only if m did not already occur in this trie. + * The domain of m is the bound variables of quantified formula q. + * If modEq is true, we check for duplication modulo equality the current + * equalities in the active equality engine of qe. + * It additionally takes a context c, for which the entry is valid in. + */ + bool addInstMatch(QuantifiersEngine* qe, + Node q, + InstMatch& m, + context::Context* c, + bool modEq = false, + unsigned index = 0, + bool onlyExist = false) + { + return addInstMatch(qe, q, m.d_vals, c, modEq, index, onlyExist); + } + /** add inst match, vector version */ + bool addInstMatch(QuantifiersEngine* qe, + Node q, + std::vector<Node>& m, + context::Context* c, + bool modEq = false, + unsigned index = 0, + bool onlyExist = false); + /** remove inst match + * + * This removes (the suffix of) m starting at the given index from this trie. + * It returns true if and only if this entry existed in this trie. + * The domain of m is the bound variables of quantified formula q. + */ + bool removeInstMatch(Node q, std::vector<Node>& m, unsigned index = 0); + /** record instantiation lemma + * + * This records that the instantiation lemma lem corresponds to the entry + * given by (the suffix of) m starting at the given index. + */ + bool recordInstLemma(Node q, + std::vector<Node>& m, + Node lem, + unsigned index = 0); + + /** get instantiations + * + * This gets the set of instantiation lemmas that were recorded in this class + * via calls to recordInstLemma. If useActive is true, we only add + * instantiations that occur in active. + */ + void getInstantiations(std::vector<Node>& insts, + Node q, + QuantifiersEngine* qe, + bool useActive, + std::vector<Node>& active) + { + std::vector<Node> terms; + getInstantiations(insts, q, terms, qe, useActive, active); + } + /** get explanation for inst lemmas + * + * This gets the explanation for the instantiation lemmas in lems for + * quantified formula q, for which this trie stores instantiation matches for. + * For each instantiation lemma lem recording in this trie via calls to + * recordInstLemma, we map lem to q in map quant, and lem to its corresponding + * vector of terms in tvec. + */ + void getExplanationForInstLemmas( + Node q, + const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec) const + { + std::vector<Node> terms; + getExplanationForInstLemmas(q, terms, lems, quant, tvec); + } + + /** print this class */ + void print(std::ostream& out, + Node q, + bool& firstTime, + bool useActive, + std::vector<Node>& active) const + { + std::vector<TNode> terms; + print(out, q, terms, firstTime, useActive, active); + } + + private: + /** the data */ + std::map<Node, CDInstMatchTrie*> d_data; + /** is valid */ + context::CDO<bool> d_valid; + /** helper for print + * terms accumulates the path we are on in the trie. + */ + void print(std::ostream& out, + Node q, + std::vector<TNode>& terms, + bool& firstTime, + bool useActive, + std::vector<Node>& active) const; + /** helper for get instantiations + * terms accumulates the path we are on in the trie. + */ + void getInstantiations(std::vector<Node>& insts, + Node q, + std::vector<Node>& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector<Node>& active) const; + /** helper for get explanation for inst lemma + * terms accumulates the path we are on in the trie. + */ + void getExplanationForInstLemmas( + Node q, + std::vector<Node>& terms, + const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec) const; + /** set instantiation lemma at this node in the trie */ + void setInstLemma(Node n) + { + d_data.clear(); + d_data[n] = NULL; + } + /** does this node of the trie store an instantiation lemma? */ + bool hasInstLemma() const { return !d_data.empty(); } + /** get the instantiation lemma stored in this node of the trie */ + Node getInstLemma() const { return d_data.begin()->first; } +}; + +/** inst match trie ordered + * + * This is an ordered version of the context-independent instantiation match + * trie. It stores a variable order and a base InstMatchTrie. + */ +class InstMatchTrieOrdered +{ + public: + InstMatchTrieOrdered(InstMatchTrie::ImtIndexOrder* imtio) : d_imtio(imtio) {} + ~InstMatchTrieOrdered() {} + /** get the ordering */ + InstMatchTrie::ImtIndexOrder* getOrdering() { return d_imtio; } + /** get the trie data */ + InstMatchTrie* getTrie() { return &d_imt; } + /** add match m for quantified formula q + * + * This method returns true if the match m was not previously added to this + * class. If modEq is true, we consider duplicates modulo the current + * equalities stored in the active equality engine of quantifiers engine. + */ + bool addInstMatch(QuantifiersEngine* qe, + Node q, + InstMatch& m, + bool modEq = false) + { + return d_imt.addInstMatch(qe, q, m, modEq, d_imtio); + } + /** returns true if this trie contains m + * + * This method returns true if the match m exists in this + * class. If modEq is true, we consider duplicates modulo the current + * equalities stored in the active equality engine of quantifiers engine. + */ + bool existsInstMatch(QuantifiersEngine* qe, + Node q, + InstMatch& m, + bool modEq = false) + { + return d_imt.existsInstMatch(qe, q, m, modEq, d_imtio); + } + + private: + /** the ordering */ + InstMatchTrie::ImtIndexOrder* d_imtio; + /** the data of this class */ + InstMatchTrie d_imt; +}; + +} /* CVC4::theory::inst namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 3c351cad5..f97413026 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -15,8 +15,9 @@ #include <vector> #include "theory/quantifiers/inst_propagator.h" -#include "theory/rewriter.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace std; @@ -670,7 +671,9 @@ void InstPropagator::filterInstantiations() { for( std::map< unsigned, InstInfo >::iterator it = d_ii.begin(); it != d_ii.end(); ++it ){ if( !it->second.d_q.isNull() ){ if( d_relevant_inst.find( it->first )==d_relevant_inst.end() ){ - if( !d_qe->removeInstantiation( it->second.d_q, it->second.d_lem, it->second.d_terms ) ){ + if (!d_qe->getInstantiate()->removeInstantiation( + it->second.d_q, it->second.d_lem, it->second.d_terms)) + { Trace("qip-warn") << "WARNING : did not remove instantiation id " << it->first << std::endl; Assert( false ); }else{ diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index b8ea2c49e..7f485750a 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -18,13 +18,14 @@ #define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H #include <iostream> +#include <map> #include <string> #include <vector> -#include <map> #include "expr/node.h" #include "expr/type_node.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 24a9f1bdf..668593842 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -19,6 +19,7 @@ #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" @@ -728,12 +729,15 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { if( d_quantEngine->getQuantAttributes()->isQuantElimPartial( d_curr_quant ) ){ d_cbqi_set_quant_inactive = true; d_incomplete_check = true; - d_quantEngine->recordInstantiationInternal( d_curr_quant, subs, false, false ); + 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->addInstantiation( d_curr_quant, subs, false, false, used_vts ) ){ + 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; diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index edd15fa2c..54689b32a 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/inst_strategy_enumerative.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -273,7 +274,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort) << std::endl; } } - if (d_quantEngine->addInstantiation(f, terms)) + if (d_quantEngine->getInstantiate()->addInstantiation(f, terms)) { Trace("inst-alg-rd") << "Success!" << std::endl; ++(d_quantEngine->d_statistics.d_instantiations_guess); diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp new file mode 100644 index 000000000..e04217b16 --- /dev/null +++ b/src/theory/quantifiers/instantiate.cpp @@ -0,0 +1,821 @@ +/********************* */ +/*! \file instantiate.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 instantiate + **/ + +#include "theory/quantifiers/instantiate.h" + +#include "options/quantifiers_options.h" +#include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/quantifiers/quantifiers_attributes.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" + +using namespace CVC4::kind; +using namespace CVC4::context; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +Instantiate::Instantiate(QuantifiersEngine* qe, context::UserContext* u) + : d_qe(qe), + d_term_db(nullptr), + d_term_util(nullptr), + d_total_inst_count_debug(0), + d_c_inst_match_trie_dom(u) +{ +} + +Instantiate::~Instantiate() +{ + for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie) + { + delete t.second; + } + d_c_inst_match_trie.clear(); +} + +bool Instantiate::reset(Theory::Effort e) +{ + if (!d_recorded_inst.empty()) + { + Trace("quant-engine-debug") << "Removing " << d_recorded_inst.size() + << " instantiations..." << std::endl; + // remove explicitly recorded instantiations + for (std::pair<Node, std::vector<Node> >& r : d_recorded_inst) + { + removeInstantiationInternal(r.first, r.second); + } + d_recorded_inst.clear(); + } + d_term_db = d_qe->getTermDatabase(); + d_term_util = d_qe->getTermUtil(); + return true; +} + +void Instantiate::registerQuantifier(Node q) {} +bool Instantiate::checkComplete() +{ + if (!d_recorded_inst.empty()) + { + Trace("quant-engine-debug") + << "Set incomplete due to recorded instantiations." << std::endl; + return false; + } + return true; +} + +void Instantiate::addNotify(InstantiationNotify* in) +{ + d_inst_notify.push_back(in); +} + +void Instantiate::notifyFlushLemmas() +{ + for (InstantiationNotify*& in : d_inst_notify) + { + in->filterInstantiations(); + } +} + +bool Instantiate::addInstantiation( + Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts) +{ + Assert(q[0].getNumChildren() == m.d_vals.size()); + return addInstantiation(q, m.d_vals, mkRep, modEq, doVts); +} + +bool Instantiate::addInstantiation( + Node q, std::vector<Node>& terms, bool mkRep, bool modEq, bool doVts) +{ + // For resource-limiting (also does a time check). + d_qe->getOutputChannel().safePoint(options::quantifierStep()); + Assert(!d_qe->inConflict()); + Assert(terms.size() == q[0].getNumChildren()); + Assert(d_term_db != nullptr); + Assert(d_term_util != nullptr); + Trace("inst-add-debug") << "For quantified formula " << q + << ", add instantiation: " << std::endl; + for (unsigned i = 0, size = terms.size(); i < size; i++) + { + Trace("inst-add-debug") << " " << q[0][i]; + Trace("inst-add-debug2") << " -> " << terms[i]; + TypeNode tn = q[0][i].getType(); + if (terms[i].isNull()) + { + terms[i] = getTermForType(tn); + } + if (mkRep) + { + // pick the best possible representative for instantiation, based on past + // use and simplicity of term + terms[i] = d_qe->getInternalRepresentative(terms[i], q, i); + } + else + { + // ensure the type is correct + terms[i] = quantifiers::TermUtil::ensureType(terms[i], tn); + } + Trace("inst-add-debug") << " -> " << terms[i] << std::endl; + if (terms[i].isNull()) + { + Trace("inst-add-debug") + << " --> Failed to make term vector, due to term/type restrictions." + << std::endl; + return false; + } +#ifdef CVC4_ASSERTIONS + bool bad_inst = false; + if (quantifiers::TermUtil::containsUninterpretedConstant(terms[i])) + { + Trace("inst") << "***& inst contains uninterpreted constant : " + << terms[i] << std::endl; + bad_inst = true; + } + else if (!terms[i].getType().isSubtypeOf(q[0][i].getType())) + { + Trace("inst") << "***& inst bad type : " << terms[i] << " " + << terms[i].getType() << "/" << q[0][i].getType() + << std::endl; + bad_inst = true; + } + else if (options::cbqi()) + { + Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]); + if (!icf.isNull()) + { + if (icf == q) + { + Trace("inst") << "***& inst contains inst constant attr : " + << terms[i] << std::endl; + bad_inst = true; + } + else if (quantifiers::TermUtil::containsTerms( + terms[i], d_term_util->d_inst_constants[q])) + { + Trace("inst") << "***& inst contains inst constants : " << terms[i] + << std::endl; + bad_inst = true; + } + } + } + // this assertion is critical to soundness + if (bad_inst) + { + Trace("inst") << "***& Bad Instantiate " << q << " with " << std::endl; + for (unsigned j = 0; j < terms.size(); j++) + { + Trace("inst") << " " << terms[j] << std::endl; + } + Assert(false); + } +#endif + } + + // Note we check for entailment before checking for term vector duplication. + // Although checking for term vector duplication is a faster check, it is + // included automatically with recordInstantiationInternal, hence we prefer + // two checks instead of three. In experiments, it is 1% slower or so to call + // existsInstantiation here. + // Alternatively, we could return an (index, trie node) in the call to + // existsInstantiation here, where this would return the node in the trie + // where we determined that there is definitely no duplication, and then + // continue from that point in recordInstantiation below. However, for + // simplicity, we do not pursue this option (as it would likely only + // lead to very small gains). + + // check for positive entailment + if (options::instNoEntail()) + { + // should check consistency of equality engine + // (if not aborting on utility's reset) + std::map<TNode, TNode> subs; + for (unsigned i = 0, size = terms.size(); i < size; i++) + { + subs[q[0][i]] = terms[i]; + } + if (d_term_db->isEntailed(q[1], subs, false, true)) + { + Trace("inst-add-debug") << " --> Currently entailed." << std::endl; + ++(d_statistics.d_inst_duplicate_ent); + return false; + } + } + + // check based on instantiation level + if (options::instMaxLevel() != -1 || options::lteRestrictInstClosure()) + { + for (Node& t : terms) + { + if (!d_term_db->isTermEligibleForInstantiation(t, q, true)) + { + return false; + } + } + } + + // record the instantiation + bool recorded = recordInstantiationInternal(q, terms, modEq); + if (!recorded) + { + Trace("inst-add-debug") << " --> Already exists (no record)." << std::endl; + ++(d_statistics.d_inst_duplicate_eq); + return false; + } + + // construct the instantiation + Trace("inst-add-debug") << "Constructing instantiation..." << std::endl; + Assert(d_term_util->d_vars[q].size() == terms.size()); + // get the instantiation + Node body = getInstantiation(q, d_term_util->d_vars[q], terms, doVts); + Node orig_body = body; + if (options::cbqiNestedQE()) + { + InstStrategyCbqi* icbqi = d_qe->getInstStrategyCbqi(); + if (icbqi) + { + body = icbqi->doNestedQE(q, terms, body, doVts); + } + } + body = quantifiers::QuantifiersRewriter::preprocess(body, true); + Trace("inst-debug") << "...preprocess to " << body << std::endl; + + // construct the lemma + Trace("inst-assert") << "(assert " << body << ")" << std::endl; + + if (d_qe->usingModelEqualityEngine() && options::instNoModelTrue()) + { + Node val_body = d_qe->getModel()->getValue(body); + if (val_body.isConst() && val_body.getConst<bool>()) + { + Trace("inst-add-debug") << " --> True in model." << std::endl; + ++(d_statistics.d_inst_duplicate_model_true); + return false; + } + } + + Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body); + + // get relevancy conditions + if (options::instRelevantCond()) + { + std::vector<Node> rlv_cond; + for (Node& t : terms) + { + quantifiers::TermUtil::getRelevancyCondition(t, rlv_cond); + } + if (!rlv_cond.empty()) + { + rlv_cond.push_back(lem); + lem = NodeManager::currentNM()->mkNode(kind::OR, rlv_cond); + } + } + + lem = Rewriter::rewrite(lem); + + // check for lemma duplication + if (!d_qe->addLemma(lem, true, false)) + { + Trace("inst-add-debug") << " --> Lemma already exists." << std::endl; + ++(d_statistics.d_inst_duplicate); + return false; + } + + d_total_inst_debug[q]++; + d_temp_inst_debug[q]++; + d_total_inst_count_debug++; + if (Trace.isOn("inst")) + { + Trace("inst") << "*** Instantiate " << q << " with " << std::endl; + for (unsigned i = 0, size = terms.size(); i < size; i++) + { + if (Trace.isOn("inst")) + { + Trace("inst") << " " << terms[i]; + if (Trace.isOn("inst-debug")) + { + Trace("inst-debug") << ", type=" << terms[i].getType() + << ", var_type=" << q[0][i].getType(); + } + Trace("inst") << std::endl; + } + } + } + if (options::instMaxLevel() != -1) + { + if (doVts) + { + // virtual term substitution/instantiation level features are + // incompatible + Assert(false); + } + else + { + uint64_t maxInstLevel = 0; + for (const Node& tc : terms) + { + if (tc.hasAttribute(InstLevelAttribute()) + && tc.getAttribute(InstLevelAttribute()) > maxInstLevel) + { + maxInstLevel = tc.getAttribute(InstLevelAttribute()); + } + } + QuantAttributes::setInstantiationLevelAttr( + orig_body, q[1], maxInstLevel + 1); + } + } + QuantifiersModule::QEffort elevel = d_qe->getCurrentQEffort(); + if (elevel > QuantifiersModule::QEFFORT_CONFLICT + && elevel < QuantifiersModule::QEFFORT_NONE + && !d_inst_notify.empty()) + { + // notify listeners + for (InstantiationNotify*& in : d_inst_notify) + { + if (!in->notifyInstantiation(elevel, q, lem, terms, body)) + { + Trace("inst-add-debug") << "...we are in conflict." << std::endl; + d_qe->setConflict(); + Assert(d_qe->getNumLemmasWaiting() > 0); + break; + } + } + } + if (options::trackInstLemmas()) + { + bool recorded; + if (options::incrementalSolving()) + { + recorded = d_c_inst_match_trie[q]->recordInstLemma(q, terms, lem); + } + else + { + recorded = d_inst_match_trie[q].recordInstLemma(q, terms, lem); + } + Trace("inst-add-debug") << "...was recorded : " << recorded << std::endl; + Assert(recorded); + } + Trace("inst-add-debug") << " --> Success." << std::endl; + ++(d_statistics.d_instantiations); + return true; +} + +bool Instantiate::removeInstantiation(Node q, + Node lem, + std::vector<Node>& terms) +{ + // lem must occur in d_waiting_lemmas + if (d_qe->removeLemma(lem)) + { + return removeInstantiationInternal(q, terms); + } + return false; +} + +bool Instantiate::recordInstantiation(Node q, + std::vector<Node>& terms, + bool modEq, + bool addedLem) +{ + return recordInstantiationInternal(q, terms, modEq, addedLem); +} + +bool Instantiate::existsInstantiation(Node q, + std::vector<Node>& terms, + bool modEq) +{ + if (options::incrementalSolving()) + { + std::map<Node, inst::CDInstMatchTrie*>::iterator it = + d_c_inst_match_trie.find(q); + if (it != d_c_inst_match_trie.end()) + { + return it->second->existsInstMatch( + d_qe, q, terms, d_qe->getUserContext(), modEq); + } + } + else + { + std::map<Node, inst::InstMatchTrie>::iterator it = + d_inst_match_trie.find(q); + if (it != d_inst_match_trie.end()) + { + return it->second.existsInstMatch(d_qe, q, terms, modEq); + } + } + return false; +} + +Node Instantiate::getInstantiation(Node q, + std::vector<Node>& vars, + std::vector<Node>& terms, + bool doVts) +{ + Node body; + Assert(vars.size() == terms.size()); + Assert(q[0].getNumChildren() == vars.size()); + // TODO (#1386) : optimize this + body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end()); + if (doVts) + { + // do virtual term substitution + body = Rewriter::rewrite(body); + Trace("quant-vts-debug") << "Rewrite vts symbols in " << body << std::endl; + Node body_r = d_term_util->rewriteVtsSymbols(body); + Trace("quant-vts-debug") << " ...result: " << body_r + << std::endl; + body = body_r; + } + return body; +} + +Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts) +{ + Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end()); + Assert(m.d_vals.size() == q[0].getNumChildren()); + return getInstantiation(q, d_term_util->d_vars[q], m.d_vals, doVts); +} + +Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts) +{ + Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end()); + return getInstantiation(q, d_term_util->d_vars[q], terms, doVts); +} + +bool Instantiate::recordInstantiationInternal(Node q, + std::vector<Node>& terms, + bool modEq, + bool addedLem) +{ + if (!addedLem) + { + // record the instantiation for deletion later + d_recorded_inst.push_back(std::pair<Node, std::vector<Node> >(q, terms)); + } + if (options::incrementalSolving()) + { + Trace("inst-add-debug") + << "Adding into context-dependent inst trie, modEq = " << modEq + << std::endl; + inst::CDInstMatchTrie* imt; + std::map<Node, inst::CDInstMatchTrie*>::iterator it = + d_c_inst_match_trie.find(q); + if (it != d_c_inst_match_trie.end()) + { + imt = it->second; + } + else + { + imt = new inst::CDInstMatchTrie(d_qe->getUserContext()); + d_c_inst_match_trie[q] = imt; + } + d_c_inst_match_trie_dom.insert(q); + return imt->addInstMatch(d_qe, q, terms, d_qe->getUserContext(), modEq); + } + Trace("inst-add-debug") << "Adding into inst trie" << std::endl; + return d_inst_match_trie[q].addInstMatch(d_qe, q, terms, modEq); +} + +bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms) +{ + if (options::incrementalSolving()) + { + std::map<Node, inst::CDInstMatchTrie*>::iterator it = + d_c_inst_match_trie.find(q); + if (it != d_c_inst_match_trie.end()) + { + return it->second->removeInstMatch(q, terms); + } + return false; + } + return d_inst_match_trie[q].removeInstMatch(q, terms); +} + +Node Instantiate::getTermForType(TypeNode tn) +{ + if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn)) + { + return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0); + } + return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn); +} + +bool Instantiate::printInstantiations(std::ostream& out) +{ + bool useUnsatCore = false; + std::vector<Node> active_lemmas; + if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas)) + { + useUnsatCore = true; + } + bool printed = false; + if (options::incrementalSolving()) + { + for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie) + { + bool firstTime = true; + t.second->print(out, t.first, firstTime, useUnsatCore, active_lemmas); + if (!firstTime) + { + out << ")" << std::endl; + } + printed = printed || !firstTime; + } + } + else + { + for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie) + { + bool firstTime = true; + t.second.print(out, t.first, firstTime, useUnsatCore, active_lemmas); + if (!firstTime) + { + out << ")" << std::endl; + } + printed = printed || !firstTime; + } + } + return printed; +} + +void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) +{ + if (options::incrementalSolving()) + { + for (context::CDHashSet<Node, NodeHashFunction>::const_iterator it = + d_c_inst_match_trie_dom.begin(); + it != d_c_inst_match_trie_dom.end(); + ++it) + { + qs.push_back(*it); + } + } + else + { + for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie) + { + qs.push_back(t.first); + } + } +} + +bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas) +{ + // only if unsat core available + if (options::proof()) + { + if (!ProofManager::currentPM()->unsatCoreAvailable()) + { + return false; + } + } + + Trace("inst-unsat-core") << "Get instantiations in unsat core..." + << std::endl; + ProofManager::currentPM()->getLemmasInUnsatCore(theory::THEORY_QUANTIFIERS, + active_lemmas); + if (Trace.isOn("inst-unsat-core")) + { + Trace("inst-unsat-core") << "Quantifiers lemmas in unsat core: " + << std::endl; + for (const Node& lem : active_lemmas) + { + Trace("inst-unsat-core") << " " << lem << std::endl; + } + Trace("inst-unsat-core") << std::endl; + } + return true; +} + +bool Instantiate::getUnsatCoreLemmas(std::vector<Node>& active_lemmas, + std::map<Node, Node>& weak_imp) +{ + if (getUnsatCoreLemmas(active_lemmas)) + { + for (unsigned i = 0, size = active_lemmas.size(); i < size; ++i) + { + Node n = ProofManager::currentPM()->getWeakestImplicantInUnsatCore( + active_lemmas[i]); + if (n != active_lemmas[i]) + { + Trace("inst-unsat-core") << " weaken : " << active_lemmas[i] << " -> " + << n << std::endl; + } + weak_imp[active_lemmas[i]] = n; + } + return true; + } + return false; +} + +void Instantiate::getInstantiationTermVectors( + Node q, std::vector<std::vector<Node> >& tvecs) +{ + std::vector<Node> lemmas; + getInstantiations(q, lemmas); + std::map<Node, Node> quant; + std::map<Node, std::vector<Node> > tvec; + getExplanationForInstLemmas(lemmas, quant, tvec); + for (std::pair<const Node, std::vector<Node> >& t : tvec) + { + tvecs.push_back(t.second); + } +} + +void Instantiate::getInstantiationTermVectors( + std::map<Node, std::vector<std::vector<Node> > >& insts) +{ + if (options::incrementalSolving()) + { + for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie) + { + getInstantiationTermVectors(t.first, insts[t.first]); + } + } + else + { + for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie) + { + getInstantiationTermVectors(t.first, insts[t.first]); + } + } +} + +void Instantiate::getExplanationForInstLemmas( + const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec) +{ + if (options::trackInstLemmas()) + { + if (options::incrementalSolving()) + { + for (std::pair<const Node, inst::CDInstMatchTrie*>& t : + d_c_inst_match_trie) + { + t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec); + } + } + else + { + for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie) + { + t.second.getExplanationForInstLemmas(t.first, lems, quant, tvec); + } + } +#ifdef CVC4_ASSERTIONS + for (unsigned j = 0; j < lems.size(); j++) + { + Assert(quant.find(lems[j]) != quant.end()); + Assert(tvec.find(lems[j]) != tvec.end()); + } +#endif + } + Assert(false); +} + +void Instantiate::getInstantiations(std::map<Node, std::vector<Node> >& insts) +{ + bool useUnsatCore = false; + std::vector<Node> active_lemmas; + if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas)) + { + useUnsatCore = true; + } + + if (options::incrementalSolving()) + { + for (std::pair<const Node, inst::CDInstMatchTrie*>& t : d_c_inst_match_trie) + { + t.second->getInstantiations( + insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas); + } + } + else + { + for (std::pair<const Node, inst::InstMatchTrie>& t : d_inst_match_trie) + { + t.second.getInstantiations( + insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas); + } + } +} + +void Instantiate::getInstantiations(Node q, std::vector<Node>& insts) +{ + if (options::incrementalSolving()) + { + std::map<Node, inst::CDInstMatchTrie*>::iterator it = + d_c_inst_match_trie.find(q); + if (it != d_c_inst_match_trie.end()) + { + std::vector<Node> active_lemmas; + it->second->getInstantiations( + insts, it->first, d_qe, false, active_lemmas); + } + } + else + { + std::map<Node, inst::InstMatchTrie>::iterator it = + d_inst_match_trie.find(q); + if (it != d_inst_match_trie.end()) + { + std::vector<Node> active_lemmas; + it->second.getInstantiations( + insts, it->first, d_qe, false, active_lemmas); + } + } +} + +Node Instantiate::getInstantiatedConjunction(Node q) +{ + Assert(q.getKind() == FORALL); + std::vector<Node> insts; + getInstantiations(q, insts); + if (insts.empty()) + { + return NodeManager::currentNM()->mkConst(true); + } + Node ret; + if (insts.size() == 1) + { + ret = insts[0]; + } + else + { + ret = NodeManager::currentNM()->mkNode(kind::AND, insts); + } + // have to remove q + // may want to do this in a better way + TNode tq = q; + TNode tt = NodeManager::currentNM()->mkConst(true); + ret = ret.substitute(tq, tt); + return ret; +} + +void Instantiate::debugPrint() +{ + // debug information + if (Trace.isOn("inst-per-quant-round")) + { + for (std::pair<const Node, int>& i : d_temp_inst_debug) + { + Trace("inst-per-quant-round") << " * " << i.second << " for " << i.first + << std::endl; + d_temp_inst_debug[i.first] = 0; + } + } +} + +void Instantiate::debugPrintModel() +{ + if (Trace.isOn("inst-per-quant")) + { + for (std::pair<const Node, int>& i : d_total_inst_debug) + { + Trace("inst-per-quant") << " * " << i.second << " for " << i.first + << std::endl; + } + } +} + +Instantiate::Statistics::Statistics() + : d_instantiations("Instantiate::Instantiations_Total", 0), + d_inst_duplicate("Instantiate::Duplicate_Inst", 0), + d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0), + d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0), + d_inst_duplicate_model_true("Instantiate::Duplicate_Inst_Model_True", 0) +{ + smtStatisticsRegistry()->registerStat(&d_instantiations); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent); + smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true); +} + +Instantiate::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_instantiations); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent); + smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true); +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h new file mode 100644 index 000000000..d1973eadb --- /dev/null +++ b/src/theory/quantifiers/instantiate.h @@ -0,0 +1,377 @@ +/********************* */ +/*! \file instantiate.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 instantiate + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H +#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H + +#include <map> + +#include "expr/node.h" +#include "theory/quantifiers/inst_match_trie.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers_engine.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class TermDb; +class TermUtil; + +/** instantiation notify + * + * This class is a listener for all instantiations generated with quantifiers. + * By default, no notify classes are used. For an example of an instantiation + * notify class, see quantifiers/inst_propagate.h, which has a notify class + * that recognizes when the set of enqueued instantiations form a conflict. + */ +class InstantiationNotify +{ + public: + InstantiationNotify() {} + virtual ~InstantiationNotify() {} + /** notify instantiation + * + * This is called when an instantiation of quantified formula q is + * instantiated by a substitution whose range is terms at quantifier effort + * quant_e. Furthermore: + * body is the substituted, preprocessed body of the quantified formula, + * lem is the instantiation lemma ( ~q V body ) after rewriting. + */ + virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e, + Node q, + Node lem, + std::vector<Node>& terms, + Node body) = 0; + /** filter instantiations + * + * This is called just before the quantifiers engine flushes its lemmas to the + * output channel. During this call, the instantiation notify object may + * call, e.g. QuantifiersEngine::getInstantiate()->removeInstantiation + * to remove instantiations that should not be sent on the output channel. + */ + virtual void filterInstantiations() = 0; +}; + +/** Instantiate + * + * This class is used for generating instantiation lemmas. It maintains an + * instantiation trie, which is represented by a different data structure + * depending on whether incremental solving is enabled (see d_inst_match_trie + * and d_c_inst_match_trie). + * + * Below, we say an instantiation lemma for q = forall x. F under substitution + * { x -> t } is the formula: + * ( ~forall x. F V F * { x -> t } ) + * where * is application of substitution. + * + * Its main interface is ::addInstantiation(...), which is called by many of + * the quantifiers modules, which enqueues instantiation lemmas in quantifiers + * engine via calls to QuantifiersEngine::addLemma. + * + * It also has utilities for constructing instantiations, and interfaces for + * getting the results of the instantiations produced during check-sat calls. + */ +class Instantiate : public QuantifiersUtil +{ + public: + Instantiate(QuantifiersEngine* qe, context::UserContext* u); + ~Instantiate(); + + /** reset */ + virtual bool reset(Theory::Effort e) override; + /** register quantifier */ + virtual void registerQuantifier(Node q) override; + /** identify */ + virtual std::string identify() const override { return "Instantiate"; } + /** check incomplete */ + virtual bool checkComplete() override; + + //--------------------------------------notify objects + /** add instantiation notify + * + * Adds an instantiation notify class to listen to the instantiations reported + * to this class. + */ + void addNotify(InstantiationNotify* in); + /** get number of instantiation notify added to this class */ + bool hasNotify() const { return !d_inst_notify.empty(); } + /** notify flush lemmas + * + * This is called just before the quantifiers engine flushes its lemmas to + * the output channel. + */ + void notifyFlushLemmas(); + //--------------------------------------end notify objects + + /** do instantiation specified by m + * + * This function returns true if the instantiation lemma for quantified + * formula q for the substitution specified by m is successfully enqueued + * via a call to QuantifiersEngine::addLemma. + * mkRep : whether to take the representatives of the terms in the range of + * the substitution m, + * modEq : whether to check for duplication modulo equality in instantiation + * tries (for performance), + * doVts : whether we must apply virtual term substitution to the + * instantiation lemma. + * + * This call may fail if it can be determined that the instantiation is not + * relevant or legal in the current context. This happens if: + * (1) The substitution is not well-typed, + * (2) The substitution involves terms whose instantiation level is above the + * allowed limit, + * (3) The resulting instantiation is entailed in the current context using a + * fast entailment check (see TermDb::isEntailed), + * (4) The range of the substitution is a duplicate of that of a previously + * added instantiation, + * (5) The instantiation lemma is a duplicate of previously added lemma. + * + */ + bool addInstantiation(Node q, + InstMatch& m, + bool mkRep = false, + bool modEq = false, + bool doVts = false); + /** add instantiation + * + * Same as above, but the substitution we are considering maps the variables + * of q to the vector terms, in order. + */ + bool addInstantiation(Node q, + std::vector<Node>& terms, + bool mkRep = false, + bool modEq = false, + bool doVts = false); + /** remove pending instantiation + * + * Removes the instantiation lemma lem from the instantiation trie. + */ + bool removeInstantiation(Node q, Node lem, std::vector<Node>& terms); + /** record instantiation + * + * Explicitly record that q has been instantiated with terms. This is the + * same as addInstantiation, but does not enqueue an instantiation lemma. + */ + bool recordInstantiation(Node q, + std::vector<Node>& terms, + bool modEq = false, + bool addedLem = true); + /** exists instantiation + * + * Returns true if and only if the instantiation already was added or + * recorded by this class. + * modEq : whether to check for duplication modulo equality + */ + bool existsInstantiation(Node q, + std::vector<Node>& terms, + bool modEq = false); + //--------------------------------------general utilities + /** get instantiation + * + * Returns the instantiation lemma for q under substitution { vars -> terms }. + * doVts is whether to apply virtual term substitution to its body. + */ + Node getInstantiation(Node q, + std::vector<Node>& vars, + std::vector<Node>& terms, + bool doVts = false); + /** get instantiation + * + * Same as above, but with vars/terms specified by InstMatch m. + */ + Node getInstantiation(Node q, InstMatch& m, bool doVts = false); + /** get instantiation + * + * Same as above but with vars equal to the bound variables of q. + */ + Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false); + /** get term for type + * + * This returns an arbitrary term for type tn. + * This term is chosen heuristically to be the best + * term for instantiation. Currently, this + * heuristic enumerates the first term of the + * type if the type is closed enumerable, otherwise + * an existing ground term from the term database if + * one exists, or otherwise a fresh variable. + */ + Node getTermForType(TypeNode tn); + //--------------------------------------end general utilities + + /** debug print, called once per instantiation round. */ + void debugPrint(); + /** debug print model, called once, before we terminate with sat/unknown. */ + void debugPrintModel(); + + //--------------------------------------user-level interface utilities + /** print instantiations + * + * Print all instantiations for all quantified formulas on out, + * returns true if at least one instantiation was printed. + */ + bool printInstantiations(std::ostream& out); + /** get instantiated quantified formulas + * + * Get the list of quantified formulas that were instantiated in the current + * user context, store them in qs. + */ + void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs); + /** get instantiations + * + * Get the body of all instantiation lemmas added in the current user context + * for quantified formula q, store them in insts. + */ + void getInstantiations(Node q, std::vector<Node>& insts); + /** get instantiations + * + * Get the body of all instantiation lemmas added in the current user context + * for all quantified formulas stored in the domain of insts, store them in + * the range of insts. + */ + void getInstantiations(std::map<Node, std::vector<Node> >& insts); + /** get instantiation term vectors + * + * Get term vectors corresponding to for all instantiations lemmas added in + * the current user context for quantified formula q, store them in tvecs. + */ + void getInstantiationTermVectors(Node q, + std::vector<std::vector<Node> >& tvecs); + /** get instantiation term vectors + * + * Get term vectors for all instantiations lemmas added in the current user + * context for quantified formula q, store them in tvecs. + */ + void getInstantiationTermVectors( + std::map<Node, std::vector<std::vector<Node> > >& insts); + /** get instantiated conjunction + * + * This gets a conjunction of the bodies of instantiation lemmas added in the + * current user context for quantified formula q. For example, if we added: + * ~forall x. P( x ) V P( a ) + * ~forall x. P( x ) V P( b ) + * Then, this method returns P( a ) ^ P( b ). + */ + Node getInstantiatedConjunction(Node q); + /** get unsat core lemmas + * + * If this method returns true, then it appends to active_lemmas all lemmas + * that are in the unsat core that originated from the theory of quantifiers. + * This method returns false if the unsat core is not available. + */ + bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas); + /** get unsat core lemmas + * + * If this method returns true, then it appends to active_lemmas all lemmas + * that are in the unsat core that originated from the theory of quantifiers. + * This method returns false if the unsat core is not available. + * + * It also computes a weak implicant for each of these lemmas. For each lemma + * L in active_lemmas, this is a formula L' such that: + * L => L' + * and replacing L by L' in the unsat core results in a set that is still + * unsatisfiable. The map weak_imp stores this formula for each formula in + * active_lemmas. + */ + bool getUnsatCoreLemmas(std::vector<Node>& active_lemmas, + std::map<Node, Node>& weak_imp); + /** get explanation for instantiation lemmas + * + * + */ + void getExplanationForInstLemmas(const std::vector<Node>& lems, + std::map<Node, Node>& quant, + std::map<Node, std::vector<Node> >& tvec); + //--------------------------------------end user-level interface utilities + + /** statistics class + * + * This tracks statistics on the number of instantiations successfully + * enqueued on the quantifiers output channel, and the number of redundant + * instantiations encountered by various criteria. + */ + class Statistics + { + public: + IntStat d_instantiations; + IntStat d_inst_duplicate; + IntStat d_inst_duplicate_eq; + IntStat d_inst_duplicate_ent; + IntStat d_inst_duplicate_model_true; + Statistics(); + ~Statistics(); + }; /* class Instantiate::Statistics */ + Statistics d_statistics; + + private: + /** record instantiation, return true if it was not a duplicate + * + * addedLem : whether an instantiation lemma was added for the vector we are + * recording. If this is false, we bookkeep the vector. + * modEq : whether to check for duplication modulo equality in instantiation + * tries (for performance), + */ + bool recordInstantiationInternal(Node q, + std::vector<Node>& terms, + bool modEq = false, + bool addedLem = true); + /** remove instantiation from the cache */ + bool removeInstantiationInternal(Node q, std::vector<Node>& terms); + + /** pointer to the quantifiers engine */ + QuantifiersEngine* d_qe; + /** cache of term database for quantifiers engine */ + TermDb* d_term_db; + /** cache of term util for quantifiers engine */ + TermUtil* d_term_util; + /** instantiation notify classes */ + std::vector<InstantiationNotify*> d_inst_notify; + + /** statistics for debugging total instantiation */ + int d_total_inst_count_debug; + /** statistics for debugging total instantiations per quantifier */ + std::map<Node, int> d_total_inst_debug; + /** statistics for debugging total instantiations per quantifier per round */ + std::map<Node, int> d_temp_inst_debug; + + /** list of all instantiations produced for each quantifier + * + * We store context (dependent, independent) versions. If incremental solving + * is disabled, we use d_inst_match_trie for performance reasons. + */ + std::map<Node, inst::InstMatchTrie> d_inst_match_trie; + std::map<Node, inst::CDInstMatchTrie*> d_c_inst_match_trie; + /** + * The list of quantified formulas for which the domain of d_c_inst_match_trie + * is valid. + */ + context::CDHashSet<Node, NodeHashFunction> d_c_inst_match_trie_dom; + + /** explicitly recorded instantiations + * + * Sometimes an instantiation is recorded internally but not sent out as a + * lemma, for instance, for partial quantifier elimination. This is a map + * of these instantiations, for each quantified formula. + */ + std::vector<std::pair<Node, std::vector<Node> > > d_recorded_inst; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 358838b11..dba04ce51 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -16,6 +16,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" @@ -118,7 +119,7 @@ void QModelBuilder::debugModel( TheoryModel* m ){ { terms.push_back( riter.getCurrentTerm( k ) ); } - Node n = d_qe->getInstantiation( f, vars, terms ); + Node n = d_qe->getInstantiate()->getInstantiation(f, vars, terms); Node val = fm->getValue( n ); if (val != d_qe->getTermUtil()->d_true) { @@ -322,7 +323,8 @@ int QModelBuilderIG::initializeQuantifier(Node f, Node fp, FirstOrderModel* fm) //try to add it Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; //add model basis instantiation - if( d_qe->addInstantiation( fp, d_quant_basis_match[f] ) ){ + if (d_qe->getInstantiate()->addInstantiation(fp, d_quant_basis_match[f])) + { d_quant_basis_match_added[f] = true; return 1; }else{ @@ -428,6 +430,9 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; fmig->resetEvaluate(); Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; + EqualityQuery* qy = d_qe->getEqualityQuery(); + Instantiate* inst = d_qe->getInstantiate(); + TermUtil* util = d_qe->getTermUtil(); while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ d_triedLemmas++; if( Debug.isOn("inst-fmf-ei-debug") ){ @@ -446,8 +451,9 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in //if evaluate(...)==1, then the instantiation is already true in the model // depIndex is the index of the least significant variable that this evaluation relies upon depIndex = riter.getNumTerms()-1; - Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermUtil()->getInstConstantBody( f ) << std::endl; - eval = fmig->evaluate( d_qe->getTermUtil()->getInstConstantBody( f ), depIndex, &riter ); + Debug("fmf-model-eval") << "We will evaluate " + << util->getInstConstantBody(f) << std::endl; + eval = fmig->evaluate(util->getInstConstantBody(f), depIndex, &riter); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; }else{ @@ -461,11 +467,12 @@ int QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, in InstMatch m( f ); for (unsigned i = 0; i < riter.getNumTerms(); i++) { - m.set( d_qe, i, riter.getCurrentTerm( i ) ); + m.set(qy, i, riter.getCurrentTerm(i)); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; //add as instantiation - if( d_qe->addInstantiation( f, m, true ) ){ + if (inst->addInstantiation(f, m, true)) + { d_addedLemmas++; if( d_qe->inConflict() ){ break; diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 5d01e04e6..fe6e3945b 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -18,6 +18,7 @@ #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" @@ -285,17 +286,20 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if( !riter.isIncomplete() ){ int triedLemmas = 0; int addedLemmas = 0; + EqualityQuery* qy = d_quantEngine->getEqualityQuery(); + Instantiate* inst = d_quantEngine->getInstantiate(); while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); for (unsigned i = 0; i < riter.getNumTerms(); i++) { - m.set( d_quantEngine, i, riter.getCurrentTerm( i ) ); + m.set(qy, i, riter.getCurrentTerm(i)); } Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl; triedLemmas++; //add as instantiation - if( d_quantEngine->addInstantiation( f, m, true ) ){ + if (inst->addInstantiation(f, m, true)) + { addedLemmas++; if( d_quantEngine->inConflict() ){ break; diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 9ed4e5996..6c2b95a52 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -19,11 +19,12 @@ #include "options/quantifiers_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/first_order_model.h" #include "theory/theory_engine.h" using namespace CVC4::kind; @@ -586,7 +587,8 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node return true; } }else{ - Node inst = p->d_quantEngine->getInstantiation( d_q, terms ); + Node inst = + p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms); Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, NULL, options::qcfTConstraint() ); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; @@ -2111,13 +2113,16 @@ void QuantConflictFind::check(Theory::Effort level, QEffort quant_e) if( !tcs ){ //for debugging if( Debug.isOn("qcf-check-inst") ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); + Node inst = d_quantEngine->getInstantiate() + ->getInstantiation(q, terms); Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; Assert( !getTermDatabase()->isEntailed( inst, true ) ); Assert(getTermDatabase()->isEntailed(inst, false) || e > EFFORT_CONFLICT); } - if( d_quantEngine->addInstantiation( q, terms ) ){ + if (d_quantEngine->getInstantiate()->addInstantiation( + q, terms)) + { Trace("qcf-check") << " ... Added instantiation" << std::endl; Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; qi->debugPrintMatch("qcf-inst"); diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index f958605b1..b1bba1842 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -167,14 +167,19 @@ public: /* reset * Called at the beginning of an instantiation round * Returns false if the reset failed. When reset fails, the utility should have - * added a lemma - * via a call to qe->addLemma. TODO: improve this contract #1163 + * added a lemma via a call to qe->addLemma. TODO: improve this contract #1163 */ virtual bool reset( Theory::Effort e ) = 0; /* Called for new quantifiers */ virtual void registerQuantifier(Node q) = 0; /** Identify this module (for debugging, dynamic configuration, etc..) */ virtual std::string identify() const = 0; + /** Check complete? + * + * Returns false if the utility's reasoning was globally incomplete + * (e.g. "sat" must be replaced with "incomplete"). + */ + virtual bool checkComplete() { return true; } }; /** Arithmetic utilities regarding monomial sums. diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index d02ad667e..92d42d578 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -388,6 +388,44 @@ Node QuantAttributes::getQuantIdNumNode( Node q ) { } } +void QuantAttributes::setInstantiationLevelAttr(Node n, Node qn, uint64_t level) +{ + Trace("inst-level-debug2") << "IL : " << n << " " << qn << " " << level + << std::endl; + // if not from the vector of terms we instantiatied + if (qn.getKind() != BOUND_VARIABLE && n != qn) + { + // if this is a new term, without an instantiation level + if (!n.hasAttribute(InstLevelAttribute())) + { + InstLevelAttribute ila; + n.setAttribute(ila, level); + Trace("inst-level-debug") << "Set instantiation level " << n << " to " + << level << std::endl; + Assert(n.getNumChildren() == qn.getNumChildren()); + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + setInstantiationLevelAttr(n[i], qn[i], level); + } + } + } +} + +void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level) +{ + if (!n.hasAttribute(InstLevelAttribute())) + { + InstLevelAttribute ila; + n.setAttribute(ila, level); + Trace("inst-level-debug") << "Set instantiation level " << n << " to " + << level << std::endl; + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + setInstantiationLevelAttr(n[i], level); + } + } +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 9a18d13fb..87315de7c 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -55,6 +55,11 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; struct SynthesisAttributeId {}; typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; +struct InstLevelAttributeId +{ +}; +typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; + /** Attribute for setting printing information for sygus variables * * For variable d of sygus datatype type, if @@ -185,7 +190,12 @@ public: /** get quant id num */ Node getQuantIdNumNode( Node q ); -private: + /** set instantiation level attr */ + static void setInstantiationLevelAttr(Node n, uint64_t level); + /** set instantiation level attr */ + static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level); + + private: /** pointer to quantifiers engine */ QuantifiersEngine * d_quantEngine; /** cache of attributes */ diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 337d61976..922a8cce6 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -19,10 +19,11 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quant_conflict_find.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/theory_engine.h" @@ -159,7 +160,8 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) { if( inst.size()>f[0].getNumChildren() ){ inst.resize( f[0].getNumChildren() ); } - if( d_quantEngine->addInstantiation( f, inst ) ){ + if (d_quantEngine->getInstantiate()->addInstantiation(f, inst)) + { addedLemmas++; tempAddedLemmas++; /* diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 2f210cc20..555058d98 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/skolemize.h" #include "options/quantifiers_options.h" +#include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/sort_inference.h" @@ -286,7 +287,7 @@ Node Skolemize::mkSkolemizedBody(Node f, // if it has an instantiation level, set the skolemized body to that level if (f.hasAttribute(InstLevelAttribute())) { - theory::QuantifiersEngine::setInstantiationLevelAttr( + QuantAttributes::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute())); } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5db58067f..19cdc68e5 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -186,7 +186,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) << std::endl; if (options::instMaxLevel() != -1) { - QuantifiersEngine::setInstantiationLevelAttr(k, 0); + QuantAttributes::setInstantiationLevelAttr(k, 0); } d_type_fv[tn] = k; return k; diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 5ac21dafb..ed6cd018f 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -34,9 +34,6 @@ typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute; struct BoundVarAttributeId {}; typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute; -struct InstLevelAttributeId {}; -typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; - struct InstVarNumAttributeId {}; typedef expr::Attribute<InstVarNumAttributeId, uint64_t> InstVarNumAttribute; @@ -97,13 +94,16 @@ namespace inst{ namespace quantifiers { class TermDatabase; +class Instantiate; // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used. class TermUtil : public QuantifiersUtil { // TODO : remove these friend class ::CVC4::theory::QuantifiersEngine; -private: + friend class Instantiate; + + private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; public: diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index b72f6c8cb..61920250e 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -16,6 +16,7 @@ #include "theory/quantifiers/candidate_generator.h" #include "theory/quantifiers/ho_trigger.h" #include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" @@ -119,7 +120,7 @@ int Trigger::addInstantiations(InstMatch& baseMatch) bool Trigger::sendInstantiation(InstMatch& m) { - return d_quantEngine->addInstantiation(d_f, m); + return d_quantEngine->getInstantiate()->addInstantiation(d_f, m); } bool Trigger::mkTriggerTerms( Node q, std::vector< Node >& nodes, unsigned n_vars, std::vector< Node >& trNodes ) { |