From a9dd62372b490ba36bf7fad3d6a9883949c341a0 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 30 Mar 2022 07:30:11 -0700 Subject: [PATCH] [API] Move `UnknownExplanation` to `cvc5_types.h` (#8450) This also fixes some minor issues in the `parseenums.py` script. --- src/CMakeLists.txt | 1 + src/api/cpp/cvc5.cpp | 37 +------------ src/api/cpp/cvc5.h | 23 -------- src/api/cpp/cvc5_types.cpp | 46 ++++++++++++++++ src/api/cpp/cvc5_types.h | 30 ++++++++++- src/api/java/CMakeLists.txt | 1 + src/api/java/io/github/cvc5/api/Result.java | 45 ---------------- src/api/parseenums.py | 5 +- src/api/python/cvc5.pxd | 20 +------ src/api/python/cvc5.pxi | 60 +-------------------- src/main/command_executor.cpp | 3 +- src/prop/prop_engine.cpp | 10 ++-- src/smt/assertions.cpp | 2 +- src/smt/command.cpp | 3 +- src/smt/optimization_solver.h | 2 +- src/smt/smt_solver.cpp | 10 ++-- src/smt/sygus_solver.cpp | 2 +- src/theory/smt_engine_subsolver.cpp | 2 +- src/util/result.cpp | 23 +------- src/util/result.h | 16 +----- src/util/synth_result.cpp | 9 ++-- src/util/synth_result.h | 10 ++-- 22 files changed, 115 insertions(+), 245 deletions(-) create mode 100644 src/api/cpp/cvc5_types.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f263bdc72..46f705d5b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -19,6 +19,7 @@ libcvc5_add_sources( api/cpp/cvc5.h api/cpp/cvc5_checks.h api/cpp/cvc5_kind.h + api/cpp/cvc5_types.cpp api/cpp/cvc5_types.h decision/assertion_list.cpp decision/assertion_list.h diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index aea5add41..a22923cc9 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -988,23 +988,9 @@ bool Result::operator!=(const Result& r) const return *d_result != *r.d_result; } -Result::UnknownExplanation Result::getUnknownExplanation(void) const +UnknownExplanation Result::getUnknownExplanation(void) const { - internal::Result::UnknownExplanation expl = d_result->getUnknownExplanation(); - switch (expl) - { - case internal::Result::REQUIRES_FULL_CHECK: return REQUIRES_FULL_CHECK; - case internal::Result::INCOMPLETE: return INCOMPLETE; - case internal::Result::TIMEOUT: return TIMEOUT; - case internal::Result::RESOURCEOUT: return RESOURCEOUT; - case internal::Result::MEMOUT: return MEMOUT; - case internal::Result::INTERRUPTED: return INTERRUPTED; - case internal::Result::NO_STATUS: return NO_STATUS; - case internal::Result::UNSUPPORTED: return UNSUPPORTED; - case internal::Result::OTHER: return OTHER; - default: return UNKNOWN_REASON; - } - return UNKNOWN_REASON; + return d_result->getUnknownExplanation(); } std::string Result::toString(void) const { return d_result->toString(); } @@ -1015,25 +1001,6 @@ std::ostream& operator<<(std::ostream& out, const Result& r) 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; -} - /* -------------------------------------------------------------------------- */ /* SynthResult */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 24107281f..2ca093399 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -188,20 +188,6 @@ class CVC5_EXPORT Result friend class Solver; public: - enum UnknownExplanation - { - REQUIRES_FULL_CHECK, - INCOMPLETE, - TIMEOUT, - RESOURCEOUT, - MEMOUT, - INTERRUPTED, - NO_STATUS, - UNSUPPORTED, - OTHER, - UNKNOWN_REASON - }; - /** Constructor. */ Result(); @@ -278,15 +264,6 @@ class CVC5_EXPORT Result */ std::ostream& operator<<(std::ostream& out, const Result& r) CVC5_EXPORT; -/** - * Serialize an UnknownExplanation to given stream. - * @param out the output stream - * @param e the explanation to be serialized to the given output stream - * @return the output stream - */ -std::ostream& operator<<(std::ostream& out, - enum Result::UnknownExplanation e) CVC5_EXPORT; - /* -------------------------------------------------------------------------- */ /* Result */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cpp/cvc5_types.cpp b/src/api/cpp/cvc5_types.cpp new file mode 100644 index 000000000..7930ae22a --- /dev/null +++ b/src/api/cpp/cvc5_types.cpp @@ -0,0 +1,46 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Common cvc5 types. These types are used internally as well as externally and + * the language bindings are generated automatically. + */ + +#include "api/cpp/cvc5_types.h" + +#include + +#include "base/check.h" + +namespace cvc5 { + +std::ostream& operator<<(std::ostream& out, UnknownExplanation e) +{ + switch (e) + { + case UnknownExplanation::REQUIRES_FULL_CHECK: + out << "REQUIRES_FULL_CHECK"; + break; + case UnknownExplanation::INCOMPLETE: out << "INCOMPLETE"; break; + case UnknownExplanation::TIMEOUT: out << "TIMEOUT"; break; + case UnknownExplanation::RESOURCEOUT: out << "RESOURCEOUT"; break; + case UnknownExplanation::MEMOUT: out << "MEMOUT"; break; + case UnknownExplanation::INTERRUPTED: out << "INTERRUPTED"; break; + case UnknownExplanation::NO_STATUS: out << "NO_STATUS"; break; + case UnknownExplanation::UNSUPPORTED: out << "UNSUPPORTED"; break; + case UnknownExplanation::OTHER: out << "OTHER"; break; + case UnknownExplanation::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; + default: Unhandled() << e; + } + return out; +} + +} // namespace cvc5 diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h index 58fb2d08c..cf694cd3f 100644 --- a/src/api/cpp/cvc5_types.h +++ b/src/api/cpp/cvc5_types.h @@ -10,7 +10,8 @@ * directory for licensing information. * **************************************************************************** * - * Common cvc5 types. + * Common cvc5 types. These types are used internally as well as externally and + * the language bindings are generated automatically. */ #include "cvc5_export.h" @@ -18,8 +19,35 @@ #ifndef CVC5__API__CVC5_TYPES_H #define CVC5__API__CVC5_TYPES_H +#include + namespace cvc5 { +/** + * The different reasons for returning an "unknown" result. + */ +enum UnknownExplanation +{ + REQUIRES_FULL_CHECK, + INCOMPLETE, + TIMEOUT, + RESOURCEOUT, + MEMOUT, + INTERRUPTED, + NO_STATUS, + UNSUPPORTED, + OTHER, + UNKNOWN_REASON +}; + +/** + * Serialize an UnknownExplanation to given stream. + * @param out the output stream + * @param e the explanation to be serialized to the given output stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, UnknownExplanation e) CVC5_EXPORT; + /** * Rounding modes for floating-point numbers. * diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index bcade92a3..b274a5145 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -42,6 +42,7 @@ add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE}) set(JAVA_TYPES_FILES "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/BlockModelsMode.java" "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/RoundingMode.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/UnknownExplanation.java" ) add_custom_command( OUTPUT diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java index 856986136..d9361e51c 100644 --- a/src/api/java/io/github/cvc5/api/Result.java +++ b/src/api/java/io/github/cvc5/api/Result.java @@ -35,51 +35,6 @@ public class Result extends AbstractPointer // endregion - public enum UnknownExplanation { - REQUIRES_FULL_CHECK(0), - INCOMPLETE(1), - TIMEOUT(2), - RESOURCEOUT(3), - MEMOUT(4), - INTERRUPTED(5), - NO_STATUS(6), - UNSUPPORTED(7), - OTHER(8), - UNKNOWN_REASON(9); - - /* the int value of the UnknownExplanation */ - private int value; - private static Map explanationMap = new HashMap<>(); - private UnknownExplanation(int value) - { - this.value = value; - } - - static - { - for (UnknownExplanation explanation : UnknownExplanation.values()) - { - explanationMap.put(explanation.getValue(), explanation); - } - } - - public static UnknownExplanation fromInt(int value) throws CVC5ApiException - { - if (value < REQUIRES_FULL_CHECK.value || value > UNKNOWN_REASON.value) - { - throw new CVC5ApiException("UnknownExplanation value " + value - + " is outside the valid range [" + REQUIRES_FULL_CHECK.value + "," - + UNKNOWN_REASON.value + "]"); - } - return explanationMap.get(value); - } - - public int getValue() - { - return value; - } - } - /** * @return true if Result is empty, i.e., a nullary Result, and not an actual * result returned from a checkSat() (and friends) query. diff --git a/src/api/parseenums.py b/src/api/parseenums.py index 172d46089..6c9391469 100644 --- a/src/api/parseenums.py +++ b/src/api/parseenums.py @@ -162,7 +162,8 @@ class EnumParser: if ENUM_END in line: self.in_enum = False - break + self.last_value = -1 + continue elif self.in_enum: if line == OCB: continue @@ -189,7 +190,7 @@ class EnumParser: fmt_comment = self.format_comment( self.latest_block_comment) enum.enumerators_doc[name] = fmt_comment - elif ENUM_START in line: + elif line.startswith(ENUM_START): self.in_enum = True tokens = line.split() name = tokens[1] diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index da78b1888..ad354bb84 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -9,7 +9,7 @@ from libcpp.vector cimport vector from libcpp.map cimport map from libcpp.pair cimport pair from cvc5kinds cimport Kind -from cvc5types cimport RoundingMode +from cvc5types cimport RoundingMode, UnknownExplanation cdef extern from "" namespace "std": @@ -203,11 +203,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": bint isUnknown() except + string toString() except + - cdef extern from "api/cpp/cvc5.h" namespace "cvc5::Result": - cdef cppclass UnknownExplanation: - pass - - cdef cppclass Solver: Solver() except + Sort getBooleanSort() except + @@ -533,16 +528,3 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": cdef cppclass TermHashFunction: TermHashFunction() except + size_t operator()(const Term & t) except + - - -cdef extern from "api/cpp/cvc5.h" namespace "cvc5::Result::UnknownExplanation": - cdef UnknownExplanation REQUIRES_FULL_CHECK - cdef UnknownExplanation INCOMPLETE - cdef UnknownExplanation TIMEOUT - cdef UnknownExplanation RESOURCEOUT - cdef UnknownExplanation MEMOUT - cdef UnknownExplanation INTERRUPTED - cdef UnknownExplanation NO_STATUS - cdef UnknownExplanation UNSUPPORTED - cdef UnknownExplanation OTHER - cdef UnknownExplanation UNKNOWN_REASON diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 637f46cd3..a8e5b13ef 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -22,7 +22,6 @@ from cvc5 cimport DatatypeDecl as c_DatatypeDecl from cvc5 cimport DatatypeSelector as c_DatatypeSelector from cvc5 cimport Result as c_Result from cvc5 cimport SynthResult as c_SynthResult -from cvc5 cimport UnknownExplanation as c_UnknownExplanation from cvc5 cimport Op as c_Op from cvc5 cimport OptionInfo as c_OptionInfo from cvc5 cimport holds as c_holds @@ -32,10 +31,6 @@ from cvc5 cimport Statistics as c_Statistics from cvc5 cimport Stat as c_Stat from cvc5 cimport Grammar as c_Grammar from cvc5 cimport Sort as c_Sort -from cvc5 cimport REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT -from cvc5 cimport RESOURCEOUT, MEMOUT, INTERRUPTED -from cvc5 cimport NO_STATUS, UNSUPPORTED, UNKNOWN_REASON -from cvc5 cimport OTHER from cvc5 cimport Term as c_Term from cvc5 cimport hash as c_hash from cvc5 cimport wstring as c_wstring @@ -43,6 +38,7 @@ from cvc5 cimport tuple as c_tuple from cvc5 cimport get0, get1, get2 from cvc5kinds cimport Kind as c_Kind from cvc5types cimport RoundingMode as c_RoundingMode +from cvc5types cimport UnknownExplanation as c_UnknownExplanation cdef extern from "Python.h": wchar_t* PyUnicode_AsWideCharString(object, Py_ssize_t *) @@ -669,32 +665,6 @@ cdef class SynthResult: def __repr__(self): return self.cr.toString().decode() -cdef class UnknownExplanation: - """ - Wrapper class for :cpp:enum:`cvc5::Result::UnknownExplanation`. - """ - cdef c_UnknownExplanation cue - cdef str name - def __cinit__(self, int ue): - # crm always assigned externally - self.cue = ue - self.name = __unknown_explanations[ue] - - def __eq__(self, UnknownExplanation other): - return ( self.cue) == ( other.cue) - - def __ne__(self, UnknownExplanation other): - return not self.__eq__(other) - - def __hash__(self): - return hash(( self.crm, self.name)) - - def __str__(self): - return self.name - - def __repr__(self): - return self.name - cdef class Solver: """Wrapper class for :cpp:class:`cvc5::Solver`.""" @@ -3777,31 +3747,3 @@ cdef class Term: res[k] = v return res - - -# Generate unknown explanations -cdef __unknown_explanations = { - REQUIRES_FULL_CHECK: "RequiresFullCheck", - INCOMPLETE: "Incomplete", - TIMEOUT: "Timeout", - RESOURCEOUT: "Resourceout", - MEMOUT: "Memout", - INTERRUPTED: "Interrupted", - NO_STATUS: "NoStatus", - UNSUPPORTED: "Unsupported", - OTHER: "Other", - UNKNOWN_REASON: "UnknownReason" -} - -mod_ref = sys.modules[__name__] -for ue_int, name in __unknown_explanations.items(): - u = UnknownExplanation(ue_int) - - if name in dir(mod_ref): - raise RuntimeError("Redefinition of Python UnknownExplanation %s."%name) - - setattr(mod_ref, name, u) - -del u -del ue_int -del name diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 801375db1..ed891e305 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -139,7 +139,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) if (d_solver->getOptionInfo("dump-models").boolValue() && (isResultSat || (res.isUnknown() - && res.getUnknownExplanation() == cvc5::Result::INCOMPLETE))) + && res.getUnknownExplanation() + == cvc5::UnknownExplanation::INCOMPLETE))) { getterCommands.emplace_back(new GetModelCommand()); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index f6b2e46a1..5a8553df2 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -364,7 +364,7 @@ Result PropEngine::checkSat() { if (options().base.preprocessOnly) { - return Result(Result::UNKNOWN, Result::REQUIRES_FULL_CHECK); + return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK); } // Reset the interrupted flag @@ -388,14 +388,14 @@ Result PropEngine::checkSat() { if( result == SAT_VALUE_UNKNOWN ) { ResourceManager* rm = resourceManager(); - Result::UnknownExplanation why = Result::INTERRUPTED; + UnknownExplanation why = UnknownExplanation::INTERRUPTED; if (rm->outOfTime()) { - why = Result::TIMEOUT; + why = UnknownExplanation::TIMEOUT; } if (rm->outOfResources()) { - why = Result::RESOURCEOUT; + why = UnknownExplanation::RESOURCEOUT; } return Result(Result::UNKNOWN, why); } @@ -407,7 +407,7 @@ Result PropEngine::checkSat() { Trace("prop") << "PropEngine::checkSat() => " << result << std::endl; if (result == SAT_VALUE_TRUE && d_theoryProxy->isIncomplete()) { - return Result(Result::UNKNOWN, Result::INCOMPLETE); + return Result(Result::UNKNOWN, UnknownExplanation::INCOMPLETE); } return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT); } diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 7247e4379..c15c07c4d 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -77,7 +77,7 @@ void Assertions::initializeCheckSat(const std::vector& assumptions) /* Assume: BIGAND assumptions */ d_assumptions = assumptions; - Result r(Result::UNKNOWN, Result::UNKNOWN_REASON); + Result r(Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON); for (const Node& e : d_assumptions) { // Substitute out any abstract values in ex. diff --git a/src/smt/command.cpp b/src/smt/command.cpp index eb144a73a..d2f80e853 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1846,7 +1846,8 @@ bool GetInstantiationsCommand::isEnabled(cvc5::Solver* solver, { return (res.isSat() || (res.isUnknown() - && res.getUnknownExplanation() == cvc5::Result::INCOMPLETE)) + && res.getUnknownExplanation() + == cvc5::UnknownExplanation::INCOMPLETE)) || res.isUnsat(); } void GetInstantiationsCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 39480919e..142ce2eab 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -64,7 +64,7 @@ class OptimizationResult { } OptimizationResult() - : d_result(Result::UNKNOWN, Result::UnknownExplanation::NO_STATUS), + : d_result(Result::UNKNOWN, UnknownExplanation::NO_STATUS), d_value(), d_infinity(FINITE) { diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 894f3dd21..accafc3d4 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -134,8 +134,9 @@ Result SmtSolver::checkSatisfiability(Assertions& as, ResourceManager* rm = d_env.getResourceManager(); if (rm->out()) { - Result::UnknownExplanation why = - rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; + UnknownExplanation why = rm->outOfResources() + ? UnknownExplanation::RESOURCEOUT + : UnknownExplanation::TIMEOUT; result = Result(Result::UNKNOWN, why); } else @@ -163,7 +164,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, || d_env.getOptions().smt.solveIntAsBV > 0) && result.getStatus() == Result::UNSAT) { - result = Result(Result::UNKNOWN, Result::UNKNOWN_REASON); + result = Result(Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON); } // flipped if we did a global negation if (as.isGlobalNegated()) @@ -188,7 +189,8 @@ Result SmtSolver::checkSatisfiability(Assertions& as, } else { - result = Result(Result::UNKNOWN, Result::UNKNOWN_REASON); + result = + Result(Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON); } } Trace("smt") << "SmtSolver::global negate returned " << result diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index a96f2fe25..2d38b26da 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -301,7 +301,7 @@ SynthResult SygusSolver::checkSynth(Assertions& as, bool isNext) else { // otherwise, we return "unknown" - sr = SynthResult(SynthResult::UNKNOWN, Result::UNKNOWN_REASON); + sr = SynthResult(SynthResult::UNKNOWN, UnknownExplanation::UNKNOWN_REASON); } return sr; } diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index 0b3a98dd2..6ea287e6c 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -38,7 +38,7 @@ Result quickCheck(Node& query) return Result(Result::SAT); } } - return Result(Result::UNKNOWN, Result::REQUIRES_FULL_CHECK); + return Result(Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK); } void initializeSubsolver(std::unique_ptr& smte, diff --git a/src/util/result.cpp b/src/util/result.cpp index 7e09fd721..740b58166 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -103,7 +103,7 @@ Result::Result(const std::string& instr, std::string inputName) } } -Result::UnknownExplanation Result::getUnknownExplanation() const +UnknownExplanation Result::getUnknownExplanation() const { PrettyCheckArgument(isUnknown(), this, "This result is not unknown, so the reason for " @@ -141,25 +141,6 @@ ostream& operator<<(ostream& out, enum Result::Status s) 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; - default: Unhandled() << e; - } - return out; -} - ostream& operator<<(ostream& out, const Result& r) { Language language = options::ioutils::getOutputLang(out); switch (language) { @@ -186,7 +167,7 @@ void Result::toStreamDefault(std::ostream& out) const { case Result::SAT: out << "sat"; break; case Result::UNKNOWN: out << "unknown"; - if (getUnknownExplanation() != Result::UNKNOWN_REASON) + if (getUnknownExplanation() != UnknownExplanation::UNKNOWN_REASON) { out << " (" << getUnknownExplanation() << ")"; } diff --git a/src/util/result.h b/src/util/result.h index 4897bb7e9..863b1d581 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -21,6 +21,7 @@ #include #include +#include "api/cpp/cvc5_types.h" #include "options/language.h" namespace cvc5::internal { @@ -47,20 +48,6 @@ class Result UNKNOWN }; - enum UnknownExplanation - { - REQUIRES_FULL_CHECK, - INCOMPLETE, - TIMEOUT, - RESOURCEOUT, - MEMOUT, - INTERRUPTED, - NO_STATUS, - UNSUPPORTED, - OTHER, - UNKNOWN_REASON - }; - public: Result(); @@ -123,7 +110,6 @@ class Result }; /* class Result */ std::ostream& operator<<(std::ostream& out, enum Result::Status s); -std::ostream& operator<<(std::ostream& out, enum Result::UnknownExplanation e); } // namespace cvc5::internal diff --git a/src/util/synth_result.cpp b/src/util/synth_result.cpp index bd4f0cd62..7d4f1a97f 100644 --- a/src/util/synth_result.cpp +++ b/src/util/synth_result.cpp @@ -22,19 +22,18 @@ using namespace std; namespace cvc5::internal { SynthResult::SynthResult() - : d_status(NONE), d_unknownExplanation(Result::UNKNOWN_REASON) + : d_status(NONE), d_unknownExplanation(UnknownExplanation::UNKNOWN_REASON) { } -SynthResult::SynthResult(Status s, - Result::UnknownExplanation unknownExplanation) +SynthResult::SynthResult(Status s, UnknownExplanation unknownExplanation) : d_status(s), d_unknownExplanation(unknownExplanation) { } SynthResult::Status SynthResult::getStatus() const { return d_status; } -Result::UnknownExplanation SynthResult::getUnknownExplanation() const +UnknownExplanation SynthResult::getUnknownExplanation() const { return d_unknownExplanation; } @@ -43,7 +42,7 @@ std::string SynthResult::toString() const { std::stringstream ss; ss << "(" << d_status; - if (d_unknownExplanation != Result::UNKNOWN_REASON) + if (d_unknownExplanation != UnknownExplanation::UNKNOWN_REASON) { ss << " :unknown-explanation " << d_unknownExplanation; } diff --git a/src/util/synth_result.h b/src/util/synth_result.h index 45287edd7..730d5c680 100644 --- a/src/util/synth_result.h +++ b/src/util/synth_result.h @@ -49,15 +49,15 @@ class SynthResult /** Default constructor */ SynthResult(); /** Constructor when the solution is not successful */ - SynthResult( - Status s, - Result::UnknownExplanation unknownExplanation = Result::UNKNOWN_REASON); + SynthResult(Status s, + UnknownExplanation unknownExplanation = + UnknownExplanation::UNKNOWN_REASON); /** Get the status */ Status getStatus() const; /** Get the unknown explanation */ - Result::UnknownExplanation getUnknownExplanation() const; + UnknownExplanation getUnknownExplanation() const; /** Get the string representation */ std::string toString() const; @@ -66,7 +66,7 @@ class SynthResult /** The status */ Status d_status; /** The unknown explanation */ - Result::UnknownExplanation d_unknownExplanation; + UnknownExplanation d_unknownExplanation; }; std::ostream& operator<<(std::ostream& out, const SynthResult& r); -- 2.30.2