mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

feat(api/ml): release runtime lock on some long-running functions

Browse source
This commit is contained in:
Simon Cruanes 2018-11-06 13:44:57 -06:00
parent b301a59899
commit 9121c74c9f
3 changed files with 17 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
scripts/update_api.py
View file

@ -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')