From e6a089e63d4783e76d11cc179d8d355cc7881da1 Mon Sep 17 00:00:00 2001
From: Phil Clayton <phil.clayton@lineone.net>
Date: Thu, 13 Feb 2025 16:46:08 +0000
Subject: [PATCH] Fix build when Z3_API macro is non-empty (#7553)
API function definitions are updated to be consistent with header files.
---
src/api/api_array.cpp | 6 +++---
src/api/api_ast.cpp | 10 +++++-----
src/api/api_context.cpp | 2 +-
src/api/api_datatype.cpp | 2 +-
src/api/api_model.cpp | 2 +-
src/api/api_quant.cpp | 2 +-
6 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/api/api_array.cpp b/src/api/api_array.cpp
index cb254dbdd..522976f01 100644
--- a/src/api/api_array.cpp
+++ b/src/api/api_array.cpp
@@ -282,15 +282,15 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
- Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
+ Z3_ast Z3_API Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
return Z3_mk_select(c, set, elem);
}
- Z3_ast Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem) {
+ Z3_ast Z3_API Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem) {
return Z3_mk_store(c, set, elem, Z3_mk_true(c));
}
- Z3_ast Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem) {
+ Z3_ast Z3_API Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem) {
return Z3_mk_store(c, set, elem, Z3_mk_false(c));
}
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index f73baa693..d7cb5f10d 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -369,7 +369,7 @@ extern "C" {
Z3_CATCH_RETURN(-1);
}
- Z3_API char const * Z3_get_symbol_string(Z3_context c, Z3_symbol s) {
+ Z3_string Z3_API Z3_get_symbol_string(Z3_context c, Z3_symbol s) {
Z3_TRY;
LOG_Z3_get_symbol_string(c, s);
RESET_ERROR_CODE();
@@ -714,7 +714,7 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
- Z3_sort_kind Z3_get_sort_kind(Z3_context c, Z3_sort t) {
+ Z3_sort_kind Z3_API Z3_get_sort_kind(Z3_context c, Z3_sort t) {
LOG_Z3_get_sort_kind(c, t);
RESET_ERROR_CODE();
CHECK_VALID_AST(t, Z3_UNKNOWN_SORT);
@@ -1019,7 +1019,7 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
- Z3_API char const * Z3_ast_to_string(Z3_context c, Z3_ast a) {
+ Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_ast_to_string(c, a);
RESET_ERROR_CODE();
@@ -1045,11 +1045,11 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
- Z3_API char const * Z3_sort_to_string(Z3_context c, Z3_sort s) {
+ Z3_string Z3_API Z3_sort_to_string(Z3_context c, Z3_sort s) {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(s));
}
- Z3_API char const * Z3_func_decl_to_string(Z3_context c, Z3_func_decl f) {
+ Z3_string Z3_API Z3_func_decl_to_string(Z3_context c, Z3_func_decl f) {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(f));
}
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index acc4d7016..82d65a5dd 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -518,7 +518,7 @@ extern "C" {
}
}
- Z3_API char const * Z3_get_error_msg(Z3_context c, Z3_error_code err) {
+ Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err) {
LOG_Z3_get_error_msg(c, err);
return _get_error_msg(c, err);
}
diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp
index 1ef4ea626..5c85ea2cd 100644
--- a/src/api/api_datatype.cpp
+++ b/src/api/api_datatype.cpp
@@ -604,7 +604,7 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
- Z3_ast Z3_datatype_update_field(
+ Z3_ast Z3_API Z3_datatype_update_field(
Z3_context c, Z3_func_decl f, Z3_ast t, Z3_ast v) {
Z3_TRY;
LOG_Z3_datatype_update_field(c, f, t, v);
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index e449cb0ea..475ce2cc6 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -422,7 +422,7 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
- Z3_API char const * Z3_model_to_string(Z3_context c, Z3_model m) {
+ Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m) {
Z3_TRY;
LOG_Z3_model_to_string(c, m);
RESET_ERROR_CODE();
diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp
index bb9efa9c3..cf5f099fa 100644
--- a/src/api/api_quant.cpp
+++ b/src/api/api_quant.cpp
@@ -575,7 +575,7 @@ extern "C" {
return (Z3_ast)(p);
}
- Z3_API char const * Z3_pattern_to_string(Z3_context c, Z3_pattern p) {
+ Z3_string Z3_API Z3_pattern_to_string(Z3_context c, Z3_pattern p) {
return Z3_ast_to_string(c, reinterpret_cast<Z3_ast>(p));
}