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.

diff --git a/src/api/cpp/cvc5_types.cpp b/src/api/cpp/cvc5_types.cpp
index 7930ae22af20104cfa17f5e63aac2244b9ad45e8..5239c6528f6d6b067705538428507e1931a8a7b6 100644 (file)
--- 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 909efc650b113417cb04abbd3e9415478fccdd8b..db99cf3c8df57a585366c460815498e8388b396d 100644 (file)
--- 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 142ce2eab97742bc0a02b2059b36367ae4930a86..599ddddf247aa05f49bc5590ff71d8300e51c52f 100644 (file)
--- 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; }