TLDR：
- 使用
Z3_mk_config 创建Z3_config。
- 使用
Z3_global_param_set 全局设置配置。
- 使用
Z3_set_param_value 设置特定于上下文的配置。
- 如果您没有任何要设置的配置，只需
- 用
Z3_mk_config创建一个Z3_config，
- 用它创建你的上下文，
- 然后用
Z3_del_config删除它。
SergeyLebedev 的评论可能引用了doc 中的这句话
在之前的 Z3 版本中，Z3_config 用于存储全局和
模块配置。现在，我们应该使用Z3_global_param_set。
过去几天我正在浏览源代码库。在示例文件test_capi.c 中，他们经常使用这个mk_context 函数，它在同一个文件中定义为
Z3_context mk_context()
{
Z3_config cfg;
Z3_context ctx;
cfg = Z3_mk_config();
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);
return ctx;
}
mk_context_custom 与
在同一个文件中定义
Z3_context mk_context_custom(Z3_config cfg, Z3_error_handler err)
{
Z3_context ctx;
Z3_set_param_value(cfg, "model", "true");
ctx = Z3_mk_context(cfg);
Z3_set_error_handler(ctx, err);
return ctx;
}
所以看起来Z3_mk_config 和Z3_set_param_value 仍在使用中。
文档说像Z3_config 和Z3_context 这样的东西应该是“不透明的指针”。然而，追到源头，看起来Z3_config 被声明为没有特定内容的结构，但似乎在任何使用它的地方都被强制转换为明确定义为类的context_params。
Z3_config 类型在 z3_api_h 中声明为
DEFINE_TYPE(Z3_config);
其中DEFINE_TYPE(T) 是在z3_macros.h 中定义的宏，并扩展为typedef struct _ ## T *T。所以真的 Z3_config 只是在原型上声明为一个结构。
函数Z3_mk_config，Z3_config 的构造函数，在z3_api.h 中声明
Z3_config Z3_API Z3_mk_config(void);
，在api_config_params.cpp中定义为
Z3_config Z3_API Z3_mk_config(void) {
try {
memory::initialize(UINT_MAX);
LOG_Z3_mk_config();
Z3_config r = reinterpret_cast<Z3_config>(alloc(context_params));
RETURN_Z3(r);
} catch (z3_exception & ex) {
// The error handler is only available for contexts
// Just throw a warning.
warning_msg("%s", ex.msg());
return nullptr;
}
}
在extern "C" 块内。注意Z3_API是在z3_macros.h中定义的宏来设置__attribute__ ((visibility ("default")))和alloc是在memory_manager.h中定义的宏，#define alloc(T,...) new (memory::allocate(sizeof(T))) T(__VA_ARGS__)和RETURN_Z3是在文件生成的某些文件中定义的宏update_api.py 和 #define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES。
看起来，当一个Z3_config被创建时，一个context_params大小的内存块被分配并转换为Z3_config，而context_params实际上是一个在context_params.h中明确定义的类.我省略了内容，因为它现在不相关。
class context_params {
....
};
接下来，Z3_set_param_value 在api_config_params.cpp 中定义为
void Z3_API Z3_set_param_value(Z3_config c, char const * param_id, char const * param_value) {
LOG_Z3_set_param_value(c, param_id, param_value);
try {
context_params * p = reinterpret_cast<context_params*>(c);
p->set(param_id, param_value);
}
catch (z3_exception & ex) {
// The error handler is only available for contexts
// Just throw a warning.
warning_msg("%s", ex.msg());
}
}
所以看起来该函数首先将Z3_config 转换回context_params，然后再像普通对象一样使用它。我不是专家，但这可能有效，因为 struct and class are almost the same 在幕后。
另一方面，在那个示例文件 test_capi.c 中，他们使用了 Z3_global_param_set，就像这样
....
cfg = Z3_mk_config();
....
/*
The current model finder for quantified formulas cannot handle injectivity.
So, we are limiting the number of iterations to avoid a long "wait".
*/
Z3_global_param_set("smt.mbqi.max_iterations", "10");
ctx = mk_context_custom(cfg, error_handler);
Z3_del_config(cfg);
s = mk_solver(ctx);
在使用Z3_global_param_set 设置配置之前，他们仍然使用Z3_mk_config 来创建上下文。所以我想说使用Z3_mk_config 构造Z3_config 并没有错，文档的意思是当你想全局设置一些东西时，不要访问Z3_config 结构本身，因为你不能在将其转换为 context_params 之前；请改用Z3_global_param_set。当您想针对某些特定上下文设置特定内容时，请使用Z3_set_param_value。
问题仍然存在，为什么我们要在结构和类之间切换？我不知道。我对 C++ 一点也不熟悉，但我猜，如果不是因为 C API 本身，那是为了让 extern "C" 部分工作 for the Python API bindings。