Function z3_sys::Z3_mk_context_rc

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

Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.

Remarks:

• Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast’s.
• After a context is created, the configuration cannot be changed.
• All main interaction with Z3 happens in the context of a Z3_context.
• Z3 uses hash-consing, i.e., when the same Z3_ast is created twice, Z3 will return the same pointer twice.