diff --git a/scripts/update_api.py b/scripts/update_api.py index 901ea4fda..65791399c 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1335,6 +1335,10 @@ z3_long_funs = frozenset([ 'Z3_simplify_ex', ]) +z3_ml_overrides = frozenset([ + 'Z3_mk_config' + ]) + 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') @@ -1346,6 +1350,10 @@ def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): # C interface ml_pref.close() for name, result, params in _dotnet_decls: + + if name in z3_ml_overrides: + continue + ip = inparams(params) op = outparams(params) ap = arrayparams(params) diff --git a/src/api/ml/z3native_stubs.c.pre b/src/api/ml/z3native_stubs.c.pre index 71ee18ce9..4d221aac3 100644 --- a/src/api/ml/z3native_stubs.c.pre +++ b/src/api/ml/z3native_stubs.c.pre @@ -448,3 +448,21 @@ CAMLprim value DLL_PUBLIC n_set_internal_error_handler(value ctx_v) Z3_set_error_handler(ctx_p->ctx, MLErrorHandler); CAMLreturn(Val_unit); } + +CAMLprim DLL_PUBLIC value n_mk_config() { + CAMLparam0(); + CAMLlocal1(result); + Z3_config z3rv; + + /* invoke Z3 function */ + z3rv = Z3_mk_config(); + + if (z3rv == NULL) { + caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "internal error"); + } + + /* construct simple return value */ + result = caml_alloc_custom(&default_custom_ops, sizeof(Z3_config), 0, 1); *(Z3_config*)Data_custom_val(result) = z3rv; + /* cleanup and return */ + CAMLreturn(result); +}