From 67a1510b8e6306993d7efb7671b8f0aa53a45deb Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Fri, 30 Apr 2021 14:40:49 -0700 Subject: [PATCH] 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/omt/bitvector_optimizer.cpp | 32 ++-- src/omt/bitvector_optimizer.h | 8 +- src/omt/integer_optimizer.cpp | 28 ++-- src/omt/integer_optimizer.h | 17 +- src/omt/omt_optimizer.cpp | 2 +- src/omt/omt_optimizer.h | 20 ++- src/smt/optimization_solver.cpp | 70 +++----- src/smt/optimization_solver.h | 186 +++++++++++++++------- test/unit/theory/theory_bv_opt_white.cpp | 75 ++++----- test/unit/theory/theory_int_opt_white.cpp | 50 +++--- 10 files changed, 257 insertions(+), 231 deletions(-) diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index ab5af03f7..7edecdb73 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -43,8 +43,8 @@ BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a, + aMod2PlusbMod2Div2)); } -std::pair OMTOptimizerBitVector::minimize( - SmtEngine* parentSMTSolver, Node target) +OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* parentSMTSolver, + TNode target) { // the smt engine to which we send intermediate queries // for the binary search. @@ -56,11 +56,11 @@ std::pair OMTOptimizerBitVector::minimize( Node value; if (intermediateSatResult.isUnknown()) { - return std::make_pair(OptResult::OPT_UNKNOWN, value); + return OptimizationResult(OptimizationResult::UNKNOWN, value); } if (intermediateSatResult.isSat() == Result::UNSAT) { - return std::make_pair(OptResult::OPT_UNSAT, value); + return OptimizationResult(OptimizationResult::UNSAT, value); } // value equals to upperBound @@ -107,7 +107,7 @@ std::pair OMTOptimizerBitVector::minimize( intermediateSatResult = optChecker->checkSat(); if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) { - return std::make_pair(OptResult::OPT_UNKNOWN, value); + return OptimizationResult(OptimizationResult::UNKNOWN, value); } if (intermediateSatResult.isSat() == Result::SAT) { @@ -121,7 +121,7 @@ std::pair OMTOptimizerBitVector::minimize( // lowerBound == pivot ==> upperbound = lowerbound + 1 // and lowerbound <= target < upperbound is UNSAT // return the upperbound - return std::make_pair(OptResult::OPT_OPTIMAL, value); + return OptimizationResult(OptimizationResult::OPTIMAL, value); } else { @@ -130,15 +130,15 @@ std::pair OMTOptimizerBitVector::minimize( } else { - return std::make_pair(OptResult::OPT_UNKNOWN, value); + return OptimizationResult(OptimizationResult::UNKNOWN, value); } optChecker->pop(); } - return std::make_pair(OptResult::OPT_OPTIMAL, value); + return OptimizationResult(OptimizationResult::OPTIMAL, value); } -std::pair OMTOptimizerBitVector::maximize( - SmtEngine* parentSMTSolver, Node target) +OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* parentSMTSolver, + TNode target) { // the smt engine to which we send intermediate queries // for the binary search. @@ -150,11 +150,11 @@ std::pair OMTOptimizerBitVector::maximize( Node value; if (intermediateSatResult.isUnknown()) { - return std::make_pair(OptResult::OPT_UNKNOWN, value); + return OptimizationResult(OptimizationResult::UNKNOWN, value); } if (intermediateSatResult.isSat() == Result::UNSAT) { - return std::make_pair(OptResult::OPT_UNSAT, value); + return OptimizationResult(OptimizationResult::UNSAT, value); } // value equals to upperBound @@ -198,7 +198,7 @@ std::pair OMTOptimizerBitVector::maximize( intermediateSatResult = optChecker->checkSat(); if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) { - return std::make_pair(OptResult::OPT_UNKNOWN, value); + return OptimizationResult(OptimizationResult::UNKNOWN, value); } if (intermediateSatResult.isSat() == Result::SAT) { @@ -212,7 +212,7 @@ std::pair OMTOptimizerBitVector::maximize( // upperbound = lowerbound + 1 // and lowerbound < target <= upperbound is UNSAT // return the lowerbound - return std::make_pair(OptResult::OPT_OPTIMAL, value); + return OptimizationResult(OptimizationResult::OPTIMAL, value); } else { @@ -221,11 +221,11 @@ std::pair OMTOptimizerBitVector::maximize( } else { - return std::make_pair(OptResult::OPT_UNKNOWN, value); + return OptimizationResult(OptimizationResult::UNKNOWN, value); } optChecker->pop(); } - return std::make_pair(OptResult::OPT_OPTIMAL, value); + return OptimizationResult(OptimizationResult::OPTIMAL, value); } } // namespace cvc5::omt diff --git a/src/omt/bitvector_optimizer.h b/src/omt/bitvector_optimizer.h index 98dc63b3f..b95c185f8 100644 --- a/src/omt/bitvector_optimizer.h +++ b/src/omt/bitvector_optimizer.h @@ -28,10 +28,10 @@ class OMTOptimizerBitVector : public OMTOptimizer public: OMTOptimizerBitVector(bool isSigned); virtual ~OMTOptimizerBitVector() = default; - std::pair minimize(SmtEngine* parentSMTSolver, - Node target) override; - std::pair maximize(SmtEngine* parentSMTSolver, - Node target) override; + smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + TNode target) override; + smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + TNode target) override; private: /** diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index f3ee24b3d..8fbfff1a2 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -21,8 +21,10 @@ using namespace cvc5::smt; namespace cvc5::omt { -std::pair OMTOptimizerInteger::optimize( - SmtEngine* parentSMTSolver, Node target, ObjectiveType objType) +OptimizationResult OMTOptimizerInteger::optimize( + SmtEngine* parentSMTSolver, + TNode target, + OptimizationObjective::ObjectiveType objType) { // linear search for integer goal // the smt engine to which we send intermediate queries @@ -36,22 +38,22 @@ std::pair OMTOptimizerInteger::optimize( Node value; if (intermediateSatResult.isUnknown()) { - return std::make_pair(OptResult::OPT_UNKNOWN, value); + return OptimizationResult(OptimizationResult::UNKNOWN, value); } if (intermediateSatResult.isSat() == Result::UNSAT) { - return std::make_pair(OptResult::OPT_UNSAT, value); + return OptimizationResult(OptimizationResult::UNSAT, value); } // asserts objective > old_value (used in optimization loop) Node increment; Kind incrementalOperator = kind::NULL_EXPR; - if (objType == ObjectiveType::OBJECTIVE_MINIMIZE) + if (objType == OptimizationObjective::MINIMIZE) { // if objective is MIN, then assert optimization_target < // current_model_value incrementalOperator = kind::LT; } - else if (objType == ObjectiveType::OBJECTIVE_MAXIMIZE) + else if (objType == OptimizationObjective::MAXIMIZE) { // if objective is MAX, then assert optimization_target > // current_model_value @@ -69,20 +71,20 @@ std::pair OMTOptimizerInteger::optimize( optChecker->assertFormula(increment); intermediateSatResult = optChecker->checkSat(); } - return std::make_pair(OptResult::OPT_OPTIMAL, value); + return OptimizationResult(OptimizationResult::OPTIMAL, value); } -std::pair OMTOptimizerInteger::minimize( - SmtEngine* parentSMTSolver, Node target) +OptimizationResult OMTOptimizerInteger::minimize( + SmtEngine* parentSMTSolver, TNode target) { return this->optimize( - parentSMTSolver, target, ObjectiveType::OBJECTIVE_MINIMIZE); + parentSMTSolver, target, OptimizationObjective::MINIMIZE); } -std::pair OMTOptimizerInteger::maximize( - SmtEngine* parentSMTSolver, Node target) +OptimizationResult OMTOptimizerInteger::maximize( + SmtEngine* parentSMTSolver, TNode target) { return this->optimize( - parentSMTSolver, target, ObjectiveType::OBJECTIVE_MAXIMIZE); + parentSMTSolver, target, OptimizationObjective::MAXIMIZE); } } // namespace cvc5::omt diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h index d92bdb8eb..48d162494 100644 --- a/src/omt/integer_optimizer.h +++ b/src/omt/integer_optimizer.h @@ -28,19 +28,20 @@ class OMTOptimizerInteger : public OMTOptimizer public: OMTOptimizerInteger() = default; virtual ~OMTOptimizerInteger() = default; - std::pair minimize(SmtEngine* parentSMTSolver, - Node target) override; - std::pair maximize(SmtEngine* parentSMTSolver, - Node target) override; + smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + TNode target) override; + smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + TNode target) override; private: /** * Handles the optimization query specified by objType - * (objType = OBJECTIVE_MINIMIZE / OBJECTIVE_MAXIMIZE) + * (objType = MINIMIZE / MAXIMIZE) **/ - std::pair optimize(SmtEngine* parentSMTSolver, - Node target, - smt::ObjectiveType objType); + smt::OptimizationResult optimize( + SmtEngine* parentSMTSolver, + TNode target, + smt::OptimizationObjective::ObjectiveType objType); }; } // namespace cvc5::omt diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index b0a8af63a..49b07fe26 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -26,7 +26,7 @@ using namespace cvc5::theory; using namespace cvc5::smt; namespace cvc5::omt { -std::unique_ptr OMTOptimizer::getOptimizerForNode(Node targetNode, +std::unique_ptr OMTOptimizer::getOptimizerForNode(TNode targetNode, bool isSigned) { // the datatype of the target node diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h index 1e4c6d4ca..792a60169 100644 --- a/src/omt/omt_optimizer.h +++ b/src/omt/omt_optimizer.h @@ -39,7 +39,7 @@ class OMTOptimizer * and this is the optimizer for targetNode **/ static std::unique_ptr getOptimizerForNode( - Node targetNode, bool isSigned = false); + TNode targetNode, bool isSigned = false); /** * Initialize an SMT subsolver for offline optimization purpose @@ -60,24 +60,22 @@ class OMTOptimizer * @param parentSMTSolver an SMT solver encoding the assertions as the * constraints * @param target the target expression to optimize - * @return pair: the result of optimization and the optimized - * value, if OptResult is OPT_UNKNOWN, value returned could be empty node or - * something suboptimal. + * @return smt::OptimizationResult the result of optimization, containing + * whether it's optimal and the optimized value. **/ - virtual std::pair minimize(SmtEngine* parentSMTSolver, - Node target) = 0; + virtual smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + TNode target) = 0; /** * Maximize the target node with constraints encoded in parentSMTSolver * * @param parentSMTSolver an SMT solver encoding the assertions as the * constraints * @param target the target expression to optimize - * @return pair: the result of optimization and the optimized - * value, if OptResult is OPT_UNKNOWN, value returned could be empty node or - * something suboptimal. + * @return smt::OptimizationResult the result of optimization, containing + * whether it's optimal and the optimized value. **/ - virtual std::pair maximize(SmtEngine* parentSMTSolver, - Node target) = 0; + virtual smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + TNode target) = 0; }; } // namespace cvc5::omt 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 diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index f94f37a19..2617472a2 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -54,19 +54,15 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); - const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MINIMIZE; - d_optslv->activateObj(x, obj_type, false); + d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(BitVector(32u, (unsigned)0x3FFFFFA1))); - - std::cout << "Passed!" << std::endl; - std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() - << std::endl; + ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), + BitVector(32u, (uint32_t)0x3FFFFFA1)); + d_optslv->popObjective(); } TEST_F(TestTheoryWhiteBVOpt, signed_min) @@ -79,22 +75,18 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); - const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MINIMIZE; - d_optslv->activateObj(x, obj_type, true); + d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, true); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); - BitVector val = d_optslv->objectiveGetValue().getConst(); + BitVector val = d_optslv->getValues()[0].getValue().getConst(); std::cout << "opt value is: " << val << std::endl; // expect the minimum x = -1 - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000))); - std::cout << "Passed!" << std::endl; - std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() - << std::endl; + ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000)); + d_optslv->popObjective(); } TEST_F(TestTheoryWhiteBVOpt, unsigned_max) @@ -110,20 +102,18 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); - const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MAXIMIZE; - d_optslv->activateObj(x, obj_type, false); + d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, false); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); - BitVector val = d_optslv->objectiveGetValue().getConst(); + BitVector val = d_optslv->getValues()[0].getValue().getConst(); std::cout << "opt value is: " << val << std::endl; - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(BitVector(32u, (unsigned)2))); - std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() - << std::endl; + ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), + BitVector(32u, 2u)); + d_optslv->popObjective(); } TEST_F(TestTheoryWhiteBVOpt, signed_max) @@ -137,18 +127,16 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); - const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MAXIMIZE; - d_optslv->activateObj(x, obj_type, true); + d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, true); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); // expect the maxmum x = - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(BitVector(32u, 10u))); - std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() - << std::endl; + ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), + BitVector(32u, 10u)); + d_optslv->popObjective(); } TEST_F(TestTheoryWhiteBVOpt, min_boundary) @@ -163,17 +151,16 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) // that existed previously d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - d_optslv->activateObj(x, ObjectiveType::OBJECTIVE_MINIMIZE, false); + d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); // expect the maximum x = 18 - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(BitVector(32u, 18u))); - std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() - << std::endl; + ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), + BitVector(32u, 18u)); + d_optslv->popObjective(); } } // namespace test diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index e8daef819..9d5c5c03f 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -58,21 +58,19 @@ TEST_F(TestTheoryWhiteIntOpt, max) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - const ObjectiveType max_type = ObjectiveType::OBJECTIVE_MAXIMIZE; // We activate our objective so the subsolver knows to optimize it - d_optslv->activateObj(max_cost, max_type); + d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); // We expect max_cost == 99 - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(Rational("99"))); + ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), + Rational("99")); - std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue() - << std::endl; + d_optslv->popObjective(); } TEST_F(TestTheoryWhiteIntOpt, min) @@ -92,21 +90,19 @@ TEST_F(TestTheoryWhiteIntOpt, min) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - const ObjectiveType min_type = ObjectiveType::OBJECTIVE_MINIMIZE; // We activate our objective so the subsolver knows to optimize it - d_optslv->activateObj(max_cost, min_type); + d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); // We expect max_cost == 99 - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(Rational("1"))); + ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), + Rational("1")); - std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue() - << std::endl; + d_optslv->popObjective(); } TEST_F(TestTheoryWhiteIntOpt, result) @@ -126,16 +122,16 @@ TEST_F(TestTheoryWhiteIntOpt, result) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - const ObjectiveType max_type = ObjectiveType::OBJECTIVE_MAXIMIZE; // We activate our objective so the subsolver knows to optimize it - d_optslv->activateObj(max_cost, max_type); + d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE); // This should return OPT_UNSAT since 0 > x > 100 is impossible. - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); // We expect our check to have returned UNSAT - ASSERT_EQ(r, OptResult::OPT_UNSAT); + ASSERT_EQ(r, OptimizationResult::UNSAT); + d_optslv->popObjective(); } TEST_F(TestTheoryWhiteIntOpt, open_interval) @@ -161,18 +157,16 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) */ Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2); - const ObjectiveType min_type = ObjectiveType::OBJECTIVE_MINIMIZE; - d_optslv->activateObj(cost3, min_type); + d_optslv->pushObjective(cost3, OptimizationObjective::MINIMIZE); - OptResult r = d_optslv->checkOpt(); + OptimizationResult::ResultType r = d_optslv->checkOpt(); - ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 - ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(Rational("112"))); - std::cout << "Optimized min value is: " << d_optslv->objectiveGetValue() - << std::endl; + ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), + Rational("112")); + d_optslv->popObjective(); } } // namespace test -- 2.30.2