diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 32 |
1 files changed, 32 insertions, 0 deletions
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 ); |