Cache param descrs when modifying solver params (#6156)

Z3Prover · Jul 14, 2022 · 2f5fef9 · 2f5fef9
1 parent 4a19285
commit 2f5fef9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
@@ -391,9 +391,11 @@ extern "C" {
             bool new_model = params.get_bool("model", true);
             if (old_model != new_model)
                 to_solver_ref(s)->set_produce_models(new_model);
-            param_descrs r;
-            to_solver_ref(s)->collect_param_descrs(r);
-            context_params::collect_solver_param_descrs(r);
+            param_descrs& r = to_solver(s)->m_param_descrs;
+            if(r.size () == 0) {
+              to_solver_ref(s)->collect_param_descrs(r);
+              context_params::collect_solver_param_descrs(r);
+            }
             params.validate(r);
             to_solver_ref(s)->updt_params(params);
         }

diff --git a/src/api/api_solver.h b/src/api/api_solver.h
@@ -42,6 +42,7 @@ struct Z3_solver_ref : public api::object {
     scoped_ptr<solver_factory> m_solver_factory;
     ref<solver>                m_solver;
     params_ref                 m_params;
+    param_descrs               m_param_descrs;
     symbol                     m_logic;
     scoped_ptr<solver2smt2_pp> m_pp;
     scoped_ptr<cmd_context>    m_cmd_context;