mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

update documentation to clarify reference counting policies

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-28 10:18:42 -07:00
parent 9e3e52f4f6
commit 8ea7109f8f
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/z3_api.h
View file

@ -1375,6 +1375,16 @@ extern "C" {
although some parameters can be changed using #Z3_update_param_value. 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. 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 Z3_ast objects
are determined by the scope level of #Z3_push and #Z3_pop.
In other words, a Z3_ast object remains valid until there is a
call to Z3_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.
\conly \sa Z3_del_context \conly \sa Z3_del_context
\conly \deprecated Use #Z3_mk_context_rc \conly \deprecated Use #Z3_mk_context_rc