mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

freeze functions with callbacks for ocaml

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-08 10:04:50 -07:00
parent cf4149d53e
commit a71ce54c34
1 changed files with 23 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

39
scripts/update_api.py
View file

@ -1332,6 +1332,25 @@ def ml_alloc_and_store(t, lhs, rhs):
alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts) alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts)
return alloc_str + ml_set_wrap(t, lhs, rhs) return alloc_str + ml_set_wrap(t, lhs, rhs)
z3_long_funs = frozenset([
'Z3_solver_check',
'Z3_solver_check_assumptions',
'Z3_simplify',
'Z3_simplify_ex',
])
z3_ml_overrides = frozenset([
'Z3_mk_config'])
z3_ml_callbacks = frozenset([
'Z3_solver_propagate_init',
'Z3_solver_propagate_fixed',
'Z3_solver_propagate_eq',
'Z3_solver_propagate_diseq',
'Z3_solver_propagate_created'
])
def mk_ml(ml_src_dir, ml_output_dir): def mk_ml(ml_src_dir, ml_output_dir):
global Type2Str global Type2Str
ml_nativef = os.path.join(ml_output_dir, 'z3native.ml') ml_nativef = os.path.join(ml_output_dir, 'z3native.ml')
@ -1345,6 +1364,8 @@ def mk_ml(ml_src_dir, ml_output_dir):
ml_native.write('\n') ml_native.write('\n')
for name, result, params in _dotnet_decls: for name, result, params in _dotnet_decls:
if name in z3_ml_callbacks:
continue
ml_native.write('external %s : ' % ml_method_name(name)) ml_native.write('external %s : ' % ml_method_name(name))
ip = inparams(params) ip = inparams(params)
op = outparams(params) op = outparams(params)
@ -1389,22 +1410,6 @@ 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',
])
z3_ml_overrides = frozenset([
'Z3_mk_config',
'Z3_solver_propagate_init',
'Z3_solver_propagate_fixed',
'Z3_solver_propagate_eq',
'Z3_solver_propagate_diseq',
'Z3_solver_propagate_created'
])
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')
@ -1419,6 +1424,8 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface
if name in z3_ml_overrides: if name in z3_ml_overrides:
continue continue
if name in z3_ml_callbacks:
continue
ip = inparams(params) ip = inparams(params)
op = outparams(params) op = outparams(params)