mk_context_rc method

Z3_context mk_context_rc(
  1. Z3_config c
)

\brief 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 \c 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 \c Z3_ast returned by Z3, and #Z3_dec_ref whenever the \c Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.

Remarks:

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

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

Implementation

Z3_context mk_context_rc(
  Z3_config c,
) {
  return _mk_context_rc(
    c,
  );
}