mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
set OCaml default behaivor to enable concurrent dec ref #6160
Add Z3_enable_concurrent_dec_ref to the API. It is enables behavior of dec_ref functions that are exposed over the API to work with concurrent GC. The API calls to dec_ref are queued and processed in the main thread where context operations take place (in a way that is assumed thread safe as context operations are only allowed to be serialized on one thread at a time).
This commit is contained in:
parent
6c5747a80e
commit
aefd336c18
|
@ -397,6 +397,14 @@ extern "C" {
|
|||
Z3_CATCH;
|
||||
}
|
||||
|
||||
void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_enable_concurrent_dec_ref(c);
|
||||
mk_c(c)->enableset_concurrent_dec_ref();
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
||||
void Z3_API Z3_toggle_warning_messages(bool enabled) {
|
||||
LOG_Z3_toggle_warning_messages(enabled);
|
||||
enable_warning_messages(enabled != 0);
|
||||
|
|
|
@ -172,8 +172,8 @@ namespace api {
|
|||
void set_error_code(Z3_error_code err, char const* opt_msg);
|
||||
void set_error_code(Z3_error_code err, std::string &&opt_msg);
|
||||
void set_error_handler(Z3_error_handler h) { m_error_handler = h; }
|
||||
|
||||
void set_concurrent_dec_ref() { m_concurrent_dec_ref = true; }
|
||||
|
||||
void enable_concurrent_dec_ref() { m_concurrent_dec_ref = true; }
|
||||
unsigned add_object(api::object* o);
|
||||
void del_object(api::object* o);
|
||||
void dec_ref(ast* a);
|
||||
|
|
|
@ -59,6 +59,7 @@ let mk_context (settings:(string * string) list) =
|
|||
Z3native.del_config cfg;
|
||||
Z3native.set_ast_print_mode res (Z3enums.int_of_ast_print_mode PRINT_SMTLIB2_COMPLIANT);
|
||||
Z3native.set_internal_error_handler res;
|
||||
Z3native.enable_concurrent_dec_ref res;
|
||||
res
|
||||
|
||||
module Symbol =
|
||||
|
|
|
@ -1705,6 +1705,16 @@ extern "C" {
|
|||
void Z3_API Z3_interrupt(Z3_context c);
|
||||
|
||||
|
||||
/**
|
||||
\brief use concurrency control for dec-ref.
|
||||
Reference counting decrements are allowed in separate threads from the context.
|
||||
If this setting is not invoked, reference counting decrements are not going to be thread safe.
|
||||
|
||||
def_API('Z3_enable_concurrent_dec_ref', VOID, (_in(CONTEXT),))
|
||||
*/
|
||||
void Z3_API Z3_enable_concurrent_dec_ref(Z3_context c);
|
||||
|
||||
|
||||
/**@}*/
|
||||
|
||||
/** @name Parameters */
|
||||
|
|
Loading…
Reference in a new issue