diff options
author | Ouyancheng <1024842937@qq.com> | 2021-05-27 00:53:58 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-27 07:53:58 +0000 |
commit | 7120cf46b38f0bede1ab8d17453ae925aa2d27fd (patch) | |
tree | b22e054d08f0312b12b6fc62a37eb2497f8d16a6 /src | |
parent | cd386643b1113c92775950b3683c2b48f7f2bf13 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/omt/bitvector_optimizer.cpp | 8 | ||||
-rw-r--r-- | src/omt/integer_optimizer.cpp | 7 | ||||
-rw-r--r-- | src/omt/omt_optimizer.cpp | 17 | ||||
-rw-r--r-- | src/smt/optimization_solver.cpp | 103 | ||||
-rw-r--r-- | src/smt/optimization_solver.h | 63 |
5 files changed, 152 insertions, 46 deletions
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> 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<OMTOptimizer> optimizer = - OMTOptimizer::getOptimizerForObjective(d_objectives[0]); - - if (!optimizer) return OptimizationResult::UNSUPPORTED; +} - OptimizationResult optResult; - std::unique_ptr<SmtEngine> 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<OptimizationResult> OptimizationSolver::getValues() return d_results; } +void OptimizationSolver::setObjectiveCombination( + ObjectiveCombination combination) +{ + d_objectiveCombination = combination; +} + std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout( SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) { @@ -91,5 +99,56 @@ std::unique_ptr<SmtEngine> 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<OMTOptimizer> 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; } /** @@ -165,20 +163,38 @@ 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<OptimizationResult> 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<SmtEngine> d_optChecker; + /** The objectives to optimize for **/ std::vector<OptimizationObjective> d_objectives; /** The results of the optimizations from the last checkOpt call **/ std::vector<OptimizationResult> d_results; + + /** The current objective combination method **/ + ObjectiveCombination d_objectiveCombination; }; } // namespace smt |