diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-27 08:34:52 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-27 08:34:52 -0600 |
commit | e179e62b57eb207d41647a6bbd50ef0f8c723e96 (patch) | |
tree | 9a768eeae815f2851f34dc3fbb3fd3661e939c8d /src/theory/quantifiers/inst_match.h | |
parent | d0add0eb12cac4e9cbcf09fe60724d280889002d (diff) |
More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 58 |
1 files changed, 13 insertions, 45 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 2cf33bc8e..eb7f50095 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -45,7 +45,7 @@ public: /** set the match of v to m */ bool setMatch( EqualityQuery* q, TNode v, TNode m ); /* This version tell if the variable has been set */ - bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & set); + bool setMatch( EqualityQuery* q, TNode v, TNode m, bool & st); /** fill all unfilled values with m */ bool add( InstMatch& m ); /** if compatible, fill all unfilled values with m and return true @@ -134,55 +134,20 @@ public: bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) { return !addInstMatch( qe, f, m, modEq, modInst, imtio, true, index ); } + bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, + bool modInst = false, ImtIndexOrder* imtio = NULL, int index = 0 ) { + return !addInstMatch( qe, f, m, modEq, modInst, 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, bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); + bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false, + bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); };/* class InstMatchTrie */ - -#if 0 - -/** 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 */ - -#else - - /** trie for InstMatch objects */ class CDInstMatchTrie { public: @@ -202,12 +167,18 @@ public: bool modInst = false, int index = 0 ) { return !addInstMatch( qe, f, m, c, modEq, modInst, index, true ); } + bool existsInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool modInst = false, int index = 0 ) { + return !addInstMatch( qe, f, m, c, modEq, modInst, 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 f, InstMatch& m, context::Context* c, bool modEq = false, bool modInst = false, int index = 0, bool onlyExist = false ); + bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false, + bool modInst = false, int index = 0, bool onlyExist = false ); };/* class CDInstMatchTrie */ @@ -232,9 +203,6 @@ public: } };/* class InstMatchTrieOrdered */ -#endif - - }/* CVC4::theory::inst namespace */ typedef CVC4::theory::inst::InstMatch InstMatch; |