diff options
author | Yancheng Ou <ou2@ualberta.ca> | 2021-04-05 06:21:40 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-05 08:21:40 -0500 |
commit | 3f1ab5672ca746a4a6573e1ebf9f74d72978d1cf (patch) | |
tree | 86518c88e615cbf7cc0cc3d37cc9866d1bfbb6c4 /src | |
parent | 69b463e1b1150715b2f4179786ddab8ba0c43b37 (diff) |
Optimizer for BitVectors (#6213)
Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 6 | ||||
-rw-r--r-- | src/omt/bitvector_optimizer.cpp | 239 | ||||
-rw-r--r-- | src/omt/bitvector_optimizer.h | 50 | ||||
-rw-r--r-- | src/omt/integer_optimizer.cpp | 87 | ||||
-rw-r--r-- | src/omt/integer_optimizer.h | 47 | ||||
-rw-r--r-- | src/omt/omt_optimizer.cpp | 69 | ||||
-rw-r--r-- | src/omt/omt_optimizer.h | 84 | ||||
-rw-r--r-- | src/smt/optimization_solver.cpp | 95 | ||||
-rw-r--r-- | src/smt/optimization_solver.h | 104 |
9 files changed, 677 insertions, 104 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 490d335a2..6c2af8226 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -47,6 +47,12 @@ libcvc4_add_sources( lib/replacements.h lib/strtok_r.c lib/strtok_r.h + omt/bitvector_optimizer.cpp + omt/bitvector_optimizer.h + omt/integer_optimizer.cpp + omt/integer_optimizer.h + omt/omt_optimizer.cpp + omt/omt_optimizer.h preprocessing/assertion_pipeline.cpp preprocessing/assertion_pipeline.h preprocessing/passes/ackermann.cpp diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp new file mode 100644 index 000000000..c8c2a39d7 --- /dev/null +++ b/src/omt/bitvector_optimizer.cpp @@ -0,0 +1,239 @@ +/********************* */ +/*! \file bitvector_optimizer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Yancheng Ou + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief Optimizer for BitVector type + **/ + +#include "omt/bitvector_optimizer.h" + +#include "options/smt_options.h" +#include "smt/smt_engine.h" + +using namespace cvc5::smt; +namespace cvc5::omt { + +OMTOptimizerBitVector::OMTOptimizerBitVector(bool isSigned) + : d_isSigned(isSigned) +{ +} + +BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a, + const BitVector& b, + bool isSigned) +{ + // computes (a + b) / 2 without overflow + // rounding towards -infinity: -1.5 --> -2, 1.5 --> 1 + // average = (a / 2) + (b / 2) + (((a % 2) + (b % 2)) / 2) + uint32_t aMod2 = static_cast<uint32_t>(a.isBitSet(0)); + uint32_t bMod2 = static_cast<uint32_t>(b.isBitSet(0)); + BitVector aMod2PlusbMod2(a.getSize(), (aMod2 + bMod2) / 2); + BitVector bv1 = BitVector::mkOne(a.getSize()); + if (isSigned) + { + return (a.arithRightShift(bv1) + b.arithRightShift(bv1) + + aMod2PlusbMod2.arithRightShift(bv1)); + } + else + { + return (a.logicalRightShift(bv1) + b.logicalRightShift(bv1) + + aMod2PlusbMod2.logicalRightShift(bv1)); + } +} + +std::pair<OptResult, Node> OMTOptimizerBitVector::minimize( + SmtEngine* parentSMTSolver, Node target) +{ + // the smt engine to which we send intermediate queries + // for the binary search. + std::unique_ptr<SmtEngine> optChecker = + OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false); + NodeManager* nm = optChecker->getNodeManager(); + Result intermediateSatResult = optChecker->checkSat(); + // Model-value of objective (used in optimization loop) + Node value; + if (intermediateSatResult.isUnknown()) + { + return std::make_pair(OptResult::OPT_UNKNOWN, value); + } + if (intermediateSatResult.isSat() == Result::UNSAT) + { + return std::make_pair(OptResult::OPT_UNSAT, value); + } + + // value equals to upperBound + value = optChecker->getValue(target); + + // this gets the bitvector! + BitVector bvValue = value.getConst<BitVector>(); + unsigned int bvSize = bvValue.getSize(); + + // lowerbound + BitVector lowerBound = ((this->d_isSigned) ? (BitVector::mkMinSigned(bvSize)) + : (BitVector::mkZero(bvSize))); + // upperbound must be a satisfying value + // and value == upperbound + BitVector upperBound = bvValue; + + Kind LTOperator = + ((d_isSigned) ? (kind::BITVECTOR_SLT) : (kind::BITVECTOR_ULT)); + Kind GEOperator = + ((d_isSigned) ? (kind::BITVECTOR_SGE) : (kind::BITVECTOR_UGE)); + + // the pivot value for binary search, + // pivot = (lowerBound + upperBound) / 2 + // rounded towards -infinity + BitVector pivot; + while (true) + { + if (d_isSigned) + { + if (!lowerBound.signedLessThan(upperBound)) break; + } + else + { + if (!lowerBound.unsignedLessThan(upperBound)) break; + } + pivot = computeAverage(lowerBound, upperBound, d_isSigned); + optChecker->push(); + // lowerBound <= target < pivot + optChecker->assertFormula( + nm->mkNode(kind::AND, + nm->mkNode(GEOperator, target, nm->mkConst(lowerBound)), + nm->mkNode(LTOperator, target, nm->mkConst(pivot)))); + intermediateSatResult = optChecker->checkSat(); + if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) + { + return std::make_pair(OptResult::OPT_UNKNOWN, value); + } + if (intermediateSatResult.isSat() == Result::SAT) + { + value = optChecker->getValue(target); + upperBound = value.getConst<BitVector>(); + } + else if (intermediateSatResult.isSat() == Result::UNSAT) + { + if (lowerBound == pivot) + { + // lowerBound == pivot ==> upperbound = lowerbound + 1 + // and lowerbound <= target < upperbound is UNSAT + // return the upperbound + return std::make_pair(OptResult::OPT_OPTIMAL, value); + } + else + { + lowerBound = pivot; + } + } + else + { + return std::make_pair(OptResult::OPT_UNKNOWN, value); + } + optChecker->pop(); + } + return std::make_pair(OptResult::OPT_OPTIMAL, value); +} + +std::pair<OptResult, Node> OMTOptimizerBitVector::maximize( + SmtEngine* parentSMTSolver, Node target) +{ + // the smt engine to which we send intermediate queries + // for the binary search. + std::unique_ptr<SmtEngine> optChecker = + OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false); + NodeManager* nm = optChecker->getNodeManager(); + Result intermediateSatResult = optChecker->checkSat(); + // Model-value of objective (used in optimization loop) + Node value; + if (intermediateSatResult.isUnknown()) + { + return std::make_pair(OptResult::OPT_UNKNOWN, value); + } + if (intermediateSatResult.isSat() == Result::UNSAT) + { + return std::make_pair(OptResult::OPT_UNSAT, value); + } + + // value equals to upperBound + value = optChecker->getValue(target); + + // this gets the bitvector! + BitVector bvValue = value.getConst<BitVector>(); + unsigned int bvSize = bvValue.getSize(); + + // lowerbound must be a satisfying value + // and value == lowerbound + BitVector lowerBound = bvValue; + + // upperbound + BitVector upperBound = ((this->d_isSigned) ? (BitVector::mkMaxSigned(bvSize)) + : (BitVector::mkOnes(bvSize))); + + Kind LEOperator = + ((d_isSigned) ? (kind::BITVECTOR_SLE) : (kind::BITVECTOR_ULE)); + Kind GTOperator = + ((d_isSigned) ? (kind::BITVECTOR_SGT) : (kind::BITVECTOR_UGT)); + + // the pivot value for binary search, + // pivot = (lowerBound + upperBound) / 2 + // rounded towards -infinity + BitVector pivot; + while (true) + { + if (d_isSigned) + { + if (!lowerBound.signedLessThan(upperBound)) break; + } + else + { + if (!lowerBound.unsignedLessThan(upperBound)) break; + } + pivot = computeAverage(lowerBound, upperBound, d_isSigned); + + optChecker->push(); + // pivot < target <= upperBound + optChecker->assertFormula( + nm->mkNode(kind::AND, + nm->mkNode(GTOperator, target, nm->mkConst(pivot)), + nm->mkNode(LEOperator, target, nm->mkConst(upperBound)))); + intermediateSatResult = optChecker->checkSat(); + if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) + { + return std::make_pair(OptResult::OPT_UNKNOWN, value); + } + if (intermediateSatResult.isSat() == Result::SAT) + { + value = optChecker->getValue(target); + lowerBound = value.getConst<BitVector>(); + } + else if (intermediateSatResult.isSat() == Result::UNSAT) + { + if (lowerBound == pivot) + { + // upperbound = lowerbound + 1 + // and lowerbound < target <= upperbound is UNSAT + // return the lowerbound + return std::make_pair(OptResult::OPT_OPTIMAL, value); + } + else + { + upperBound = pivot; + } + } + else + { + return std::make_pair(OptResult::OPT_UNKNOWN, value); + } + optChecker->pop(); + } + return std::make_pair(OptResult::OPT_OPTIMAL, value); +} + +} // namespace cvc5::omt diff --git a/src/omt/bitvector_optimizer.h b/src/omt/bitvector_optimizer.h new file mode 100644 index 000000000..9cafea38b --- /dev/null +++ b/src/omt/bitvector_optimizer.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file bitvector_optimizer.h + ** \verbatim + ** Top contributors (to current version): + ** Yancheng Ou + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief Optimizer for BitVector type + **/ + +#ifndef CVC4__OMT__BITVECTOR_OPTIMIZER_H +#define CVC4__OMT__BITVECTOR_OPTIMIZER_H + +#include "omt/omt_optimizer.h" + +namespace cvc5::omt { + +/** + * Optimizer for BitVector type + */ +class OMTOptimizerBitVector : public OMTOptimizer +{ + public: + OMTOptimizerBitVector(bool isSigned); + virtual ~OMTOptimizerBitVector() = default; + std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver, + Node target) override; + std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver, + Node target) override; + + private: + /** + * Computes the BitVector version of (a + b) / 2 without overflow, + * rounding towards -infinity: -1.5 --> -2 and 1.5 --> 1 + * same as the rounding scheme for int32_t + **/ + BitVector computeAverage(const BitVector& a, + const BitVector& b, + bool isSigned); + /** Is the BitVector doing signed comparison? **/ + bool d_isSigned; +}; + +} // namespace cvc5::omt + +#endif /* CVC4__OMT__BITVECTOR_OPTIMIZER_H */ diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp new file mode 100644 index 000000000..f9509b47d --- /dev/null +++ b/src/omt/integer_optimizer.cpp @@ -0,0 +1,87 @@ +/********************* */ +/*! \file integer_optimizer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Yancheng Ou + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief Optimizer for Integer type + **/ + +#include "omt/integer_optimizer.h" + +#include "options/smt_options.h" +#include "smt/smt_engine.h" + +using namespace cvc5::smt; +namespace cvc5::omt { + +std::pair<OptResult, Node> OMTOptimizerInteger::optimize( + SmtEngine* parentSMTSolver, Node target, ObjectiveType objType) +{ + // linear search for integer goal + // the smt engine to which we send intermediate queries + // for the linear search. + std::unique_ptr<SmtEngine> optChecker = + OMTOptimizer::createOptCheckerWithTimeout(parentSMTSolver, false); + NodeManager* nm = optChecker->getNodeManager(); + + Result intermediateSatResult = optChecker->checkSat(); + // Model-value of objective (used in optimization loop) + Node value; + if (intermediateSatResult.isUnknown()) + { + return std::make_pair(OptResult::OPT_UNKNOWN, value); + } + if (intermediateSatResult.isSat() == Result::UNSAT) + { + return std::make_pair(OptResult::OPT_UNSAT, value); + } + // asserts objective > old_value (used in optimization loop) + Node increment; + Kind incrementalOperator = kind::NULL_EXPR; + if (objType == ObjectiveType::OBJECTIVE_MINIMIZE) + { + // if objective is MIN, then assert optimization_target < + // current_model_value + incrementalOperator = kind::LT; + } + else if (objType == ObjectiveType::OBJECTIVE_MAXIMIZE) + { + // if objective is MAX, then assert optimization_target > + // current_model_value + incrementalOperator = kind::GT; + } + // Workhorse of linear search: + // This loop will keep incrmenting/decrementing the objective until unsat + // When unsat is hit, + // the optimized value is the model value just before the unsat call + while (intermediateSatResult.isSat() == Result::SAT) + { + value = optChecker->getValue(target); + Assert(!value.isNull()); + increment = nm->mkNode(incrementalOperator, target, value); + optChecker->assertFormula(increment); + intermediateSatResult = optChecker->checkSat(); + } + return std::make_pair(OptResult::OPT_OPTIMAL, value); +} + +std::pair<OptResult, Node> OMTOptimizerInteger::minimize( + SmtEngine* parentSMTSolver, Node target) +{ + return this->optimize( + parentSMTSolver, target, ObjectiveType::OBJECTIVE_MINIMIZE); +} +std::pair<OptResult, Node> OMTOptimizerInteger::maximize( + SmtEngine* parentSMTSolver, Node target) +{ + return this->optimize( + parentSMTSolver, target, ObjectiveType::OBJECTIVE_MAXIMIZE); +} + +} // namespace cvc5::omt diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h new file mode 100644 index 000000000..398aed616 --- /dev/null +++ b/src/omt/integer_optimizer.h @@ -0,0 +1,47 @@ +/********************* */ +/*! \file integer_optimizer.h + ** \verbatim + ** Top contributors (to current version): + ** Yancheng Ou + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief Optimizer for Integer type + **/ + +#ifndef CVC4__OMT__INTEGER_OPTIMIZER_H +#define CVC4__OMT__INTEGER_OPTIMIZER_H + +#include "omt/omt_optimizer.h" + +namespace cvc5::omt { + +/** + * Optimizer for Integer type + */ +class OMTOptimizerInteger : public OMTOptimizer +{ + public: + OMTOptimizerInteger() = default; + virtual ~OMTOptimizerInteger() = default; + std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver, + Node target) override; + std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver, + Node target) override; + + private: + /** + * Handles the optimization query specified by objType + * (objType = OBJECTIVE_MINIMIZE / OBJECTIVE_MAXIMIZE) + **/ + std::pair<smt::OptResult, Node> optimize(SmtEngine* parentSMTSolver, + Node target, + smt::ObjectiveType objType); +}; + +} // namespace cvc5::omt + +#endif /* CVC4__OMT__INTEGER_OPTIMIZER_H */ diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp new file mode 100644 index 000000000..4f64026e2 --- /dev/null +++ b/src/omt/omt_optimizer.cpp @@ -0,0 +1,69 @@ +/********************* */ +/*! \file omt_optimizer.cpp + ** \verbatim + ** Top contributors (to current version): + ** Yancheng Ou + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief The base class for optimizers of individual CVC4 type + **/ + +#include "omt/omt_optimizer.h" + +#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> OMTOptimizer::getOptimizerForNode(Node targetNode, + bool isSigned) +{ + // the datatype of the target node + TypeNode objectiveType = targetNode.getType(true); + if (objectiveType.isInteger()) + { + // integer type: use OMTOptimizerInteger + return std::unique_ptr<OMTOptimizer>(new OMTOptimizerInteger()); + } + else if (objectiveType.isBitVector()) + { + // bitvector type: use OMTOptimizerBitVector + return std::unique_ptr<OMTOptimizer>(new OMTOptimizerBitVector(isSigned)); + } + else + { + return nullptr; + } +} + +std::unique_ptr<SmtEngine> OMTOptimizer::createOptCheckerWithTimeout( + SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout) +{ + std::unique_ptr<SmtEngine> 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<Node> p_assertions = parentSMTSolver->getExpandedAssertions(); + for (const Node& e : p_assertions) + { + optChecker->assertFormula(e); + } + return optChecker; +} + +} // namespace cvc5::omt diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h new file mode 100644 index 000000000..da84556da --- /dev/null +++ b/src/omt/omt_optimizer.h @@ -0,0 +1,84 @@ +/********************* */ +/*! \file omt_optimizer.h + ** \verbatim + ** Top contributors (to current version): + ** Yancheng Ou + ** This file is part of the CVC4 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.\endverbatim + ** + ** \brief The base class for optimizers of individual CVC4 type + **/ + +#ifndef CVC4__OMT__OMT_OPTIMIZER_H +#define CVC4__OMT__OMT_OPTIMIZER_H + +#include "smt/optimization_solver.h" + +namespace cvc5::omt { + +/** + * The base class for optimizers of individual CVC type + */ +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 + * @return a unique_pointer pointing to a derived class of OMTOptimizer + * and this is the optimizer for targetNode + **/ + static std::unique_ptr<OMTOptimizer> getOptimizerForNode( + Node targetNode, bool isSigned = false); + + /** + * 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<SmtEngine> createOptCheckerWithTimeout( + SmtEngine* parentSMTSolver, + bool needsTimeout = false, + unsigned long timeout = 0); + + /** + * Minimize the target node with constraints encoded in parentSMTSolver + * + * @param parentSMTSolver an SMT solver encoding the assertions as the + * constraints + * @param target the target expression to optimize + * @return pair<OptResult, Node>: the result of optimization and the optimized + * value, if OptResult is OPT_UNKNOWN, value returned could be empty node or + * something suboptimal. + **/ + virtual std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver, + Node target) = 0; + /** + * Maximize the target node with constraints encoded in parentSMTSolver + * + * @param parentSMTSolver an SMT solver encoding the assertions as the + * constraints + * @param target the target expression to optimize + * @return pair<OptResult, Node>: the result of optimization and the optimized + * value, if OptResult is OPT_UNKNOWN, value returned could be empty node or + * something suboptimal. + **/ + virtual std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver, + Node target) = 0; +}; + +} // namespace cvc5::omt + +#endif /* CVC4__OMT__OMT_OPTIMIZER_H */ diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index ae1ce7057..70fa0f28c 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -2,7 +2,7 @@ /*! \file optimization_solver.cpp ** \verbatim ** Top contributors (to current version): - ** Michael Chang + ** Michael Chang, Yancheng Ou ** This file is part of the CVC4 project. ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. @@ -14,13 +14,10 @@ #include "smt/optimization_solver.h" -#include "options/smt_options.h" -#include "smt/smt_engine.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/smt_engine_subsolver.h" +#include "omt/omt_optimizer.h" using namespace cvc5::theory; - +using namespace cvc5::omt; namespace cvc5 { namespace smt { @@ -33,7 +30,7 @@ namespace smt { OptimizationSolver::OptimizationSolver(SmtEngine* parent) : d_parent(parent), - d_activatedObjective(Node(), OBJECTIVE_UNDEFINED), + d_activatedObjective(Node(), ObjectiveType::OBJECTIVE_UNDEFINED), d_savedValue() { } @@ -43,80 +40,35 @@ OptimizationSolver::~OptimizationSolver() {} OptResult OptimizationSolver::checkOpt() { // Make sure that the objective is not the default one - Assert(d_activatedObjective.getType() != OBJECTIVE_UNDEFINED); + Assert(d_activatedObjective.getType() != ObjectiveType::OBJECTIVE_UNDEFINED); Assert(!d_activatedObjective.getNode().isNull()); - // the smt engine to which we send intermediate queries - // for the linear search. - std::unique_ptr<SmtEngine> optChecker; - initializeSubsolver(optChecker); - NodeManager* nm = optChecker->getNodeManager(); - - // 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<Node> p_assertions = d_parent->getExpandedAssertions(); - for (const Node& e : p_assertions) - { - optChecker->assertFormula(e); - } + std::unique_ptr<OMTOptimizer> optimizer = OMTOptimizer::getOptimizerForNode( + d_activatedObjective.getNode(), d_activatedObjective.getSigned()); - // We need to checksat once before the optimization loop so we have a - // baseline value to increment - Result loop_r = optChecker->checkSat(); + Assert(optimizer != nullptr); - if (loop_r.isUnknown()) + std::pair<OptResult, Node> optResult; + if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MAXIMIZE) { - return OPT_UNKNOWN; + optResult = optimizer->maximize(this->d_parent, + this->d_activatedObjective.getNode()); } - if (!loop_r.isSat()) + else if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MINIMIZE) { - return OPT_UNSAT; + optResult = optimizer->minimize(this->d_parent, + this->d_activatedObjective.getNode()); } - // Model-value of objective (used in optimization loop) - Node value; - // asserts objective > old_value (used in optimization loop) - Node increment; - - // Workhorse of linear optimization: - // This loop will keep incrmenting the objective until unsat - // When unsat is hit, the optimized value is the model value just before the - // unsat call - while (loop_r.isSat()) - { - // get the model-value of objective in last sat call - value = optChecker->getValue(d_activatedObjective.getNode()); - - // We need to save the value since we need the model value just before the - // unsat call - Assert(!value.isNull()); - d_savedValue = value; - - // increment on the model-value of objective: - // if we're maximizing increment = objective > old_objective value - // if we're minimizing increment = objective < old_objective value - if (d_activatedObjective.getType() == OBJECTIVE_MAXIMIZE) - { - increment = nm->mkNode(kind::GT, d_activatedObjective.getNode(), value); - } - else - { - increment = nm->mkNode(kind::LT, d_activatedObjective.getNode(), value); - } - optChecker->assertFormula(increment); - loop_r = optChecker->checkSat(); - } - - return OPT_OPTIMAL; + this->d_savedValue = optResult.second; + return optResult.first; } -void OptimizationSolver::activateObj(const Node& obj, const int& type) +void OptimizationSolver::activateObj(const Node& obj, + const ObjectiveType type, + bool bvSigned) { - d_activatedObjective = Objective(obj, (ObjectiveType)type); + d_activatedObjective = Objective(obj, type, bvSigned); } Node OptimizationSolver::objectiveGetValue() @@ -125,7 +77,8 @@ Node OptimizationSolver::objectiveGetValue() return d_savedValue; } -Objective::Objective(Node obj, ObjectiveType type) : d_type(type), d_node(obj) +Objective::Objective(Node obj, ObjectiveType type, bool bvSigned) + : d_type(type), d_node(obj), d_bvSigned(bvSigned) { } @@ -133,5 +86,7 @@ ObjectiveType Objective::getType() { return d_type; } Node Objective::getNode() { return d_node; } +bool Objective::getSigned() { return d_bvSigned; } + } // namespace smt } // namespace cvc5 diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h index b79a4a823..b7f264ef1 100644 --- a/src/smt/optimization_solver.h +++ b/src/smt/optimization_solver.h @@ -2,7 +2,7 @@ /*! \file optimization_solver.h ** \verbatim ** Top contributors (to current version): - ** Michael Chang + ** Michael Chang, Yancheng Ou ** This file is part of the CVC4 project. ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS ** in the top-level source directory and their institutional affiliations. @@ -33,7 +33,7 @@ namespace smt { * * Represents whether an objective should be minimized or maximized */ -enum ObjectiveType +enum class ObjectiveType { OBJECTIVE_MINIMIZE, OBJECTIVE_MAXIMIZE, @@ -46,7 +46,7 @@ enum ObjectiveType * Represents the result of a checkopt query * (unimplemented) OPT_OPTIMAL: if value was found */ -enum OptResult +enum class OptResult { // the original set of assertions has result UNKNOWN OPT_UNKNOWN, @@ -55,6 +55,9 @@ enum OptResult // the optimization loop finished and optimal OPT_OPTIMAL, + // the goal is unbounded, so it would be -inf or +inf + OPT_UNBOUNDED, + // The last value is here as a preparation for future work // in which pproximate optimizations will be supported. @@ -62,16 +65,32 @@ enum OptResult OPT_SAT_APPROX }; +/** + * The optimization objective, which contains: + * - the optimization target node, + * - whether it's maximize/minimize + * - and whether it's signed for BitVectors + **/ class Objective { public: - Objective(Node n, ObjectiveType type); + /** + * Constructor + * @param n the optimization target node + * @param type speficies whether it's maximize/minimize + * @param bvSigned specifies whether it's using signed or unsigned comparison + * for BitVectors this parameter is only valid when the type of target node + * is BitVector + **/ + Objective(Node n, ObjectiveType type, bool bvSigned = false); ~Objective(){}; /** A getter for d_type **/ ObjectiveType getType(); /** A getter for d_node **/ Node getNode(); + /** A getter for d_bvSigned **/ + bool getSigned(); private: /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR @@ -80,38 +99,55 @@ class Objective /** The node associated to the term that was used to construct the objective. * **/ Node d_node; - }; + /** Specify whether to use signed or unsigned comparison + * for BitVectors (only for BitVectors), this variable is defaulted to false + * **/ + bool d_bvSigned; +}; + +/** + * A solver for optimization queries. + * + * This class is responsible for responding to optmization queries. It + * spawns a subsolver SmtEngine that captures the parent assertions and + * implements a linear optimization loop. Supports activateObjective, + * checkOpt, and objectiveGetValue in that order. + */ +class OptimizationSolver +{ + public: /** - * A solver for optimization queries. - * - * This class is responsible for responding to optmization queries. It - * spawns a subsolver SmtEngine that captures the parent assertions and - * implements a linear optimization loop. Supports activateObjective, - * checkOpt, and objectiveGetValue in that order. - */ - class OptimizationSolver - { - public: - /** parent is the smt_solver that the user added their assertions to **/ - OptimizationSolver(SmtEngine* parent); - ~OptimizationSolver(); - - /** Runs the optimization loop for the activated objective **/ - OptResult checkOpt(); - /** Activates an objective: will be optimized for **/ - void activateObj(const Node& obj, const int& type); - /** Gets the value of the optimized objective after checkopt is called **/ - Node objectiveGetValue(); - - private: - /** The parent SMT engine **/ - SmtEngine* d_parent; - /** The objectives to optimize for **/ - Objective d_activatedObjective; - /** A saved value of the objective from the last sat call. **/ - Node d_savedValue; - }; + * Constructor + * @param parent the smt_solver that the user added their assertions to + **/ + OptimizationSolver(SmtEngine* parent); + ~OptimizationSolver(); + + /** Runs the optimization loop for the activated objective **/ + OptResult checkOpt(); + /** + * Activates an objective: will be optimized for + * @param obj the Node representing the expression that will be optimized for + * @param type specifies whether it's maximize or minimize + * @param bvSigned specifies whether we should use signed/unsigned + * comparison for BitVectors (only effective for BitVectors) + * and its default is false + **/ + void activateObj(const Node& obj, + const ObjectiveType type, + bool bvSigned = false); + /** Gets the value of the optimized objective after checkopt is called **/ + Node objectiveGetValue(); + + private: + /** The parent SMT engine **/ + SmtEngine* d_parent; + /** The objectives to optimize for **/ + Objective d_activatedObjective; + /** A saved value of the objective from the last sat call. **/ + Node d_savedValue; +}; } // namespace smt } // namespace cvc5 |