TLDR:
- Use
Z3_mk_config to create a Z3_config.
- Use
Z3_global_param_set to set configs globally.
- Use
Z3_set_param_value to set context-specific configs.
- If you don't have any config to set, simply
- make a
Z3_config with Z3_mk_config,
- create your context with it,
- and then delete it with
Z3_del_config.
The comment by SergeyLebedev is probably referencing to this remark in the doc
In previous versions of Z3, the Z3_config was used to store global and
module configurations. Now, we should use Z3_global_param_set.
I was going through the source repo the past few days. In the example file test_capi.c, they use this mk_context function a lot, which is defined in the same file with
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;
}
where mk_context_custom is defined in the same file with
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;
}
So it looks like Z3_mk_config and Z3_set_param_value are still used.
The doc says that stuff like Z3_config and Z3_context are supposed to be "opaque pointers". However, chasing it to the source, it looks like Z3_config is declared as a struct without the specific content but seems like wherever it's used it's cast to context_params which is defined clearly as a class.
The type Z3_config is declared in z3_api_h with
DEFINE_TYPE(Z3_config);
where DEFINE_TYPE(T) is a macro defined in z3_macros.h and expands to typedef struct _ ## T *T. So really Z3_config is only prototypically declared as a struct.
The function Z3_mk_config, the constructor for a Z3_config, declared in z3_api.h with
Z3_config Z3_API Z3_mk_config(void);
, is defined in api_config_params.cpp as
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;
}
}
within an extern "C" block. Note that Z3_API is a macro also defined in z3_macros.h to set __attribute__ ((visibility ("default"))) and alloc is a macro defined in memory_manager.h with #define alloc(T,...) new (memory::allocate(sizeof(T))) T(__VA_ARGS__) and RETURN_Z3 is a macro defined in some file generated by the file update_api.py with #define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES.
It appears that, when a Z3_config is created, a memory block of the size of a context_params is allocated and cast as Z3_config, and context_params is in fact a class defined clearly in context_params.h. I omit the content because it's not relevant right now.
class context_params {
....
};
Next, Z3_set_param_value is defined in api_config_params.cpp with
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());
}
}
So it appears that the function first cast Z3_config back to context_params before using it like a normal object. I'm not an expert but this probably works because struct and class are almost the same underneath the hood.
On the other hand, in that exmaple file test_capi.c, they used Z3_global_param_set like so
....
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);
They did still use Z3_mk_config before making a context while using Z3_global_param_set to set configs. So I'd say there's nothing wrong with using Z3_mk_config to construct a Z3_config, and what the doc is saying is when you want to set something globally, don't access the Z3_config struct itself since you can't before casting it to a context_params anyway; use Z3_global_param_set instead. And when you want to set something specific to some specific context, use Z3_set_param_value.
The question remains that why would we want to switch between structs and classes? I don't know. I'm not at all familiar with C++, but I'm guessing, if not for the C API itself, it's for making the extern "C" part works for the Python API bindings.
