diff options
Diffstat (limited to 'src/theory/quantifiers/inst_match.cpp')
| -rw-r--r-- | src/theory/quantifiers/inst_match.cpp | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 5eca87903..f2d5c640d 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -212,6 +212,18 @@ void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& term } } +void InstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const { + if( terms.size()==q[0].getNumChildren() ){ + insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + }else{ + for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second.getInstantiations( insts, q, vars, 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 ){ @@ -298,6 +310,20 @@ void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& te } } +void CDInstMatchTrie::getInstantiations( std::vector< Node >& insts, Node q, std::vector< TNode >& vars, std::vector< TNode >& terms ) const{ + if( d_valid.get() ){ + if( terms.size()==q[0].getNumChildren() ){ + insts.push_back( q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ) ); + }else{ + for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){ + terms.push_back( it->first ); + it->second->getInstantiations( insts, q, vars, terms ); + terms.pop_back(); + } + } + } +} + }/* CVC4::theory::inst namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |