mk_context method

Z3_context mk_context(Z3_config c)

\brief 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 \c Z3_context.

In contrast to #Z3_mk_context_rc, the life time of \c Z3_ast objects are determined by the scope level of #Z3_solver_push and #Z3_solver_pop. In other words, a \c 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 \c Z3_model, \c Z3_solver, \c Z3_func_interp have to be managed by the caller. Their reference counts are not handled by the context.

\remark Thread safety: objects created using a given context should not be accessed from different threads without synchronization. In other words, operations on a context are not thread safe. To use Z3 from different threads create separate context objects. The \c Z3_translate, \c Z3_solver_translate, \c Z3_model_translate, \c Z3_goal_translate methods are exposed to allow copying state from one context to another.

\remark

• \c Z3_sort, \c Z3_func_decl, \c Z3_app, \c Z3_pattern are \c Z3_ast's.
• Z3 uses hash-consing, i.e., when the same \c Z3_ast is created twice, Z3 will return the same pointer twice.

\sa Z3_del_context

def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),))

Implementation

Z3_context mk_context(
  Z3_config c,
) {
  return _mk_context(
    c,
  );
}