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

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