From a2ecb19d0384e20446138213c1ac7d27081efb94 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 5 Mar 2016 17:58:32 +0000 Subject: [PATCH] Added hash-consing remarks to mk_context and mk_context_rc. Fixes #452 --- src/api/z3_api.h | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 15bcedcb0..5c7a819da 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1457,7 +1457,7 @@ extern "C" { /*@{*/ /** - \deprecated + \deprecated \brief Create a context using the given configuration. After a context is created, the configuration cannot be changed, @@ -1474,6 +1474,11 @@ extern "C" { Z3_solver, Z3_func_interp have to be managed by the caller. 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 def_API('Z3_mk_context', CONTEXT, (_in(CONFIG),)) @@ -1492,11 +1497,13 @@ extern "C" { anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD. - Remark: Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are - Z3_ast's. + Remarks: - 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_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 \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),)) */