From f9eee2d3a33c38bec3efb5dda91d43ef55c992d7 Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Tue, 4 May 2021 17:34:54 -0700 Subject: [PATCH] Add helper functions for multi-objective optimization + refactoring (#6473) add 3 helper functions judge whether a node is optimizable make strong improvement expression according to optimization objective make weak improvement expression according to optimization objective optChecker is now created by optimizationSolver instead of the minimize/maximize functions Slightly refactors function signatures so that they are accepting OptimizationObjective instead of accepting target, type in separate parameters. --- src/omt/bitvector_optimizer.cpp | 8 +- src/omt/bitvector_optimizer.h | 4 +- src/omt/integer_optimizer.cpp | 35 ++++---- src/omt/integer_optimizer.h | 11 +-- src/omt/omt_optimizer.cpp | 152 +++++++++++++++++++++++++++----- src/omt/omt_optimizer.h | 92 +++++++++++++------ src/smt/optimization_solver.cpp | 34 ++++++- src/smt/optimization_solver.h | 13 +++ 8 files changed, 264 insertions(+), 85 deletions(-) diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index 7edecdb73..1c3faddff 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -43,13 +43,11 @@ BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a, + aMod2PlusbMod2Div2)); } -OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* parentSMTSolver, +OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker, TNode target) { // the smt engine to which we send intermediate queries // for the binary search. - std::unique_ptr optChecker = - OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false); NodeManager* nm = optChecker->getNodeManager(); Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) @@ -137,13 +135,11 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* parentSMTSolver, return OptimizationResult(OptimizationResult::OPTIMAL, value); } -OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* parentSMTSolver, +OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker, TNode target) { // the smt engine to which we send intermediate queries // for the binary search. - std::unique_ptr optChecker = - OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false); NodeManager* nm = optChecker->getNodeManager(); Result intermediateSatResult = optChecker->checkSat(); // Model-value of objective (used in optimization loop) diff --git a/src/omt/bitvector_optimizer.h b/src/omt/bitvector_optimizer.h index b95c185f8..3b1bdebca 100644 --- a/src/omt/bitvector_optimizer.h +++ b/src/omt/bitvector_optimizer.h @@ -28,9 +28,9 @@ class OMTOptimizerBitVector : public OMTOptimizer public: OMTOptimizerBitVector(bool isSigned); virtual ~OMTOptimizerBitVector() = default; - smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + smt::OptimizationResult minimize(SmtEngine* optChecker, TNode target) override; - smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + smt::OptimizationResult maximize(SmtEngine* optChecker, TNode target) override; private: diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp index 8fbfff1a2..5e3dc15ff 100644 --- a/src/omt/integer_optimizer.cpp +++ b/src/omt/integer_optimizer.cpp @@ -21,16 +21,13 @@ using namespace cvc5::smt; namespace cvc5::omt { -OptimizationResult OMTOptimizerInteger::optimize( - SmtEngine* parentSMTSolver, - TNode target, - OptimizationObjective::ObjectiveType objType) +OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker, + TNode target, + bool isMinimize) { // linear search for integer goal // the smt engine to which we send intermediate queries // for the linear search. - std::unique_ptr optChecker = - OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false); NodeManager* nm = optChecker->getNodeManager(); Result intermediateSatResult = optChecker->checkSat(); @@ -47,16 +44,16 @@ OptimizationResult OMTOptimizerInteger::optimize( // asserts objective > old_value (used in optimization loop) Node increment; Kind incrementalOperator = kind::NULL_EXPR; - if (objType == OptimizationObjective::MINIMIZE) + if (isMinimize) { - // if objective is MIN, then assert optimization_target < - // current_model_value + // if objective is minimize, + // then assert optimization_target < current_model_value incrementalOperator = kind::LT; } - else if (objType == OptimizationObjective::MAXIMIZE) + else { - // if objective is MAX, then assert optimization_target > - // current_model_value + // if objective is maximize, + // then assert optimization_target > current_model_value incrementalOperator = kind::GT; } // Workhorse of linear search: @@ -74,17 +71,15 @@ OptimizationResult OMTOptimizerInteger::optimize( return OptimizationResult(OptimizationResult::OPTIMAL, value); } -OptimizationResult OMTOptimizerInteger::minimize( - SmtEngine* parentSMTSolver, TNode target) +OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker, + TNode target) { - return this->optimize( - parentSMTSolver, target, OptimizationObjective::MINIMIZE); + return this->optimize(optChecker, target, true); } -OptimizationResult OMTOptimizerInteger::maximize( - SmtEngine* parentSMTSolver, TNode target) +OptimizationResult OMTOptimizerInteger::maximize(SmtEngine* optChecker, + TNode target) { - return this->optimize( - parentSMTSolver, target, OptimizationObjective::MAXIMIZE); + return this->optimize(optChecker, target, false); } } // namespace cvc5::omt diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h index 48d162494..34605cc71 100644 --- a/src/omt/integer_optimizer.h +++ b/src/omt/integer_optimizer.h @@ -28,20 +28,21 @@ class OMTOptimizerInteger : public OMTOptimizer public: OMTOptimizerInteger() = default; virtual ~OMTOptimizerInteger() = default; - smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + smt::OptimizationResult minimize(SmtEngine* optChecker, TNode target) override; - smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + smt::OptimizationResult maximize(SmtEngine* optChecker, TNode target) override; private: /** * Handles the optimization query specified by objType - * (objType = MINIMIZE / MAXIMIZE) + * isMinimize = true will trigger minimization, + * otherwise trigger maximization **/ smt::OptimizationResult optimize( - SmtEngine* parentSMTSolver, + SmtEngine* optChecker, TNode target, - smt::OptimizationObjective::ObjectiveType objType); + bool isMinimize); }; } // namespace cvc5::omt diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp index 49b07fe26..bcf84cb53 100644 --- a/src/omt/omt_optimizer.cpp +++ b/src/omt/omt_optimizer.cpp @@ -17,20 +17,23 @@ #include "omt/bitvector_optimizer.h" #include "omt/integer_optimizer.h" -#include "options/smt_options.h" -#include "smt/smt_engine.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/smt_engine_subsolver.h" using namespace cvc5::theory; using namespace cvc5::smt; namespace cvc5::omt { -std::unique_ptr OMTOptimizer::getOptimizerForNode(TNode targetNode, - bool isSigned) +bool OMTOptimizer::nodeSupportsOptimization(TNode node) +{ + TypeNode type = node.getType(); + // only supports Integer and BitVectors as of now + return (type.isInteger() || type.isBitVector()); +} + +std::unique_ptr OMTOptimizer::getOptimizerForObjective( + OptimizationObjective& objective) { // the datatype of the target node - TypeNode objectiveType = targetNode.getType(true); + TypeNode objectiveType = objective.getTarget().getType(true); if (objectiveType.isInteger()) { // integer type: use OMTOptimizerInteger @@ -39,7 +42,8 @@ std::unique_ptr OMTOptimizer::getOptimizerForNode(TNode targetNode else if (objectiveType.isBitVector()) { // bitvector type: use OMTOptimizerBitVector - return std::unique_ptr(new OMTOptimizerBitVector(isSigned)); + return std::unique_ptr( + new OMTOptimizerBitVector(objective.bvIsSigned())); } else { @@ -47,24 +51,126 @@ std::unique_ptr OMTOptimizer::getOptimizerForNode(TNode targetNode } } -std::unique_ptr OMTOptimizer::createOptCheckerWithTimeout( - SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) +Node OMTOptimizer::mkStrongIncrementalExpression( + NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective) +{ + constexpr const char lhsTypeError[] = + "lhs type does not match or is not implicitly convertable to the target " + "type"; + constexpr const char rhsTypeError[] = + "rhs type does not match or is not implicitly convertable to the target " + "type"; + TypeNode targetType = objective.getTarget().getType(); + switch (objective.getType()) + { + case OptimizationObjective::MINIMIZE: + { + if (targetType.isInteger()) + { + Assert(lhs.getType().isInteger()) << lhsTypeError; + Assert(rhs.getType().isInteger()) << rhsTypeError; + return nm->mkNode(Kind::LT, lhs, rhs); + } + else if (targetType.isBitVector()) + { + Assert(lhs.getType() == targetType) << lhsTypeError; + Assert(rhs.getType() == targetType) << rhsTypeError; + return (objective.bvIsSigned()) + ? (nm->mkNode(Kind::BITVECTOR_SLT, lhs, rhs)) + : (nm->mkNode(Kind::BITVECTOR_ULT, lhs, rhs)); + } + else + { + Unimplemented() << "Target type does not support optimization"; + } + } + case OptimizationObjective::MAXIMIZE: + { + if (targetType.isInteger()) + { + Assert(lhs.getType().isInteger()) << lhsTypeError; + Assert(rhs.getType().isInteger()) << rhsTypeError; + return nm->mkNode(Kind::GT, lhs, rhs); + } + else if (targetType.isBitVector()) + { + Assert(lhs.getType() == targetType) << lhsTypeError; + Assert(rhs.getType() == targetType) << rhsTypeError; + return (objective.bvIsSigned()) + ? (nm->mkNode(Kind::BITVECTOR_SGT, lhs, rhs)) + : (nm->mkNode(Kind::BITVECTOR_UGT, lhs, rhs)); + } + else + { + Unimplemented() << "Target type does not support optimization"; + } + } + default: + CVC5_FATAL() << "Optimization objective is neither MAXIMIZE nor MINIMIZE"; + } + Unreachable(); +} + +Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm, + TNode lhs, + TNode rhs, + OptimizationObjective& objective) { - std::unique_ptr optChecker; - // initializeSubSolver will copy the options and theories enabled - // from the current solver to optChecker and adds timeout - theory::initializeSubsolver(optChecker, needsTimeout, timeout); - // we need to be in incremental mode for multiple objectives since we need to - // push pop we need to produce models to inrement on our objective - optChecker->setOption("incremental", "true"); - optChecker->setOption("produce-models", "true"); - // Move assertions from the parent solver to the subsolver - std::vector p_assertions = parentSMTSolver->getExpandedAssertions(); - for (const Node& e : p_assertions) + constexpr const char lhsTypeError[] = + "lhs type does not match or is not implicitly convertable to the target " + "type"; + constexpr const char rhsTypeError[] = + "rhs type does not match or is not implicitly convertable to the target " + "type"; + TypeNode targetType = objective.getTarget().getType(); + switch (objective.getType()) { - optChecker->assertFormula(e); + case OptimizationObjective::MINIMIZE: + { + if (targetType.isInteger()) + { + Assert(lhs.getType().isInteger()) << lhsTypeError; + Assert(rhs.getType().isInteger()) << rhsTypeError; + return nm->mkNode(Kind::LEQ, lhs, rhs); + } + else if (targetType.isBitVector()) + { + Assert(lhs.getType() == targetType) << lhsTypeError; + Assert(rhs.getType() == targetType) << rhsTypeError; + return (objective.bvIsSigned()) + ? (nm->mkNode(Kind::BITVECTOR_SLE, lhs, rhs)) + : (nm->mkNode(Kind::BITVECTOR_ULE, lhs, rhs)); + } + else + { + Unimplemented() << "Target type does not support optimization"; + } + } + case OptimizationObjective::MAXIMIZE: + { + if (targetType.isInteger()) + { + Assert(lhs.getType().isInteger()) << lhsTypeError; + Assert(rhs.getType().isInteger()) << rhsTypeError; + return nm->mkNode(Kind::GEQ, lhs, rhs); + } + else if (targetType.isBitVector()) + { + Assert(lhs.getType() == targetType) << lhsTypeError; + Assert(rhs.getType() == targetType) << rhsTypeError; + return (objective.bvIsSigned()) + ? (nm->mkNode(Kind::BITVECTOR_SGE, lhs, rhs)) + : (nm->mkNode(Kind::BITVECTOR_UGE, lhs, rhs)); + } + else + { + Unimplemented() << "Target type does not support optimization"; + } + } + default: + CVC5_FATAL() << "Optimization objective is neither MAXIMIZE nor MINIMIZE"; } - return optChecker; + Unreachable(); } } // namespace cvc5::omt diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h index 792a60169..1052865b0 100644 --- a/src/omt/omt_optimizer.h +++ b/src/omt/omt_optimizer.h @@ -27,54 +27,96 @@ class OMTOptimizer { public: virtual ~OMTOptimizer() = default; + /** - * Given a target node, retrieve an optimizer specific for the node's type - * the second field isSigned specifies whether we should use signed comparison - * for BitVectors and it's only valid when the type is BitVector - * - * @param targetNode the target node for the expression to be optimized - * @param isSigned speficies whether to use signed comparison for BitVectors - * and it's only valid when the type of targetNode is BitVector + * Returns whether node supports optimization + * Currently supported: BitVectors, Integers (preliminary). + * @param node the target node to check for optimizability + * @return whether node supports optimization + **/ + static bool nodeSupportsOptimization(TNode node); + + /** + * Given an optimization objective, + * retrieve an optimizer specific for the optimization target + * @param objective the an OptimizationObjective object containing + * the optimization target, whether it's maximized or minimized + * and whether it's signed for BV (only applies when the target type is BV) * @return a unique_pointer pointing to a derived class of OMTOptimizer * and this is the optimizer for targetNode **/ - static std::unique_ptr getOptimizerForNode( - TNode targetNode, bool isSigned = false); + static std::unique_ptr getOptimizerForObjective( + smt::OptimizationObjective& objective); + + /** + * Given the lhs and rhs expressions, with an optimization objective, + * makes an incremental expression stating that + * lhs `better than` rhs + * under the context specified by objective + * for minimize, it would be lhs < rhs + * for maximize, it would be lhs > rhs + * + * Note: the types of lhs and rhs nodes must match or be convertable + * to the type of the optimization target! + * + * @param nm the NodeManager to manage the made expression + * @param lhs the left hand side of the expression + * @param rhs the right hand side of the expression + * @param objective the optimization objective + * stating whether it's maximize / minimize etc. + * @return an expression stating lhs `better than` rhs, + **/ + static Node mkStrongIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + smt::OptimizationObjective& objective); /** - * Initialize an SMT subsolver for offline optimization purpose - * @param parentSMTSolver the parental solver containing the assertions - * @param needsTimeout specifies whether it needs timeout for each single - * query - * @param timeout the timeout value, given in milliseconds (ms) - * @return a unique_pointer of SMT subsolver + * Given the lhs and rhs expressions, with an optimization objective, + * makes an incremental expression stating that + * lhs `better than or equal to` rhs + * under the context specified by objective + * for minimize, it would be lhs <= rhs + * for maximize, it would be lhs >= rhs + * + * Note: the types of lhs and rhs nodes must match or be convertable + * to the type of the optimization target! + * + * @param nm the NodeManager to manage the made expression + * @param lhs the left hand side of the expression + * @param rhs the right hand side of the expression + * @param objective the optimization objective + * stating whether it's maximize / minimize etc. + * @return an expression stating lhs `better than or equal to` rhs, **/ - static std::unique_ptr createOptCheckerWithTimeout( - SmtEngine* parentSMTSolver, - bool needsTimeout = false, - unsigned long timeout = 0); + static Node mkWeakIncrementalExpression( + NodeManager* nm, + TNode lhs, + TNode rhs, + smt::OptimizationObjective& objective); /** - * Minimize the target node with constraints encoded in parentSMTSolver + * Minimize the target node with constraints encoded in optChecker * - * @param parentSMTSolver an SMT solver encoding the assertions as the + * @param optChecker an SMT solver encoding the assertions as the * constraints * @param target the target expression to optimize * @return smt::OptimizationResult the result of optimization, containing * whether it's optimal and the optimized value. **/ - virtual smt::OptimizationResult minimize(SmtEngine* parentSMTSolver, + virtual smt::OptimizationResult minimize(SmtEngine* optChecker, TNode target) = 0; /** - * Maximize the target node with constraints encoded in parentSMTSolver + * Maximize the target node with constraints encoded in optChecker * - * @param parentSMTSolver an SMT solver encoding the assertions as the + * @param optChecker an SMT solver encoding the assertions as the * constraints * @param target the target expression to optimize * @return smt::OptimizationResult the result of optimization, containing * whether it's optimal and the optimized value. **/ - virtual smt::OptimizationResult maximize(SmtEngine* parentSMTSolver, + virtual smt::OptimizationResult maximize(SmtEngine* optChecker, TNode target) = 0; }; diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 1c8fe6514..e66e4e2ca 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -16,7 +16,10 @@ #include "smt/optimization_solver.h" #include "omt/omt_optimizer.h" +#include "options/smt_options.h" #include "smt/assertions.h" +#include "smt/smt_engine.h" +#include "theory/smt_engine_subsolver.h" using namespace cvc5::theory; using namespace cvc5::omt; @@ -27,19 +30,22 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt() { Assert(d_objectives.size() == 1); // NOTE: currently we are only dealing with single obj - std::unique_ptr optimizer = OMTOptimizer::getOptimizerForNode( - d_objectives[0].getTarget(), d_objectives[0].bvIsSigned()); + 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(d_parent, d_objectives[0].getTarget()); + optResult = + optimizer->maximize(optChecker.get(), d_objectives[0].getTarget()); } else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE) { - optResult = optimizer->minimize(d_parent, d_objectives[0].getTarget()); + optResult = + optimizer->minimize(optChecker.get(), d_objectives[0].getTarget()); } d_results[0] = optResult; @@ -65,5 +71,25 @@ std::vector OptimizationSolver::getValues() return d_results; } +std::unique_ptr OptimizationSolver::createOptCheckerWithTimeout( + SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) +{ + std::unique_ptr optChecker; + // initializeSubSolver will copy the options and theories enabled + // from the current solver to optChecker and adds timeout + theory::initializeSubsolver(optChecker, needsTimeout, timeout); + // we need to be in incremental mode for multiple objectives since we need to + // push pop we need to produce models to inrement on our objective + optChecker->setOption("incremental", "true"); + optChecker->setOption("produce-models", "true"); + // Move assertions from the parent solver to the subsolver + std::vector p_assertions = parentSMTSolver->getExpandedAssertions(); + for (const Node& e : p_assertions) + { + optChecker->assertFormula(e); + } + return optChecker; +} + } // namespace smt } // namespace cvc5 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index 0babd7a4a..3037c2924 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -208,6 +208,19 @@ class OptimizationSolver std::vector getValues(); private: + /** + * Initialize an SMT subsolver for offline optimization purpose + * @param parentSMTSolver the parental solver containing the assertions + * @param needsTimeout specifies whether it needs timeout for each single + * query + * @param timeout the timeout value, given in milliseconds (ms) + * @return a unique_pointer of SMT subsolver + **/ + static std::unique_ptr createOptCheckerWithTimeout( + SmtEngine* parentSMTSolver, + bool needsTimeout = false, + unsigned long timeout = 0); + /** The parent SMT engine **/ SmtEngine* d_parent; -- 2.30.2