4 files changed, 30 insertions, 23 deletions

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 1381ef87c..b6cdfb67b 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -43,6 +43,7 @@ Env::Env(NodeManager* nm, Options* opts)
       d_logic(),
       d_statisticsRegistry(std::make_unique<StatisticsRegistry>()),
       d_options(),
+      d_originalOptions(opts),
       d_resourceManager()
 {
   if (opts != nullptr)
@@ -97,6 +98,8 @@ StatisticsRegistry& Env::getStatisticsRegistry()
 
 const Options& Env::getOptions() const { return d_options; }
 
+const Options& Env::getOriginalOptions() const { return *d_originalOptions; }
+
 ResourceManager* Env::getResourceManager() const
 {
   return d_resourceManager.get();
diff --git a/src/smt/env.h b/src/smt/env.h
index 29a360209..57b5ad9c7 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -94,6 +94,9 @@ class Env
   /** Get the options object (const version only) owned by this Env. */
   const Options& getOptions() const;
 
+  /** Get the original options object (const version only). */
+  const Options& getOriginalOptions() const;
+
   /** Get the resource manager owned by this Env. */
   ResourceManager* getResourceManager() const;
 
@@ -180,6 +183,12 @@ class Env
    * consider during solving and initialization.
    */
   Options d_options;
+  /**
+   * A pointer to the original options object as stored in the api::Solver.
+   * The referenced objects holds the options as initially parsed before being
+   * changed, e.g., by setDefaults().
+   */
+  const Options* d_originalOptions;
   /** Manager for limiting time and abstract resource usage. */
   std::unique_ptr<ResourceManager> d_resourceManager;
 }; /* class Env */
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()
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 64591d8f1..6d138deb2 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -18,6 +18,8 @@
 #ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
 #define CVC5__SMT__OPTIMIZATION_SOLVER_H
 
+#include "context/cdhashmap_forward.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "util/result.h"
@@ -74,14 +76,14 @@ class OptimizationResult
    * @return an enum showing whether the result is optimal, unbounded,
    *   unsat or unknown.
    **/
-  ResultType getType() { return d_type; }
+  ResultType getType() const { return d_type; }
   /**
    * Returns the optimal value.
    * @return Node containing the optimal value,
    *   if getType() is not OPTIMAL, it might return an empty node or a node
    *   containing non-optimal value
    **/
-  Node getValue() { return d_value; }
+  Node getValue() const { return d_value; }
 
  private:
   /** the indicating whether the result is optimal or something else **/
@@ -124,13 +126,13 @@ class OptimizationObjective
   ~OptimizationObjective() = default;
 
   /** A getter for d_type **/
-  ObjectiveType getType() { return d_type; }
+  ObjectiveType getType() const { return d_type; }
 
   /** A getter for d_target **/
-  Node getTarget() { return d_target; }
+  Node getTarget() const { return d_target; }
 
   /** A getter for d_bvSigned **/
-  bool bvIsSigned() { return d_bvSigned; }
+  bool bvIsSigned() const { return d_bvSigned; }
 
  private:
   /**
@@ -173,7 +175,7 @@ class OptimizationSolver
    *
    * Lexicographic: optimize the objectives one-by-one, in the order they are
    * added:
-   *   v_x = max(x) s.t. phi(x, y) = sat 
+   *   v_x = max(x) s.t. phi(x, y) = sat
    *   v_y = max(y) s.t. phi(v_x, y) = sat
    *
    * Pareto: optimize multiple goals to a state such that
@@ -215,11 +217,6 @@ class OptimizationSolver
                     bool bvSigned = false);
 
   /**
-   * Clear all the added optimization objectives
-   **/
-  void resetObjectives();
-
-  /**
    * Returns the values of the optimized objective after checkOpt is called
    * @return a vector of Optimization Result,
    *   each containing the outcome and the value.
@@ -293,7 +290,7 @@ class OptimizationSolver
   std::unique_ptr<SmtEngine> d_optChecker;
 
   /** The objectives to optimize for **/
-  std::vector<OptimizationObjective> d_objectives;
+  context::CDList<OptimizationObjective> d_objectives;
 
   /** The results of the optimizations from the last checkOpt call **/
   std::vector<OptimizationResult> d_results;