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.cpp | |
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.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index a74c51a9a..096d0cab2 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -198,6 +198,24 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No } } +void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const { + if( terms.size()==q[0].getNumChildren() ){ + Trace(c) << " ( "; + for( unsigned i=0; i<terms.size(); i++ ){ + if( i>0 ) Trace(c) << ", "; + Trace(c) << terms[i]; + } + Trace(c) << " )" << std::endl; + }else{ + for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second.print( c, q, terms ); + terms.pop_back(); + } + } +} + + bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){ bool reset = false; @@ -264,6 +282,25 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< } } +void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{ + if( d_valid.get() ){ + if( terms.size()==q[0].getNumChildren() ){ + Trace(c) << " ( "; + for( unsigned i=0; i<terms.size(); i++ ){ + if( i>0 ) Trace(c) << ", "; + Trace(c) << terms[i]; + } + Trace(c) << " )" << std::endl; + }else{ + for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second->print( c, q, terms ); + terms.pop_back(); + } + } + } +} + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |