diff options
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/optimization_solver.cpp | 103 | ||||
| -rw-r--r-- | src/smt/optimization_solver.h | 63 |
2 files changed, 130 insertions, 36 deletions
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 |