From 1da002d7b1e6ced16e9871744c29b2f934f2f9b0 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 22 May 2018 14:49:52 -0700
Subject: [PATCH] scoped params on solver

solver::push_params() saves current parameters
solver::pop_params() restores previously saved parameters
---
 src/smt/smt_solver.cpp | 14 ++++++++++++++
 src/solver/solver.cpp  |  6 ++++++
 src/solver/solver.h    | 16 ++++++++++++++++
 3 files changed, 36 insertions(+)

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index d282a59da..0bef90a48 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -118,6 +118,20 @@ namespace smt {
             m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns();
         }
 
+        params_ref m_params_save;
+        smt_params m_smt_params_save;
+
+        void push_params() override {
+            m_params_save.reset();
+            m_params_save.copy(solver::get_params());
+            m_smt_params_save = m_smt_params;
+        }
+
+        void pop_params() override {
+            m_smt_params = m_smt_params_save;
+            solver::reset_params(m_params_save);
+        }
+
         void collect_param_descrs(param_descrs & r) override {
             m_context.collect_param_descrs(r);
         }
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 4b812f83b..cc1d472ca 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -206,6 +206,12 @@ void solver::collect_param_descrs(param_descrs & r) {
     r.insert("solver.enforce_model_conversion", CPK_BOOL, "(default: false) enforce model conversion when asserting formulas");
 }
 
+void solver::reset_params(params_ref const & p) { 
+    m_params.reset();
+    m_params.copy(p); 
+    m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
+}
+
 void solver::updt_params(params_ref const & p) { 
     m_params.copy(p); 
     m_enforce_model_conversion = m_params.get_bool("solver.enforce_model_conversion", false);
diff --git a/src/solver/solver.h b/src/solver/solver.h
index bb330636f..4c0c361ff 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -60,6 +60,11 @@ public:
     */
     virtual void updt_params(params_ref const & p);
 
+    /**
+       \brief reset parameters.
+    */
+    virtual void reset_params(params_ref const& p);
+
     /**
        \brief Retrieve set of parameters set on solver.
      */
@@ -70,6 +75,17 @@ public:
        parameters available in this solver.
     */
     virtual void collect_param_descrs(param_descrs & r);
+
+    /**
+       \brief Push a parameter state. It is restored upon pop.
+       Only a single scope of push is supported.
+    */
+    virtual void push_params() {}
+
+    /**
+       \brief Pop a parameter state. \sa push_params.
+    */
+    virtual void pop_params() {}
     
     /**
        \brief Enable/Disable model generation for this solver object.