From c299e8661f24d3a6acb736e9e5df1b1920488ac3 Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Tue, 15 Jun 2021 16:20:20 -0700 Subject: [Optimization] Use Result in OptimizationResult (#6740) OptimizationResult now contains: - cvc5::Result - optimal value for objective - whether the objective is unbounded This gets benefit from cvc5::Result (e.g., we could get explanation for UNKNOWN) and it's slightly easier to integrate to the current API. Also refactors BV optimizer so that it uses switch statement (instead of if-then-else) to judge the checkSat results (I was planning to do this a long while ago)... --- test/unit/theory/theory_bv_opt_white.cpp | 20 +++++----- test/unit/theory/theory_int_opt_white.cpp | 16 ++++---- test/unit/theory/theory_opt_multigoal_white.cpp | 49 +++++++++++-------------- 3 files changed, 39 insertions(+), 46 deletions(-) (limited to 'test') 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(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(); 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(); 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(), @@ -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(), 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(), @@ -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(), @@ -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(), 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 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 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 std::set> 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 results = optSolver.getValues(); std::pair res = { results[0].getValue().getConst().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().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().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 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(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); } -- cgit v1.2.3