From 30fd01b526df65aa09e7d1785bc5fb333b12a680 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Fri, 6 Nov 2020 10:51:51 +0000
Subject: [PATCH] api: avoid copying param_refs whenever possible

---
 src/api/api_ast.cpp    |  2 +-
 src/api/api_opt.cpp    |  3 +--
 src/api/api_solver.cpp | 11 ++++++-----
 src/api/api_tactic.cpp | 10 ++++++----
 src/api/api_util.h     |  2 +-
 5 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 9d764bd2f..7d26e55ff 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -740,7 +740,7 @@ extern "C" {
         RESET_ERROR_CODE();
         ast_manager & m = mk_c(c)->m();
         expr * a = to_expr(_a);
-        params_ref p = to_param_ref(_p);
+        auto &p = to_param_ref(_p);
         unsigned timeout     = p.get_uint("timeout", mk_c(c)->get_timeout());
         bool     use_ctrl_c  = p.get_bool("ctrl_c", false);
         th_rewriter m_rw(m, p);
diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 2076ee5f6..690264623 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -230,8 +230,7 @@ extern "C" {
         param_descrs descrs;
         to_optimize_ptr(o)->collect_param_descrs(descrs);
         to_params(p)->m_params.validate(descrs);
-        params_ref pr = to_param_ref(p);
-        to_optimize_ptr(o)->updt_params(pr);
+        to_optimize_ptr(o)->updt_params(to_param_ref(p));
         Z3_CATCH;
     }
     
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index e50ee3aad..fd8997a2c 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -367,22 +367,23 @@ extern "C" {
         LOG_Z3_solver_set_params(c, s, p);
         RESET_ERROR_CODE();
 
-        symbol logic = to_param_ref(p).get_sym("smt.logic", symbol::null);
+        auto &params = to_param_ref(p);
+        symbol logic = params.get_sym("smt.logic", symbol::null);
         if (logic != symbol::null) {
             to_solver(s)->m_logic = logic;
         }
         if (to_solver(s)->m_solver) {
             bool old_model = to_solver(s)->m_params.get_bool("model", true);
-            bool new_model = to_param_ref(p).get_bool("model", true);
+            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);
-            to_param_ref(p).validate(r);
-            to_solver_ref(s)->updt_params(to_param_ref(p));
+            params.validate(r);
+            to_solver_ref(s)->updt_params(params);
         }
-        to_solver(s)->m_params.append(to_param_ref(p));
+        to_solver(s)->m_params.append(params);
 
         init_solver_log(c, s);
         
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 865fbf6d4..7314c9b60 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -226,8 +226,9 @@ extern "C" {
         RESET_ERROR_CODE();
         param_descrs r;
         to_tactic_ref(t)->collect_param_descrs(r);
-        to_param_ref(p).validate(r);
-        tactic * new_t = using_params(to_tactic_ref(t), to_param_ref(p));
+        auto &params = to_param_ref(p);
+        params.validate(r);
+        tactic * new_t = using_params(to_tactic_ref(t), params);
         RETURN_TACTIC(new_t);
         Z3_CATCH_RETURN(nullptr);
     }
@@ -456,8 +457,9 @@ extern "C" {
         RESET_ERROR_CODE();
         param_descrs pd;
         to_tactic_ref(t)->collect_param_descrs(pd);
-        to_param_ref(p).validate(pd);
-        Z3_apply_result r = _tactic_apply(c, t, g, to_param_ref(p));
+        auto &params = to_param_ref(p);
+        params.validate(pd);
+        Z3_apply_result r = _tactic_apply(c, t, g, params);
         RETURN_Z3(r);
         Z3_CATCH_RETURN(nullptr);
     }
diff --git a/src/api/api_util.h b/src/api/api_util.h
index 65d566d62..80fea1ac3 100644
--- a/src/api/api_util.h
+++ b/src/api/api_util.h
@@ -92,7 +92,7 @@ struct Z3_params_ref : public api::object {
 
 inline Z3_params_ref * to_params(Z3_params p) { return reinterpret_cast<Z3_params_ref *>(p); }
 inline Z3_params of_params(Z3_params_ref * p) { return reinterpret_cast<Z3_params>(p); }
-inline params_ref to_param_ref(Z3_params p) { return p == nullptr ? params_ref() : to_params(p)->m_params; }
+inline params_ref& to_param_ref(Z3_params p) { return p == nullptr ? const_cast<params_ref&>(params_ref::get_empty()) : to_params(p)->m_params; }
 
 struct Z3_param_descrs_ref : public api::object {
     param_descrs m_descrs;