[Optimization] support for push/pop (#6706)

Use CDList for optimization objectives so that optimization solver supports push and pop (just use SmtEngine's push/pop).
SmtEngine::resetAssertions will also clears the optimization objectives, so no need to have the reset objectives function.

3 files changed, 73 insertions, 9 deletions

diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index 66efe7eff..c23ce79dd 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, (uint32_t)0x3FFFFFA1));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, signed_min)
@@ -87,7 +87,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
 
   // expect the minimum x = -1
   ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
@@ -114,7 +114,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 2u));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, signed_max)
@@ -137,7 +137,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
   // expect the maxmum x =
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 10u));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, min_boundary)
@@ -161,7 +161,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
   // expect the maximum x = 18
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 18u));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 }  // namespace test
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index f16db0c0e..cf0434ddc 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("99"));
 
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, min)
@@ -101,7 +101,7 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("1"));
 
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, result)
@@ -129,7 +129,7 @@ TEST_F(TestTheoryWhiteIntOpt, result)
 
   // We expect our check to have returned UNSAT
   ASSERT_EQ(r, OptimizationResult::UNSAT);
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, open_interval)
@@ -164,7 +164,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
   // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("112"));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 }  // namespace test
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index 1950d9ae2..73c6d9e7e 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -240,5 +240,69 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.size(), 0);
 }
 
+TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
+{
+  d_smtEngine->resetAssertions();
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+  Node y = d_nodeManager->mkVar(*d_BV32Type);
+  Node z = d_nodeManager->mkVar(*d_BV32Type);
+
+  // 18 <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(
+      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
+
+  // y <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+
+  // Lexico optimization
+  OptimizationSolver optSolver(d_smtEngine.get());
+
+  optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
+
+  // minimize x
+  optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
+
+  // push
+  d_smtEngine->push();
+
+  // maximize y with `signed` comparison over bit-vectors.
+  optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
+  // maximize z
+  optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
+
+  OptimizationResult::ResultType r = optSolver.checkOpt();
+
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+
+  std::vector<OptimizationResult> results = optSolver.getValues();
+
+  // x == 18
+  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // y == 18
+  ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // z == 0xFFFFFFFF
+  ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
+            BitVector(32u, (unsigned)0xFFFFFFFF));
+
+  // pop
+  d_smtEngine->pop();
+
+  // now we only have one objective: (minimize x)
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  results = optSolver.getValues();
+  ASSERT_EQ(results.size(), 1);
+  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // resetting the assertions also resets the optimization objectives
+  d_smtEngine->resetAssertions();
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  results = optSolver.getValues();
+  ASSERT_EQ(results.size(), 0);
+}
+
 }  // namespace test
 }  // namespace cvc5