mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Added hash-consing remarks to mk_context and mk_context_rc.

Browse source 
Fixes #452
This commit is contained in:
Christoph M. Wintersteiger 2016-03-05 17:58:32 +00:00
parent 8abedbf389
commit a2ecb19d03
1 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/api/z3_api.h
View file

@ -1474,6 +1474,11 @@ extern "C" {
Z3_solver, Z3_func_interp have to be managed by the caller. Z3_solver, Z3_func_interp have to be managed by the caller.
Their reference counts are not handled by the context. 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.
\sa Z3_del_context \sa Z3_del_context
def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),)) def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),))
@ -1492,11 +1497,13 @@ extern "C" {
anymore. This idiom is similar to the one used in anymore. This idiom is similar to the one used in
BDD (binary decision diagrams) packages such as CUDD. BDD (binary decision diagrams) packages such as CUDD.
Remark: Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Remarks:
Z3_ast's.
After a context is created, the configuration cannot be changed. - Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
All main interaction with Z3 happens in the context of a \c Z3_context. - 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 Z3_ast is created twice,
Z3 will return the same pointer twice.
def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),)) def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),))
*/ */