From 0c982a7486ef9b6991589685f9091602e0cf5572 Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Wed, 9 Jun 2021 08:53:16 -0700 Subject: [PATCH] [Optimization] support for push/pop (#6706) Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop). SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function. --- src/omt/integer_optimizer.h | 9 ++- src/omt/omt_optimizer.cpp | 16 +++-- src/omt/omt_optimizer.h | 6 +- src/smt/optimization_solver.cpp | 20 +++--- src/smt/optimization_solver.h | 21 +++--- test/unit/theory/theory_bv_opt_white.cpp | 10 +-- test/unit/theory/theory_int_opt_white.cpp | 8 +-- .../theory/theory_opt_multigoal_white.cpp | 64 +++++++++++++++++++ 8 files changed, 108 insertions(+), 46 deletions(-) diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h index 34605cc71..0b62c0816 100644 --- a/src/omt/integer_optimizer.h +++ b/src/omt/integer_optimizer.h @@ -36,13 +36,12 @@ class OMTOptimizerInteger : public OMTOptimizer private: /** * Handles the optimization query specified by objType - * isMinimize = true will trigger minimization, + * isMinimize = true will trigger minimization, * otherwise trigger maximization **/ - smt::OptimizationResult optimize( - SmtEngine* optChecker, - TNode target, - bool isMinimize); + smt::OptimizationResult optimize(SmtEngine* optChecker, + TNode target, + bool isMinimize); }; } // namespace cvc5::omt diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index 08f1809ec..2145492db 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -30,7 +30,7 @@ bool OMTOptimizer::nodeSupportsOptimization(TNode node) } std::unique_ptr OMTOptimizer::getOptimizerForObjective( - OptimizationObjective& objective) + const OptimizationObjective& objective) { // the datatype of the target node TypeNode objectiveType = objective.getTarget().getType(true); @@ -53,7 +53,10 @@ std::unique_ptr OMTOptimizer::getOptimizerForObjective( } Node OMTOptimizer::mkStrongIncrementalExpression( - NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective) + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " @@ -114,10 +117,11 @@ Node OMTOptimizer::mkStrongIncrementalExpression( Unreachable(); } -Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, - TNode lhs, - TNode rhs, - OptimizationObjective& objective) +Node OMTOptimizer::mkWeakIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + const OptimizationObjective& objective) { constexpr const char lhsTypeError[] = "lhs type does not match or is not implicitly convertable to the target " diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h index 1052865b0..1e8d9e763 100644 --- a/src/omt/omt_optimizer.h +++ b/src/omt/omt_optimizer.h @@ -46,7 +46,7 @@ class OMTOptimizer * and this is the optimizer for targetNode **/ static std::unique_ptr getOptimizerForObjective( - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Given the lhs and rhs expressions, with an optimization objective, @@ -70,7 +70,7 @@ class OMTOptimizer NodeManager* nm, TNode lhs, TNode rhs, - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Given the lhs and rhs expressions, with an optimization objective, @@ -94,7 +94,7 @@ class OMTOptimizer NodeManager* nm, TNode lhs, TNode rhs, - smt::OptimizationObjective& objective); + const smt::OptimizationObjective& objective); /** * Minimize the target node with constraints encoded in optChecker diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index ffc49710a..e85ea82ef 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -15,6 +15,8 @@ #include "smt/optimization_solver.h" +#include "context/cdhashmap.h" +#include "context/cdlist.h" #include "omt/omt_optimizer.h" #include "options/smt_options.h" #include "smt/assertions.h" @@ -29,7 +31,7 @@ namespace smt { OptimizationSolver::OptimizationSolver(SmtEngine* parent) : d_parent(parent), d_optChecker(), - d_objectives(), + d_objectives(parent->getUserContext()), d_results(), d_objectiveCombination(LEXICOGRAPHIC) { @@ -37,10 +39,14 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent) OptimizationResult::ResultType OptimizationSolver::checkOpt() { + // if the results of the previous call have different size than the + // objectives, then we should clear the pareto optimization context + if (d_results.size() != d_objectives.size()) d_optChecker.reset(); + // initialize the result vector + d_results.clear(); for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) { - // reset the optimization results - d_results[i] = OptimizationResult(); + d_results.emplace_back(); } switch (d_objectiveCombination) { @@ -66,14 +72,6 @@ void OptimizationSolver::addObjective(TNode target, } d_optChecker.reset(); d_objectives.emplace_back(target, type, bvSigned); - d_results.emplace_back(OptimizationResult::UNKNOWN, Node()); -} - -void OptimizationSolver::resetObjectives() -{ - d_optChecker.reset(); - 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 64591d8f1..6d138deb2 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -18,6 +18,8 @@ #ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H #define CVC5__SMT__OPTIMIZATION_SOLVER_H +#include "context/cdhashmap_forward.h" +#include "context/cdlist.h" #include "expr/node.h" #include "expr/type_node.h" #include "util/result.h" @@ -74,14 +76,14 @@ class OptimizationResult * @return an enum showing whether the result is optimal, unbounded, * unsat or unknown. **/ - ResultType getType() { return d_type; } + ResultType getType() const { 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; } + Node getValue() const { return d_value; } private: /** the indicating whether the result is optimal or something else **/ @@ -124,13 +126,13 @@ class OptimizationObjective ~OptimizationObjective() = default; /** A getter for d_type **/ - ObjectiveType getType() { return d_type; } + ObjectiveType getType() const { return d_type; } /** A getter for d_target **/ - Node getTarget() { return d_target; } + Node getTarget() const { return d_target; } /** A getter for d_bvSigned **/ - bool bvIsSigned() { return d_bvSigned; } + bool bvIsSigned() const { return d_bvSigned; } private: /** @@ -173,7 +175,7 @@ class OptimizationSolver * * Lexicographic: optimize the objectives one-by-one, in the order they are * added: - * v_x = max(x) s.t. phi(x, y) = sat + * 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 @@ -214,11 +216,6 @@ class OptimizationSolver OptimizationObjective::ObjectiveType type, bool bvSigned = false); - /** - * Clear all the added optimization objectives - **/ - void resetObjectives(); - /** * Returns the values of the optimized objective after checkOpt is called * @return a vector of Optimization Result, @@ -293,7 +290,7 @@ class OptimizationSolver std::unique_ptr d_optChecker; /** The objectives to optimize for **/ - std::vector d_objectives; + context::CDList d_objectives; /** The results of the optimizations from the last checkOpt call **/ std::vector d_results; diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 66efe7eff..c23ce79dd 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, (uint32_t)0x3FFFFFA1)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, signed_min) @@ -87,7 +87,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min) // expect the minimum x = -1 ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, unsigned_max) @@ -114,7 +114,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 2u)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, signed_max) @@ -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->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteBVOpt, min_boundary) @@ -161,7 +161,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) // expect the maximum x = 18 ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), BitVector(32u, 18u)); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } } // namespace test diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index f16db0c0e..cf0434ddc 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("99")); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, min) @@ -101,7 +101,7 @@ TEST_F(TestTheoryWhiteIntOpt, min) ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst(), Rational("1")); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, result) @@ -129,7 +129,7 @@ TEST_F(TestTheoryWhiteIntOpt, result) // We expect our check to have returned UNSAT ASSERT_EQ(r, OptimizationResult::UNSAT); - d_optslv->resetObjectives(); + d_smtEngine->resetAssertions(); } TEST_F(TestTheoryWhiteIntOpt, open_interval) @@ -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->resetObjectives(); + d_smtEngine->resetAssertions(); } } // namespace test diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 1950d9ae2..73c6d9e7e 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -240,5 +240,69 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto) ASSERT_EQ(possibleResults.size(), 0); } +TEST_F(TestTheoryWhiteOptMultigoal, pushpop) +{ + d_smtEngine->resetAssertions(); + Node x = d_nodeManager->mkVar(*d_BV32Type); + Node y = d_nodeManager->mkVar(*d_BV32Type); + Node z = d_nodeManager->mkVar(*d_BV32Type); + + // 18 <= x + d_smtEngine->assertFormula(d_nodeManager->mkNode( + kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x)); + + // y <= x + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x)); + + // Lexico optimization + OptimizationSolver optSolver(d_smtEngine.get()); + + optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC); + + // minimize x + optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false); + + // push + d_smtEngine->push(); + + // maximize y with `signed` comparison over bit-vectors. + optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true); + // maximize z + optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false); + + OptimizationResult::ResultType r = optSolver.checkOpt(); + + ASSERT_EQ(r, OptimizationResult::OPTIMAL); + + std::vector results = optSolver.getValues(); + + // x == 18 + ASSERT_EQ(results[0].getValue().getConst(), BitVector(32u, 18u)); + + // y == 18 + ASSERT_EQ(results[1].getValue().getConst(), BitVector(32u, 18u)); + + // z == 0xFFFFFFFF + ASSERT_EQ(results[2].getValue().getConst(), + BitVector(32u, (unsigned)0xFFFFFFFF)); + + // pop + d_smtEngine->pop(); + + // now we only have one objective: (minimize x) + r = optSolver.checkOpt(); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); + results = optSolver.getValues(); + ASSERT_EQ(results.size(), 1); + ASSERT_EQ(results[0].getValue().getConst(), BitVector(32u, 18u)); + + // resetting the assertions also resets the optimization objectives + d_smtEngine->resetAssertions(); + r = optSolver.checkOpt(); + ASSERT_EQ(r, OptimizationResult::OPTIMAL); + results = optSolver.getValues(); + ASSERT_EQ(results.size(), 0); +} + } // namespace test } // namespace cvc5 -- 2.30.2