diff options
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 67990ef69..95b01bc7b 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1382,6 +1382,29 @@ bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas, } } +void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { + std::vector< Node > lemmas; + getInstantiations( q, lemmas ); + std::map< Node, Node > quant; + std::map< Node, std::vector< Node > > tvec; + getExplanationForInstLemmas( lemmas, quant, tvec ); + for( std::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){ + tvecs.push_back( it->second ); + } +} + +void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { + 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 ){ + getInstantiationTermVectors( it->first, insts[it->first] ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + getInstantiationTermVectors( it->first, insts[it->first] ); + } + } +} + void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) { if( d_trackInstLemmas ){ if( options::incrementalSolving() ){ @@ -1456,6 +1479,18 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) { } } +void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { + 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 ){ + qs.push_back( it->first ); + } + }else{ + for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){ + qs.push_back( it->first ); + } + } +} + void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { bool useUnsatCore = false; std::vector< Node > active_lemmas; |