Function z3_sys::Z3_mk_context
source · pub unsafe extern "C" fn Z3_mk_context(c: Z3_config) -> Z3_context
Expand description
Create a context using the given configuration.
After a context is created, the configuration cannot be changed,
although some parameters can be changed using Z3_update_param_value
.
All main interaction with Z3 happens in the context of a Z3_context
.
In contrast to Z3_mk_context_rc
, the life time of Z3_ast
objects are determined by the scope level of Z3_solver_push
and Z3_solver_pop
. In other words, a Z3_ast
object remains
valid until there is a call to Z3_solver_pop
that
takes the current scope below the level where
the object was created.
Note that all other reference counted objects, including Z3_model
,
Z3_solver
, Z3_func_interp
have to be managed by the caller.
Their reference counts are not handled by the context.
Further remarks:
Z3_sort
,Z3_func_decl
,Z3_app
,Z3_pattern
areZ3_ast
’s.- Z3 uses hash-consing, i.e., when the same
Z3_ast
is created twice, Z3 will return the same pointer twice.