api: avoid some string copies when using mk_external_string

Z3Prover · Dec 28, 2024 · bd8c870 · bd8c870
1 parent 0b9ed92
commit bd8c870
Show file tree

Hide file tree

Showing 11 changed files with 25 additions and 40 deletions.
diff --git a/scripts/update_api.py b/scripts/update_api.py
@@ -1799,7 +1799,7 @@ def write_log_h_preamble(log_h):
   log_h.write('extern atomic<bool> g_z3_log_enabled;\n')
   log_h.write('void ctx_enable_logging();\n')
   log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n')
-  log_h.write('void SetR(void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n')
+  log_h.write('void SetR(const void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n')
   log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) { SetR(tmp_ret); } return tmp_ret; } while (0)\n')
 
 

diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
@@ -209,21 +209,10 @@ namespace api {
             invoke_error_handler(err);
         }
     }
-
-    char * context::mk_external_string(char const * str) {
-        m_string_buffer = str?str:"";
-        return const_cast<char *>(m_string_buffer.c_str());
-    }
-
-    char * context::mk_external_string(char const * str, unsigned n) {
-        m_string_buffer.clear();
-        m_string_buffer.append(str, n);
-        return const_cast<char *>(m_string_buffer.c_str());
-    }
 
-    char * context::mk_external_string(std::string && str) {
+    const char * context::mk_external_string(std::string && str) {
         m_string_buffer = std::move(str);
-        return const_cast<char *>(m_string_buffer.c_str());
+        return m_string_buffer.c_str();
     }
 
     expr * context::mk_numeral_core(rational const & n, sort * s) {

diff --git a/src/api/api_context.h b/src/api/api_context.h
@@ -199,9 +199,7 @@ namespace api {
 
         // Store a copy of str in m_string_buffer, and return a reference to it.
         // This method is used to communicate local/internal strings with the "external world"
-        char * mk_external_string(char const * str, unsigned n);
-        char * mk_external_string(char const * str);
-        char * mk_external_string(std::string && str);
+        const char * mk_external_string(std::string && str);
         sbuffer<char>              m_char_buffer;
 
 

diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
@@ -559,7 +559,7 @@ extern "C" {
         param_descrs descrs;
         to_fixedpoint_ref(d)->collect_param_descrs(descrs);
         descrs.display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 

diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp
@@ -34,7 +34,7 @@ static mutex g_log_mux;
 #endif
 
 // functions called from api_log_macros.*
-void SetR(void * obj) {
+void SetR(const void * obj) {
     *g_z3_log << "= " << obj << '\n';
 }
 

diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp
@@ -217,20 +217,20 @@ extern "C" {
             if (mk_c(c)->fpautil().is_rm_numeral(to_expr(a), rm)) {
                 switch (rm) {
                 case MPF_ROUND_NEAREST_TEVEN:
-                    return mk_c(c)->mk_external_string("roundNearestTiesToEven");
+                    return "roundNearestTiesToEven";
                     break;
                 case MPF_ROUND_NEAREST_TAWAY:
-                    return mk_c(c)->mk_external_string("roundNearestTiesToAway");
+                    return "roundNearestTiesToAway";
                     break;
                 case MPF_ROUND_TOWARD_POSITIVE:
-                    return mk_c(c)->mk_external_string("roundTowardPositive");
+                    return "roundTowardPositive";
                     break;
                 case MPF_ROUND_TOWARD_NEGATIVE:
-                    return mk_c(c)->mk_external_string("roundTowardNegative");
+                    return "roundTowardNegative";
                     break;
                 case MPF_ROUND_TOWARD_ZERO:
                 default:
-                    return mk_c(c)->mk_external_string("roundTowardZero");
+                    return "roundTowardZero";
                     break;
                 }
             }

diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
@@ -313,7 +313,7 @@ extern "C" {
         param_descrs descrs;
         to_optimize_ptr(d)->collect_param_descrs(descrs);
         descrs.display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 

diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp
@@ -191,7 +191,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             RETURN_Z3(nullptr);
         }
-        return mk_c(c)->mk_external_string(result);
+        return result;
         Z3_CATCH_RETURN(nullptr);
     }
 

diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp
@@ -235,9 +235,9 @@ extern "C" {
 
     Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) {
         std::stringstream ous;
-        Z3_TRY;
         RESET_ERROR_CODE();
         LOG_Z3_eval_smtlib2_string(c, str);
+        Z3_TRY;
         if (!mk_c(c)->cmd()) {
             auto* ctx = alloc(cmd_context, false, &(mk_c(c)->m()));
             mk_c(c)->cmd() = ctx;
@@ -257,15 +257,13 @@ extern "C" {
             // See api::context::m_parser for a motivation about the reuse of the parser
             if (!parse_smt2_commands_with_parser(mk_c(c)->m_parser, *ctx.get(), is)) {
                 SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
-                RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
             }
         }
         catch (z3_exception& e) {
             if (ous.str().empty()) ous << e.what();
             SET_ERROR_CODE(Z3_PARSER_ERROR, ous.str());
-            RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
         }
-        RETURN_Z3(mk_c(c)->mk_external_string(ous.str()));
-        Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str()));
+        Z3_CATCH_CORE();
+        RETURN_Z3(mk_c(c)->mk_external_string(std::move(ous).str()));
     }
 }
diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp
@@ -274,7 +274,7 @@ extern "C" {
         reset_rcf_cancel(c);
         std::ostringstream buffer;
         rcfm(c).display(buffer, to_rcnumeral(a), compact, html);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -285,7 +285,7 @@ extern "C" {
         reset_rcf_cancel(c);
         std::ostringstream buffer;
         rcfm(c).display_decimal(buffer, to_rcnumeral(a), prec);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 

diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
@@ -339,7 +339,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return "";
         }        
-        return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str());
+        return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str());
         Z3_CATCH_RETURN("");
     }
 
@@ -359,7 +359,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return "";
         }
-        return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str());
+        return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str());
         Z3_CATCH_RETURN("");
     }
 
@@ -371,7 +371,7 @@ extern "C" {
         param_descrs descrs;
         to_tactic_ref(t)->collect_param_descrs(descrs);
         descrs.display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -499,8 +499,8 @@ extern "C" {
         for (unsigned i = 0; i < sz; i++) {
             to_apply_result(r)->m_subgoals[i]->display(buffer);
         }
-        buffer << ")";
-        return mk_c(c)->mk_external_string(buffer.str());
+        buffer << ')';
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }
 
@@ -578,7 +578,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB, nullptr);
             return "";
         }        
-        return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str().c_str());
+        return mk_c(c)->mk_external_string(mk_c(c)->get_simplifier(idx)->get_name().str());
         Z3_CATCH_RETURN("");
     }
 
@@ -634,7 +634,7 @@ extern "C" {
         scoped_ptr<dependent_expr_simplifier> simp = (*to_simplifier_ref(t))(m, p, st);
         simp->collect_param_descrs(descrs);
         descrs.display(buffer);
-        return mk_c(c)->mk_external_string(buffer.str());
+        return mk_c(c)->mk_external_string(std::move(buffer).str());
         Z3_CATCH_RETURN("");
     }