From 6987d112496849d72b34d93d482c3555d1634fea Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 1 Apr 2022 05:36:48 -0700 Subject: [PATCH] Remove `UnknownExplanation::NO_STATUS` (#8518) Result already supports storing a NONE result, so UnknownExplanation::NO_STATUS seems redundant. This removes that explanation, which was only being used in the optimization solver. --- src/api/cpp/cvc5_types.cpp | 1 - src/api/cpp/cvc5_types.h | 1 - src/smt/optimization_solver.h | 9 ++------- 3 files changed, 2 insertions(+), 9 deletions(-) diff --git a/src/api/cpp/cvc5_types.cpp b/src/api/cpp/cvc5_types.cpp index 7930ae22a..5239c6528 100644 --- a/src/api/cpp/cvc5_types.cpp +++ b/src/api/cpp/cvc5_types.cpp @@ -34,7 +34,6 @@ std::ostream& operator<<(std::ostream& out, UnknownExplanation e) 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; diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h index 909efc650..db99cf3c8 100644 --- a/src/api/cpp/cvc5_types.h +++ b/src/api/cpp/cvc5_types.h @@ -34,7 +34,6 @@ enum UnknownExplanation RESOURCEOUT, MEMOUT, INTERRUPTED, - NO_STATUS, UNSUPPORTED, OTHER, UNKNOWN_REASON diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 142ce2eab..599ddddf2 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -63,18 +63,13 @@ class OptimizationResult : d_result(result), d_value(value), d_infinity(isInf) { } - OptimizationResult() - : d_result(Result::UNKNOWN, UnknownExplanation::NO_STATUS), - d_value(), - d_infinity(FINITE) - { - } + OptimizationResult() : d_result(), d_value(), d_infinity(FINITE) {} ~OptimizationResult() = default; /** * Returns an enum indicating whether * the result is SAT or not. - * @return whether the result is SAT, UNSAT or UNKNOWN + * @return whether the result is SAT, UNSAT or NONE **/ Result getResult() const { return d_result; } -- 2.30.2