From 80efd9fb51d25a7e2f3de802b41e4802e42596d7 Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Mon, 5 Jul 2021 20:22:14 -0700 Subject: [PATCH] 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]) --- src/smt/optimization_solver.cpp | 69 ++++++++++++++++++++++++++++++-- src/smt/optimization_solver.h | 70 ++++++++++++++++++++------------- 2 files changed, 109 insertions(+), 30 deletions(-) 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; -- 2.30.2