Add get instantiations utilities to API.

1 files changed, 11 insertions, 0 deletions

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.