1 files changed, 37 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f288c6c0a..e3a0533af 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5125,6 +5125,43 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   }
 }
 
+void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
+  SmtScope smts(this);
+  if( d_theoryEngine ){
+    std::vector< Node > qs_n;
+    d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n );
+    for( unsigned i=0; i<qs_n.size(); i++ ){
+      qs.push_back( qs_n[i].toExpr() );
+    }
+  }
+}
+
+void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
+  SmtScope smts(this);
+  if( d_theoryEngine ){
+    std::vector< Node > insts_n;
+    d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n );
+    for( unsigned i=0; i<insts_n.size(); i++ ){
+      insts.push_back( insts_n[i].toExpr() );
+    }
+  }
+}
+
+void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
+  SmtScope smts(this);
+  if( d_theoryEngine ){
+    std::vector< std::vector< Node > > tvecs_n;
+    d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n );
+    for( unsigned i=0; i<tvecs_n.size(); i++ ){
+      std::vector< Expr > tvec;
+      for( unsigned j=0; j<tvecs_n[i].size(); j++ ){
+        tvec.push_back( tvecs_n[i][j].toExpr() );
+      }
+      tvecs.push_back( tvec );
+    }
+  }
+}
+
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();