[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, 9 insertions, 11 deletions

diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index ffc49710a..e85ea82ef 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -15,6 +15,8 @@
 
 #include "smt/optimization_solver.h"
 
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
 #include "omt/omt_optimizer.h"
 #include "options/smt_options.h"
 #include "smt/assertions.h"
@@ -29,7 +31,7 @@ namespace smt {
 OptimizationSolver::OptimizationSolver(SmtEngine* parent)
     : d_parent(parent),
       d_optChecker(),
-      d_objectives(),
+      d_objectives(parent->getUserContext()),
       d_results(),
       d_objectiveCombination(LEXICOGRAPHIC)
 {
@@ -37,10 +39,14 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent)
 
 OptimizationResult::ResultType OptimizationSolver::checkOpt()
 {
+  // if the results of the previous call have different size than the
+  // objectives, then we should clear the pareto optimization context
+  if (d_results.size() != d_objectives.size()) d_optChecker.reset();
+  // initialize the result vector
+  d_results.clear();
   for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
   {
-    // reset the optimization results
-    d_results[i] = OptimizationResult();
+    d_results.emplace_back();
   }
   switch (d_objectiveCombination)
   {
@@ -66,14 +72,6 @@ void OptimizationSolver::addObjective(TNode target,
   }
   d_optChecker.reset();
   d_objectives.emplace_back(target, type, bvSigned);
-  d_results.emplace_back(OptimizationResult::UNKNOWN, Node());
-}
-
-void OptimizationSolver::resetObjectives()
-{
-  d_optChecker.reset();
-  d_objectives.clear();
-  d_results.clear();
 }
 
 std::vector<OptimizationResult> OptimizationSolver::getValues()