New C++ API: Clean up usage of internal Result. (#6043)

This disables the temporarily available internals of Result.
It further changes the interface for getUnknownExplanation, which now
returns an enum value instead of a string.

7 files changed, 86 insertions, 59 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 410198920..a426c9270 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -936,25 +936,52 @@ bool Result::operator!=(const Result& r) const
   return *d_result != *r.d_result;
 }
 
-std::string Result::getUnknownExplanation(void) const
+Result::UnknownExplanation Result::getUnknownExplanation(void) const
 {
-  std::stringstream ss;
-  ss << d_result->whyUnknown();
-  return ss.str();
+  CVC4::Result::UnknownExplanation expl = d_result->whyUnknown();
+  switch (expl)
+  {
+    case CVC4::Result::REQUIRES_FULL_CHECK: return REQUIRES_FULL_CHECK;
+    case CVC4::Result::INCOMPLETE: return INCOMPLETE;
+    case CVC4::Result::TIMEOUT: return TIMEOUT;
+    case CVC4::Result::RESOURCEOUT: return RESOURCEOUT;
+    case CVC4::Result::MEMOUT: return MEMOUT;
+    case CVC4::Result::INTERRUPTED: return INTERRUPTED;
+    case CVC4::Result::NO_STATUS: return NO_STATUS;
+    case CVC4::Result::UNSUPPORTED: return UNSUPPORTED;
+    case CVC4::Result::OTHER: return OTHER;
+    default: return UNKNOWN_REASON;
+  }
+  return UNKNOWN_REASON;
 }
 
 std::string Result::toString(void) const { return d_result->toString(); }
 
-// !!! This is only temporarily available until the parser is fully migrated
-// to the new API. !!!
-CVC4::Result Result::getResult(void) const { return *d_result; }
-
 std::ostream& operator<<(std::ostream& out, const Result& r)
 {
   out << r.toString();
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e)
+{
+  switch (e)
+  {
+    case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
+    case Result::INCOMPLETE: out << "INCOMPLETE"; break;
+    case Result::TIMEOUT: out << "TIMEOUT"; break;
+    case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
+    case Result::MEMOUT: out << "MEMOUT"; break;
+    case Result::INTERRUPTED: out << "INTERRUPTED"; break;
+    case Result::NO_STATUS: out << "NO_STATUS"; break;
+    case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
+    case Result::OTHER: out << "OTHER"; break;
+    case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
+    default: Unhandled() << e;
+  }
+  return out;
+}
+
 /* -------------------------------------------------------------------------- */
 /* Sort                                                                       */
 /* -------------------------------------------------------------------------- */
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index e52fe2524..f68fe4c0b 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -97,14 +97,19 @@ class CVC4_PUBLIC Result
   friend class Solver;
 
  public:
-  // !!! This constructor is only temporarily public until the parser is fully
-  // migrated to the new API. !!!
-  /**
-   * Constructor.
-   * @param r the internal result that is to be wrapped by this result
-   * @return the Result
-   */
-  Result(const CVC4::Result& r);
+  enum UnknownExplanation
+  {
+    REQUIRES_FULL_CHECK,
+    INCOMPLETE,
+    TIMEOUT,
+    RESOURCEOUT,
+    MEMOUT,
+    INTERRUPTED,
+    NO_STATUS,
+    UNSUPPORTED,
+    OTHER,
+    UNKNOWN_REASON
+  };
 
   /** Constructor. */
   Result();
@@ -167,19 +172,22 @@ class CVC4_PUBLIC Result
   /**
    * @return an explanation for an unknown query result.
    */
-  std::string getUnknownExplanation() const;
+  UnknownExplanation getUnknownExplanation() const;
 
   /**
    * @return a string representation of this result.
    */
   std::string toString() const;
 
-  // !!! This is only temporarily available until the parser is fully migrated
-  // to the new API. !!!
-  CVC4::Result getResult(void) const;
-
  private:
   /**
+   * Constructor.
+   * @param r the internal result that is to be wrapped by this result
+   * @return the Result
+   */
+  Result(const CVC4::Result& r);
+
+  /**
    * The interal result wrapped by this result.
    * This is a shared_ptr rather than a unique_ptr since CVC4::Result is
    * not ref counted.
@@ -188,13 +196,22 @@ class CVC4_PUBLIC Result
 };
 
 /**
- * Serialize a result to given stream.
+ * Serialize a Result to given stream.
  * @param out the output stream
  * @param r the result to be serialized to the given output stream
  * @return the output stream
  */
 std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC;
 
+/**
+ * Serialize an UnknownExplanation to given stream.
+ * @param out the output stream
+ * @param r the explanation to be serialized to the given output stream
+ * @return the output stream
+ */
+std::ostream& operator<<(std::ostream& out,
+                         enum Result::UnknownExplanation e) CVC4_PUBLIC;
+
 /* -------------------------------------------------------------------------- */
 /* Sort                                                                       */
 /* -------------------------------------------------------------------------- */
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 04ed5147a..8f4b2d4d2 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -163,7 +163,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     if (d_options.getDumpModels()
         && (res.isSat()
             || (res.isSatUnknown()
-                && res.getResult().whyUnknown() == Result::INCOMPLETE)))
+                && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
@@ -176,7 +176,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
         && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
              && (res.isSat()
                  || (res.isSatUnknown()
-                     && res.getResult().whyUnknown() == Result::INCOMPLETE)))
+                     && res.getUnknownExplanation()
+                            == api::Result::INCOMPLETE)))
             || isResultUnsat))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
diff --git a/src/smt/command.h b/src/smt/command.h
index a2230e12a..67b824852 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -28,7 +28,6 @@
 #include <vector>
 
 #include "api/cvc4cpp.h"
-#include "util/result.h"
 #include "util/sexpr.h"
 
 namespace CVC4 {
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 09445fa3b..bb280b515 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -270,38 +270,20 @@ ostream& operator<<(ostream& out, enum Result::Entailment e)
   return out;
 }
 
-ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) {
-  switch (e) {
-    case Result::REQUIRES_FULL_CHECK:
-      out << "REQUIRES_FULL_CHECK";
-      break;
-    case Result::INCOMPLETE:
-      out << "INCOMPLETE";
-      break;
-    case Result::TIMEOUT:
-      out << "TIMEOUT";
-      break;
-    case Result::RESOURCEOUT:
-      out << "RESOURCEOUT";
-      break;
-    case Result::MEMOUT:
-      out << "MEMOUT";
-      break;
-    case Result::INTERRUPTED:
-      out << "INTERRUPTED";
-      break;
-    case Result::NO_STATUS:
-      out << "NO_STATUS";
-      break;
-    case Result::UNSUPPORTED:
-      out << "UNSUPPORTED";
-      break;
-    case Result::OTHER:
-      out << "OTHER";
-      break;
-    case Result::UNKNOWN_REASON:
-      out << "UNKNOWN_REASON";
-      break;
+ostream& operator<<(ostream& out, enum Result::UnknownExplanation e)
+{
+  switch (e)
+  {
+    case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break;
+    case Result::INCOMPLETE: out << "INCOMPLETE"; break;
+    case Result::TIMEOUT: out << "TIMEOUT"; break;
+    case Result::RESOURCEOUT: out << "RESOURCEOUT"; break;
+    case Result::MEMOUT: out << "MEMOUT"; break;
+    case Result::INTERRUPTED: out << "INTERRUPTED"; break;
+    case Result::NO_STATUS: out << "NO_STATUS"; break;
+    case Result::UNSUPPORTED: out << "UNSUPPORTED"; break;
+    case Result::OTHER: out << "OTHER"; break;
+    case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break;
     default: Unhandled() << e;
   }
   return out;
diff --git a/src/util/result.h b/src/util/result.h
index d0b0896bc..8ded88e15 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -51,7 +51,8 @@ class CVC4_PUBLIC Result {
     TYPE_NONE
   };
 
-  enum UnknownExplanation {
+  enum UnknownExplanation
+  {
     REQUIRES_FULL_CHECK,
     INCOMPLETE,
     TIMEOUT,
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index 887be8fe0..a3e693b27 100644
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -115,7 +115,7 @@ TEST_F(TestApiBlackResult, isEntailmentUnknown)
   CVC4::api::Result res = d_solver.checkEntailed(x.eqTerm(x));
   ASSERT_FALSE(res.isEntailed());
   ASSERT_TRUE(res.isEntailmentUnknown());
-  ASSERT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON");
+  ASSERT_EQ(res.getUnknownExplanation(), api::Result::UNKNOWN_REASON);
 }
 }  // namespace test
 }  // namespace CVC4