From 9026ff28bca557d276c00dad9d225de1c6287b5c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 29 Oct 2020 12:57:13 -0700 Subject: [PATCH] #4762 --- src/api/z3_api.h | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 05c9dfb0c..eb5f10c76 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1584,7 +1584,14 @@ extern "C" { \c Z3_solver, \c Z3_func_interp have to be managed by the caller. Their reference counts are not handled by the context. - Further remarks: + \remark Thread safety: objects created using a given context should not be + accessed from different threads without synchronization. In other words, + operations on a context are not thread safe. To use Z3 from different threads + create separate context objects. The \c Z3_translate, \c Z3_solver_translate, + \c Z3_model_translate, \c Z3_goal_translate + methods are exposed to allow copying state from one context to another. + + \remark - \c Z3_sort, \c Z3_func_decl, \c Z3_app, \c Z3_pattern are \c Z3_ast's. - Z3 uses hash-consing, i.e., when the same \c Z3_ast is created twice, Z3 will return the same pointer twice. @@ -5235,6 +5242,10 @@ extern "C" { /** \brief translate model from context \c c to context \c dst. + \remark Use this method for cloning state between contexts. Note that + operations on contexts are not thread safe and therefore all operations + that related to a given context have to be synchronized (or run in the same thread). + def_API('Z3_model_translate', MODEL, (_in(CONTEXT), _in(MODEL), _in(CONTEXT))) */ Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst);