From 67a1510b8e6306993d7efb7671b8f0aa53a45deb Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Fri, 30 Apr 2021 14:40:49 -0700 Subject: Refactor optimization result and objective classes + add preliminary support for multiple objectives (#6459) This PR is one part of multiple. Preliminary support means currently only supports single objective. It supports queue-ing up objectives and it always optimizes the first. Multiple-obj optimization algorithm will be up next. * Refactor optimization result and objective classes * Add preliminary support for multiple objectives * The unit tests are now comparing node values instead of node addresses --- src/smt/optimization_solver.cpp | 70 +++++---------- src/smt/optimization_solver.h | 186 +++++++++++++++++++++++++++------------- 2 files changed, 150 insertions(+), 106 deletions(-) (limited to 'src/smt') diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index f854ec402..1c8fe6514 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -16,78 +16,54 @@ #include "smt/optimization_solver.h" #include "omt/omt_optimizer.h" +#include "smt/assertions.h" using namespace cvc5::theory; using namespace cvc5::omt; namespace cvc5 { namespace smt { -/** - * d_activatedObjective is initialized to a default objective: - * default objective constructed with Null Node and OBJECTIVE_UNDEFINED - * - * d_savedValue is initialized to a default node (Null Node) - */ - -OptimizationSolver::OptimizationSolver(SmtEngine* parent) - : d_parent(parent), - d_activatedObjective(Node(), ObjectiveType::OBJECTIVE_UNDEFINED), - d_savedValue() +OptimizationResult::ResultType OptimizationSolver::checkOpt() { -} - -OptimizationSolver::~OptimizationSolver() {} - -OptResult OptimizationSolver::checkOpt() -{ - // Make sure that the objective is not the default one - Assert(d_activatedObjective.getType() != ObjectiveType::OBJECTIVE_UNDEFINED); - Assert(!d_activatedObjective.getNode().isNull()); - + Assert(d_objectives.size() == 1); + // NOTE: currently we are only dealing with single obj std::unique_ptr optimizer = OMTOptimizer::getOptimizerForNode( - d_activatedObjective.getNode(), d_activatedObjective.getSigned()); + d_objectives[0].getTarget(), d_objectives[0].bvIsSigned()); - Assert(optimizer != nullptr); + if (!optimizer) return OptimizationResult::UNSUPPORTED; - std::pair optResult; - if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MAXIMIZE) + OptimizationResult optResult; + if (d_objectives[0].getType() == OptimizationObjective::MAXIMIZE) { - optResult = optimizer->maximize(this->d_parent, - this->d_activatedObjective.getNode()); + optResult = optimizer->maximize(d_parent, d_objectives[0].getTarget()); } - else if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MINIMIZE) + else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE) { - optResult = optimizer->minimize(this->d_parent, - this->d_activatedObjective.getNode()); + optResult = optimizer->minimize(d_parent, d_objectives[0].getTarget()); } - this->d_savedValue = optResult.second; - return optResult.first; + d_results[0] = optResult; + return optResult.getType(); } -void OptimizationSolver::activateObj(const Node& obj, - const ObjectiveType type, - bool bvSigned) +void OptimizationSolver::pushObjective( + TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned) { - d_activatedObjective = Objective(obj, type, bvSigned); + d_objectives.emplace_back(target, type, bvSigned); + d_results.emplace_back(OptimizationResult::UNSUPPORTED, Node()); } -Node OptimizationSolver::objectiveGetValue() +void OptimizationSolver::popObjective() { - Assert(!d_savedValue.isNull()); - return d_savedValue; + d_objectives.pop_back(); + d_results.pop_back(); } -Objective::Objective(Node obj, ObjectiveType type, bool bvSigned) - : d_type(type), d_node(obj), d_bvSigned(bvSigned) +std::vector OptimizationSolver::getValues() { + Assert(d_objectives.size() == d_results.size()); + return d_results; } -ObjectiveType Objective::getType() { return d_type; } - -Node Objective::getNode() { return d_node; } - -bool Objective::getSigned() { return d_bvSigned; } - } // namespace smt } // namespace cvc5 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 59c228e27..0babd7a4a 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -20,7 +20,6 @@ #include "expr/node.h" #include "expr/type_node.h" -#include "smt/assertions.h" #include "util/result.h" namespace cvc5 { @@ -30,40 +29,67 @@ class SmtEngine; namespace smt { /** - * An enum for optimization queries. - * - * Represents whether an objective should be minimized or maximized - */ -enum class ObjectiveType -{ - OBJECTIVE_MINIMIZE, - OBJECTIVE_MAXIMIZE, - OBJECTIVE_UNDEFINED -}; - -/** - * An enum for optimization queries. - * - * Represents the result of a checkopt query - * (unimplemented) OPT_OPTIMAL: if value was found + * The optimization result of an optimization objective + * containing: + * - whether it's optimal or not + * - if so, the optimal value, otherwise the value might be empty node or + * something suboptimal */ -enum class OptResult +class OptimizationResult { - // the original set of assertions has result UNKNOWN - OPT_UNKNOWN, - // the original set of assertions has result UNSAT - OPT_UNSAT, - // the optimization loop finished and optimal - OPT_OPTIMAL, + public: + /** + * Enum indicating whether the checkOpt result + * is optimal or not. + **/ + enum ResultType + { + // the type of the target is not supported + UNSUPPORTED, + // whether the value is optimal is UNKNOWN + UNKNOWN, + // the original set of assertions has result UNSAT + UNSAT, + // the value is optimal + OPTIMAL, + // the goal is unbounded, + // if objective is maximize, it's +infinity + // if objective is minimize, it's -infinity + UNBOUNDED, + }; - // the goal is unbounded, so it would be -inf or +inf - OPT_UNBOUNDED, + /** + * Constructor + * @param type the optimization outcome + * @param value the optimized value + **/ + OptimizationResult(ResultType type, TNode value) + : d_type(type), d_value(value) + { + } + OptimizationResult() : d_type(UNSUPPORTED), d_value() {} + ~OptimizationResult() = default; - // The last value is here as a preparation for future work - // in which pproximate optimizations will be supported. + /** + * Returns an enum indicating whether + * the result is optimal or not. + * @return an enum showing whether the result is optimal, unbounded, + * unsat, unknown or unsupported. + **/ + ResultType getType() { return d_type; } + /** + * Returns the optimal value. + * @return Node containing the optimal value, + * if getType() is not OPTIMAL, it might return an empty node or a node + * containing non-optimal value + **/ + Node getValue() { return d_value; } - // if the solver halted early and value is only approximate - OPT_SAT_APPROX + private: + /** the indicating whether the result is optimal or something else **/ + ResultType d_type; + /** if the result is optimal, this is storing the optimal value **/ + Node d_value; }; /** @@ -72,38 +98,58 @@ enum class OptResult * - whether it's maximize/minimize * - and whether it's signed for BitVectors */ -class Objective +class OptimizationObjective { public: + /** + * An enum for optimization queries. + * Represents whether an objective should be minimized or maximized + */ + enum ObjectiveType + { + MINIMIZE, + MAXIMIZE, + }; + /** * Constructor - * @param n the optimization target node + * @param target the optimization target node * @param type speficies whether it's maximize/minimize * @param bvSigned specifies whether it's using signed or unsigned comparison * for BitVectors this parameter is only valid when the type of target node * is BitVector **/ - Objective(Node n, ObjectiveType type, bool bvSigned = false); - ~Objective(){}; + OptimizationObjective(TNode target, ObjectiveType type, bool bvSigned = false) + : d_type(type), d_target(target), d_bvSigned(bvSigned) + { + } + ~OptimizationObjective() = default; /** A getter for d_type **/ - ObjectiveType getType(); - /** A getter for d_node **/ - Node getNode(); + ObjectiveType getType() { return d_type; } + + /** A getter for d_target **/ + Node getTarget() { return d_target; } + /** A getter for d_bvSigned **/ - bool getSigned(); + bool bvIsSigned() { return d_bvSigned; } private: - /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR - * OBJECTIVE_MINIMIZE **/ + /** + * The type of objective, + * it's either MAXIMIZE OR MINIMIZE + **/ ObjectiveType d_type; - /** The node associated to the term that was used to construct the objective. - * **/ - Node d_node; - /** Specify whether to use signed or unsigned comparison + /** + * The node associated to the term that was used to construct the objective. + **/ + Node d_target; + + /** + * Specify whether to use signed or unsigned comparison * for BitVectors (only for BitVectors), this variable is defaulted to false - * **/ + **/ bool d_bvSigned; }; @@ -122,32 +168,54 @@ class OptimizationSolver * Constructor * @param parent the smt_solver that the user added their assertions to **/ - OptimizationSolver(SmtEngine* parent); - ~OptimizationSolver(); + OptimizationSolver(SmtEngine* parent) + : d_parent(parent), d_objectives(), d_results() + { + } + ~OptimizationSolver() = default; - /** Runs the optimization loop for the activated objective **/ - OptResult checkOpt(); /** - * Activates an objective: will be optimized for - * @param obj the Node representing the expression that will be optimized for + * Run the optimization loop for the pushed objective + * NOTE: this function currently supports only single objective + * for multiple pushed objectives it always optimizes the first one. + * Add support for multi-obj later + */ + OptimizationResult::ResultType checkOpt(); + + /** + * Push an objective. + * @param target the Node representing the expression that will be optimized + *for * @param type specifies whether it's maximize or minimize * @param bvSigned specifies whether we should use signed/unsigned * comparison for BitVectors (only effective for BitVectors) * and its default is false **/ - void activateObj(const Node& obj, - const ObjectiveType type, - bool bvSigned = false); - /** Gets the value of the optimized objective after checkopt is called **/ - Node objectiveGetValue(); + void pushObjective(TNode target, + OptimizationObjective::ObjectiveType type, + bool bvSigned = false); + + /** + * Pop the most recent objective. + **/ + void popObjective(); + + /** + * Returns the values of the optimized objective after checkOpt is called + * @return a vector of Optimization Result, + * each containing the outcome and the value. + **/ + std::vector getValues(); private: /** The parent SMT engine **/ SmtEngine* d_parent; + /** The objectives to optimize for **/ - Objective d_activatedObjective; - /** A saved value of the objective from the last sat call. **/ - Node d_savedValue; + std::vector d_objectives; + + /** The results of the optimizations from the last checkOpt call **/ + std::vector d_results; }; } // namespace smt -- cgit v1.2.3