summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/omt/bitvector_optimizer.cpp128
-rw-r--r--src/omt/integer_optimizer.cpp13
-rw-r--r--src/smt/optimization_solver.cpp91
-rw-r--r--src/smt/optimization_solver.h121
-rw-r--r--test/unit/theory/theory_bv_opt_white.cpp20
-rw-r--r--test/unit/theory/theory_int_opt_white.cpp16
-rw-r--r--test/unit/theory/theory_opt_multigoal_white.cpp49
7 files changed, 214 insertions, 224 deletions
diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp
index bce6c9b6d..01cb6da42 100644
--- a/src/omt/bitvector_optimizer.cpp
+++ b/src/omt/bitvector_optimizer.cpp
@@ -53,15 +53,13 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
Result intermediateSatResult = optChecker->checkSat();
// Model-value of objective (used in optimization loop)
Node value;
- if (intermediateSatResult.isUnknown())
+ if (intermediateSatResult.isUnknown()
+ || intermediateSatResult.isSat() == Result::UNSAT)
{
- return OptimizationResult(OptimizationResult::UNKNOWN, value);
+ return OptimizationResult(intermediateSatResult, value);
}
- if (intermediateSatResult.isSat() == Result::UNSAT)
- {
- return OptimizationResult(OptimizationResult::UNSAT, value);
- }
-
+ // the last result that is SAT
+ Result lastSatResult = intermediateSatResult;
// value equals to upperBound
value = optChecker->getValue(target);
@@ -104,39 +102,35 @@ OptimizationResult OMTOptimizerBitVector::minimize(SmtEngine* optChecker,
nm->mkNode(LTOperator, target, nm->mkConst(pivot))));
}
intermediateSatResult = optChecker->checkSat();
- if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
- {
- optChecker->pop();
- return OptimizationResult(OptimizationResult::UNKNOWN, value);
- }
- if (intermediateSatResult.isSat() == Result::SAT)
+ switch (intermediateSatResult.isSat())
{
- 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
+ case Result::SAT_UNKNOWN:
optChecker->pop();
- return OptimizationResult(OptimizationResult::OPTIMAL, value);
- }
- else
- {
- lowerBound = pivot;
- }
- }
- else
- {
- optChecker->pop();
- return OptimizationResult(OptimizationResult::UNKNOWN, value);
+ return OptimizationResult(intermediateSatResult, value);
+ case Result::SAT:
+ lastSatResult = intermediateSatResult;
+ value = optChecker->getValue(target);
+ upperBound = value.getConst<BitVector>();
+ break;
+ case Result::UNSAT:
+ if (lowerBound == pivot)
+ {
+ // lowerBound == pivot ==> upperbound = lowerbound + 1
+ // and lowerbound <= target < upperbound is UNSAT
+ // return the upperbound
+ optChecker->pop();
+ return OptimizationResult(lastSatResult, value);
+ }
+ else
+ {
+ lowerBound = pivot;
+ }
+ break;
+ default: Unreachable();
}
optChecker->pop();
}
- return OptimizationResult(OptimizationResult::OPTIMAL, value);
+ return OptimizationResult(lastSatResult, value);
}
OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
@@ -148,15 +142,13 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
Result intermediateSatResult = optChecker->checkSat();
// Model-value of objective (used in optimization loop)
Node value;
- if (intermediateSatResult.isUnknown())
+ if (intermediateSatResult.isUnknown()
+ || intermediateSatResult.isSat() == Result::UNSAT)
{
- return OptimizationResult(OptimizationResult::UNKNOWN, value);
+ return OptimizationResult(intermediateSatResult, value);
}
- if (intermediateSatResult.isSat() == Result::UNSAT)
- {
- return OptimizationResult(OptimizationResult::UNSAT, value);
- }
-
+ // the last result that is SAT
+ Result lastSatResult = intermediateSatResult;
// value equals to upperBound
value = optChecker->getValue(target);
@@ -196,39 +188,35 @@ OptimizationResult OMTOptimizerBitVector::maximize(SmtEngine* optChecker,
nm->mkNode(GTOperator, target, nm->mkConst(pivot)),
nm->mkNode(LEOperator, target, nm->mkConst(upperBound))));
intermediateSatResult = optChecker->checkSat();
- if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull())
- {
- optChecker->pop();
- return OptimizationResult(OptimizationResult::UNKNOWN, value);
- }
- if (intermediateSatResult.isSat() == Result::SAT)
+ switch (intermediateSatResult.isSat())
{
- 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
+ case Result::SAT_UNKNOWN:
optChecker->pop();
- return OptimizationResult(OptimizationResult::OPTIMAL, value);
- }
- else
- {
- upperBound = pivot;
- }
- }
- else
- {
- optChecker->pop();
- return OptimizationResult(OptimizationResult::UNKNOWN, value);
+ return OptimizationResult(intermediateSatResult, value);
+ case Result::SAT:
+ lastSatResult = intermediateSatResult;
+ value = optChecker->getValue(target);
+ lowerBound = value.getConst<BitVector>();
+ break;
+ case Result::UNSAT:
+ if (lowerBound == pivot)
+ {
+ // upperbound = lowerbound + 1
+ // and lowerbound < target <= upperbound is UNSAT
+ // return the lowerbound
+ optChecker->pop();
+ return OptimizationResult(lastSatResult, value);
+ }
+ else
+ {
+ upperBound = pivot;
+ }
+ break;
+ default: Unreachable();
}
optChecker->pop();
}
- return OptimizationResult(OptimizationResult::OPTIMAL, value);
+ return OptimizationResult(lastSatResult, value);
}
} // namespace cvc5::omt
diff --git a/src/omt/integer_optimizer.cpp b/src/omt/integer_optimizer.cpp
index 045268337..379b0cd43 100644
--- a/src/omt/integer_optimizer.cpp
+++ b/src/omt/integer_optimizer.cpp
@@ -33,13 +33,10 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
Result intermediateSatResult = optChecker->checkSat();
// Model-value of objective (used in optimization loop)
Node value;
- if (intermediateSatResult.isUnknown())
+ if (intermediateSatResult.isUnknown()
+ || intermediateSatResult.isSat() == Result::UNSAT)
{
- return OptimizationResult(OptimizationResult::UNKNOWN, value);
- }
- if (intermediateSatResult.isSat() == Result::UNSAT)
- {
- return OptimizationResult(OptimizationResult::UNSAT, value);
+ return OptimizationResult(intermediateSatResult, value);
}
// node storing target > old_value (used in optimization loop)
Node increment;
@@ -56,12 +53,14 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
// then assert optimization_target > current_model_value
incrementalOperator = kind::GT;
}
+ Result lastSatResult = intermediateSatResult;
// 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)
{
+ lastSatResult = intermediateSatResult;
value = optChecker->getValue(target);
Assert(!value.isNull());
increment = nm->mkNode(incrementalOperator, target, value);
@@ -69,7 +68,7 @@ OptimizationResult OMTOptimizerInteger::optimize(SmtEngine* optChecker,
intermediateSatResult = optChecker->checkSat();
}
optChecker->pop();
- return OptimizationResult(OptimizationResult::OPTIMAL, value);
+ return OptimizationResult(lastSatResult, value);
}
OptimizationResult OMTOptimizerInteger::minimize(SmtEngine* optChecker,
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index e85ea82ef..a46452004 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -32,12 +32,11 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent)
: d_parent(parent),
d_optChecker(),
d_objectives(parent->getUserContext()),
- d_results(),
- d_objectiveCombination(LEXICOGRAPHIC)
+ d_results()
{
}
-OptimizationResult::ResultType OptimizationSolver::checkOpt()
+Result OptimizationSolver::checkOpt(ObjectiveCombination combination)
{
// if the results of the previous call have different size than the
// objectives, then we should clear the pareto optimization context
@@ -48,7 +47,7 @@ OptimizationResult::ResultType OptimizationSolver::checkOpt()
{
d_results.emplace_back();
}
- switch (d_objectiveCombination)
+ switch (combination)
{
case BOX: return optimizeBox(); break;
case LEXICOGRAPHIC: return optimizeLexicographicIterative(); break;
@@ -76,16 +75,9 @@ void OptimizationSolver::addObjective(TNode target,
std::vector<OptimizationResult> OptimizationSolver::getValues()
{
- Assert(d_objectives.size() == d_results.size());
return d_results;
}
-void OptimizationSolver::setObjectiveCombination(
- ObjectiveCombination combination)
-{
- d_objectiveCombination = combination;
-}
-
std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
SmtEngine* parentSMTSolver, bool needsTimeout, unsigned long timeout)
{
@@ -106,13 +98,12 @@ std::unique_ptr<SmtEngine> OptimizationSolver::createOptCheckerWithTimeout(
return optChecker;
}
-OptimizationResult::ResultType OptimizationSolver::optimizeBox()
+Result OptimizationSolver::optimizeBox()
{
// resets the optChecker
d_optChecker = createOptCheckerWithTimeout(d_parent);
OptimizationResult partialResult;
- OptimizationResult::ResultType aggregatedResultType =
- OptimizationResult::OPTIMAL;
+ Result aggregatedResult(Result::Sat::SAT);
std::unique_ptr<OMTOptimizer> optimizer;
for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
{
@@ -134,18 +125,19 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox()
}
// match the optimization result type, and aggregate the results of
// subproblems
- switch (partialResult.getType())
+ switch (partialResult.getResult().isSat())
{
- case OptimizationResult::OPTIMAL: break;
- case OptimizationResult::UNBOUNDED: break;
- case OptimizationResult::UNSAT:
- if (aggregatedResultType == OptimizationResult::OPTIMAL)
+ case Result::SAT: break;
+ case Result::UNSAT:
+ // the assertions are unsatisfiable
+ for (size_t j = 0; j < numObj; ++j)
{
- aggregatedResultType = OptimizationResult::UNSAT;
+ d_results[j] = partialResult;
}
- break;
- case OptimizationResult::UNKNOWN:
- aggregatedResultType = OptimizationResult::UNKNOWN;
+ d_optChecker.reset();
+ return partialResult.getResult();
+ case Result::SAT_UNKNOWN:
+ aggregatedResult = partialResult.getResult();
break;
default: Unreachable();
}
@@ -154,15 +146,20 @@ OptimizationResult::ResultType OptimizationSolver::optimizeBox()
}
// kill optChecker after optimization ends
d_optChecker.reset();
- return aggregatedResultType;
+ return aggregatedResult;
}
-OptimizationResult::ResultType
-OptimizationSolver::optimizeLexicographicIterative()
+Result OptimizationSolver::optimizeLexicographicIterative()
{
// resets the optChecker
d_optChecker = createOptCheckerWithTimeout(d_parent);
- OptimizationResult partialResult;
+ // partialResult defaults to SAT if no objective is present
+ // NOTE: the parenthesis around Result(Result::SAT) is required,
+ // otherwise the compiler will report "parameter declarator cannot be
+ // qualified". For more details:
+ // https://stackoverflow.com/questions/44045257/c-compiler-error-c2751-what-exactly-causes-it
+ // https://en.wikipedia.org/wiki/Most_vexing_parse
+ OptimizationResult partialResult((Result(Result::SAT)), TNode());
std::unique_ptr<OMTOptimizer> optimizer;
for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
{
@@ -186,26 +183,33 @@ OptimizationSolver::optimizeLexicographicIterative()
d_results[i] = partialResult;
// checks the optimization result of the current objective
- switch (partialResult.getType())
+ switch (partialResult.getResult().isSat())
{
- case OptimizationResult::OPTIMAL:
+ case Result::SAT:
// assert target[i] == value[i] and proceed
d_optChecker->assertFormula(d_optChecker->getNodeManager()->mkNode(
kind::EQUAL, d_objectives[i].getTarget(), d_results[i].getValue()));
break;
- case OptimizationResult::UNBOUNDED: return OptimizationResult::UNBOUNDED;
- case OptimizationResult::UNSAT: return OptimizationResult::UNSAT;
- case OptimizationResult::UNKNOWN: return OptimizationResult::UNKNOWN;
+ case Result::UNSAT:
+ d_optChecker.reset();
+ return partialResult.getResult();
+ case Result::SAT_UNKNOWN:
+ d_optChecker.reset();
+ return partialResult.getResult();
default: Unreachable();
}
+
+ // if the result for the current objective is unbounded
+ // then just stop
+ if (partialResult.isUnbounded()) break;
}
// kill optChecker in case pareto misuses it
d_optChecker.reset();
- // now all objectives are OPTIMAL, just return OPTIMAL as overall result
- return OptimizationResult::OPTIMAL;
+ // now all objectives are optimal, just return SAT as the overall result
+ return partialResult.getResult();
}
-OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
+Result OptimizationSolver::optimizeParetoNaiveGIA()
{
// initial call to Pareto optimizer, create the checker
if (!d_optChecker) d_optChecker = createOptCheckerWithTimeout(d_parent);
@@ -216,8 +220,8 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
switch (satResult.isSat())
{
- case Result::Sat::UNSAT: return OptimizationResult::UNSAT;
- case Result::Sat::SAT_UNKNOWN: return OptimizationResult::UNKNOWN;
+ case Result::Sat::UNSAT: return satResult;
+ case Result::Sat::SAT_UNKNOWN: return satResult;
case Result::Sat::SAT:
{
// if satisfied, use d_results to store the initial results
@@ -226,14 +230,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
{
d_results[i] = OptimizationResult(
- OptimizationResult::OPTIMAL,
- d_optChecker->getValue(d_objectives[i].getTarget()));
+ satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
}
break;
}
default: Unreachable();
}
+ Result lastSatResult = satResult;
+
// a vector storing assertions saying that no objective is worse
std::vector<Node> noWorseObj;
// a vector storing assertions saying that there is at least one objective
@@ -278,15 +283,15 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
case Result::Sat::SAT_UNKNOWN:
// if result is UNKNOWN, abort the current session and return UNKNOWN
d_optChecker.reset();
- return OptimizationResult::UNKNOWN;
+ return satResult;
case Result::Sat::SAT:
{
+ lastSatResult = satResult;
// if result is SAT, update d_results to the more optimal values
for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
{
d_results[i] = OptimizationResult(
- OptimizationResult::OPTIMAL,
- d_optChecker->getValue(d_objectives[i].getTarget()));
+ satResult, d_optChecker->getValue(d_objectives[i].getTarget()));
}
break;
}
@@ -302,7 +307,7 @@ OptimizationResult::ResultType OptimizationSolver::optimizeParetoNaiveGIA()
// for the next run.
d_optChecker->assertFormula(nm->mkOr(someObjBetter));
- return OptimizationResult::OPTIMAL;
+ return lastSatResult;
}
} // namespace smt
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 6d138deb2..d13168780 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -33,63 +33,75 @@ namespace smt {
/**
* 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
+ * - the optimization result: SAT/UNSAT/UNKNOWN
+ * - the optimal value if SAT and bounded
+ * (optimal value reached and it's not infinity),
+ * or an empty node if SAT and unbounded
+ * (optimal value is +inf for maximum or -inf for minimum),
+ * otherwise the value might be empty node
+ * or something suboptimal
+ * - whether the objective is unbounded
*/
class OptimizationResult
{
public:
/**
- * Enum indicating whether the checkOpt result
- * is optimal or not.
- **/
- enum ResultType
- {
- // 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,
- };
-
- /**
* Constructor
* @param type the optimization outcome
* @param value the optimized value
+ * @param unbounded whether the objective is unbounded
**/
- OptimizationResult(ResultType type, TNode value)
- : d_type(type), d_value(value)
+ OptimizationResult(Result result, TNode value, bool unbounded = false)
+ : d_result(result), d_value(value), d_unbounded(unbounded)
+ {
+ }
+ OptimizationResult()
+ : d_result(Result::Sat::SAT_UNKNOWN,
+ Result::UnknownExplanation::NO_STATUS),
+ d_value(),
+ d_unbounded(false)
{
}
- OptimizationResult() : d_type(UNKNOWN), d_value() {}
~OptimizationResult() = default;
/**
* Returns an enum indicating whether
- * the result is optimal or not.
- * @return an enum showing whether the result is optimal, unbounded,
- * unsat or unknown.
+ * the result is SAT or not.
+ * @return whether the result is SAT, UNSAT or SAT_UNKNOWN
**/
- ResultType getType() const { return d_type; }
+ Result getResult() const { return d_result; }
+
/**
* 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
+ * if result is unbounded, this will be an empty node,
+ * if getResult() is UNSAT, it will return an empty node,
+ * if getResult() is SAT_UNKNOWN, it will return something suboptimal
+ * or an empty node, depending on how the solver runs.
**/
Node getValue() const { return d_value; }
+ /**
+ * Checks whether the objective is unbouned
+ * @return whether the objective is unbounded
+ * if the objective is unbounded (this function returns true),
+ * then the optimal value is:
+ * +inf, if it's maximize;
+ * -inf, if it's minimize
+ **/
+ bool isUnbounded() const { return d_unbounded; }
+
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 **/
+ /** indicating whether the result is SAT, UNSAT or UNKNOWN **/
+ Result d_result;
+ /** if the result is bounded, this is storing the value **/
Node d_value;
+ /** whether the objective is unbounded
+ * If this is true, then:
+ * if objective is maximize, it's +infinity;
+ * if objective is minimize, it's -infinity
+ **/
+ bool d_unbounded;
};
/**
@@ -199,10 +211,10 @@ class OptimizationSolver
/**
* Run the optimization loop for the added objective
* For multiple objective combination, it defaults to lexicographic,
- * and combination could be set by calling
- * setObjectiveCombination(BOX/LEXICOGRAPHIC/PARETO)
+ * possible combinations: BOX, LEXICOGRAPHIC, PARETO
+ * @param combination BOX / LEXICOGRAPHIC / PARETO
*/
- OptimizationResult::ResultType checkOpt();
+ Result checkOpt(ObjectiveCombination combination = LEXICOGRAPHIC);
/**
* Add an optimization objective.
@@ -223,11 +235,6 @@ class OptimizationSolver
**/
std::vector<OptimizationResult> getValues();
- /**
- * Sets the objective combination
- **/
- void setObjectiveCombination(ObjectiveCombination combination);
-
private:
/**
* Initialize an SMT subsolver for offline optimization purpose
@@ -244,26 +251,26 @@ class OptimizationSolver
/**
* Optimize multiple goals in Box order
- * @return OPTIMAL if all of the objectives are either OPTIMAL or UNBOUNDED;
- * UNSAT if at least one objective is UNSAT and no objective is UNKNOWN;
- * UNKNOWN if any of the objective is UNKNOWN.
+ * @return SAT if all of the objectives are optimal or unbounded;
+ * UNSAT if at least one objective is UNSAT and no objective is SAT_UNKNOWN;
+ * SAT_UNKNOWN if any of the objective is SAT_UNKNOWN.
**/
- OptimizationResult::ResultType optimizeBox();
+ Result optimizeBox();
/**
* Optimize multiple goals in Lexicographic order,
* using iterative implementation
- * @return OPTIMAL if all objectives are OPTIMAL and bounded;
- * UNBOUNDED if one of the objectives is UNBOUNDED
+ * @return SAT if the objectives are optimal,
+ * if one of the objectives is unbounded,
+ * the optimization will stop at that objective;
+ * UNSAT if any of the objectives is UNSAT
* and optimization will stop at that objective;
- * UNSAT if one of the objectives is UNSAT
- * and optimization will stop at that objective;
- * UNKNOWN if one of the objectives is UNKNOWN
+ * SAT_UNKNOWN if any of the objectives is UNKNOWN
* and optimization will stop at that objective;
* If the optimization is stopped at an objective,
- * all objectives following that objective will be UNKNOWN.
+ * all objectives following that objective will be SAT_UNKNOWN.
**/
- OptimizationResult::ResultType optimizeLexicographicIterative();
+ Result optimizeLexicographicIterative();
/**
* Optimize multiple goals in Pareto order
@@ -277,11 +284,12 @@ class OptimizationSolver
* D. Rayside, H.-C. Estler, and D. Jackson. The Guided Improvement Algorithm.
* Technical Report MIT-CSAIL-TR-2009-033, MIT, 2009.
*
- * @return if it finds a new Pareto optimal result it will return OPTIMAL;
+ * @return if it finds a new Pareto optimal result it will return SAT;
* if it exhausts the results in the Pareto front it will return UNSAT;
- * if the underlying SMT solver returns UNKNOWN, it will return UNKNOWN.
+ * if the underlying SMT solver returns SAT_UNKNOWN,
+ * it will return SAT_UNKNOWN.
**/
- OptimizationResult::ResultType optimizeParetoNaiveGIA();
+ Result optimizeParetoNaiveGIA();
/** A pointer to the parent SMT engine **/
SmtEngine* d_parent;
@@ -294,9 +302,6 @@ class OptimizationSolver
/** The results of the optimizations from the last checkOpt call **/
std::vector<OptimizationResult> d_results;
-
- /** The current objective combination method **/
- ObjectiveCombination d_objectiveCombination;
};
} // namespace smt
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index c23ce79dd..5cd29878e 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -57,9 +57,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
BitVector(32u, (uint32_t)0x3FFFFFA1));
@@ -78,9 +78,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, true);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
std::cout << "opt value is: " << val << std::endl;
@@ -105,9 +105,9 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, false);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
BitVector val = d_optslv->getValues()[0].getValue().getConst<BitVector>();
std::cout << "opt value is: " << val << std::endl;
@@ -130,9 +130,9 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
d_optslv->addObjective(x, OptimizationObjective::MAXIMIZE, true);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
// expect the maxmum x =
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
@@ -154,9 +154,9 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
d_optslv->addObjective(x, OptimizationObjective::MINIMIZE, false);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
// expect the maximum x = 18
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index cf0434ddc..583f908e7 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -62,9 +62,9 @@ TEST_F(TestTheoryWhiteIntOpt, max)
// We activate our objective so the subsolver knows to optimize it
d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
// We expect max_cost == 99
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
@@ -93,9 +93,9 @@ TEST_F(TestTheoryWhiteIntOpt, min)
// We activate our objective so the subsolver knows to optimize it
d_optslv->addObjective(max_cost, OptimizationObjective::MINIMIZE);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
// We expect max_cost == 99
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
@@ -125,10 +125,10 @@ TEST_F(TestTheoryWhiteIntOpt, result)
d_optslv->addObjective(max_cost, OptimizationObjective::MAXIMIZE);
// This should return OPT_UNSAT since 0 > x > 100 is impossible.
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
// We expect our check to have returned UNSAT
- ASSERT_EQ(r, OptimizationResult::UNSAT);
+ ASSERT_EQ(r.isSat(), Result::UNSAT);
d_smtEngine->resetAssertions();
}
@@ -157,9 +157,9 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
d_optslv->addObjective(cost3, OptimizationObjective::MINIMIZE);
- OptimizationResult::ResultType r = d_optslv->checkOpt();
+ Result r = d_optslv->checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
// expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index 73c6d9e7e..9a091fb3b 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -54,11 +54,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
// y <= x
d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
- // Box optimization
OptimizationSolver optSolver(d_smtEngine.get());
- optSolver.setObjectiveCombination(OptimizationSolver::BOX);
-
// minimize x
optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
// maximize y with `signed` comparison over bit-vectors.
@@ -66,9 +63,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, box)
// maximize z
optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
- OptimizationResult::ResultType r = optSolver.checkOpt();
+ // Box optimization
+ Result r = optSolver.checkOpt(OptimizationSolver::BOX);
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
@@ -100,8 +98,6 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex)
OptimizationSolver optSolver(d_smtEngine.get());
- optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
-
// minimize x
optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
// maximize y with `signed` comparison over bit-vectors.
@@ -109,9 +105,9 @@ TEST_F(TestTheoryWhiteOptMultigoal, lex)
// maximize z
optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
- OptimizationResult::ResultType r = optSolver.checkOpt();
+ Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
@@ -180,18 +176,17 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
(maximize b)
*/
OptimizationSolver optSolver(d_smtEngine.get());
- optSolver.setObjectiveCombination(OptimizationSolver::PARETO);
optSolver.addObjective(a, OptimizationObjective::MAXIMIZE);
optSolver.addObjective(b, OptimizationObjective::MAXIMIZE);
- OptimizationResult::ResultType r;
+ Result r;
// all possible result pairs <a, b>
std::set<std::pair<uint32_t, uint32_t>> possibleResults = {
{1, 3}, {2, 2}, {3, 1}};
- r = optSolver.checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ r = optSolver.checkOpt(OptimizationSolver::PARETO);
+ ASSERT_EQ(r.isSat(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
std::pair<uint32_t, uint32_t> res = {
results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -205,8 +200,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
ASSERT_EQ(possibleResults.count(res), 1);
possibleResults.erase(res);
- r = optSolver.checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ r = optSolver.checkOpt(OptimizationSolver::PARETO);
+ ASSERT_EQ(r.isSat(), Result::SAT);
results = optSolver.getValues();
res = {
results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -220,8 +215,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
ASSERT_EQ(possibleResults.count(res), 1);
possibleResults.erase(res);
- r = optSolver.checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ r = optSolver.checkOpt(OptimizationSolver::PARETO);
+ ASSERT_EQ(r.isSat(), Result::SAT);
results = optSolver.getValues();
res = {
results[0].getValue().getConst<BitVector>().toInteger().toUnsignedInt(),
@@ -235,8 +230,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
ASSERT_EQ(possibleResults.count(res), 1);
possibleResults.erase(res);
- r = optSolver.checkOpt();
- ASSERT_EQ(r, OptimizationResult::UNSAT);
+ r = optSolver.checkOpt(OptimizationSolver::PARETO);
+ ASSERT_EQ(r.isSat(), Result::UNSAT);
ASSERT_EQ(possibleResults.size(), 0);
}
@@ -254,11 +249,8 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
// y <= x
d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
- // Lexico optimization
OptimizationSolver optSolver(d_smtEngine.get());
- optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
-
// minimize x
optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
@@ -270,9 +262,10 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
// maximize z
optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
- OptimizationResult::ResultType r = optSolver.checkOpt();
+ // Lexico optimization
+ Result r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ ASSERT_EQ(r.isSat(), Result::SAT);
std::vector<OptimizationResult> results = optSolver.getValues();
@@ -290,16 +283,16 @@ TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
d_smtEngine->pop();
// now we only have one objective: (minimize x)
- r = optSolver.checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
+ ASSERT_EQ(r.isSat(), Result::SAT);
results = optSolver.getValues();
ASSERT_EQ(results.size(), 1);
ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
// resetting the assertions also resets the optimization objectives
d_smtEngine->resetAssertions();
- r = optSolver.checkOpt();
- ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+ r = optSolver.checkOpt(OptimizationSolver::LEXICOGRAPHIC);
+ ASSERT_EQ(r.isSat(), Result::SAT);
results = optSolver.getValues();
ASSERT_EQ(results.size(), 0);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback