Function z3_sys::Z3_mk_context

pub unsafe extern "C" fn Z3_mk_context(c: Z3_config) -> Z3_context

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 are Z3_ast’s.
• Z3 uses hash-consing, i.e., when the same Z3_ast is created twice, Z3 will return the same pointer twice.

See also:

• Z3_del_context