From f62b46414cc47762857a4e3241318733ca8c973d Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Fri, 28 May 2021 14:00:16 -0700 Subject: [PATCH] (Optimization) remove popObjective, add resetObjectives, rename pushObjective => addObjective (#6634) In order for OptimizationSolver to support pushing & popping, we could remove popObjective because it might be difficult to handle cases like: optSlv->pushObjective(...); optSlv->push(); optSlv->popObjective(); optSlv->pop(); In this case we need to add back the popped objective... If push/pop is supported, pop does not bring back objectives if you resetObjective but it will revert the objs you add. just like assertFormula and resetAssertions. --- src/smt/optimization_solver.cpp | 13 +++++----- src/smt/optimization_solver.h | 24 +++++++++---------- test/unit/theory/theory_bv_opt_white.cpp | 21 ++++++++-------- test/unit/theory/theory_int_opt_white.cpp | 16 ++++++------- .../theory/theory_opt_multigoal_white.cpp | 16 ++++++------- 5 files changed, 45 insertions(+), 45 deletions(-) diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 5f50c76c1..ffc49710a 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -55,24 +55,25 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt() Unreachable(); } -void OptimizationSolver::pushObjective( - TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned) +void OptimizationSolver::addObjective(TNode target, + OptimizationObjective::ObjectiveType type, + bool bvSigned) { if (!OMTOptimizer::nodeSupportsOptimization(target)) { CVC5_FATAL() - << "Objective not pushed: Target node does not support optimization"; + << "Objective failed to add: Target node does not support optimization"; } d_optChecker.reset(); d_objectives.emplace_back(target, type, bvSigned); d_results.emplace_back(OptimizationResult::UNKNOWN, Node()); } -void OptimizationSolver::popObjective() +void OptimizationSolver::resetObjectives() { d_optChecker.reset(); - d_objectives.pop_back(); - d_results.pop_back(); + d_objectives.clear(); + d_results.clear(); } std::vector OptimizationSolver::getValues() diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index b0f4de1c5..64591d8f1 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -171,12 +171,13 @@ class OptimizationSolver * v_x = max(x) s.t. phi(x, y) = sat * v_y = max(y) s.t. phi(x, y) = sat * - * Lexicographic: optimize the objectives one-by-one, in the order they push - * v_x = max(x) s.t. phi(x, y) = sat + * Lexicographic: optimize the objectives one-by-one, in the order they are + * added: + * v_x = max(x) s.t. phi(x, y) = sat * v_y = max(y) s.t. phi(v_x, y) = sat * * Pareto: optimize multiple goals to a state such that - * further optimization of one goal will worsen the other goal(s) + * further optimization of one goal will worsen the other goal(s) * (v_x, v_y) s.t. phi(v_x, v_y) = sat, and * forall (x, y), (phi(x, y) = sat) -> (x <= v_x or y <= v_y) **/ @@ -194,7 +195,7 @@ class OptimizationSolver ~OptimizationSolver() = default; /** - * Run the optimization loop for the pushed objective + * Run the optimization loop for the added objective * For multiple objective combination, it defaults to lexicographic, * and combination could be set by calling * setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO) @@ -202,22 +203,21 @@ class OptimizationSolver OptimizationResult::ResultType checkOpt(); /** - * Push an objective. - * @param target the Node representing the expression that will be optimized - *for + * Add an optimization objective. + * @param target 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 pushObjective(TNode target, - OptimizationObjective::ObjectiveType type, - bool bvSigned = false); + void addObjective(TNode target, + OptimizationObjective::ObjectiveType type, + bool bvSigned = false); /** - * Pop the most recently successfully-pushed objective. + * Clear all the added optimization objectives **/ - void popObjective(); + void resetObjectives(); /** * Returns the values of the optimized objective after checkOpt is called diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 42dcb9fee..66efe7eff 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -55,7 +55,7 @@ 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)); - d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false); + d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, (uint32_t)0x3FFFFFA1)); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } TEST_F(TestTheoryWhiteBVOpt, signed_min) @@ -76,7 +76,7 @@ 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)); - d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, true); + d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -87,7 +87,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) // expect the minimum x = -1 ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000)); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } TEST_F(TestTheoryWhiteBVOpt, unsigned_max) @@ -103,7 +103,7 @@ 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)); - d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, false); + d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -114,7 +114,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 2u)); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } TEST_F(TestTheoryWhiteBVOpt, signed_max) @@ -128,7 +128,7 @@ 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)); - d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, true); + d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -137,7 +137,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max) // expect the maxmum x = ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 10u)); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } TEST_F(TestTheoryWhiteBVOpt, min_boundary) @@ -152,7 +152,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) // that existed previously d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); - d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false); + d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -161,9 +161,8 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 18u)); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } - } // namespace test } // namespace cvc5 diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index efb963f16..f16db0c0e 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -60,7 +60,7 @@ TEST_F(TestTheoryWhiteIntOpt, max) d_smtEngine->assertFormula(lowb); // We activate our objective so the subsolver knows to optimize it - d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE); + d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("99")); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } TEST_F(TestTheoryWhiteIntOpt, min) @@ -91,7 +91,7 @@ TEST_F(TestTheoryWhiteIntOpt, min) d_smtEngine->assertFormula(lowb); // We activate our objective so the subsolver knows to optimize it - d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE); + d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -101,7 +101,7 @@ TEST_F(TestTheoryWhiteIntOpt, min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("1")); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } TEST_F(TestTheoryWhiteIntOpt, result) @@ -122,14 +122,14 @@ TEST_F(TestTheoryWhiteIntOpt, result) d_smtEngine->assertFormula(lowb); // We activate our objective so the subsolver knows to optimize it - d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE); + d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE); // This should return OPT_UNSAT since 0 > x > 100 is impossible. OptimizationResult::ResultType r = d_optslv->checkOpt(); // We expect our check to have returned UNSAT ASSERT_EQ(r, OptimizationResult::UNSAT); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } TEST_F(TestTheoryWhiteIntOpt, open_interval) @@ -155,7 +155,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) */ Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2); - d_optslv->pushObjective(cost3, OptimizationObjective::MINIMIZE); + d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE); OptimizationResult::ResultType r = d_optslv->checkOpt(); @@ -164,7 +164,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval) // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("112")); - d_optslv->popObjective(); + d_optslv->resetObjectives(); } } // namespace test diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index ed3de10a9..1950d9ae2 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -60,11 +60,11 @@ TEST_F(TestTheoryWhiteOptMultigoal, box) optSolver.setObjectiveCombination(OptimizationSolver::BOX); // minimize x - optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false); + optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. - optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true); + optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true); // maximize z - optSolver.pushObjective(z, OptimizationObjective::MAXIMIZE, false); + optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); OptimizationResult::ResultType r = optSolver.checkOpt(); @@ -103,11 +103,11 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex) optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); // minimize x - optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false); + optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); // maximize y with `signed` comparison over bit-vectors. - optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true); + optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true); // maximize z - optSolver.pushObjective(z, OptimizationObjective::MAXIMIZE, false); + optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); OptimizationResult::ResultType r = optSolver.checkOpt(); @@ -181,8 +181,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) */ OptimizationSolver optSolver(d_smtEngine.get()); optSolver.setObjectiveCombination(OptimizationSolver::PARETO); - optSolver.pushObjective(a, OptimizationObjective::MAXIMIZE); - optSolver.pushObjective(b, OptimizationObjective::MAXIMIZE); + optSolver.addObjective(a, OptimizationObjective::MAXIMIZE); + optSolver.addObjective(b, OptimizationObjective::MAXIMIZE); OptimizationResult::ResultType r; -- 2.30.2