From eca92626dafa1e22e59aec94f6e34788c51e777a Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 3 Mar 2021 17:36:57 -0800 Subject: [PATCH] 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. --- src/api/cvc4cpp.cpp | 43 +++++++++++++++++++++++++------ src/api/cvc4cpp.h | 45 ++++++++++++++++++++++----------- src/main/command_executor.cpp | 5 ++-- src/smt/command.h | 1 - src/util/result.cpp | 46 +++++++++++----------------------- src/util/result.h | 3 ++- test/unit/api/result_black.cpp | 2 +- 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,18 +172,21 @@ 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 @@ -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 #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 -- 2.30.2