diff options
author | Ouyancheng <1024842937@qq.com> | 2021-04-30 14:40:49 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-30 14:40:49 -0700 |
commit | 67a1510b8e6306993d7efb7671b8f0aa53a45deb (patch) | |
tree | 39745800f0d4ecdbb286516be26cd971db53cfd9 /test | |
parent | 327a24508ed1d02a3fa233e680ffd0b30aa685a9 (diff) |
Refactor optimization result and objective classes + add preliminary support for multiple objectives (#6459)
This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.
* Refactor optimization result and objective classes
* Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/theory_bv_opt_white.cpp | 75 | ||||
-rw-r--r-- | test/unit/theory/theory_int_opt_white.cpp | 50 |
2 files changed, 53 insertions, 72 deletions
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 |