From 67a1510b8e6306993d7efb7671b8f0aa53a45deb Mon Sep 17 00:00:00 2001 From: Ouyancheng <1024842937@qq.com> Date: Fri, 30 Apr 2021 14:40:49 -0700 Subject: 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 --- test/unit/theory/theory_bv_opt_white.cpp | 75 +++++++++++++------------------ test/unit/theory/theory_int_opt_white.cpp | 50 +++++++++------------ 2 files changed, 53 insertions(+), 72 deletions(-) (limited to 'test/unit/theory') 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(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 val = d_optslv->getValues()[0].getValue().getConst(); 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 val = d_optslv->getValues()[0].getValue().getConst(); 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(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(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(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("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("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("112")); + d_optslv->popObjective(); } } // namespace test -- cgit v1.2.3