From c5d1a5d8f898bf22c6bbc98f1d484b07706c035b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 28 Jan 2013 01:57:20 -0600 Subject: [PATCH] made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486 --- src/theory/quantifiers/inst_match.cpp | 82 +++++++++++++++++++ src/theory/quantifiers/inst_match.h | 37 +++++++++ .../quantifiers/instantiation_engine.cpp | 4 +- src/theory/quantifiers/options | 3 + src/theory/quantifiers_engine.cpp | 27 ++++-- src/theory/quantifiers_engine.h | 7 +- src/theory/theory_engine.cpp | 2 +- 7 files changed, 151 insertions(+), 11 deletions(-) diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 1a48ec161..dcd7a1b79 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -217,6 +217,88 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, b } + +/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ +void CDInstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ){ + if( long(index)d_order.size()) ) ){ + int i_index = imtio ? imtio->d_order[index] : index; + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + it->second->addInstMatch2( qe, f, m, c, index+1, imtio ); + }else{ + CDInstMatchTrie* imt = new CDInstMatchTrie( c ); + d_data[n] = imt; + imt->d_valid = true; + imt->addInstMatch2( qe, f, m, c, index+1, imtio ); + } + } +} + +/** exists match */ +bool CDInstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){ + if( !d_valid ){ + return false; + }else if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){ + return true; + }else{ + int i_index = imtio ? imtio->d_order[index] : index; + Node n = m.getValue( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); + std::map< Node, CDInstMatchTrie* >::iterator it = d_data.find( n ); + if( it!=d_data.end() ){ + if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ + return true; + } + } + //check if m is an instance of another instantiation if modInst is true + if( modInst ){ + if( !n.isNull() ){ + Node nl; + it = d_data.find( nl ); + if( it!=d_data.end() ){ + if( it->second->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ + return true; + } + } + } + } + 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->existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ + return true; + } + } + } + ++eqc; + } + } + } + return false; + } +} + +bool CDInstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio ); +} + +bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, Context* c, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){ + addInstMatch2( qe, f, m, c, 0, imtio ); + return true; + }else{ + return false; + } +} + + }/* 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 c8f843c90..8b2d9726b 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -18,6 +18,7 @@ #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H #include "util/hash.h" +#include "context/cdo.h" #include #include @@ -141,6 +142,42 @@ public: bool modInst = false, ImtIndexOrder* imtio = NULL ); };/* class InstMatchTrie */ + +/** trie for InstMatch objects */ +class CDInstMatchTrie { +public: + class ImtIndexOrder { + public: + std::vector< int > d_order; + };/* class InstMatchTrie ImtIndexOrder */ +private: + /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ + void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, context::Context* c, int index, ImtIndexOrder* imtio ); + /** exists match */ + bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ); +public: + /** the data */ + std::map< Node, CDInstMatchTrie* > d_data; + /** is valid */ + context::CDO< bool > d_valid; +public: + CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} + ~CDInstMatchTrie(){} +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, + bool modInst = false, ImtIndexOrder* imtio = NULL ); + /** 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, context::Context* c, bool modEq = false, + bool modInst = false, ImtIndexOrder* imtio = NULL ); +};/* class CDInstMatchTrie */ + class InstMatchTrieOrdered{ private: InstMatchTrie::ImtIndexOrder* d_imtio; diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 653016d1c..53977ee4f 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -48,8 +48,8 @@ void InstantiationEngine::finishInit(){ }else{ d_isup = NULL; } - InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, - InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT, 3 ); + int rlv = options::relevantTriggers() ? InstStrategyAutoGenTriggers::RELEVANCE_DEFAULT : InstStrategyAutoGenTriggers::RELEVANCE_NONE; + InstStrategyAutoGenTriggers* i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, Trigger::TS_ALL, rlv, 3 ); i_ag->setGenerateAdditional( true ); addInstStrategy( i_ag ); //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 24d0c4047..bc45e6051 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -44,6 +44,9 @@ option macrosQuant --macros-quant bool :default false # Whether to use smart triggers option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers +# Whether to use relevent triggers +option relevantTriggers /--relevant-triggers bool :default true + prefer triggers that are more relevant based on SInE style method # Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c04920ab8..08bdd496b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -35,9 +35,10 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; -QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te): +QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te): d_te( te ), -d_quant_rel( false ){ //currently do not care about relevance +d_quant_rel( false ), +d_lemmas_produced_c(u){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); d_tr_trie = new inst::TriggerTrie; @@ -92,6 +93,10 @@ context::Context* QuantifiersEngine::getSatContext(){ return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext(); } +context::Context* QuantifiersEngine::getUserContext(){ + return d_te->theoryOf( THEORY_QUANTIFIERS )->getUserContext(); +} + OutputChannel& QuantifiersEngine::getOutputChannel(){ return d_te->theoryOf( THEORY_QUANTIFIERS )->getOutputChannel(); } @@ -309,7 +314,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ if( d_inst_match_trie.find( f )!=d_inst_match_trie.end() ){ - if( d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ) ){ + if( d_inst_match_trie[f]->existsInstMatch( this, f, m, modEq, modInst ) ){ return true; } } @@ -323,9 +328,9 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b bool QuantifiersEngine::addLemma( Node lem ){ Debug("inst-engine-debug") << "Adding lemma : " << lem << std::endl; lem = Rewriter::rewrite(lem); - if( d_lemmas_produced.find( lem )==d_lemmas_produced.end() ){ + if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){ //d_curr_out->lemma( lem ); - d_lemmas_produced[ lem ] = true; + d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); Debug("inst-engine-debug") << "Added lemma : " << lem << std::endl; return true; @@ -355,11 +360,21 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool modEq, bool } } //check for duplication modulo equality - if( !d_inst_match_trie[f].addInstMatch( this, f, m, modEq, modInst ) ){ + inst::CDInstMatchTrie* imt; + std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_inst_match_trie.find( f ); + if( it!=d_inst_match_trie.end() ){ + imt = it->second; + }else{ + imt = new CDInstMatchTrie( getUserContext() ); + d_inst_match_trie[f] = imt; + } + Trace("inst-add-debug") << "Adding into inst trie" << std::endl; + if( !imt->addInstMatch( this, f, m, getUserContext(), modEq, modInst ) ){ Trace("inst-add-debug") << " -> Already exists." << std::endl; ++(d_statistics.d_inst_duplicate); return false; } + Trace("inst-add-debug") << "compute terms" << std::endl; //compute the vector of terms for the instantiation std::vector< Node > terms; for( size_t i=0; id_inst_constants[f].size(); i++ ){ diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 8169c78fb..29381a309 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -104,12 +104,13 @@ private: std::vector< Node > d_quants; /** list of all lemmas produced */ std::map< Node, bool > d_lemmas_produced; + BoolMap d_lemmas_produced_c; /** lemmas waiting */ std::vector< Node > d_lemmas_waiting; /** has added lemma this round */ bool d_hasAddedLemma; /** list of all instantiations produced for each quantifier */ - std::map< Node, inst::InstMatchTrie > d_inst_match_trie; + std::map< Node, inst::CDInstMatchTrie* > d_inst_match_trie; /** term database */ quantifiers::TermDb* d_term_db; /** all triggers will be stored in this trie */ @@ -121,7 +122,7 @@ private: private: KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); public: - QuantifiersEngine(context::Context* c, TheoryEngine* te); + QuantifiersEngine(context::Context* c, context::UserContext* u, TheoryEngine* te); ~QuantifiersEngine(); /** get instantiator for id */ //Instantiator* getInstantiator( theory::TheoryId id ); @@ -136,6 +137,8 @@ public: quantifiers::ModelEngine* getModelEngine() { return d_model_engine; } /** get default sat context for quantifiers engine */ context::Context* getSatContext(); + /** get default sat context for quantifiers engine */ + context::Context* getUserContext(); /** get default output channel for the quantifiers engine */ OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a23480eeb..35ed63bed 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -127,7 +127,7 @@ TheoryEngine::TheoryEngine(context::Context* context, } // initialize the quantifiers engine - d_quantEngine = new QuantifiersEngine(context, this); + d_quantEngine = new QuantifiersEngine(context, userContext, this); // build model information if applicable d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true); -- 2.30.2