From: Ouyancheng <1024842937@qq.com>
Date: Tue, 6 Jul 2021 03:22:14 +0000 (-0700)
Subject: Add some printing functions for OptimizationObjective and OptimizationResult (#6809)
X-Git-Tag: cvc5-1.0.0~1526
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=80efd9fb51d25a7e2f3de802b41e4802e42596d7;p=cvc5.git

Add some printing functions for OptimizationObjective and OptimizationResult (#6809)

Implement the operator << with std::ostream for OptimizationObjective and OptimizationResult. Currently only supports SMTLib2 or Sygus as output languages.
Objective: (maximize [node] :signed) or (minimize [node]) or ...
Result: (sat [expr]) or (unsat) or (unknown([explanation]) [expr/null])
---

diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index 027ba71ec..5730ea062 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -18,6 +18,8 @@
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 #include "omt/omt_optimizer.h"
+#include "options/base_options.h"
+#include "options/language.h"
 #include "options/smt_options.h"
 #include "smt/assertions.h"
 #include "smt/smt_engine.h"
@@ -28,6 +30,67 @@ using namespace cvc5::omt;
 namespace cvc5 {
 namespace smt {
 
+std::ostream& operator<<(std::ostream& out, const OptimizationResult& result)
+{
+  // check the output language first
+  OutputLanguage lang = language::SetLanguage::getLanguage(out);
+  if (!language::isOutputLang_smt2(lang))
+  {
+    Unimplemented()
+        << "Only the SMTLib2 language supports optimization right now";
+  }
+  out << "(" << result.getResult();
+  switch (result.getResult().isSat())
+  {
+    case Result::SAT:
+    case Result::SAT_UNKNOWN:
+    {
+      switch (result.isInfinity())
+      {
+        case OptimizationResult::FINITE:
+          out << "\t" << result.getValue();
+          break;
+        case OptimizationResult::POSTITIVE_INF: out << "\t+Inf"; break;
+        case OptimizationResult::NEGATIVE_INF: out << "\t-Inf"; break;
+        default: break;
+      }
+      break;
+    }
+    case Result::UNSAT: break;
+    default: Unreachable();
+  }
+  out << ")";
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out,
+                         const OptimizationObjective& objective)
+{
+  // check the output language first
+  OutputLanguage lang = language::SetLanguage::getLanguage(out);
+  if (!language::isOutputLang_smt2(lang))
+  {
+    Unimplemented()
+        << "Only the SMTLib2 language supports optimization right now";
+  }
+  out << "(";
+  switch (objective.getType())
+  {
+    case OptimizationObjective::MAXIMIZE: out << "maximize "; break;
+    case OptimizationObjective::MINIMIZE: out << "minimize "; break;
+    default: Unreachable();
+  }
+  TNode target = objective.getTarget();
+  TypeNode type = target.getType();
+  out << target;
+  if (type.isBitVector())
+  {
+    out << (objective.bvIsSigned() ? " :signed" : " :unsigned");
+  }
+  out << ")";
+  return out;
+}
+
 OptimizationSolver::OptimizationSolver(SmtEngine* parent)
     : d_parent(parent),
       d_optChecker(),
@@ -200,8 +263,8 @@ Result OptimizationSolver::optimizeLexicographicIterative()
     }
 
     // if the result for the current objective is unbounded
-    // then just stop
-    if (partialResult.isUnbounded()) break;
+    // (result is not finite) then just stop
+    if (partialResult.isInfinity() != OptimizationResult::FINITE) break;
   }
   // kill optChecker in case pareto misuses it
   d_optChecker.reset();
@@ -220,7 +283,7 @@ Result OptimizationSolver::optimizeParetoNaiveGIA()
 
   switch (satResult.isSat())
   {
-    case Result::Sat::UNSAT: return satResult;
+    case Result::Sat::UNSAT:
     case Result::Sat::SAT_UNKNOWN: return satResult;
     case Result::Sat::SAT:
     {
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index d13168780..339ba9ea7 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -30,36 +30,43 @@ class SmtEngine;
 
 namespace smt {
 
+class OptimizationObjective;
+class OptimizationResult;
+
 /**
- * The optimization result of an optimization objective
- * containing:
+ * The optimization result, containing:
  * - the optimization result: SAT/UNSAT/UNKNOWN
- * - the optimal value if SAT and bounded
+ * - the optimal value if SAT and finite
  *     (optimal value reached and it's not infinity),
- *   or an empty node if SAT and unbounded
- *     (optimal value is +inf for maximum or -inf for minimum),
+ *   or an empty node if SAT and infinite
  *   otherwise the value might be empty node
  *   or something suboptimal
- * - whether the objective is unbounded
+ * - whether the result is finite/+-infinity
  */
 class OptimizationResult
 {
  public:
+  enum IsInfinity
+  {
+    FINITE = 0,
+    POSTITIVE_INF,
+    NEGATIVE_INF
+  };
   /**
    * Constructor
    * @param type the optimization outcome
    * @param value the optimized value
-   * @param unbounded whether the objective is unbounded
+   * @param isInf whether the result is FINITE/POSITIVE_INF/NEGATIVE_INF
    **/
-  OptimizationResult(Result result, TNode value, bool unbounded = false)
-      : d_result(result), d_value(value), d_unbounded(unbounded)
+  OptimizationResult(Result result, TNode value, IsInfinity isInf = FINITE)
+      : d_result(result), d_value(value), d_infinity(isInf)
   {
   }
   OptimizationResult()
       : d_result(Result::Sat::SAT_UNKNOWN,
                  Result::UnknownExplanation::NO_STATUS),
         d_value(),
-        d_unbounded(false)
+        d_infinity(FINITE)
   {
   }
   ~OptimizationResult() = default;
@@ -74,7 +81,7 @@ class OptimizationResult
   /**
    * Returns the optimal value.
    * @return Node containing the optimal value,
-   *   if result is unbounded, this will be an empty node,
+   *   if result is infinite, this will be an empty node,
    *   if getResult() is UNSAT, it will return an empty node,
    *   if getResult() is SAT_UNKNOWN, it will return something suboptimal
    *   or an empty node, depending on how the solver runs.
@@ -82,28 +89,28 @@ class OptimizationResult
   Node getValue() const { return d_value; }
 
   /**
-   * Checks whether the objective is unbouned
-   * @return whether the objective is unbounded
-   *   if the objective is unbounded (this function returns true), 
-   *   then the optimal value is:
-   *   +inf, if it's maximize;
-   *   -inf, if it's minimize
+   * Checks whether the result is infinity
+   * @return whether the result is FINITE/POSITIVE_INF/NEGATIVE_INF
    **/
-  bool isUnbounded() const { return d_unbounded; }
+  IsInfinity isInfinity() const { return d_infinity; }
 
  private:
   /** indicating whether the result is SAT, UNSAT or UNKNOWN **/
   Result d_result;
-  /** if the result is bounded, this is storing the value **/
+  /** if the result is finite, this is storing the value **/
   Node d_value;
-  /** whether the objective is unbounded
-   * If this is true, then:
-   * if objective is maximize, it's +infinity;
-   * if objective is minimize, it's -infinity
-   **/
-  bool d_unbounded;
+  /** whether the result is finite/+infinity/-infinity **/
+  IsInfinity d_infinity;
 };
 
+/**
+ * To serialize the OptimizationResult.
+ * @param out the stream to put the serialized result
+ * @param result the OptimizationResult object to serialize
+ * @return the parameter out
+ **/
+std::ostream& operator<<(std::ostream& out, const OptimizationResult& result);
+
 /**
  * The optimization objective, which contains:
  * - the optimization target node,
@@ -165,6 +172,15 @@ class OptimizationObjective
   bool d_bvSigned;
 };
 
+/**
+ * To serialize the OptimizationObjective.
+ * @param out the stream to put the serialized result
+ * @param objective the OptimizationObjective object to serialize
+ * @return the parameter out
+ **/
+std::ostream& operator<<(std::ostream& out,
+                         const OptimizationObjective& objective);
+
 /**
  * A solver for optimization queries.
  *
@@ -251,7 +267,7 @@ class OptimizationSolver
 
   /**
    * Optimize multiple goals in Box order
-   * @return SAT if all of the objectives are optimal or unbounded;
+   * @return SAT if all of the objectives are optimal (could be infinite);
    *   UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
    *   SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
    **/
@@ -261,7 +277,7 @@ class OptimizationSolver
    * Optimize multiple goals in Lexicographic order,
    * using iterative implementation
    * @return SAT if the objectives are optimal,
-   *     if one of the objectives is unbounded,
+   *     if one of the objectives is unbounded (result is infinite),
    *     the optimization will stop at that objective;
    *   UNSAT if any of the objectives is UNSAT
    *     and optimization will stop at that objective;