summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-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
3 files changed, 39 insertions, 46 deletions
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