Add get instantiations utilities to API.

2 files changed, 48 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();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 2741cea85..760c7c071 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -566,6 +566,17 @@ public:
   Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
+   * Get list of quantified formulas that were instantiated
+   */
+  void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs );
+   
+  /**
+   * Get instantiations
+   */
+  void getInstantiations( Expr q, std::vector< Expr >& insts );
+  void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs );
+
+  /**
    * Get an unsatisfiable core (only if immediately preceded by an
    * UNSAT or VALID query).  Only permitted if CVC4 was built with
    * unsat-core support and produce-unsat-cores is on.