diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 08:13:05 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-08 08:13:05 -0500 |
commit | ce831651caf58c1005fd3ebfdd2b75923d594328 (patch) | |
tree | 8787737dde71b80722bbf39718c38e739596d9fd /src/theory/quantifiers/inst_match.h | |
parent | 2ca4e063ca007851ebf73ccb2ac6b7c85e73133d (diff) |
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.
Diffstat (limited to 'src/theory/quantifiers/inst_match.h')
-rw-r--r-- | src/theory/quantifiers/inst_match.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index c366c4a09..2cf63210b 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -100,6 +100,8 @@ public: public: /** the data */ std::map< Node, InstMatchTrie > d_data; +private: + void print( const char * c, Node q, std::vector< Node >& terms ) const; public: InstMatchTrie(){} ~InstMatchTrie(){} @@ -126,6 +128,10 @@ public: } 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 ); + void print( const char * c, Node q ) const{ + std::vector< Node > terms; + print( c, q, terms ); + } };/* class InstMatchTrie */ /** trie for InstMatch objects */ @@ -135,6 +141,8 @@ public: std::map< Node, CDInstMatchTrie* > d_data; /** is valid */ context::CDO< bool > d_valid; +private: + void print( const char * c, Node q, std::vector< Node >& terms ) const; public: CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){} ~CDInstMatchTrie(){} @@ -161,6 +169,10 @@ public: } 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 ); + void print( const char * c, Node q ) const{ + std::vector< Node > terms; + print( c, q, terms ); + } };/* class CDInstMatchTrie */ |