Initial implementation of an optimization solver with unit tests. (#5849)

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