diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 82 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 37 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 3 |
4 files changed, 124 insertions, 2 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)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->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 <ext/hash_set> #include <map> @@ -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 |