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_engine.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_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 929a638d7..8fecc6ee0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -623,6 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } } +void QuantifiersEngine::printInstantiations( const char * c ) { + if( options::incrementalSolving() ){ + for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){ + Trace(c) << "Instantiations of " << it->first << " : " << std::endl; + it->second->print( c, it->first ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + Trace(c) << "Instantiations of " << it->first << " : " << std::endl; + it->second.print( c, it->first ); + } + } +} + QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), |