From 3f1ab5672ca746a4a6573e1ebf9f74d72978d1cf Mon Sep 17 00:00:00 2001 From: Yancheng Ou Date: Mon, 5 Apr 2021 06:21:40 -0700 Subject: [PATCH] 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. --- src/CMakeLists.txt | 6 + src/omt/bitvector_optimizer.cpp | 239 ++++++++++++++++++++++ src/omt/bitvector_optimizer.h | 50 +++++ src/omt/integer_optimizer.cpp | 87 ++++++++ src/omt/integer_optimizer.h | 47 +++++ src/omt/omt_optimizer.cpp | 69 +++++++ src/omt/omt_optimizer.h | 84 ++++++++ src/smt/optimization_solver.cpp | 95 +++------ src/smt/optimization_solver.h | 104 +++++++--- test/unit/theory/CMakeLists.txt | 1 + test/unit/theory/theory_bv_opt_white.cpp | 154 ++++++++++++++ test/unit/theory/theory_int_opt_white.cpp | 71 +++++-- 12 files changed, 887 insertions(+), 120 deletions(-) create mode 100644 src/omt/bitvector_optimizer.cpp create mode 100644 src/omt/bitvector_optimizer.h create mode 100644 src/omt/integer_optimizer.cpp create mode 100644 src/omt/integer_optimizer.h create mode 100644 src/omt/omt_optimizer.cpp create mode 100644 src/omt/omt_optimizer.h create mode 100644 test/unit/theory/theory_bv_opt_white.cpp 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(a.isBitSet(0)); + uint32_t bMod2 = static_cast(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 OMTOptimizerBitVector::minimize( + SmtEngine* parentSMTSolver, Node 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) + 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(); + 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(); + } + 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 OMTOptimizerBitVector::maximize( + SmtEngine* parentSMTSolver, Node 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) + 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(); + 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(); + } + 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 minimize(SmtEngine* parentSMTSolver, + Node target) override; + std::pair 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 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 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 OMTOptimizerInteger::minimize( + SmtEngine* parentSMTSolver, Node target) +{ + return this->optimize( + parentSMTSolver, target, ObjectiveType::OBJECTIVE_MINIMIZE); +} +std::pair 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 minimize(SmtEngine* parentSMTSolver, + Node target) override; + std::pair maximize(SmtEngine* parentSMTSolver, + Node target) override; + + private: + /** + * Handles the optimization query specified by objType + * (objType = OBJECTIVE_MINIMIZE / OBJECTIVE_MAXIMIZE) + **/ + std::pair 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::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(new OMTOptimizerInteger()); + } + else if (objectiveType.isBitVector()) + { + // bitvector type: use OMTOptimizerBitVector + return std::unique_ptr(new OMTOptimizerBitVector(isSigned)); + } + else + { + return nullptr; + } +} + +std::unique_ptr OMTOptimizer::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 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 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 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: 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 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: 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 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 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 p_assertions = d_parent->getExpandedAssertions(); - for (const Node& e : p_assertions) - { - optChecker->assertFormula(e); - } + std::unique_ptr 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; + 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 diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 723369200..fef2bdd38 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -20,6 +20,7 @@ cvc4_add_unit_test_white(theory_bags_rewriter_white theory) cvc4_add_unit_test_white(theory_bags_type_rules_white theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) +cvc4_add_unit_test_white(theory_bv_opt_white theory) cvc4_add_unit_test_white(theory_bv_int_blaster_white theory) cvc4_add_unit_test_white(theory_engine_white theory) cvc4_add_unit_test_white(theory_int_opt_white theory) diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp new file mode 100644 index 000000000..fde7a5e2e --- /dev/null +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -0,0 +1,154 @@ +/********************* */ +/*! \file theory_bv_opt_white.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 White-box testing for optimization module for BitVectors. + **/ +#include + +#include "smt/optimization_solver.h" +#include "test_smt.h" + +namespace cvc5 { + +using namespace theory; +using namespace smt; + +namespace test { + +class TestTheoryWhiteBVOpt : public TestSmtNoFinishInit +{ + protected: + void SetUp() override + { + TestSmtNoFinishInit::SetUp(); + d_smtEngine->setOption("produce-assertions", "true"); + d_smtEngine->finishInit(); + + d_optslv.reset(new OptimizationSolver(d_smtEngine.get())); + d_BV32Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(32u))); + d_BV16Type.reset(new TypeNode(d_nodeManager->mkBitVectorType(16u))); + } + + std::unique_ptr d_optslv; + std::unique_ptr d_BV32Type; + std::unique_ptr d_BV16Type; +}; + +TEST_F(TestTheoryWhiteBVOpt, unsigned_min) +{ + Node x = d_nodeManager->mkVar(*d_BV32Type); + + Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x3FFFFFA1)); + Node b = d_nodeManager->mkConst(BitVector(32u, (unsigned)0xFFFFFFF1)); + + // (unsigned)0x3FFFFFA1 <= x <= (unsigned)0xFFFFFFF1 + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); + + const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MINIMIZE; + d_optslv->activateObj(x, obj_type, false); + + OptResult r = d_optslv->checkOpt(); + + ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(BitVector(32u, (unsigned)0x3FFFFFA1))); + + std::cout << "Passed!" << std::endl; + std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() + << std::endl; +} + +TEST_F(TestTheoryWhiteBVOpt, signed_min) +{ + Node x = d_nodeManager->mkVar(*d_BV32Type); + + Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000)); + Node b = d_nodeManager->mkConst(BitVector(32u, 2147483647u)); + // -2147483648 <= x <= 2147483647 + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); + + const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MINIMIZE; + d_optslv->activateObj(x, obj_type, true); + + OptResult r = d_optslv->checkOpt(); + + ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + + BitVector val = d_optslv->objectiveGetValue().getConst(); + std::cout << "opt value is: " << val << std::endl; + + // expect the minimum x = -1 + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000))); + std::cout << "Passed!" << std::endl; + std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() + << std::endl; +} + +TEST_F(TestTheoryWhiteBVOpt, unsigned_max) +{ + Node x = d_nodeManager->mkVar(*d_BV32Type); + + Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)1)); + Node b = d_nodeManager->mkConst(BitVector(32u, (unsigned)2)); + + // If the gap is too large, it will have a performance issue!!! + // Need binary search! + // (unsigned)1 <= x <= (unsigned)2 + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, a, x)); + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_ULE, x, b)); + + const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MAXIMIZE; + d_optslv->activateObj(x, obj_type, false); + + OptResult r = d_optslv->checkOpt(); + + ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + + BitVector val = d_optslv->objectiveGetValue().getConst(); + std::cout << "opt value is: " << val << std::endl; + + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(BitVector(32u, (unsigned)2))); + std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() + << std::endl; +} + +TEST_F(TestTheoryWhiteBVOpt, signed_max) +{ + Node x = d_nodeManager->mkVar(*d_BV32Type); + + Node a = d_nodeManager->mkConst(BitVector(32u, (unsigned)0x80000000)); + Node b = d_nodeManager->mkConst(BitVector(32u, 10u)); + + // -2147483648 <= x <= 10 + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, a, x)); + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, x, b)); + + const ObjectiveType obj_type = ObjectiveType::OBJECTIVE_MAXIMIZE; + d_optslv->activateObj(x, obj_type, true); + + OptResult r = d_optslv->checkOpt(); + + ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + + // expect the maxmum x = + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(BitVector(32u, 10u))); + std::cout << "Optimized value is: " << d_optslv->objectiveGetValue() + << std::endl; +} + +} // 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 6111c2640..feab15b2b 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -2,16 +2,17 @@ /*! \file theory_int_opt_white.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. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief White-box testing for optimization module. + ** \brief White-box testing for optimization module for Integers. **/ #include + #include "smt/optimization_solver.h" #include "test_smt.h" @@ -56,20 +57,21 @@ TEST_F(TestTheoryWhiteIntOpt, max) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - const ObjectiveType max_type = OBJECTIVE_MAXIMIZE; + const ObjectiveType max_type = ObjectiveType::OBJECTIVE_MAXIMIZE; // We activate our objective so the subsolver knows to optimize it d_optslv->activateObj(max_cost, max_type); OptResult r = d_optslv->checkOpt(); + ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + // We expect max_cost == 99 ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(Rational("99"))); + d_nodeManager->mkConst(Rational("99"))); - std::cout << "Result is :" << r << std::endl; - std::cout << "Optimized max value is: " - << d_optslv->objectiveGetValue() << std::endl; + std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue() + << std::endl; } TEST_F(TestTheoryWhiteIntOpt, min) @@ -89,20 +91,21 @@ TEST_F(TestTheoryWhiteIntOpt, min) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - const ObjectiveType min_type = OBJECTIVE_MINIMIZE; + const ObjectiveType min_type = ObjectiveType::OBJECTIVE_MINIMIZE; // We activate our objective so the subsolver knows to optimize it d_optslv->activateObj(max_cost, min_type); OptResult r = d_optslv->checkOpt(); + ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + // We expect max_cost == 99 ASSERT_EQ(d_optslv->objectiveGetValue(), - d_nodeManager->mkConst(Rational("1"))); + d_nodeManager->mkConst(Rational("1"))); - std::cout << "Result is :" << r << std::endl; - std::cout << "Optimized max value is: " - << d_optslv->objectiveGetValue() << std::endl; + std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue() + << std::endl; } TEST_F(TestTheoryWhiteIntOpt, result) @@ -122,18 +125,54 @@ TEST_F(TestTheoryWhiteIntOpt, result) d_smtEngine->assertFormula(upb); d_smtEngine->assertFormula(lowb); - const ObjectiveType max_type = OBJECTIVE_MAXIMIZE; + const ObjectiveType max_type = ObjectiveType::OBJECTIVE_MAXIMIZE; // We activate our objective so the subsolver knows to optimize it d_optslv->activateObj(max_cost, max_type); // This should return OPT_UNSAT since 0 > x > 100 is impossible. OptResult r = d_optslv->checkOpt(); - + // We expect our check to have returned UNSAT - ASSERT_EQ(r, OPT_UNSAT); + ASSERT_EQ(r, OptResult::OPT_UNSAT); +} + +TEST_F(TestTheoryWhiteIntOpt, open_interval) +{ + Node ub1 = d_nodeManager->mkConst(Rational("100")); + Node lb1 = d_nodeManager->mkConst(Rational("0")); + Node lb2 = d_nodeManager->mkConst(Rational("110")); + + Node cost1 = d_nodeManager->mkVar(*d_intType); + Node cost2 = d_nodeManager->mkVar(*d_intType); + + /* Result of assertion is: + 0 < cost1 < 100 + 110 < cost2 + */ + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb1, cost1)); + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, cost1, ub1)); - std::cout << "Result is :" << r << std::endl; + d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::LT, lb2, cost2)); + + /* Optimization objective: + cost1 + cost2 + */ + Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2); + + const ObjectiveType min_type = ObjectiveType::OBJECTIVE_MINIMIZE; + d_optslv->activateObj(cost3, min_type); + + OptResult r = d_optslv->checkOpt(); + + ASSERT_EQ(r, OptResult::OPT_OPTIMAL); + + // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112 + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(Rational("112"))); + std::cout << "Optimized min value is: " << d_optslv->objectiveGetValue() + << std::endl; } + } // namespace test } // namespace cvc5 -- 2.30.2