scoped params on solver

solver::push_params() saves current parameters
solver::pop_params() restores previously saved parameters

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);
         }

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);

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.
      */
@@ -71,6 +76,17 @@ public:
     */
     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.