diff options
author | mcjuneho <63680275+mcjuneho@users.noreply.github.com> | 2021-03-05 11:51:23 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-05 11:51:23 -0800 |
commit | ba90594ea59be5cfbcbfe81cf9510dab1efc3130 (patch) | |
tree | a2fb69e2356f91feb0faab800f19f2cb1babbb0b /test | |
parent | 4a72fbf9c96d5dda96cc2b198a4ef2e7c23c7b44 (diff) |
Initial implementation of an optimization solver with unit tests. (#5849)
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/theory/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/unit/theory/theory_int_opt_white.cpp | 126 |
2 files changed, 127 insertions, 0 deletions
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index f3c340a74..9a8bc4dee 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -21,6 +21,7 @@ cvc4_add_unit_test_white(theory_bags_type_rules_white theory) cvc4_add_unit_test_white(theory_bv_rewriter_white theory) cvc4_add_unit_test_white(theory_bv_white theory) cvc4_add_unit_test_white(theory_engine_white theory) +cvc4_add_unit_test_white(theory_int_opt_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory) cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory) cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory) diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp new file mode 100644 index 000000000..1e5c2c437 --- /dev/null +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -0,0 +1,126 @@ +#include <iostream> +#include "smt/optimization_solver.h" +#include "test_smt.h" + +namespace CVC4 { + +using namespace theory; +using namespace smt; + +namespace test { + +class TestTheoryWhiteIntOpt : public TestSmtNoFinishInit +{ + protected: + void SetUp() override + { + TestSmtNoFinishInit::SetUp(); + d_smtEngine->setOption("produce-assertions", "true"); + d_smtEngine->finishInit(); + + d_optslv.reset(new OptimizationSolver(d_smtEngine.get())); + d_intType.reset(new TypeNode(d_nodeManager->integerType())); + } + + std::unique_ptr<OptimizationSolver> d_optslv; + std::unique_ptr<TypeNode> d_intType; +}; + +TEST_F(TestTheoryWhiteIntOpt, max) +{ + Node ub = d_nodeManager->mkConst(Rational("100")); + Node lb = d_nodeManager->mkConst(Rational("0")); + + // Objectives to be optimized max_cost is max objective + Node max_cost = d_nodeManager->mkVar(*d_intType); + + Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost); + Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb); + + /* Result of asserts is: + 0 < max_cost < 100 + */ + d_smtEngine->assertFormula(upb); + d_smtEngine->assertFormula(lowb); + + const ObjectiveType max_type = OBJECTIVE_MAXIMIZE; + + // We activate our objective so the subsolver knows to optimize it + d_optslv->activateObj(max_cost, max_type); + + OptResult r = d_optslv->checkOpt(); + + // We expect max_cost == 99 + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(Rational("99"))); + + std::cout << "Result is :" << r << std::endl; + std::cout << "Optimized max value is: " + << d_optslv->objectiveGetValue() << std::endl; +} + +TEST_F(TestTheoryWhiteIntOpt, min) +{ + Node ub = d_nodeManager->mkConst(Rational("100")); + Node lb = d_nodeManager->mkConst(Rational("0")); + + // Objectives to be optimized max_cost is max objective + Node max_cost = d_nodeManager->mkVar(*d_intType); + + Node upb = d_nodeManager->mkNode(kind::GT, ub, max_cost); + Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, lb); + + /* Result of asserts is: + 0 < max_cost < 100 + */ + d_smtEngine->assertFormula(upb); + d_smtEngine->assertFormula(lowb); + + const ObjectiveType min_type = OBJECTIVE_MINIMIZE; + + // We activate our objective so the subsolver knows to optimize it + d_optslv->activateObj(max_cost, min_type); + + OptResult r = d_optslv->checkOpt(); + + // We expect max_cost == 99 + ASSERT_EQ(d_optslv->objectiveGetValue(), + d_nodeManager->mkConst(Rational("1"))); + + std::cout << "Result is :" << r << std::endl; + std::cout << "Optimized max value is: " + << d_optslv->objectiveGetValue() << std::endl; +} + +TEST_F(TestTheoryWhiteIntOpt, result) +{ + Node ub = d_nodeManager->mkConst(Rational("100")); + Node lb = d_nodeManager->mkConst(Rational("0")); + + // Objectives to be optimized max_cost is max objective + Node max_cost = d_nodeManager->mkVar(*d_intType); + + Node upb = d_nodeManager->mkNode(kind::GT, lb, max_cost); + Node lowb = d_nodeManager->mkNode(kind::GT, max_cost, ub); + + /* Result of asserts is: + 0 > max_cost > 100 + */ + d_smtEngine->assertFormula(upb); + d_smtEngine->assertFormula(lowb); + + const ObjectiveType max_type = OBJECTIVE_MAXIMIZE; + + // We activate our objective so the subsolver knows to optimize it + d_optslv->activateObj(max_cost, max_type); + + // This should return OPT_UNSAT since 0 > x > 100 is impossible. + OptResult r = d_optslv->checkOpt(); + + // We expect our check to have returned UNSAT + ASSERT_EQ(r, OPT_UNSAT); + + std::cout << "Result is :" << r << std::endl; +} +} // namespace test +} // namespace CVC4 |