From 9121c74c9fd8e0832fec72498d53673a157ac2b0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 6 Nov 2018 13:44:57 -0600 Subject: [PATCH] feat(api/ml): release runtime lock on some long-running functions --- scripts/update_api.py | 15 +++++++++++++++ src/api/ml/META.in | 2 +- src/api/ml/z3native_stubs.c.pre | 1 + 3 files changed, 17 insertions(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 917df94a2..87bdd3551 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1328,6 +1328,13 @@ def mk_ml(ml_src_dir, ml_output_dir): mk_z3native_stubs_c(ml_src_dir, ml_output_dir) +z3_long_funs = frozenset([ + 'Z3_solver_check', + 'Z3_solver_check_assumptions', + 'Z3_simplify', + 'Z3_simplify_ex', + ]) + def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c') ml_wrapper = open(ml_wrapperf, 'w') @@ -1491,6 +1498,10 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface ml_wrapper.write(' assert(_iter == Val_emptylist);\n\n') i = i + 1 + release_caml_gc= name in z3_long_funs + if release_caml_gc: + ml_wrapper.write('\n caml_release_runtime_system();\n') + ml_wrapper.write('\n /* invoke Z3 function */\n ') if result != VOID: ts = type2str(result) @@ -1499,6 +1510,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface else: ml_wrapper.write('z3rv = ') + # invoke procedure ml_wrapper.write('%s(' % name) i = 0 @@ -1516,6 +1528,9 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface i = i + 1 ml_wrapper.write(');\n') + if release_caml_gc: + ml_wrapper.write('\n caml_acquire_runtime_system();\n') + if have_context and name not in Unwrapped: ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n') ml_wrapper.write(' if (ec != Z3_OK) {\n') diff --git a/src/api/ml/META.in b/src/api/ml/META.in index 1951e60b3..e58ebf722 100644 --- a/src/api/ml/META.in +++ b/src/api/ml/META.in @@ -1,7 +1,7 @@ # META file for the "z3" package: version = "@VERSION@" description = "Z3 Theorem Prover (OCaml API)" -requires = "num" +requires = "num threads" archive(byte) = "z3ml.cma" archive(native) = "z3ml.cmxa" archive(byte,plugin) = "z3ml.cma" diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index c1c772c85..71ee18ce9 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -11,6 +11,7 @@ extern "C" { #include #include #include +#include #ifdef Custom_tag #include