From af930471df9bfe02d8848e1dc1a1eda47dbe8cbe Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Mar 2022 08:58:27 -0600
Subject: [PATCH] Change interface for printing instantiations in the API
 (#8251)

Furthermore note that this should take several modes, similar to the discussion with `blockModel` / `getLearnedLiterals`.  It is currently limited to a fixed print mode.
---
 src/api/cpp/cvc5.cpp                        |  6 ++++--
 src/api/cpp/cvc5.h                          |  6 +++---
 src/api/java/io/github/cvc5/api/Solver.java | 11 ++++++++---
 src/api/java/jni/solver.cpp                 | 17 +++++++++++++++++
 src/api/python/cvc5.pxd                     |  1 +
 src/api/python/cvc5.pxi                     |  7 +++++++
 src/smt/command.cpp                         |  2 +-
 7 files changed, 41 insertions(+), 9 deletions(-)

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 8f5fc6566..2a9234a2f 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7719,11 +7719,13 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
   CVC5_API_TRY_CATCH_END;
 }
 
-void Solver::printInstantiations(std::ostream& out) const
+std::string Solver::getInstantiations() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
-  d_slv->printInstantiations(out);
+  std::stringstream ss;
+  d_slv->printInstantiations(ss);
+  return ss.str();
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 6b614f49a..316d26910 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4586,10 +4586,10 @@ class CVC5_EXPORT Solver
   void blockModelValues(const std::vector<Term>& terms) const;
 
   /**
-   * Print all instantiations made by the quantifiers module.
-   * @param out the output stream
+   * @return a string that contains information about all instantiations made by
+   * the quantifiers module.
    */
-  void printInstantiations(std::ostream& out) const;
+  std::string getInstantiations() const;
 
   /**
    * Push (a) level(s) to the assertion stack.
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 762eb4c79..62e6d94eb 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -2323,10 +2323,15 @@ public class Solver implements IPointer, AutoCloseable
   private native void blockModelValues(long pointer, long[] termPointers);
 
   /**
-   * Print all instantiations made by the quantifiers module.
-   * @param out the output stream
+   * Return a string that contains information about all instantiations made by
+   * the quantifiers module.
    */
-  // TODO: void printInstantiations(std::ostream& out)
+  public String getInstantiations()
+  {
+    return getInstantiations(pointer);
+  }
+
+  private native String getInstantiations(long pointer);
 
   /**
    * Push a level to the assertion stack.
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index 9af316cbf..63a6c179a 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -2311,6 +2311,23 @@ JNIEXPORT void JNICALL Java_io_github_cvc5_api_Solver_blockModelValues(
   CVC5_JAVA_API_TRY_CATCH_END(env);
 }
 
+/*
+ * Class:     io_github_cvc5_api_Solver
+ * Method:    getInstantiations
+ * Signature: (J[J[J)Ljava/lang/String;
+ */
+JNIEXPORT jstring JNICALL
+Java_io_github_cvc5_api_Solver_getInstantiations(JNIEnv* env,
+                                        jobject,
+                                        jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  std::string insts = solver->getInstantiations();
+  return env->NewStringUTF(insts.c_str());
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
 /*
  * Class:     io_github_cvc5_api_Solver
  * Method:    push
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 392e7b412..bff77fbce 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -303,6 +303,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint getAbductNext(const Term& conj) except +
         void blockModel() except +
         void blockModelValues(const vector[Term]& terms) except +
+        string getInstantiations() except +
 
     cdef cppclass Grammar:
         Grammar() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 46703d36f..2c535b2e4 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2394,6 +2394,13 @@ cdef class Solver:
             nts.push_back((<Term?> t).cterm)
         self.csolver.blockModelValues(nts)
 
+    def getInstantiations(self):
+        """
+        Return a string that contains information about all instantiations made
+        by the quantifiers module.
+        """
+        return self.csolver.getInstantiations()
+
 
 cdef class Sort:
     """
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f96488452..2766c6510 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1914,7 +1914,7 @@ void GetInstantiationsCommand::printResult(std::ostream& out) const
   }
   else
   {
-    d_solver->printInstantiations(out);
+    out << d_solver->getInstantiations();
   }
 }
 
-- 
2.30.2