diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-28 01:57:20 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-28 01:57:20 -0600 |
commit | c5d1a5d8f898bf22c6bbc98f1d484b07706c035b (patch) | |
tree | 49b5cc92ea74d720178d60bab2837bf897559813 /src/theory/quantifiers/inst_match.h | |
parent | bcbf52ffbe0416ecf70bdb644017c338c0540793 (diff) |
made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 37 |
1 files changed, 37 insertions, 0 deletions
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; |