diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-28 17:14:04 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-28 17:14:04 -0500 |
commit | b1dea08db5a965d8d9d6f38bd05c280a8a126352 (patch) | |
tree | 5bd385da8faf2043da66ae1ff2230ca759c36a49 /src/theory | |
parent | 360ad23aa7f04d7059aff6314066e47e975fe5be (diff) |
Add get instantiations utilities to API.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 5 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 32 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 13 |
4 files changed, 84 insertions, 1 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; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 232d1d889..ff6a8a36c 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -374,9 +374,14 @@ public: void printInstantiations( std::ostream& out ); /** print solution for synthesis conjectures */ void printSynthSolution( std::ostream& out ); + /** get list of quantified formulas that were instantiated */ + void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); /** get instantiations */ void getInstantiations( Node q, std::vector< Node >& insts ); void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + /** get instantiation term vectors */ + void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); + void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); /** get instantiated conjunction */ Node getInstantiatedConjunction( Node q ); /** get unsat core lemmas */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a14534efe..c3e853ec0 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1445,6 +1445,30 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) { } } +void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiatedQuantifiedFormulas( qs ); + }else{ + Assert( false ); + } +} + +void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiations( q, insts ); + }else{ + Assert( false ); + } +} + +void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiationTermVectors( q, tvecs ); + }else{ + Assert( false ); + } +} + void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) { if( d_quantEngine ){ d_quantEngine->getInstantiations( insts ); @@ -1453,6 +1477,14 @@ void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& ins } } +void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) { + if( d_quantEngine ){ + d_quantEngine->getInstantiationTermVectors( insts ); + }else{ + Assert( false ); + } +} + Node TheoryEngine::getInstantiatedConjunction( Node q ) { if( d_quantEngine ){ return d_quantEngine->getInstantiatedConjunction( q ); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 4366f8d3a..fc98c6e3a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -786,9 +786,20 @@ public: void printSynthSolution( std::ostream& out ); /** - * Get instantiations + * Get list of quantified formulas that were instantiated */ + void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ); + + /** + * Get instantiation methods + * first inputs forall x.q[x] and returns ( q[a], ..., q[z] ) + * second inputs forall x.q[x] and returns ( a, ..., z ) + * third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) , ... , forall x.qn[x] -> ( qn[a]...qn[z] ) + */ + void getInstantiations( Node q, std::vector< Node >& insts ); + void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ); void getInstantiations( std::map< Node, std::vector< Node > >& insts ); + void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ); /** * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q. |