From 7120cf46b38f0bede1ab8d17453ae925aa2d27fd Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Thu, 27 May 2021 00:53:58 -0700 Subject: [PATCH] Add support for Box optimization (#6599) Add support for box optimization -- independently optimize each goal as if the other goals do not exist. Single minimize() / maximize() now maintains the pushed / popped context. Of course unit tests are here as well. --- src/omt/bitvector_optimizer.cpp | 8 +- src/omt/integer_optimizer.cpp | 7 +- src/omt/omt_optimizer.cpp | 17 ++- src/smt/optimization_solver.cpp | 103 ++++++++++++++---- src/smt/optimization_solver.h | 63 ++++++++--- test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/theory_bv_opt_white.cpp | 3 +- test/unit/theory/theory_int_opt_white.cpp | 5 +- .../theory/theory_opt_multigoal_white.cpp | 88 +++++++++++++++ 9 files changed, 244 insertions(+), 51 deletions(-) create mode 100644 test/unit/theory/theory_opt_multigoal_white.cpp diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index cd233295e..bce6c9b6d 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Yancheng Ou, Michael Chang + * Yancheng Ou * * This file is part of the cvc5 project. * @@ -106,6 +106,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, intermediateSatResult = optChecker->checkSat(); if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) { + optChecker->pop(); return OptimizationResult(OptimizationResult::UNKNOWN, value); } if (intermediateSatResult.isSat() == Result::SAT) @@ -120,6 +121,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, // lowerBound == pivot ==> upperbound = lowerbound + 1 // and lowerbound <= target < upperbound is UNSAT // return the upperbound + optChecker->pop(); return OptimizationResult(OptimizationResult::OPTIMAL, value); } else @@ -129,6 +131,7 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, } else { + optChecker->pop(); return OptimizationResult(OptimizationResult::UNKNOWN, value); } optChecker->pop(); @@ -195,6 +198,7 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, intermediateSatResult = optChecker->checkSat(); if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) { + optChecker->pop(); return OptimizationResult(OptimizationResult::UNKNOWN, value); } if (intermediateSatResult.isSat() == Result::SAT) @@ -209,6 +213,7 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, // upperbound = lowerbound + 1 // and lowerbound < target <= upperbound is UNSAT // return the lowerbound + optChecker->pop(); return OptimizationResult(OptimizationResult::OPTIMAL, value); } else @@ -218,6 +223,7 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, } else { + optChecker->pop(); return OptimizationResult(OptimizationResult::UNKNOWN, value); } optChecker->pop(); diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index 5e3dc15ff..045268337 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Yancheng Ou, Michael Chang + * Michael Chang, Yancheng Ou * * This file is part of the cvc5 project. * @@ -29,7 +29,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, // the smt engine to which we send intermediate queries // for the linear search. NodeManager* nm = optChecker->getNodeManager(); - + optChecker->push(); Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) Node value; @@ -41,7 +41,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, { return OptimizationResult(OptimizationResult::UNSAT, value); } - // asserts objective > old_value (used in optimization loop) + // node storing target > old_value (used in optimization loop) Node increment; Kind incrementalOperator = kind::NULL_EXPR; if (isMinimize) @@ -68,6 +68,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, optChecker->assertFormula(increment); intermediateSatResult = optChecker->checkSat(); } + optChecker->pop(); return OptimizationResult(OptimizationResult::OPTIMAL, value); } diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index bcf84cb53..08f1809ec 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Yancheng Ou, Michael Chang, Aina Niemetz + * Yancheng Ou, Aina Niemetz * * This file is part of the cvc5 project. * @@ -47,7 +47,8 @@ std::unique_ptr OMTOptimizer::getOptimizerForObjective( } else { - return nullptr; + Unimplemented() << "Target type " << objectiveType + << " does not support optimization"; } } @@ -81,7 +82,8 @@ Node OMTOptimizer::mkStrongIncrementalExpression( } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } case OptimizationObjective::MAXIMIZE: @@ -102,7 +104,8 @@ Node OMTOptimizer::mkStrongIncrementalExpression( } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } default: @@ -143,7 +146,8 @@ Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } case OptimizationObjective::MAXIMIZE: @@ -164,7 +168,8 @@ Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, } else { - Unimplemented() << "Target type does not support optimization"; + Unimplemented() << "Target type " << targetType + << " does not support optimization"; } } default: diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index e66e4e2ca..f73bc90b7 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Michael Chang, Yancheng Ou, Aina Niemetz + * Yancheng Ou, Michael Chang, Aina Niemetz * * This file is part of the cvc5 project. * @@ -26,41 +26,43 @@ using namespace cvc5::omt; namespace cvc5 { namespace smt { -OptimizationResult::ResultType OptimizationSolver::checkOpt() +OptimizationSolver::OptimizationSolver(SmtEngine* parent) + : d_parent(parent), + d_optChecker(), + d_objectives(), + d_results(), + d_objectiveCombination(BOX) { - Assert(d_objectives.size() == 1); - // NOTE: currently we are only dealing with single obj - std::unique_ptr optimizer = - OMTOptimizer::getOptimizerForObjective(d_objectives[0]); - - if (!optimizer) return OptimizationResult::UNSUPPORTED; +} - OptimizationResult optResult; - std::unique_ptr optChecker = createOptCheckerWithTimeout(d_parent); - if (d_objectives[0].getType() == OptimizationObjective::MAXIMIZE) - { - optResult = - optimizer->maximize(optChecker.get(), d_objectives[0].getTarget()); - } - else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE) +OptimizationResult::ResultType OptimizationSolver::checkOpt() +{ + switch (d_objectiveCombination) { - optResult = - optimizer->minimize(optChecker.get(), d_objectives[0].getTarget()); + case BOX: return optimizeBox(); break; + default: + Unimplemented() + << "Only BOX objective combination is supported in current version"; } - - d_results[0] = optResult; - return optResult.getType(); + Unreachable(); } void OptimizationSolver::pushObjective( TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned) { + if (!OMTOptimizer::nodeSupportsOptimization(target)) + { + CVC5_FATAL() + << "Objective not pushed: Target node does not support optimization"; + } + d_optChecker.reset(); d_objectives.emplace_back(target, type, bvSigned); - d_results.emplace_back(OptimizationResult::UNSUPPORTED, Node()); + d_results.emplace_back(OptimizationResult::UNKNOWN, Node()); } void OptimizationSolver::popObjective() { + d_optChecker.reset(); d_objectives.pop_back(); d_results.pop_back(); } @@ -71,6 +73,12 @@ std::vector OptimizationSolver::getValues() return d_results; } +void OptimizationSolver::setObjectiveCombination( + ObjectiveCombination combination) +{ + d_objectiveCombination = combination; +} + std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) { @@ -91,5 +99,56 @@ std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( return optChecker; } +OptimizationResult::ResultType OptimizationSolver::optimizeBox() +{ + // resets the optChecker + d_optChecker = createOptCheckerWithTimeout(d_parent); + OptimizationResult partialResult; + OptimizationResult::ResultType aggregatedResultType = + OptimizationResult::OPTIMAL; + std::unique_ptr optimizer; + for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i) + { + optimizer = OMTOptimizer::getOptimizerForObjective(d_objectives[i]); + // checks whether the objective type is maximize or minimize + switch (d_objectives[i].getType()) + { + case OptimizationObjective::MAXIMIZE: + partialResult = optimizer->maximize(d_optChecker.get(), + d_objectives[i].getTarget()); + break; + case OptimizationObjective::MINIMIZE: + partialResult = optimizer->minimize(d_optChecker.get(), + d_objectives[i].getTarget()); + break; + default: + CVC5_FATAL() + << "Optimization objective is neither MAXIMIZE nor MINIMIZE"; + } + // match the optimization result type, and aggregate the results of + // subproblems + switch (partialResult.getType()) + { + case OptimizationResult::OPTIMAL: break; + case OptimizationResult::UNBOUNDED: break; + case OptimizationResult::UNSAT: + if (aggregatedResultType == OptimizationResult::OPTIMAL) + { + aggregatedResultType = OptimizationResult::UNSAT; + } + break; + case OptimizationResult::UNKNOWN: + aggregatedResultType = OptimizationResult::UNKNOWN; + break; + default: Unreachable(); + } + + d_results[i] = partialResult; + } + // kill optChecker after optimization ends + d_optChecker.reset(); + return aggregatedResultType; +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 3037c2924..0a1883737 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Michael Chang, Yancheng Ou, Aina Niemetz + * Yancheng Ou, Michael Chang, Aina Niemetz * * This file is part of the cvc5 project. * @@ -44,8 +44,6 @@ class OptimizationResult **/ 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 @@ -67,14 +65,14 @@ class OptimizationResult : d_type(type), d_value(value) { } - OptimizationResult() : d_type(UNSUPPORTED), d_value() {} + OptimizationResult() : d_type(UNKNOWN), d_value() {} ~OptimizationResult() = default; /** * 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. + * unsat or unknown. **/ ResultType getType() { return d_type; } /** @@ -164,21 +162,39 @@ class OptimizationObjective class OptimizationSolver { public: + /** + * An enum specifying how multiple objectives are dealt with. + * Definition: + * phi(x, y): set of assertions with variables x and y + * + * Box: treat the objectives as independent objectives + * 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 + * 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) + * (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) + **/ + enum ObjectiveCombination + { + BOX, + LEXICOGRAPHIC, + PARETO, + }; /** * Constructor * @param parent the smt_solver that the user added their assertions to **/ - OptimizationSolver(SmtEngine* parent) - : d_parent(parent), d_objectives(), d_results() - { - } + OptimizationSolver(SmtEngine* parent); ~OptimizationSolver() = default; /** * 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(); @@ -196,7 +212,7 @@ class OptimizationSolver bool bvSigned = false); /** - * Pop the most recent objective. + * Pop the most recently successfully-pushed objective. **/ void popObjective(); @@ -207,6 +223,11 @@ class OptimizationSolver **/ std::vector getValues(); + /** + * Sets the objective combination + **/ + void setObjectiveCombination(ObjectiveCombination combination); + private: /** * Initialize an SMT subsolver for offline optimization purpose @@ -221,14 +242,28 @@ class OptimizationSolver bool needsTimeout = false, unsigned long timeout = 0); - /** The parent SMT engine **/ + /** + * Optimize multiple goals in Box order + * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED; + * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN; + * UNKNOWN if any of the objective is UNKNOWN. + **/ + OptimizationResult::ResultType optimizeBox(); + + /** A pointer to the parent SMT engine **/ SmtEngine* d_parent; + /** A subsolver for offline optimization **/ + std::unique_ptr d_optChecker; + /** The objectives to optimize for **/ std::vector d_objectives; /** The results of the optimizations from the last checkOpt call **/ std::vector d_results; + + /** The current objective combination method **/ + ObjectiveCombination d_objectiveCombination; }; } // namespace smt diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 9fb0e21f1..5d5f4c680 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -30,6 +30,7 @@ cvc5_add_unit_test_white(theory_bv_opt_white theory) cvc5_add_unit_test_white(theory_bv_int_blaster_white theory) cvc5_add_unit_test_white(theory_engine_white theory) cvc5_add_unit_test_white(theory_int_opt_white theory) +cvc5_add_unit_test_white(theory_opt_multigoal_white theory) cvc5_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc5_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc5_add_unit_test_white(theory_sets_type_enumerator_white theory) diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 3422b2784..42dcb9fee 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Yancheng Ou, Michael Chang + * Yancheng Ou * * This file is part of the cvc5 project. * @@ -164,5 +164,6 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary) d_optslv->popObjective(); } + } // 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 770927544..efb963f16 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -59,7 +59,6 @@ TEST_F(TestTheoryWhiteIntOpt, max) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - // We activate our objective so the subsolver knows to optimize it d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE); @@ -91,7 +90,6 @@ TEST_F(TestTheoryWhiteIntOpt, min) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - // We activate our objective so the subsolver knows to optimize it d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE); @@ -123,13 +121,12 @@ TEST_F(TestTheoryWhiteIntOpt, result) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - // We activate our objective so the subsolver knows to optimize it d_optslv->pushObjective(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(); diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp new file mode 100644 index 000000000..3bffc9af1 --- /dev/null +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -0,0 +1,88 @@ +/****************************************************************************** + * Top contributors (to current version): + * Yancheng Ou + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * White-box testing for multigoal optimization. + */ +#include + +#include "smt/optimization_solver.h" +#include "test_smt.h" +#include "util/bitvector.h" + +namespace cvc5 { + +using namespace theory; +using namespace smt; + +namespace test { + +class TestTheoryWhiteOptMultigoal : public TestSmtNoFinishInit +{ + protected: + void SetUp() override + { + TestSmtNoFinishInit::SetUp(); + d_smtEngine->setOption("produce-assertions", "true"); + d_smtEngine->finishInit(); + + d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u))); + } + + std::unique_ptr d_BV32Type; +}; + +TEST_F(TestTheoryWhiteOptMultigoal, box) +{ + 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)); + + // Box optimization + OptimizationSolver optSolver(d_smtEngine.get()); + + optSolver.setObjectiveCombination(OptimizationSolver::BOX); + + // minimize x + optSolver.pushObjective(x, OptimizationObjective::MINIMIZE, false); + // maximize y with `signed` comparison over bit-vectors. + optSolver.pushObjective(y, OptimizationObjective::MAXIMIZE, true); + // maximize z + optSolver.pushObjective(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 == 0x7FFFFFFF + ASSERT_EQ(results[1].getValue().getConst(), + BitVector(32u, (unsigned)0x7FFFFFFF)); + + // z == 0xFFFFFFFF + ASSERT_EQ(results[2].getValue().getConst(), + BitVector(32u, (unsigned)0xFFFFFFFF)); +} + +} // namespace test +} // namespace cvc5 -- 2.30.2