Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
/*! \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.
#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 {
OptimizationSolver::OptimizationSolver(SmtEngine* parent)
: d_parent(parent),
- d_activatedObjective(Node(), OBJECTIVE_UNDEFINED),
+ d_activatedObjective(Node(), ObjectiveType::OBJECTIVE_UNDEFINED),
d_savedValue()
{
}
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()
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)
{
}
Node Objective::getNode() { return d_node; }
+bool Objective::getSigned() { return d_bvSigned; }
+
} // namespace smt
} // namespace cvc5
/*! \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.
*
* Represents whether an objective should be minimized or maximized
*/
-enum ObjectiveType
+enum class ObjectiveType
{
OBJECTIVE_MINIMIZE,
OBJECTIVE_MAXIMIZE,
* 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,
// 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.
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
/** 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
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)
--- /dev/null
+/********************* */
+/*! \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 <iostream>
+
+#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<OptimizationSolver> d_optslv;
+ std::unique_ptr<TypeNode> d_BV32Type;
+ std::unique_ptr<TypeNode> 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<BitVector>();
+ 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<BitVector>();
+ 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
/*! \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 <iostream>
+
#include "smt/optimization_solver.h"
#include "test_smt.h"
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)
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)
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
projects / cvc5.git / commitdiff