diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-26 14:23:51 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-26 14:24:02 -0600 |
commit | d0add0eb12cac4e9cbcf09fe60724d280889002d (patch) | |
tree | 217528663e877f15832a5cb00005e5a15a69f2ee /src/theory/quantifiers/inst_match.h | |
parent | 160572318e251a98a58b3f506c31fb233070d477 (diff) |
More optimization of QCF. Fixed InstMatchTrie for caching instantiations. Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 47 |
1 files changed, 40 insertions, 7 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 72447fd66..2cf33bc8e 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -119,11 +119,6 @@ public: 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, 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, InstMatchTrie > d_data; @@ -136,16 +131,20 @@ public: 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 ); + 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 modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 ); };/* class InstMatchTrie */ +#if 0 + /** trie for InstMatch objects */ class CDInstMatchTrie { public: @@ -181,6 +180,37 @@ public: bool modInst = false, ImtIndexOrder* imtio = NULL ); };/* class CDInstMatchTrie */ +#else + + +/** trie for InstMatch objects */ +class CDInstMatchTrie { +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, 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 ); +};/* class CDInstMatchTrie */ + + class InstMatchTrieOrdered{ private: InstMatchTrie::ImtIndexOrder* d_imtio; @@ -202,6 +232,9 @@ public: } };/* class InstMatchTrieOrdered */ +#endif + + }/* CVC4::theory::inst namespace */ typedef CVC4::theory::inst::InstMatch InstMatch; |