From 3ab0db55341e7e752411bb003fb203fcd9ec9120 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 24 Nov 2017 19:08:41 -0600 Subject: [PATCH] (Refactor) Instantiate utility (#1387) --- src/Makefile.am | 4 + src/theory/quantifiers/ambqi_builder.cpp | 4 +- .../quantifiers/candidate_generator.cpp | 5 +- .../quantifiers/ce_guided_conjecture.cpp | 7 +- src/theory/quantifiers/ce_guided_single_inv.h | 1 + src/theory/quantifiers/equality_query.cpp | 3 +- src/theory/quantifiers/full_model_check.cpp | 9 +- src/theory/quantifiers/ho_trigger.cpp | 5 +- src/theory/quantifiers/inst_match.cpp | 420 +-------- src/theory/quantifiers/inst_match.h | 216 +---- .../quantifiers/inst_match_generator.cpp | 20 +- src/theory/quantifiers/inst_match_generator.h | 2 +- src/theory/quantifiers/inst_match_trie.cpp | 527 +++++++++++ src/theory/quantifiers/inst_match_trie.h | 439 ++++++++++ src/theory/quantifiers/inst_propagator.cpp | 7 +- src/theory/quantifiers/inst_propagator.h | 5 +- src/theory/quantifiers/inst_strategy_cbqi.cpp | 8 +- .../quantifiers/inst_strategy_enumerative.cpp | 3 +- src/theory/quantifiers/instantiate.cpp | 821 ++++++++++++++++++ src/theory/quantifiers/instantiate.h | 377 ++++++++ src/theory/quantifiers/model_builder.cpp | 19 +- src/theory/quantifiers/model_engine.cpp | 8 +- .../quantifiers/quant_conflict_find.cpp | 13 +- src/theory/quantifiers/quant_util.h | 9 +- .../quantifiers/quantifiers_attributes.cpp | 38 + .../quantifiers/quantifiers_attributes.h | 12 +- src/theory/quantifiers/rewrite_engine.cpp | 6 +- src/theory/quantifiers/skolemize.cpp | 3 +- src/theory/quantifiers/term_database.cpp | 2 +- src/theory/quantifiers/term_util.h | 8 +- src/theory/quantifiers/trigger.cpp | 3 +- src/theory/quantifiers_engine.cpp | 695 ++------------- src/theory/quantifiers_engine.h | 105 +-- 33 files changed, 2493 insertions(+), 1311 deletions(-) create mode 100644 src/theory/quantifiers/inst_match_trie.cpp create mode 100644 src/theory/quantifiers/inst_match_trie.h create mode 100644 src/theory/quantifiers/instantiate.cpp create mode 100644 src/theory/quantifiers/instantiate.h diff --git a/src/Makefile.am b/src/Makefile.am index b3c4ec98c..f50893497 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -395,8 +395,12 @@ libcvc4_la_SOURCES = \ theory/quantifiers/fun_def_process.h \ theory/quantifiers/ho_trigger.cpp \ theory/quantifiers/ho_trigger.h \ + theory/quantifiers/instantiate.cpp \ + theory/quantifiers/instantiate.h \ theory/quantifiers/inst_match.cpp \ theory/quantifiers/inst_match.h \ + theory/quantifiers/inst_match_trie.cpp \ + theory/quantifiers/inst_match_trie.h \ theory/quantifiers/inst_match_generator.cpp \ theory/quantifiers/inst_match_generator.h \ theory/quantifiers/inst_propagator.cpp \ 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 #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; id_vals.begin(), m->d_vals.end() ); } -bool InstMatch::add( InstMatch& m ){ - for( unsigned i=0; i " << d_vals[i] << std::endl; } @@ -71,8 +73,10 @@ void InstMatch::debugPrint( const char* c ){ } bool InstMatch::isComplete() { - for( unsigned i=0; igetEqualityQuery()->getEngine()->hasTerm( d_vals[i] ) ){ - d_vals[i] = qe->getEqualityQuery()->getEngine()->getRepresentative( d_vals[i] ); - } - } - } -} - -void InstMatch::applyRewrite(){ - for( unsigned i=0; i& inst ){ - for( size_t i=0; i& 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; i0 ){ 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; i0 ) 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 +#include -#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 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& 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 +#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& 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::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::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& 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::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& 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::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& terms, + bool& firstTime, + bool useActive, + std::vector& 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& 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& insts, + Node q, + std::vector& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector& 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& 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& terms, + const std::vector& lems, + std::map& quant, + std::map >& 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& d : d_data) + { + terms.push_back(d.first); + d.second.getExplanationForInstLemmas(q, terms, lems, quant, tvec); + terms.pop_back(); + } + } +} + +CDInstMatchTrie::~CDInstMatchTrie() +{ + for (std::pair& d : d_data) + { + CDInstMatchTrie* current = d.second; + delete current; + } + d_data.clear(); +} + +bool CDInstMatchTrie::addInstMatch(QuantifiersEngine* qe, + Node f, + std::vector& 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::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::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& m, + unsigned index) +{ + if (index == q[0].getNumChildren()) + { + if (d_valid.get()) + { + d_valid.set(false); + return true; + } + return false; + } + std::map::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& m, + Node lem, + unsigned index) +{ + if (index == q[0].getNumChildren()) + { + if (d_valid.get()) + { + setInstLemma(lem); + return true; + } + return false; + } + std::map::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& terms, + bool& firstTime, + bool useActive, + std::vector& 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& 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& insts, + Node q, + std::vector& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector& 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& 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& terms, + const std::vector& lems, + std::map& quant, + std::map >& 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& 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 + +#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 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& 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& 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& 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& 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& insts, + Node q, + QuantifiersEngine* qe, + bool useActive, + std::vector& active) + { + std::vector 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& lems, + std::map& quant, + std::map >& tvec) const + { + std::vector 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& active) const + { + std::vector terms; + print(out, q, terms, firstTime, useActive, active); + } + /** the data */ + std::map 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& terms, + bool& firstTime, + bool useActive, + std::vector& active) const; + /** helper for get instantiations + * terms accumulates the path we are on in the trie. + */ + void getInstantiations(std::vector& insts, + Node q, + std::vector& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector& 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& terms, + const std::vector& lems, + std::map& quant, + std::map >& 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& 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& 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& 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& 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& insts, + Node q, + QuantifiersEngine* qe, + bool useActive, + std::vector& active) + { + std::vector 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& lems, + std::map& quant, + std::map >& tvec) const + { + std::vector terms; + getExplanationForInstLemmas(q, terms, lems, quant, tvec); + } + + /** print this class */ + void print(std::ostream& out, + Node q, + bool& firstTime, + bool useActive, + std::vector& active) const + { + std::vector terms; + print(out, q, terms, firstTime, useActive, active); + } + + private: + /** the data */ + std::map d_data; + /** is valid */ + context::CDO d_valid; + /** helper for print + * terms accumulates the path we are on in the trie. + */ + void print(std::ostream& out, + Node q, + std::vector& terms, + bool& firstTime, + bool useActive, + std::vector& active) const; + /** helper for get instantiations + * terms accumulates the path we are on in the trie. + */ + void getInstantiations(std::vector& insts, + Node q, + std::vector& terms, + QuantifiersEngine* qe, + bool useActive, + std::vector& 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& terms, + const std::vector& lems, + std::map& quant, + std::map >& 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 #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 +#include #include #include -#include #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& 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 >& 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& 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 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()) + { + 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 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& 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& terms, + bool modEq, + bool addedLem) +{ + return recordInstantiationInternal(q, terms, modEq, addedLem); +} + +bool Instantiate::existsInstantiation(Node q, + std::vector& terms, + bool modEq) +{ + if (options::incrementalSolving()) + { + std::map::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::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& vars, + std::vector& 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& 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& terms, + bool modEq, + bool addedLem) +{ + if (!addedLem) + { + // record the instantiation for deletion later + d_recorded_inst.push_back(std::pair >(q, terms)); + } + if (options::incrementalSolving()) + { + Trace("inst-add-debug") + << "Adding into context-dependent inst trie, modEq = " << modEq + << std::endl; + inst::CDInstMatchTrie* imt; + std::map::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& terms) +{ + if (options::incrementalSolving()) + { + std::map::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 active_lemmas; + if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas)) + { + useUnsatCore = true; + } + bool printed = false; + if (options::incrementalSolving()) + { + for (std::pair& 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& 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& qs) +{ + if (options::incrementalSolving()) + { + for (context::CDHashSet::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& t : d_inst_match_trie) + { + qs.push_back(t.first); + } + } +} + +bool Instantiate::getUnsatCoreLemmas(std::vector& 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& active_lemmas, + std::map& 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 >& tvecs) +{ + std::vector lemmas; + getInstantiations(q, lemmas); + std::map quant; + std::map > tvec; + getExplanationForInstLemmas(lemmas, quant, tvec); + for (std::pair >& t : tvec) + { + tvecs.push_back(t.second); + } +} + +void Instantiate::getInstantiationTermVectors( + std::map > >& insts) +{ + if (options::incrementalSolving()) + { + for (std::pair& t : d_c_inst_match_trie) + { + getInstantiationTermVectors(t.first, insts[t.first]); + } + } + else + { + for (std::pair& t : d_inst_match_trie) + { + getInstantiationTermVectors(t.first, insts[t.first]); + } + } +} + +void Instantiate::getExplanationForInstLemmas( + const std::vector& lems, + std::map& quant, + std::map >& tvec) +{ + if (options::trackInstLemmas()) + { + if (options::incrementalSolving()) + { + for (std::pair& t : + d_c_inst_match_trie) + { + t.second->getExplanationForInstLemmas(t.first, lems, quant, tvec); + } + } + else + { + for (std::pair& 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 >& insts) +{ + bool useUnsatCore = false; + std::vector active_lemmas; + if (options::trackInstLemmas() && getUnsatCoreLemmas(active_lemmas)) + { + useUnsatCore = true; + } + + if (options::incrementalSolving()) + { + for (std::pair& t : d_c_inst_match_trie) + { + t.second->getInstantiations( + insts[t.first], t.first, d_qe, useUnsatCore, active_lemmas); + } + } + else + { + for (std::pair& 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& insts) +{ + if (options::incrementalSolving()) + { + std::map::iterator it = + d_c_inst_match_trie.find(q); + if (it != d_c_inst_match_trie.end()) + { + std::vector active_lemmas; + it->second->getInstantiations( + insts, it->first, d_qe, false, active_lemmas); + } + } + else + { + std::map::iterator it = + d_inst_match_trie.find(q); + if (it != d_inst_match_trie.end()) + { + std::vector active_lemmas; + it->second.getInstantiations( + insts, it->first, d_qe, false, active_lemmas); + } + } +} + +Node Instantiate::getInstantiatedConjunction(Node q) +{ + Assert(q.getKind() == FORALL); + std::vector 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& 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& 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 + +#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& 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& 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& 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& 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& 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& vars, + std::vector& 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& 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& 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& 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 >& 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 >& 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 > >& 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& 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& active_lemmas, + std::map& weak_imp); + /** get explanation for instantiation lemmas + * + * + */ + void getExplanationForInstLemmas(const std::vector& lems, + std::map& quant, + std::map >& 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& terms, + bool modEq = false, + bool addedLem = true); + /** remove instantiation from the cache */ + bool removeInstantiationInternal(Node q, std::vector& 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 d_inst_notify; + + /** statistics for debugging total instantiation */ + int d_total_inst_count_debug; + /** statistics for debugging total instantiations per quantifier */ + std::map d_total_inst_debug; + /** statistics for debugging total instantiations per quantifier per round */ + std::map 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 d_inst_match_trie; + std::map d_c_inst_match_trie; + /** + * The list of quantified formulas for which the domain of d_c_inst_match_trie + * is valid. + */ + context::CDHashSet 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 > > 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 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 InstConstantAttribute; struct BoundVarAttributeId {}; typedef expr::Attribute BoundVarAttribute; -struct InstLevelAttributeId {}; -typedef expr::Attribute InstLevelAttribute; - struct InstVarNumAttributeId {}; typedef expr::Attribute 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 ) { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index bc2b533be..59a85de1f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -35,6 +35,7 @@ #include "theory/quantifiers/inst_strategy_cbqi.h" #include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_strategy_enumerative.h" +#include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/model_engine.h" @@ -71,6 +72,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te) : d_te(te), d_quant_attr(new quantifiers::QuantAttributes(this)), + d_instantiate(new quantifiers::Instantiate(this, u)), d_skolemize(new quantifiers::Skolemize(this, u)), d_term_enum(new quantifiers::TermEnumeration), d_conflict_c(c, false), @@ -108,7 +110,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, // notice that this option is incompatible with options::qcfAllConflict() d_inst_prop = new quantifiers::InstPropagator( this ); d_util.push_back( d_inst_prop ); - d_inst_notify.push_back( d_inst_prop->getInstantiationNotify() ); + d_instantiate->addNotify(d_inst_prop->getInstantiationNotify()); }else{ d_inst_prop = NULL; } @@ -119,6 +121,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_eq_inference = NULL; } + d_util.push_back(d_instantiate.get()); + d_tr_trie = new inst::TriggerTrie; d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; d_conflict = false; @@ -165,7 +169,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, d_bv_invert = NULL; d_builder = NULL; - d_total_inst_count_debug = 0; //allow theory combination to go first, once initially d_ierCounter = options::instWhenTcFirst() ? 0 : 1; d_ierCounter_c = d_ierCounter; @@ -175,14 +178,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, } QuantifiersEngine::~QuantifiersEngine(){ - for(std::map< Node, inst::CDInstMatchTrie* >::iterator - i = d_c_inst_match_trie.begin(), iend = d_c_inst_match_trie.end(); - i != iend; ++i) - { - delete (*i).second; - } - d_c_inst_match_trie.clear(); - delete d_alpha_equiv; delete d_builder; delete d_qepr; @@ -406,7 +401,8 @@ void QuantifiersEngine::ppNotifyAssertions( d_qepr != NULL) { for (unsigned i = 0; i < assertions.size(); i++) { if (options::instLevelInputOnly() && options::instMaxLevel() != -1) { - setInstantiationLevelAttr(assertions[i], 0); + quantifiers::QuantAttributes::setInstantiationLevelAttr(assertions[i], + 0); } if (d_qepr != NULL) { d_qepr->registerAssertion(assertions[i]); @@ -448,13 +444,15 @@ void QuantifiersEngine::check( Theory::Effort e ){ std::vector< QuantifiersModule* > qm; if( d_model->checkNeeded() ){ needsCheck = needsCheck || e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call - for( unsigned i=0; ineedsCheck( e ) ){ - qm.push_back( d_modules[i] ); + for (QuantifiersModule*& mdl : d_modules) + { + if (mdl->needsCheck(e)) + { + qm.push_back(mdl); needsCheck = true; //can only request model at last call since theory combination can find inconsistencies if( e>=Theory::EFFORT_LAST_CALL ){ - QuantifiersModule::QEffort me = d_modules[i]->needsModel(e); + QuantifiersModule::QEffort me = mdl->needsModel(e); needsModelE = meidentify().c_str() << "..." << std::endl; - if( !d_util[i]->reset( e ) ){ + for (QuantifiersUtil*& util : d_util) + { + Trace("quant-engine-debug2") << "Reset " << util->identify().c_str() + << "..." << std::endl; + if (!util->reset(e)) + { flushLemmas(); if( d_hasAddedLemma ){ return; @@ -539,9 +532,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ //reset the modules Trace("quant-engine-debug") << "Resetting all modules..." << std::endl; - for( unsigned i=0; iidentify().c_str() << std::endl; - d_modules[i]->reset_round( e ); + for (QuantifiersModule*& mdl : d_modules) + { + Trace("quant-engine-debug2") << "Reset " << mdl->identify().c_str() + << std::endl; + mdl->reset_round(e); } Trace("quant-engine-debug") << "Done resetting all modules." << std::endl; //reset may have added lemmas @@ -579,9 +574,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ } if( !d_hasAddedLemma ){ //check each module - for( unsigned i=0; iidentify().c_str() << " at effort " << quant_e << "..." << std::endl; - qm[i]->check( e, quant_e ); + for (QuantifiersModule*& mdl : qm) + { + Trace("quant-engine-debug") << "Check " << mdl->identify().c_str() + << " at effort " << quant_e << "..." + << std::endl; + mdl->check(e, quant_e); if( d_conflict ){ Trace("quant-engine-debug") << "...conflict!" << std::endl; break; @@ -612,17 +610,27 @@ void QuantifiersEngine::check( Theory::Effort e ){ { if( e==Theory::EFFORT_LAST_CALL ){ //sources of incompleteness - if( !d_recorded_inst.empty() ){ - Trace("quant-engine-debug") << "Set incomplete due to recorded instantiations." << std::endl; - setIncomplete = true; + for (QuantifiersUtil*& util : d_util) + { + if (!util->checkComplete()) + { + Trace("quant-engine-debug") << "Set incomplete because utility " + << util->identify().c_str() + << " was incomplete." << std::endl; + setIncomplete = true; + } } //if we have a chance not to set incomplete if( !setIncomplete ){ - setIncomplete = false; //check if we should set the incomplete flag - for( unsigned i=0; icheckComplete() ){ - Trace("quant-engine-debug") << "Set incomplete because " << d_modules[i]->identify().c_str() << " was incomplete." << std::endl; + for (QuantifiersModule*& mdl : d_modules) + { + if (!mdl->checkComplete()) + { + Trace("quant-engine-debug") + << "Set incomplete because module " + << mdl->identify().c_str() << " was incomplete." + << std::endl; setIncomplete = true; break; } @@ -666,13 +674,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ d_curr_effort_level = QuantifiersModule::QEFFORT_NONE; Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; if( d_hasAddedLemma ){ - //debug information - if( Trace.isOn("inst-per-quant-round") ){ - for( std::map< Node, int >::iterator it = d_temp_inst_debug.begin(); it != d_temp_inst_debug.end(); ++it ){ - Trace("inst-per-quant-round") << " * " << it->second << " for " << it->first << std::endl; - d_temp_inst_debug[it->first] = 0; - } - } + d_instantiate->debugPrint(); } if( Trace.isOn("quant-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); @@ -703,11 +705,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ getOutputChannel().setIncomplete(); } //output debug stats - if( Trace.isOn("inst-per-quant") ){ - for( std::map< Node, int >::iterator it = d_total_inst_debug.begin(); it != d_total_inst_debug.end(); ++it ){ - Trace("inst-per-quant") << " * " << it->second << " for " << it->first << std::endl; - } - } + d_instantiate->debugPrintModel(); } } @@ -907,192 +905,6 @@ void QuantifiersEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { //} } -void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){ - for( size_t i=0; i& 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 CDInstMatchTrie( getUserContext() ); - d_c_inst_match_trie[q] = imt; - } - return imt->addInstMatch( this, q, terms, getUserContext(), modEq ); - }else{ - Trace("inst-add-debug") << "Adding into inst trie" << std::endl; - return d_inst_match_trie[q].addInstMatch( this, q, terms, modEq ); - } -} - -bool QuantifiersEngine::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( this, q, terms ); - }else{ - return false; - } - }else{ - return d_inst_match_trie[q].removeInstMatch( this, q, terms ); - } -} - -void QuantifiersEngine::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& terms, std::map< Node, Node >& visited ){ - std::map< Node, Node >::iterator itv = visited.find( n ); - if( itv==visited.end() ){ - Node ret = n; - if( n.getKind()==INST_CONSTANT ){ - Debug("check-inst") << "Substitute inst constant : " << n << std::endl; - ret = terms[n.getAttribute(InstVarNumAttribute())]; - }else{ - //if( !quantifiers::TermUtil::hasInstConstAttr( n ) ){ - //Debug("check-inst") << "No inst const attr : " << n << std::endl; - //return n; - //}else{ - //Debug("check-inst") << "Recurse on : " << n << std::endl; - std::vector< Node > cc; - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - cc.push_back( n.getOperator() ); - } - bool changed = false; - for( unsigned i=0; imkNode( n.getKind(), cc ); - } - } - visited[n] = ret; - return ret; - }else{ - return itv->second; - } -} - - -Node QuantifiersEngine::getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts ){ - Node body; - Assert( vars.size()==terms.size() ); - //process partial instantiation if necessary - if( q[0].getNumChildren()!=vars.size() ){ - body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - std::vector< Node > uninst_vars; - //doing a partial instantiation, must add quantifier for all uninstantiated variables - for( unsigned i=0; imkNode( BOUND_VAR_LIST, uninst_vars ); - body = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); - Trace("partial-inst") << "Partial instantiation : " << q << std::endl; - Trace("partial-inst") << " : " << body << std::endl; - }else{ - if( options::cbqi() ){ - body = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - }else{ - //do optimized version - Node icb = d_term_util->getInstConstantBody( q ); - std::map< Node, Node > visited; - body = getSubstitute( icb, terms, visited ); - if( Debug.isOn("check-inst") ){ - Node body2 = q[ 1 ].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); - if( body!=body2 ){ - Debug("check-inst") << "Substitution is wrong : " << body << " " << body2 << std::endl; - } - } - } - } - 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 QuantifiersEngine::getInstantiation( Node q, InstMatch& m, bool doVts ){ - std::vector< Node > vars; - std::vector< Node > terms; - computeTermVector( q, m, vars, terms ); - return getInstantiation( q, vars, terms, doVts ); -} - -Node QuantifiersEngine::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 QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq ){ - if( options::incrementalSolving() ){ - if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){ - if( d_c_inst_match_trie[f]->existsInstMatch( this, f, m, getUserContext(), modEq ) ){ - return true; - } - } - }else{ - if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){ - if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq ) ){ - return true; - } - } - } - return false; -} -*/ - bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ if( doCache ){ if( doRewrite ){ @@ -1132,217 +944,6 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } -bool QuantifiersEngine::addInstantiation( Node q, InstMatch& m, bool mkRep, bool modEq, bool doVts ){ - std::vector< Node > terms; - m.getTerms( q, terms ); - return addInstantiation( q, terms, mkRep, modEq, doVts ); -} - -bool QuantifiersEngine::addInstantiation( Node q, std::vector< Node >& terms, bool mkRep, bool modEq, bool doVts ) { - // For resource-limiting (also does a time check). - getOutputChannel().safePoint(options::quantifierStep()); - Assert( !d_conflict ); - Assert( terms.size()==q[0].getNumChildren() ); - Trace("inst-add-debug") << "For quantified formula " << q << ", add instantiation: " << std::endl; - std::vector< Node > rlv_cond; - for( unsigned i=0; i " << 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] = 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; - }else{ - //get relevancy conditions - if( options::instRelevantCond() ){ - quantifiers::TermUtil::getRelevancyCondition( terms[i], rlv_cond ); - } - } -#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; jisTermEligibleForInstantiation( terms[i], q, true ) ){ - return false; - } - } - } - - //check for positive entailment - if( options::instNoEntail() ){ - //TODO: check consistency of equality engine (if not aborting on utility's reset) - std::map< TNode, TNode > subs; - for( unsigned i=0; iisEntailed( q[1], subs, false, true ) ){ - Trace("inst-add-debug") << " --> Currently entailed." << std::endl; - ++(d_statistics.d_inst_duplicate_ent); - return false; - } - //Node eval = d_term_db->evaluateTerm( q[1], subs, false, true ); - //Trace("inst-add-debug2") << "Instantiation evaluates to : " << std::endl; - //Trace("inst-add-debug2") << " " << eval << std::endl; - } - - //check for term vector duplication - bool alreadyExists = !recordInstantiationInternal( q, terms, modEq ); - if( alreadyExists ){ - Trace("inst-add-debug") << " --> Already exists." << 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() ); - Node body = getInstantiation( q, d_term_util->d_vars[q], terms, doVts ); //do virtual term substitution - Node orig_body = body; - if( options::cbqiNestedQE() && d_i_cbqi ){ - body = d_i_cbqi->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; - body = Rewriter::rewrite(body); - - if( d_useModelEe && options::instNoModelTrue() ){ - Node val_body = d_model->getValue( body ); - if( val_body==d_term_util->d_true ){ - Trace("inst-add-debug") << " --> True in model." << std::endl; - ++(d_statistics.d_inst_duplicate_model_true); - return false; - } - } - - Node lem; - if( rlv_cond.empty() ){ - lem = NodeManager::currentNM()->mkNode( kind::OR, q.negate(), body ); - }else{ - rlv_cond.push_back( q.negate() ); - rlv_cond.push_back( body ); - lem = NodeManager::currentNM()->mkNode( kind::OR, rlv_cond ); - } - lem = Rewriter::rewrite(lem); - - //check for lemma duplication - if( addLemma( lem, true, 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; imaxInstLevel ){ - maxInstLevel = terms[i].getAttribute(InstLevelAttribute()); - } - } - } - setInstantiationLevelAttr( orig_body, q[1], maxInstLevel+1 ); - } - } - if (d_curr_effort_level > QuantifiersModule::QEFFORT_CONFLICT - && d_curr_effort_level < QuantifiersModule::QEFFORT_NONE) - { - //notify listeners - for( unsigned j=0; jnotifyInstantiation( d_curr_effort_level, q, lem, terms, body ) ){ - Trace("inst-add-debug") << "...we are in conflict." << std::endl; - setConflict(); - Assert( !d_lemmas_waiting.empty() ); - 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; - }else{ - Trace("inst-add-debug") << " --> Lemma already exists." << std::endl; - ++(d_statistics.d_inst_duplicate); - return false; - } -} - -bool QuantifiersEngine::removeInstantiation( Node q, Node lem, std::vector< Node >& terms ) { - //lem must occur in d_waiting_lemmas - if( removeLemma( lem ) ){ - return removeInstantiationInternal( q, terms ); - }else{ - return false; - } -} - bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ n = Rewriter::rewrite( n ); Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() ); @@ -1419,11 +1020,10 @@ quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() { void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ //filter based on notify classes - if( !d_inst_notify.empty() ){ + if (d_instantiate->hasNotify()) + { unsigned prev_lem_sz = d_lemmas_waiting.size(); - for( unsigned j=0; jfilterInstantiations(); - } + d_instantiate->notifyFlushLemmas(); if( prev_lem_sz!=d_lemmas_waiting.size() ){ Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl; } @@ -1446,94 +1046,30 @@ void QuantifiersEngine::flushLemmas(){ } bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas ) { - //only if unsat core available - bool isUnsatCoreAvailable = false; - if( options::proof() ){ - isUnsatCoreAvailable = ProofManager::currentPM()->unsatCoreAvailable(); - } - if( isUnsatCoreAvailable ){ - 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 (unsigned i = 0; i < active_lemmas.size(); ++i) { - Trace("inst-unsat-core") << " " << active_lemmas[i] << std::endl; - } - Trace("inst-unsat-core") << std::endl; - } - return true; - }else{ - return false; - } + return d_instantiate->getUnsatCoreLemmas(active_lemmas); } bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ) { - if( getUnsatCoreLemmas( active_lemmas ) ){ - for (unsigned i = 0; i < active_lemmas.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; - }else{ - return false; - } + return d_instantiate->getUnsatCoreLemmas(active_lemmas, weak_imp); } void QuantifiersEngine::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::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){ - tvecs.push_back( it->second ); - } + d_instantiate->getInstantiationTermVectors(q, tvecs); } void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { - if( options::incrementalSolving() ){ - for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - getInstantiationTermVectors( it->first, insts[it->first] ); - } - }else{ - for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - getInstantiationTermVectors( it->first, insts[it->first] ); - } - } + d_instantiate->getInstantiationTermVectors(insts); } -void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) { - if( options::trackInstLemmas() ){ - if( options::incrementalSolving() ){ - for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - it->second->getExplanationForInstLemmas( it->first, lems, quant, tvec ); - } - }else{ - for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - it->second.getExplanationForInstLemmas( it->first, lems, quant, tvec ); - } - } -#ifdef CVC4_ASSERTIONS - for( unsigned j=0; j& lems, + std::map& quant, + std::map >& tvec) +{ + d_instantiate->getExplanationForInstLemmas(lems, quant, tvec); } void QuantifiersEngine::printInstantiations( std::ostream& out ) { - bool useUnsatCore = false; - std::vector< Node > active_lemmas; - if( options::trackInstLemmas() && getUnsatCoreLemmas( active_lemmas ) ){ - useUnsatCore = true; - } - bool printed = false; // print the skolemizations if (d_skolemize->printSkolemization(out)) @@ -1541,24 +1077,9 @@ void QuantifiersEngine::printInstantiations( std::ostream& out ) { printed = true; } // print the instantiations - if( options::incrementalSolving() ){ - for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - bool firstTime = true; - it->second->print( out, it->first, firstTime, useUnsatCore, active_lemmas ); - if( !firstTime ){ - out << ")" << std::endl; - } - printed = printed || !firstTime; - } - }else{ - for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - bool firstTime = true; - it->second.print( out, it->first, firstTime, useUnsatCore, active_lemmas ); - if( !firstTime ){ - out << ")" << std::endl; - } - printed = printed || !firstTime; - } + if (d_instantiate->printInstantiations(out)) + { + printed = true; } if( !printed ){ out << "No instantiations" << std::endl; @@ -1574,70 +1095,19 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { - if( options::incrementalSolving() ){ - for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - qs.push_back( it->first ); - } - }else{ - for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - qs.push_back( it->first ); - } - } + d_instantiate->getInstantiatedQuantifiedFormulas(qs); } void QuantifiersEngine::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::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ - it->second->getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas ); - } - }else{ - for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ - it->second.getInstantiations( insts[it->first], it->first, this, useUnsatCore, active_lemmas ); - } - } + d_instantiate->getInstantiations(insts); } void QuantifiersEngine::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, this, 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, this, false, active_lemmas ); - } - } + d_instantiate->getInstantiations(q, insts); } Node QuantifiersEngine::getInstantiatedConjunction( Node q ) { - Assert( q.getKind()==FORALL ); - std::vector< Node > insts; - getInstantiations( q, insts ); - if( insts.empty() ){ - return NodeManager::currentNM()->mkConst(true); - }else{ - Node ret; - if( insts.size()==1 ){ - ret = insts[0]; - }else{ - ret = NodeManager::currentNM()->mkNode( kind::AND, insts ); - } - //have to remove q, TODO: avoid this in a better way - TNode tq = q; - TNode tt = d_term_util->d_true; - ret = ret.substitute( tq, tt ); - return ret; - } + return d_instantiate->getInstantiatedConjunction(q); } QuantifiersEngine::Statistics::Statistics() @@ -1647,11 +1117,6 @@ QuantifiersEngine::Statistics::Statistics() d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), d_instantiation_rounds_lc("QuantifiersEngine::Rounds_Instantiation_Last_Call", 0), - d_instantiations("QuantifiersEngine::Instantiations_Total", 0), - d_inst_duplicate("QuantifiersEngine::Duplicate_Inst", 0), - d_inst_duplicate_eq("QuantifiersEngine::Duplicate_Inst_Eq", 0), - d_inst_duplicate_ent("QuantifiersEngine::Duplicate_Inst_Entailed", 0), - d_inst_duplicate_model_true("QuantifiersEngine::Duplicate_Inst_Model_True", 0), d_triggers("QuantifiersEngine::Triggers", 0), d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0), d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0), @@ -1673,11 +1138,6 @@ QuantifiersEngine::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_num_quant); smtStatisticsRegistry()->registerStat(&d_instantiation_rounds); smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc); - 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); smtStatisticsRegistry()->registerStat(&d_triggers); smtStatisticsRegistry()->registerStat(&d_simple_triggers); smtStatisticsRegistry()->registerStat(&d_multi_triggers); @@ -1701,11 +1161,6 @@ QuantifiersEngine::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_num_quant); smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds); smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc); - 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); smtStatisticsRegistry()->unregisterStat(&d_triggers); smtStatisticsRegistry()->unregisterStat(&d_simple_triggers); smtStatisticsRegistry()->unregisterStat(&d_multi_triggers); @@ -1742,18 +1197,6 @@ Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){ return ret; } -Node QuantifiersEngine::getTermForType(TypeNode tn) -{ - if (d_term_enum->isClosedEnumerableType(tn)) - { - return d_term_enum->getEnumerateTerm(tn, 0); - } - else - { - return d_term_db->getOrMakeTypeGroundTerm(tn); - } -} - void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) { eq::EqualityEngine* ee = getActiveEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 37691488e..6c7820cef 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -40,18 +40,6 @@ namespace theory { class QuantifiersEngine; -class InstantiationNotify { -public: - InstantiationNotify(){} - virtual ~InstantiationNotify() {} - virtual bool notifyInstantiation(QuantifiersModule::QEffort quant_e, - Node q, - Node lem, - std::vector& terms, - Node body) = 0; - virtual void filterInstantiations() = 0; -}; - namespace quantifiers { //TODO: organize this more/review this, github issue #1163 //TODO: include these instead of doing forward declarations? #1307 @@ -59,6 +47,7 @@ namespace quantifiers { class TermDb; class TermDbSygus; class TermUtil; + class Instantiate; class Skolemize; class TermEnumeration; class FirstOrderModel; @@ -97,6 +86,7 @@ namespace inst { class QuantifiersEngine { + // TODO: remove these github issue #1163 friend class quantifiers::InstantiationEngine; friend class quantifiers::InstStrategyCbqi; friend class quantifiers::InstStrategyCegqi; @@ -115,8 +105,6 @@ private: std::vector< QuantifiersUtil* > d_util; /** vector of modules for quantifiers */ std::vector< QuantifiersModule* > d_modules; - /** instantiation notify */ - std::vector< InstantiationNotify* > d_inst_notify; /** equality query class */ quantifiers::EqualityQueryQuantifiersEngine* d_eq_query; /** equality inference class */ @@ -141,6 +129,8 @@ private: quantifiers::TermUtil* d_term_util; /** quantifiers attributes */ std::unique_ptr d_quant_attr; + /** instantiate utility */ + std::unique_ptr d_instantiate; /** skolemize utility */ std::unique_ptr d_skolemize; /** term enumeration utility */ @@ -199,19 +189,10 @@ private: std::vector< Node > d_lemmas_waiting; /** phase requirements waiting */ std::map< Node, bool > d_phase_req_waiting; - /** list of all instantiations produced for each quantifier */ - std::map< Node, inst::InstMatchTrie > d_inst_match_trie; - std::map< Node, inst::CDInstMatchTrie* > d_c_inst_match_trie; - /** recorded instantiations */ - std::vector< std::pair< Node, std::vector< Node > > > d_recorded_inst; /** all triggers will be stored in this trie */ inst::TriggerTrie* d_tr_trie; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** statistics for debugging */ - std::map< Node, int > d_total_inst_debug; - std::map< Node, int > d_temp_inst_debug; - int d_total_inst_count_debug; /** inst round counters TODO: make context-dependent? */ context::CDO< int > d_ierCounter_c; int d_ierCounter; @@ -319,37 +300,15 @@ public: private: /** reduceQuantifier, return true if reduced */ bool reduceQuantifier( Node q ); - /** compute term vector */ - void computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ); - /** record instantiation, return true if it was non-duplicate */ - bool recordInstantiationInternal( Node q, std::vector< Node >& terms, bool modEq = false, bool addedLem = true ); - /** remove instantiation */ - bool removeInstantiationInternal( Node q, std::vector< Node >& terms ); - /** set instantiation level attr */ - static void setInstantiationLevelAttr( Node n, Node qn, uint64_t level ); /** flush lemmas */ void flushLemmas(); public: - /** get instantiation */ - Node getInstantiation( Node q, std::vector< Node >& vars, std::vector< Node >& terms, bool doVts = false ); - /** get instantiation */ - Node getInstantiation( Node q, InstMatch& m, bool doVts = false ); - /** get instantiation */ - Node getInstantiation( Node q, std::vector< Node >& terms, bool doVts = false ); - /** do substitution */ - Node getSubstitute( Node n, std::vector< Node >& terms, std::map< Node, Node >& visited ); /** add lemma lem */ bool addLemma( Node lem, bool doCache = true, bool doRewrite = true ); /** remove pending lemma */ bool removeLemma( Node lem ); /** add require phase */ void addRequirePhase( Node lit, bool req ); - /** do instantiation specified by m */ - bool addInstantiation( Node q, InstMatch& m, bool mkRep = false, bool modEq = false, bool doVts = false ); - /** add instantiation */ - bool addInstantiation( Node q, std::vector< Node >& terms, bool mkRep = false, bool modEq = false, bool doVts = false ); - /** remove pending instantiation */ - bool removeInstantiation( Node q, Node lem, std::vector< Node >& terms ); /** split on node n */ bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); /** add split equality */ @@ -364,14 +323,14 @@ public: bool inConflict() { return d_conflict; } /** set conflict */ void setConflict(); + /** get current q effort */ + QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; } /** get number of waiting lemmas */ unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */ bool getInstWhenNeedsCheck( Theory::Effort e ); /** get user pat mode */ quantifiers::UserPatMode getInstUserPatMode(); - /** set instantiation level attr */ - static void setInstantiationLevelAttr( Node n, uint64_t level ); public: /** get model */ quantifiers::FirstOrderModel* getModel() { return d_model; } @@ -385,6 +344,8 @@ public: quantifiers::QuantAttributes* getQuantAttributes() { return d_quant_attr.get(); } + /** get instantiate utility */ + quantifiers::Instantiate* getInstantiate() { return d_instantiate.get(); } /** get skolemize utility */ quantifiers::Skolemize* getSkolemize() { return d_skolemize.get(); } /** get term enumeration utility */ @@ -405,42 +366,41 @@ public: eq::EqualityEngine* getMasterEqualityEngine(); /** get the active equality engine */ eq::EqualityEngine* getActiveEqualityEngine(); + /** use model equality engine */ + bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ void debugPrintEqualityEngine( const char * c ); /** get internal representative */ Node getInternalRepresentative( Node a, Node q, int index ); - /** 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); public: + //----------user interface for instantiations (see quantifiers/instantiate.h) /** print instantiations */ - void printInstantiations( std::ostream& out ); + void printInstantiations(std::ostream& out); /** print solution for synthesis conjectures */ - void printSynthSolution( std::ostream& out ); + void printSynthSolution(std::ostream& out); /** get list of quantified formulas that were instantiated */ - void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); + void getInstantiatedQuantifiedFormulas(std::vector& qs); /** get instantiations */ - void getInstantiations( Node q, std::vector< Node >& insts ); - void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + void getInstantiations(Node q, std::vector& insts); + void getInstantiations(std::map >& insts); /** get instantiation term vectors */ - void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); - void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); + void getInstantiationTermVectors(Node q, + std::vector >& tvecs); + void getInstantiationTermVectors( + std::map > >& insts); /** get instantiated conjunction */ - Node getInstantiatedConjunction( Node q ); + Node getInstantiatedConjunction(Node q); /** get unsat core lemmas */ - bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas ); - bool getUnsatCoreLemmas( std::vector< Node >& active_lemmas, std::map< Node, Node >& weak_imp ); - /** get inst for lemmas */ - void getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ); + bool getUnsatCoreLemmas(std::vector& active_lemmas); + bool getUnsatCoreLemmas(std::vector& active_lemmas, + std::map& weak_imp); + /** get explanation for instantiation lemmas */ + void getExplanationForInstLemmas(const std::vector& lems, + std::map& quant, + std::map >& tvec); + //----------end user interface for instantiations + /** statistics class */ class Statistics { public: @@ -450,11 +410,6 @@ public: IntStat d_num_quant; IntStat d_instantiation_rounds; IntStat d_instantiation_rounds_lc; - IntStat d_instantiations; - IntStat d_inst_duplicate; - IntStat d_inst_duplicate_eq; - IntStat d_inst_duplicate_ent; - IntStat d_inst_duplicate_model_true; IntStat d_triggers; IntStat d_simple_triggers; IntStat d_multi_triggers; -- 2.30.2