summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/omt/bitvector_optimizer.cpp32
-rw-r--r--src/omt/bitvector_optimizer.h8
-rw-r--r--src/omt/integer_optimizer.cpp28
-rw-r--r--src/omt/integer_optimizer.h17
-rw-r--r--src/omt/omt_optimizer.cpp2
-rw-r--r--src/omt/omt_optimizer.h20
-rw-r--r--src/smt/optimization_solver.cpp70
-rw-r--r--src/smt/optimization_solver.h186
-rw-r--r--test/unit/theory/theory_bv_opt_white.cpp75
-rw-r--r--test/unit/theory/theory_int_opt_white.cpp50
10 files changed, 257 insertions, 231 deletions
diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp
index ab5af03f7..7edecdb73 100644
--- a/src/omt/bitvector_optimizer.cpp
+++ b/src/omt/bitvector_optimizer.cpp
@@ -43,8 +43,8 @@ BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a,
+ aMod2PlusbMod2Div2));
}
-std::pair<OptResult, Node> OMTOptimizerBitVector::minimize(
- SmtEngine* parentSMTSolver, Node target)
+OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* parentSMTSolver,
+ TNode target)
{
// the smt engine to which we send intermediate queries
// for the binary search.
@@ -56,11 +56,11 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::minimize(
Node value;
if (intermediateSatResult.isUnknown())
{
- return std::make_pair(OptResult::OPT_UNKNOWN, value);
+ return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
if (intermediateSatResult.isSat() == Result::UNSAT)
{
- return std::make_pair(OptResult::OPT_UNSAT, value);
+ return OptimizationResult(OptimizationResult::UNSAT, value);
}
// value equals to upperBound
@@ -107,7 +107,7 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::minimize(
intermediateSatResult = optChecker->checkSat();
if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
{
- return std::make_pair(OptResult::OPT_UNKNOWN, value);
+ return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
if (intermediateSatResult.isSat() == Result::SAT)
{
@@ -121,7 +121,7 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::minimize(
// lowerBound == pivot ==> upperbound = lowerbound + 1
// and lowerbound <= target < upperbound is UNSAT
// return the upperbound
- return std::make_pair(OptResult::OPT_OPTIMAL, value);
+ return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
else
{
@@ -130,15 +130,15 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::minimize(
}
else
{
- return std::make_pair(OptResult::OPT_UNKNOWN, value);
+ return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
optChecker->pop();
}
- return std::make_pair(OptResult::OPT_OPTIMAL, value);
+ return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
-std::pair<OptResult, Node> OMTOptimizerBitVector::maximize(
- SmtEngine* parentSMTSolver, Node target)
+OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* parentSMTSolver,
+ TNode target)
{
// the smt engine to which we send intermediate queries
// for the binary search.
@@ -150,11 +150,11 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::maximize(
Node value;
if (intermediateSatResult.isUnknown())
{
- return std::make_pair(OptResult::OPT_UNKNOWN, value);
+ return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
if (intermediateSatResult.isSat() == Result::UNSAT)
{
- return std::make_pair(OptResult::OPT_UNSAT, value);
+ return OptimizationResult(OptimizationResult::UNSAT, value);
}
// value equals to upperBound
@@ -198,7 +198,7 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::maximize(
intermediateSatResult = optChecker->checkSat();
if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
{
- return std::make_pair(OptResult::OPT_UNKNOWN, value);
+ return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
if (intermediateSatResult.isSat() == Result::SAT)
{
@@ -212,7 +212,7 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::maximize(
// upperbound = lowerbound + 1
// and lowerbound < target <= upperbound is UNSAT
// return the lowerbound
- return std::make_pair(OptResult::OPT_OPTIMAL, value);
+ return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
else
{
@@ -221,11 +221,11 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::maximize(
}
else
{
- return std::make_pair(OptResult::OPT_UNKNOWN, value);
+ return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
optChecker->pop();
}
- return std::make_pair(OptResult::OPT_OPTIMAL, value);
+ return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
} // namespace cvc5::omt
diff --git a/src/omt/bitvector_optimizer.h b/src/omt/bitvector_optimizer.h
index 98dc63b3f..b95c185f8 100644
--- a/src/omt/bitvector_optimizer.h
+++ b/src/omt/bitvector_optimizer.h
@@ -28,10 +28,10 @@ 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;
+ smt::OptimizationResult minimize(SmtEngine* parentSMTSolver,
+ TNode target) override;
+ smt::OptimizationResult maximize(SmtEngine* parentSMTSolver,
+ TNode target) override;
private:
/**
diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp
index f3ee24b3d..8fbfff1a2 100644
--- a/src/omt/integer_optimizer.cpp
+++ b/src/omt/integer_optimizer.cpp
@@ -21,8 +21,10 @@
using namespace cvc5::smt;
namespace cvc5::omt {
-std::pair<OptResult, Node> OMTOptimizerInteger::optimize(
- SmtEngine* parentSMTSolver, Node target, ObjectiveType objType)
+OptimizationResult OMTOptimizerInteger::optimize(
+ SmtEngine* parentSMTSolver,
+ TNode target,
+ OptimizationObjective::ObjectiveType objType)
{
// linear search for integer goal
// the smt engine to which we send intermediate queries
@@ -36,22 +38,22 @@ std::pair<OptResult, Node> OMTOptimizerInteger::optimize(
Node value;
if (intermediateSatResult.isUnknown())
{
- return std::make_pair(OptResult::OPT_UNKNOWN, value);
+ return OptimizationResult(OptimizationResult::UNKNOWN, value);
}
if (intermediateSatResult.isSat() == Result::UNSAT)
{
- return std::make_pair(OptResult::OPT_UNSAT, value);
+ return OptimizationResult(OptimizationResult::UNSAT, value);
}
// asserts objective > old_value (used in optimization loop)
Node increment;
Kind incrementalOperator = kind::NULL_EXPR;
- if (objType == ObjectiveType::OBJECTIVE_MINIMIZE)
+ if (objType == OptimizationObjective::MINIMIZE)
{
// if objective is MIN, then assert optimization_target <
// current_model_value
incrementalOperator = kind::LT;
}
- else if (objType == ObjectiveType::OBJECTIVE_MAXIMIZE)
+ else if (objType == OptimizationObjective::MAXIMIZE)
{
// if objective is MAX, then assert optimization_target >
// current_model_value
@@ -69,20 +71,20 @@ std::pair<OptResult, Node> OMTOptimizerInteger::optimize(
optChecker->assertFormula(increment);
intermediateSatResult = optChecker->checkSat();
}
- return std::make_pair(OptResult::OPT_OPTIMAL, value);
+ return OptimizationResult(OptimizationResult::OPTIMAL, value);
}
-std::pair<OptResult, Node> OMTOptimizerInteger::minimize(
- SmtEngine* parentSMTSolver, Node target)
+OptimizationResult OMTOptimizerInteger::minimize(
+ SmtEngine* parentSMTSolver, TNode target)
{
return this->optimize(
- parentSMTSolver, target, ObjectiveType::OBJECTIVE_MINIMIZE);
+ parentSMTSolver, target, OptimizationObjective::MINIMIZE);
}
-std::pair<OptResult, Node> OMTOptimizerInteger::maximize(
- SmtEngine* parentSMTSolver, Node target)
+OptimizationResult OMTOptimizerInteger::maximize(
+ SmtEngine* parentSMTSolver, TNode target)
{
return this->optimize(
- parentSMTSolver, target, ObjectiveType::OBJECTIVE_MAXIMIZE);
+ parentSMTSolver, target, OptimizationObjective::MAXIMIZE);
}
} // namespace cvc5::omt
diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h
index d92bdb8eb..48d162494 100644
--- a/src/omt/integer_optimizer.h
+++ b/src/omt/integer_optimizer.h
@@ -28,19 +28,20 @@ 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;
+ smt::OptimizationResult minimize(SmtEngine* parentSMTSolver,
+ TNode target) override;
+ smt::OptimizationResult maximize(SmtEngine* parentSMTSolver,
+ TNode target) override;
private:
/**
* Handles the optimization query specified by objType
- * (objType = OBJECTIVE_MINIMIZE / OBJECTIVE_MAXIMIZE)
+ * (objType = MINIMIZE / MAXIMIZE)
**/
- std::pair<smt::OptResult, Node> optimize(SmtEngine* parentSMTSolver,
- Node target,
- smt::ObjectiveType objType);
+ smt::OptimizationResult optimize(
+ SmtEngine* parentSMTSolver,
+ TNode target,
+ smt::OptimizationObjective::ObjectiveType objType);
};
} // namespace cvc5::omt
diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp
index b0a8af63a..49b07fe26 100644
--- a/src/omt/omt_optimizer.cpp
+++ b/src/omt/omt_optimizer.cpp
@@ -26,7 +26,7 @@ using namespace cvc5::theory;
using namespace cvc5::smt;
namespace cvc5::omt {
-std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForNode(Node targetNode,
+std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForNode(TNode targetNode,
bool isSigned)
{
// the datatype of the target node
diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h
index 1e4c6d4ca..792a60169 100644
--- a/src/omt/omt_optimizer.h
+++ b/src/omt/omt_optimizer.h
@@ -39,7 +39,7 @@ class OMTOptimizer
* and this is the optimizer for targetNode
**/
static std::unique_ptr<OMTOptimizer> getOptimizerForNode(
- Node targetNode, bool isSigned = false);
+ TNode targetNode, bool isSigned = false);
/**
* Initialize an SMT subsolver for offline optimization purpose
@@ -60,24 +60,22 @@ class OMTOptimizer
* @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.
+ * @return smt::OptimizationResult the result of optimization, containing
+ * whether it's optimal and the optimized value.
**/
- virtual std::pair<smt::OptResult, Node> minimize(SmtEngine* parentSMTSolver,
- Node target) = 0;
+ virtual smt::OptimizationResult minimize(SmtEngine* parentSMTSolver,
+ TNode 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.
+ * @return smt::OptimizationResult the result of optimization, containing
+ * whether it's optimal and the optimized value.
**/
- virtual std::pair<smt::OptResult, Node> maximize(SmtEngine* parentSMTSolver,
- Node target) = 0;
+ virtual smt::OptimizationResult maximize(SmtEngine* parentSMTSolver,
+ TNode target) = 0;
};
} // namespace cvc5::omt
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index f854ec402..1c8fe6514 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -16,78 +16,54 @@
#include "smt/optimization_solver.h"
#include "omt/omt_optimizer.h"
+#include "smt/assertions.h"
using namespace cvc5::theory;
using namespace cvc5::omt;
namespace cvc5 {
namespace smt {
-/**
- * d_activatedObjective is initialized to a default objective:
- * default objective constructed with Null Node and OBJECTIVE_UNDEFINED
- *
- * d_savedValue is initialized to a default node (Null Node)
- */
-
-OptimizationSolver::OptimizationSolver(SmtEngine* parent)
- : d_parent(parent),
- d_activatedObjective(Node(), ObjectiveType::OBJECTIVE_UNDEFINED),
- d_savedValue()
+OptimizationResult::ResultType OptimizationSolver::checkOpt()
{
-}
-
-OptimizationSolver::~OptimizationSolver() {}
-
-OptResult OptimizationSolver::checkOpt()
-{
- // Make sure that the objective is not the default one
- Assert(d_activatedObjective.getType() != ObjectiveType::OBJECTIVE_UNDEFINED);
- Assert(!d_activatedObjective.getNode().isNull());
-
+ Assert(d_objectives.size() == 1);
+ // NOTE: currently we are only dealing with single obj
std::unique_ptr<OMTOptimizer> optimizer = OMTOptimizer::getOptimizerForNode(
- d_activatedObjective.getNode(), d_activatedObjective.getSigned());
+ d_objectives[0].getTarget(), d_objectives[0].bvIsSigned());
- Assert(optimizer != nullptr);
+ if (!optimizer) return OptimizationResult::UNSUPPORTED;
- std::pair<OptResult, Node> optResult;
- if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MAXIMIZE)
+ OptimizationResult optResult;
+ if (d_objectives[0].getType() == OptimizationObjective::MAXIMIZE)
{
- optResult = optimizer->maximize(this->d_parent,
- this->d_activatedObjective.getNode());
+ optResult = optimizer->maximize(d_parent, d_objectives[0].getTarget());
}
- else if (d_activatedObjective.getType() == ObjectiveType::OBJECTIVE_MINIMIZE)
+ else if (d_objectives[0].getType() == OptimizationObjective::MINIMIZE)
{
- optResult = optimizer->minimize(this->d_parent,
- this->d_activatedObjective.getNode());
+ optResult = optimizer->minimize(d_parent, d_objectives[0].getTarget());
}
- this->d_savedValue = optResult.second;
- return optResult.first;
+ d_results[0] = optResult;
+ return optResult.getType();
}
-void OptimizationSolver::activateObj(const Node& obj,
- const ObjectiveType type,
- bool bvSigned)
+void OptimizationSolver::pushObjective(
+ TNode target, OptimizationObjective::ObjectiveType type, bool bvSigned)
{
- d_activatedObjective = Objective(obj, type, bvSigned);
+ d_objectives.emplace_back(target, type, bvSigned);
+ d_results.emplace_back(OptimizationResult::UNSUPPORTED, Node());
}
-Node OptimizationSolver::objectiveGetValue()
+void OptimizationSolver::popObjective()
{
- Assert(!d_savedValue.isNull());
- return d_savedValue;
+ d_objectives.pop_back();
+ d_results.pop_back();
}
-Objective::Objective(Node obj, ObjectiveType type, bool bvSigned)
- : d_type(type), d_node(obj), d_bvSigned(bvSigned)
+std::vector<OptimizationResult> OptimizationSolver::getValues()
{
+ Assert(d_objectives.size() == d_results.size());
+ return d_results;
}
-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 59c228e27..0babd7a4a 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -20,7 +20,6 @@
#include "expr/node.h"
#include "expr/type_node.h"
-#include "smt/assertions.h"
#include "util/result.h"
namespace cvc5 {
@@ -30,40 +29,67 @@ class SmtEngine;
namespace smt {
/**
- * An enum for optimization queries.
- *
- * Represents whether an objective should be minimized or maximized
- */
-enum class ObjectiveType
-{
- OBJECTIVE_MINIMIZE,
- OBJECTIVE_MAXIMIZE,
- OBJECTIVE_UNDEFINED
-};
-
-/**
- * An enum for optimization queries.
- *
- * Represents the result of a checkopt query
- * (unimplemented) OPT_OPTIMAL: if value was found
+ * The optimization result of an optimization objective
+ * containing:
+ * - whether it's optimal or not
+ * - if so, the optimal value, otherwise the value might be empty node or
+ * something suboptimal
*/
-enum class OptResult
+class OptimizationResult
{
- // the original set of assertions has result UNKNOWN
- OPT_UNKNOWN,
- // the original set of assertions has result UNSAT
- OPT_UNSAT,
- // the optimization loop finished and optimal
- OPT_OPTIMAL,
+ public:
+ /**
+ * Enum indicating whether the checkOpt result
+ * is optimal or not.
+ **/
+ enum ResultType
+ {
+ // the type of the target is not supported
+ UNSUPPORTED,
+ // whether the value is optimal is UNKNOWN
+ UNKNOWN,
+ // the original set of assertions has result UNSAT
+ UNSAT,
+ // the value is optimal
+ OPTIMAL,
+ // the goal is unbounded,
+ // if objective is maximize, it's +infinity
+ // if objective is minimize, it's -infinity
+ UNBOUNDED,
+ };
- // the goal is unbounded, so it would be -inf or +inf
- OPT_UNBOUNDED,
+ /**
+ * Constructor
+ * @param type the optimization outcome
+ * @param value the optimized value
+ **/
+ OptimizationResult(ResultType type, TNode value)
+ : d_type(type), d_value(value)
+ {
+ }
+ OptimizationResult() : d_type(UNSUPPORTED), d_value() {}
+ ~OptimizationResult() = default;
- // The last value is here as a preparation for future work
- // in which pproximate optimizations will be supported.
+ /**
+ * Returns an enum indicating whether
+ * the result is optimal or not.
+ * @return an enum showing whether the result is optimal, unbounded,
+ * unsat, unknown or unsupported.
+ **/
+ ResultType getType() { return d_type; }
+ /**
+ * Returns the optimal value.
+ * @return Node containing the optimal value,
+ * if getType() is not OPTIMAL, it might return an empty node or a node
+ * containing non-optimal value
+ **/
+ Node getValue() { return d_value; }
- // if the solver halted early and value is only approximate
- OPT_SAT_APPROX
+ private:
+ /** the indicating whether the result is optimal or something else **/
+ ResultType d_type;
+ /** if the result is optimal, this is storing the optimal value **/
+ Node d_value;
};
/**
@@ -72,38 +98,58 @@ enum class OptResult
* - whether it's maximize/minimize
* - and whether it's signed for BitVectors
*/
-class Objective
+class OptimizationObjective
{
public:
/**
+ * An enum for optimization queries.
+ * Represents whether an objective should be minimized or maximized
+ */
+ enum ObjectiveType
+ {
+ MINIMIZE,
+ MAXIMIZE,
+ };
+
+ /**
* Constructor
- * @param n the optimization target node
+ * @param target 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(){};
+ OptimizationObjective(TNode target, ObjectiveType type, bool bvSigned = false)
+ : d_type(type), d_target(target), d_bvSigned(bvSigned)
+ {
+ }
+ ~OptimizationObjective() = default;
/** A getter for d_type **/
- ObjectiveType getType();
- /** A getter for d_node **/
- Node getNode();
+ ObjectiveType getType() { return d_type; }
+
+ /** A getter for d_target **/
+ Node getTarget() { return d_target; }
+
/** A getter for d_bvSigned **/
- bool getSigned();
+ bool bvIsSigned() { return d_bvSigned; }
private:
- /** The type of objective this is, either OBJECTIVE_MAXIMIZE OR
- * OBJECTIVE_MINIMIZE **/
+ /**
+ * The type of objective,
+ * it's either MAXIMIZE OR MINIMIZE
+ **/
ObjectiveType d_type;
- /** The node associated to the term that was used to construct the objective.
- * **/
- Node d_node;
- /** Specify whether to use signed or unsigned comparison
+ /**
+ * The node associated to the term that was used to construct the objective.
+ **/
+ Node d_target;
+
+ /**
+ * Specify whether to use signed or unsigned comparison
* for BitVectors (only for BitVectors), this variable is defaulted to false
- * **/
+ **/
bool d_bvSigned;
};
@@ -122,32 +168,54 @@ class OptimizationSolver
* Constructor
* @param parent the smt_solver that the user added their assertions to
**/
- OptimizationSolver(SmtEngine* parent);
- ~OptimizationSolver();
+ OptimizationSolver(SmtEngine* parent)
+ : d_parent(parent), d_objectives(), d_results()
+ {
+ }
+ ~OptimizationSolver() = default;
- /** 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
+ * Run the optimization loop for the pushed objective
+ * NOTE: this function currently supports only single objective
+ * for multiple pushed objectives it always optimizes the first one.
+ * Add support for multi-obj later
+ */
+ OptimizationResult::ResultType checkOpt();
+
+ /**
+ * Push an objective.
+ * @param target 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();
+ void pushObjective(TNode target,
+ OptimizationObjective::ObjectiveType type,
+ bool bvSigned = false);
+
+ /**
+ * Pop the most recent objective.
+ **/
+ void popObjective();
+
+ /**
+ * Returns the values of the optimized objective after checkOpt is called
+ * @return a vector of Optimization Result,
+ * each containing the outcome and the value.
+ **/
+ std::vector<OptimizationResult> getValues();
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;
+ std::vector<OptimizationObjective> d_objectives;
+
+ /** The results of the optimizations from the last checkOpt call **/
+ std::vector<OptimizationResult> d_results;
};
} // namespace smt
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index f94f37a19..2617472a2 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -54,19 +54,15 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
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);
+ d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::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;
+ ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
+ BitVector(32u, (uint32_t)0x3FFFFFA1));
+ d_optslv->popObjective();
}
TEST_F(TestTheoryWhiteBVOpt, signed_min)
@@ -79,22 +75,18 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
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);
+ d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, true);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
- BitVector val = d_optslv->objectiveGetValue().getConst<BitVector>();
+ BitVector val = d_optslv->getValues()[0].getValue().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;
+ ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000));
+ d_optslv->popObjective();
}
TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
@@ -110,20 +102,18 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
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);
+ d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, false);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
- BitVector val = d_optslv->objectiveGetValue().getConst<BitVector>();
+ BitVector val = d_optslv->getValues()[0].getValue().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;
+ ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
+ BitVector(32u, 2u));
+ d_optslv->popObjective();
}
TEST_F(TestTheoryWhiteBVOpt, signed_max)
@@ -137,18 +127,16 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
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);
+ d_optslv->pushObjective(x, OptimizationObjective::MAXIMIZE, true);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::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;
+ ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
+ BitVector(32u, 10u));
+ d_optslv->popObjective();
}
TEST_F(TestTheoryWhiteBVOpt, min_boundary)
@@ -163,17 +151,16 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
// that existed previously
d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
- d_optslv->activateObj(x, ObjectiveType::OBJECTIVE_MINIMIZE, false);
+ d_optslv->pushObjective(x, OptimizationObjective::MINIMIZE, false);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
// expect the maximum x = 18
- ASSERT_EQ(d_optslv->objectiveGetValue(),
- d_nodeManager->mkConst(BitVector(32u, 18u)));
- std::cout << "Optimized value is: " << d_optslv->objectiveGetValue()
- << std::endl;
+ ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
+ BitVector(32u, 18u));
+ d_optslv->popObjective();
}
} // namespace test
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index e8daef819..9d5c5c03f 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -58,21 +58,19 @@ TEST_F(TestTheoryWhiteIntOpt, max)
d_smtEngine->assertFormula(upb);
d_smtEngine->assertFormula(lowb);
- 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);
+ d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
// We expect max_cost == 99
- ASSERT_EQ(d_optslv->objectiveGetValue(),
- d_nodeManager->mkConst(Rational("99")));
+ ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
+ Rational("99"));
- std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue()
- << std::endl;
+ d_optslv->popObjective();
}
TEST_F(TestTheoryWhiteIntOpt, min)
@@ -92,21 +90,19 @@ TEST_F(TestTheoryWhiteIntOpt, min)
d_smtEngine->assertFormula(upb);
d_smtEngine->assertFormula(lowb);
- 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);
+ d_optslv->pushObjective(max_cost, OptimizationObjective::MINIMIZE);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::OPTIMAL);
// We expect max_cost == 99
- ASSERT_EQ(d_optslv->objectiveGetValue(),
- d_nodeManager->mkConst(Rational("1")));
+ ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
+ Rational("1"));
- std::cout << "Optimized max value is: " << d_optslv->objectiveGetValue()
- << std::endl;
+ d_optslv->popObjective();
}
TEST_F(TestTheoryWhiteIntOpt, result)
@@ -126,16 +122,16 @@ TEST_F(TestTheoryWhiteIntOpt, result)
d_smtEngine->assertFormula(upb);
d_smtEngine->assertFormula(lowb);
- 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);
+ d_optslv->pushObjective(max_cost, OptimizationObjective::MAXIMIZE);
// This should return OPT_UNSAT since 0 > x > 100 is impossible.
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
// We expect our check to have returned UNSAT
- ASSERT_EQ(r, OptResult::OPT_UNSAT);
+ ASSERT_EQ(r, OptimizationResult::UNSAT);
+ d_optslv->popObjective();
}
TEST_F(TestTheoryWhiteIntOpt, open_interval)
@@ -161,18 +157,16 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
*/
Node cost3 = d_nodeManager->mkNode(kind::PLUS, cost1, cost2);
- const ObjectiveType min_type = ObjectiveType::OBJECTIVE_MINIMIZE;
- d_optslv->activateObj(cost3, min_type);
+ d_optslv->pushObjective(cost3, OptimizationObjective::MINIMIZE);
- OptResult r = d_optslv->checkOpt();
+ OptimizationResult::ResultType r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+ ASSERT_EQ(r, OptimizationResult::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;
+ ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
+ Rational("112"));
+ d_optslv->popObjective();
}
} // namespace test
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback