mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity

Merge pull request #1918 from c-cube/ocaml-release-gc

Browse source 
feat(api/ml): release runtime lock on some long-running functions
This commit is contained in:
Nikolaj Bjorner 2018-11-06 15:03:30 -08:00 • committed by GitHub
commit 1bf934e53a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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) 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 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_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c')
ml_wrapper = open(ml_wrapperf, 'w') 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') ml_wrapper.write(' assert(_iter == Val_emptylist);\n\n')
i = i + 1 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 ') ml_wrapper.write('\n /* invoke Z3 function */\n ')
if result != VOID: if result != VOID:
ts = type2str(result) ts = type2str(result)
@ -1499,6 +1510,7 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
else: else:
ml_wrapper.write('z3rv = ') ml_wrapper.write('z3rv = ')
# invoke procedure # invoke procedure
ml_wrapper.write('%s(' % name) ml_wrapper.write('%s(' % name)
i = 0 i = 0
@ -1516,6 +1528,9 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
i = i + 1 i = i + 1
ml_wrapper.write(');\n') 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: if have_context and name not in Unwrapped:
ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n') ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n')
ml_wrapper.write(' if (ec != Z3_OK) {\n') ml_wrapper.write(' if (ec != Z3_OK) {\n')

2
src/api/ml/META.in
View file

@ -1,7 +1,7 @@
# META file for the "z3" package: # META file for the "z3" package:
version = "@VERSION@" version = "@VERSION@"
description = "Z3 Theorem Prover (OCaml API)" description = "Z3 Theorem Prover (OCaml API)"
requires = "num" requires = "num threads"
archive(byte) = "z3ml.cma" archive(byte) = "z3ml.cma"
archive(native) = "z3ml.cmxa" archive(native) = "z3ml.cmxa"
archive(byte,plugin) = "z3ml.cma" archive(byte,plugin) = "z3ml.cma"

1
src/api/ml/z3native_stubs.c.pre
View file

@ -11,6 +11,7 @@ extern "C" {
#include <caml/alloc.h> #include <caml/alloc.h>
#include <caml/fail.h> #include <caml/fail.h>
#include <caml/callback.h> #include <caml/callback.h>
#include <caml/threads.h>
#ifdef Custom_tag #ifdef Custom_tag
#include <caml/custom.h> #include <caml/custom.h>