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 );