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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 8f5fc6566f701a1a3d8e0ed0dfde012022eebfb1..2a9234a2f24b66ff67a136de0c26f0f7dd4a54a6 100644 (file)
--- 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 6b614f49a4f5cd42ddc1e57b8f0aa6c650cb935b..316d2691095d253a18ec0bf77886a96554c585b2 100644 (file)
--- 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 762eb4c798a3028774734e6c2a049f8470f931cd..62e6d94eb4d4538ad894c141ec4c22c720141b1d 100644 (file)
--- 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 9af316cbf68ff7cb56867d102bfe9b690ff02f3a..63a6c179abc31a220f73a89091ef2e5c66f06090 100644 (file)
--- 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 392e7b412c6d2e990862f8b7fc0f4a0f523a1089..bff77fbce5841863bf224dd7f1a2fea3d14fa5dd 100644 (file)
--- 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 46703d36fb872188371fbcdc84cc9d67d576c62f..2c535b2e44612d6ca9836aa31ab60d4d211823ac 100644 (file)
--- 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 f96488452dd07fbaccafe66dc394a1dcd1920750..2766c651083fb0cad7fbe61d5db8540585fe5b09 100644 (file)
--- 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();
   }
 }