[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.

1 files changed, 10 insertions, 6 deletions

diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp
index 08f1809ec..2145492db 100644
--- a/src/omt/omt_optimizer.cpp
+++ b/src/omt/omt_optimizer.cpp
@@ -30,7 +30,7 @@ bool OMTOptimizer::nodeSupportsOptimization(TNode node)
 }
 
 std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
-    OptimizationObjective& objective)
+    const OptimizationObjective& objective)
 {
   // the datatype of the target node
   TypeNode objectiveType = objective.getTarget().getType(true);
@@ -53,7 +53,10 @@ std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
 }
 
 Node OMTOptimizer::mkStrongIncrementalExpression(
-    NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective)
+    NodeManager* nm,
+    TNode lhs,
+    TNode rhs,
+    const OptimizationObjective& objective)
 {
   constexpr const char lhsTypeError[] =
       "lhs type does not match or is not implicitly convertable to the target "
@@ -114,10 +117,11 @@ Node OMTOptimizer::mkStrongIncrementalExpression(
   Unreachable();
 }
 
-Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm,
-                                               TNode lhs,
-                                               TNode rhs,
-                                               OptimizationObjective& objective)
+Node OMTOptimizer::mkWeakIncrementalExpression(
+    NodeManager* nm,
+    TNode lhs,
+    TNode rhs,
+    const OptimizationObjective& objective)
 {
   constexpr const char lhsTypeError[] =
       "lhs type does not match or is not implicitly convertable to the target "