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

New OCaml API

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-13 22:09:45 +00:00
parent 8fc58e1ace
commit 824169da0a
7 changed files with 2134 additions and 2537 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
scripts/mk_make.py
View file

@ -13,11 +13,9 @@ parse_options()
check_eol()
API_files = init_project_def()
update_version()
mk_auto_src()
#update_version()
#mk_auto_src()
mk_bindings(API_files)
mk_vs_proj('z3', ['shell'])
mk_vs_proj_dll('libz3', ['api_dll'])
mk_makefile()
#mk_vs_proj('z3', ['shell'])
#mk_vs_proj_dll('libz3', ['api_dll'])
#mk_makefile()

180
scripts/mk_util.py
View file

@ -1793,6 +1793,10 @@ class MLComponent(Component):
def mk_makefile(self, out):
if is_ml_enabled():
CP_CMD = 'cp'
if IS_WINDOWS:
CP_CMD='copy'
src_dir = self.to_src_dir
mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
api_src = get_component(API_COMPONENT).to_src_dir
@ -1809,10 +1813,6 @@ class MLComponent(Component):
os.path.join(BUILD_DIR, self.sub_dir, 'META'),
substitutions)
mlis = ''
for m in self.modules:
mlis = os.path.join(src_dir, m) + '.mli ' + mlis
stubsc = os.path.join(src_dir, self.stubs + '.c')
stubso = os.path.join(self.sub_dir, self.stubs) + '$(OBJ_EXT)'
z3dllso = get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT)'
@ -1820,29 +1820,27 @@ class MLComponent(Component):
out.write('\t%s -ccopt "$(CXXFLAGS_OCAML) -I %s -I %s -I %s $(CXX_OUT_FLAG)%s" -c %s\n' %
(OCAMLC, OCAML_LIB, api_src, src_dir, stubso, stubsc))
cmis = ''
for m in self.modules:
ff = os.path.join(src_dir, m + '.mli')
ft = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s\n' % (ft, cmis))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, ft, ff))
cmis = cmis + ' ' + ft
cmos = ''
for m in self.modules:
ff = os.path.join(src_dir, m + '.ml')
ft = os.path.join(self.sub_dir, m + '.cmo')
fd = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (ft, ff, fd))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, ft, ff))
cmos = cmos + ' ' + ft
ml = os.path.join(src_dir, m + '.ml')
cmo = os.path.join(self.sub_dir, m + '.cmo')
existing_mli = os.path.join(src_dir, m + '.mli')
mli = os.path.join(self.sub_dir, m + '.mli')
cmi = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (cmo, ml, cmos))
if (os.path.exists(existing_mli[3:])):
out.write('\t%s %s %s\n' % (CP_CMD, existing_mli, mli))
else:
out.write('\t%s -i -I %s -c %s > %s\n' % (OCAMLC, self.sub_dir, ml, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, cmi, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLC, self.sub_dir, cmo, ml))
cmos = cmos + cmo + ' '
cmxs = ''
for m in self.modules:
ff = os.path.join(src_dir, m + '.ml')
ft = os.path.join(self.sub_dir, m + '.cmx')
fd = os.path.join(self.sub_dir, m + '.cmi')
out.write('%s: %s %s\n' % (ft, ff, fd))
out.write('%s: %s %s\n' % (ft, ff, cmos))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPT, self.sub_dir, ft, ff))
cmxs = cmxs + ' ' + ft
@ -1896,7 +1894,11 @@ class MLComponent(Component):
metafile=os.path.join(self.sub_dir, 'META')))
for m in self.modules:
out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
mli = os.path.join(self.src_dir, m) + '.mli'
if os.path.exists(mli):
out.write(' ' + os.path.join(self.to_src_dir, m) + '.mli')
else:
out.write(' ' + os.path.join(self.sub_dir, m) + '.mli')
out.write(' ' + os.path.join(self.sub_dir, m) + '.cmi')
out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml$(LIB_EXT)'))))
@ -3301,78 +3303,78 @@ def mk_z3consts_ml(api_files):
efile.close()
if VERBOSE:
print ('Generated "%s/z3enums.ml"' % ('%s' % gendir))
efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
efile.write('(* Automatically generated file *)\n\n')
efile.write('(** The enumeration types of Z3. *)\n\n')
for api_file in api_files:
api_file_c = ml.find_file(api_file, ml.name)
api_file = os.path.join(api_file_c.src_dir, api_file)
# efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
# efile.write('(* Automatically generated file *)\n\n')
# efile.write('(** The enumeration types of Z3. *)\n\n')
# for api_file in api_files:
# api_file_c = ml.find_file(api_file, ml.name)
# api_file = os.path.join(api_file_c.src_dir, api_file)
api = open(api_file, 'r')
# api = open(api_file, 'r')
SEARCHING = 0
FOUND_ENUM = 1
IN_ENUM = 2
# SEARCHING = 0
# FOUND_ENUM = 1
# IN_ENUM = 2
mode = SEARCHING
decls = {}
idx = 0
# mode = SEARCHING
# decls = {}
# idx = 0
linenum = 1
for line in api:
m1 = blank_pat.match(line)
m2 = comment_pat.match(line)
if m1 or m2:
# skip blank lines and comments
linenum = linenum + 1
elif mode == SEARCHING:
m = typedef_pat.match(line)
if m:
mode = FOUND_ENUM
m = typedef2_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
elif mode == FOUND_ENUM:
m = openbrace_pat.match(line)
if m:
mode = IN_ENUM
decls = {}
idx = 0
else:
assert False, "Invalid %s, line: %s" % (api_file, linenum)
else:
assert mode == IN_ENUM
words = re.split('[^\-a-zA-Z0-9_]+', line)
m = closebrace_pat.match(line)
if m:
name = words[1]
if name not in DeprecatedEnums:
efile.write('(** %s *)\n' % name[3:])
efile.write('type %s =\n' % name[3:]) # strip Z3_
for k, i in decls.items():
efile.write(' | %s \n' % k[3:]) # strip Z3_
efile.write('\n')
efile.write('(** Convert %s to int*)\n' % name[3:])
efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
efile.write('(** Convert int to %s*)\n' % name[3:])
efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
efile.write('\n')
mode = SEARCHING
else:
if words[2] != '':
if len(words[2]) > 1 and words[2][1] == 'x':
idx = int(words[2], 16)
else:
idx = int(words[2])
decls[words[1]] = idx
idx = idx + 1
linenum = linenum + 1
api.close()
efile.close()
if VERBOSE:
print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))
# linenum = 1
# for line in api:
# m1 = blank_pat.match(line)
# m2 = comment_pat.match(line)
# if m1 or m2:
# # skip blank lines and comments
# linenum = linenum + 1
# elif mode == SEARCHING:
# m = typedef_pat.match(line)
# if m:
# mode = FOUND_ENUM
# m = typedef2_pat.match(line)
# if m:
# mode = IN_ENUM
# decls = {}
# idx = 0
# elif mode == FOUND_ENUM:
# m = openbrace_pat.match(line)
# if m:
# mode = IN_ENUM
# decls = {}
# idx = 0
# else:
# assert False, "Invalid %s, line: %s" % (api_file, linenum)
# else:
# assert mode == IN_ENUM
# words = re.split('[^\-a-zA-Z0-9_]+', line)
# m = closebrace_pat.match(line)
# if m:
# name = words[1]
# if name not in DeprecatedEnums:
# efile.write('(** %s *)\n' % name[3:])
# efile.write('type %s =\n' % name[3:]) # strip Z3_
# for k, i in decls.items():
# efile.write(' | %s \n' % k[3:]) # strip Z3_
# efile.write('\n')
# efile.write('(** Convert %s to int*)\n' % name[3:])
# efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
# efile.write('(** Convert int to %s*)\n' % name[3:])
# efile.write('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
# efile.write('\n')
# mode = SEARCHING
# else:
# if words[2] != '':
# if len(words[2]) > 1 and words[2][1] == 'x':
# idx = int(words[2], 16)
# else:
# idx = int(words[2])
# decls[words[1]] = idx
# idx = idx + 1
# linenum = linenum + 1
# api.close()
# efile.close()
# if VERBOSE:
# print ('Generated "%s/z3enums.mli"' % ('%s' % gendir))
def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id

376
scripts/update_api.py
View file

@ -219,7 +219,11 @@ def type2javaw(ty):
def type2ml(ty):
global Type2ML
return Type2ML[ty]
q = Type2ML[ty]
if q[0:3] == 'z3_':
return q[3:]
else:
return q;
def _in(ty):
return (IN, ty)
@ -1125,6 +1129,110 @@ def arrayparams(params):
return op
def ml_plus_type(ts):
if ts == 'Z3_context':
return 'Z3_context_plus'
elif ts == 'Z3_ast' or ts == 'Z3_sort' or ts == 'Z3_func_decl' or ts == 'Z3_app' or ts == 'Z3_pattern':
return 'Z3_ast_plus'
elif ts == 'Z3_symbol':
return 'Z3_symbol_plus'
elif ts == 'Z3_constructor':
return 'Z3_constructor_plus'
elif ts == 'Z3_constructor_list':
return 'Z3_constructor_list_plus'
elif ts == 'Z3_rcf_num':
return 'Z3_rcf_num_plus'
elif ts == 'Z3_params':
return 'Z3_params_plus'
elif ts == 'Z3_param_descrs':
return 'Z3_param_descrs_plus'
elif ts == 'Z3_model':
return 'Z3_model_plus'
elif ts == 'Z3_func_interp':
return 'Z3_func_interp_plus'
elif ts == 'Z3_func_entry':
return 'Z3_func_entry_plus'
elif ts == 'Z3_goal':
return 'Z3_goal_plus'
elif ts == 'Z3_tactic':
return 'Z3_tactic_plus'
elif ts == 'Z3_probe':
return 'Z3_probe_plus'
elif ts == 'Z3_apply_result':
return 'Z3_apply_result_plus'
elif ts == 'Z3_solver':
return 'Z3_solver_plus'
elif ts == 'Z3_stats':
return 'Z3_stats_plus'
elif ts == 'Z3_ast_vector':
return 'Z3_ast_vector_plus'
elif ts == 'Z3_ast_map':
return 'Z3_ast_map_plus'
elif ts == 'Z3_fixedpoint':
return 'Z3_fixedpoint_plus'
elif ts == 'Z3_optimize':
return 'Z3_optimize_plus'
else:
return ts
def ml_minus_type(ts):
if ts == 'Z3_ast' or ts == 'Z3_sort' or ts == 'Z3_func_decl' or ts == 'Z3_app' or ts == 'Z3_pattern':
return 'Z3_ast'
elif ts == 'Z3_constructor_plus':
return 'Z3_constructor'
elif ts == 'Z3_constructor_list_plus':
return 'Z3_constructor_list'
elif ts == 'Z3_rcf_num_plus':
return 'Z3_rcf_num'
elif ts == 'Z3_params_plus':
return 'Z3_params'
elif ts == 'Z3_param_descrs_plus':
return 'Z3_param_descrs'
elif ts == 'Z3_model_plus':
return 'Z3_model'
elif ts == 'Z3_func_interp_plus':
return 'Z3_func_interp'
elif ts == 'Z3_func_entry_plus':
return 'Z3_func_entry'
elif ts == 'Z3_goal_plus':
return 'Z3_goal'
elif ts == 'Z3_tactic_plus':
return 'Z3_tactic'
elif ts == 'Z3_probe_plus':
return 'Z3_probe'
elif ts == 'Z3_apply_result_plus':
return 'Z3_apply_result'
elif ts == 'Z3_solver_plus':
return 'Z3_solver'
elif ts == 'Z3_stats_plus':
return 'Z3_stats'
elif ts == 'Z3_ast_vector_plus':
return 'Z3_ast_vector'
elif ts == 'Z3_ast_map_plus':
return 'Z3_ast_map'
elif ts == 'Z3_fixedpoint_plus':
return 'Z3_fixedpoint'
elif ts == 'Z3_optimize_plus':
return 'Z3_optimize'
else:
return ts
def ml_plus_type_raw(ts):
if ml_has_plus_type(ts):
return ml_plus_type(ts) + '_raw';
else:
return ts
def ml_plus_ops_type(ts):
if ml_has_plus_type(ts):
return ml_plus_type(ts) + '_custom_ops'
else:
return 'Z3_default_custom_ops'
def ml_has_plus_type(ts):
return ts != ml_plus_type(ts)
def ml_unwrap(t, ts, s):
if t == STRING:
return '(' + ts + ') String_val(' + s + ')'
@ -1140,8 +1248,11 @@ def ml_unwrap(t, ts, s):
return '(' + ts + ') Unsigned_long_val(' + s + ')'
elif t == DOUBLE:
return '(' + ts + ') Double_val(' + s + ')'
elif ml_has_plus_type(ts):
pts = ml_plus_type(ts)
return '(' + ts + ') ' + ml_plus_type_raw(ts) + '((' + pts + '*) Data_custom_val(' + s + '))'
else:
return '* (' + ts + '*) Data_custom_val(' + s + ')'
return '* ((' + ts + '*) Data_custom_val(' + s + '))'
def ml_set_wrap(t, d, n):
if t == VOID:
@ -1158,78 +1269,43 @@ def ml_set_wrap(t, d, n):
return d + ' = caml_copy_string((const char*) ' + n + ');'
else:
ts = type2str(t)
return d + ' = caml_alloc_custom(&default_custom_ops, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));'
pts = ml_plus_type(ts)
return 'memcpy(Data_custom_val(' + d + '), &' + n + ', sizeof(' + pts + '));'
def mk_ml():
global Type2Str
if not is_ml_enabled():
return
ml_dir = get_component('ml').src_dir
def mk_z3native_ml(ml_dir):
ml_nativef = os.path.join(ml_dir, 'z3native.ml')
ml_nativefi = os.path.join(ml_dir, 'z3native.mli')
ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c')
ml_native = open(ml_nativef, 'w')
ml_i = open(ml_nativefi, 'w')
ml_native.write('(* Automatically generated file *)\n\n')
ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n')
ml_i.write('(* Automatically generated file *)\n\n')
ml_i.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n')
ml_i.write('(**/**)\n\n')
ml_native.write('open Z3enums\n\n')
ml_native.write('(**/**)\n')
ml_native.write('type ptr\n')
ml_i.write('type ptr\n')
ml_native.write('and z3_symbol = ptr\n')
ml_i.write('and z3_symbol = ptr\n')
for k, v in Type2Str.items():
if is_obj(k):
ml_native.write('and %s = ptr\n' % v.lower())
ml_i.write('and %s = ptr\n' % v.lower())
ml_native.write('\n')
ml_i.write('\n')
ml_native.write('external is_null : ptr -> bool\n = "n_is_null"\n\n')
ml_native.write('external mk_null : unit -> ptr\n = "n_mk_null"\n\n')
ml_native.write('external set_internal_error_handler : ptr -> unit\n = "n_set_internal_error_handler"\n\n')
ml_native.write('exception Exception of string\n\n')
ml_i.write('val is_null : ptr -> bool\n')
ml_i.write('val mk_null : unit -> ptr\n')
ml_i.write('val set_internal_error_handler : ptr -> unit\n\n')
ml_i.write('exception Exception of string\n\n')
# ML declarations
ml_pref = open(os.path.join(ml_dir, 'z3native.ml.pre'), 'r')
for s in ml_pref:
ml_native.write(s);
ml_pref.close()
ml_native.write('module ML2C = struct\n\n')
for name, result, params in _dotnet_decls:
ml_native.write(' external n_%s : ' % ml_method_name(name))
ml_i.write('val %s : ' % ml_method_name(name))
ip = inparams(params)
op = outparams(params)
if len(ip) == 0:
ml_native.write(' unit -> ')
ml_i.write(' unit -> ')
for p in ip:
ml_native.write('%s -> ' % param2ml(p))
ml_i.write('%s -> ' % param2ml(p))
if len(op) > 0:
ml_native.write('(')
ml_i.write('(')
first = True
if result != VOID or len(op) == 0:
ml_native.write('%s' % type2ml(result))
ml_i.write('%s' % type2ml(result))
first = False
for p in op:
if first:
first = False
else:
ml_native.write(' * ')
ml_i.write(' * ')
ml_native.write('%s' % param2ml(p))
ml_i.write('%s' % param2ml(p))
if len(op) > 0:
ml_native.write(')')
ml_i.write(')')
ml_native.write('\n')
ml_i.write('\n')
if len(ip) > 5:
ml_native.write(' = "n_%s_bytecode"\n' % ml_method_name(name))
ml_native.write(' "n_%s"\n' % ml_method_name(name))
@ -1237,7 +1313,6 @@ def mk_ml():
ml_native.write(' = "n_%s"\n' % ml_method_name(name))
ml_native.write('\n')
ml_native.write(' end\n\n')
ml_i.write('\n(**/**)\n')
# Exception wrappers
for name, result, params in _dotnet_decls:
@ -1284,91 +1359,22 @@ def mk_ml():
ml_native.write(' res\n')
ml_native.write('\n')
ml_native.write('(**/**)\n')
ml_native.close()
# C interface
if is_verbose():
print ('Generated "%s"' % ml_nativef)
def mk_z3native_stubs_c(ml_dir): # C interface
ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c')
ml_wrapper = open(ml_wrapperf, 'w')
ml_wrapper.write('// Automatically generated file\n\n')
ml_wrapper.write('#include <stddef.h>\n')
ml_wrapper.write('#include <string.h>\n\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('extern "C" {\n')
ml_wrapper.write('#endif\n')
ml_wrapper.write('#include <caml/mlvalues.h>\n')
ml_wrapper.write('#include <caml/memory.h>\n')
ml_wrapper.write('#include <caml/alloc.h>\n')
ml_wrapper.write('#include <caml/fail.h>\n')
ml_wrapper.write('#include <caml/callback.h>\n')
ml_wrapper.write('#ifdef Custom_tag\n')
ml_wrapper.write('#include <caml/custom.h>\n')
ml_wrapper.write('#include <caml/bigarray.h>\n')
ml_wrapper.write('#endif\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('}\n')
ml_wrapper.write('#endif\n\n')
ml_wrapper.write('#include <z3.h>\n')
ml_wrapper.write('#include <z3native_stubs.h>\n\n')
ml_wrapper.write('#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal1(X6) \n')
ml_wrapper.write('#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal2(X6,X7) \n')
ml_wrapper.write('#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n')
ml_wrapper.write(' CAMLlocal5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLlocal3(X6,X7,X8) \n')
ml_wrapper.write('\n')
ml_wrapper.write('#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam2(X6,X7) \n')
ml_wrapper.write('#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam3(X6,X7,X8) \n')
ml_wrapper.write('#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam4(X6,X7,X8,X9) \n')
ml_wrapper.write('#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n')
ml_wrapper.write(' CAMLxparam2(X11,X12) \n')
ml_wrapper.write('#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \\\n')
ml_wrapper.write(' CAMLparam5(X1,X2,X3,X4,X5); \\\n')
ml_wrapper.write(' CAMLxparam5(X6,X7,X8,X9,X10); \\\n')
ml_wrapper.write(' CAMLxparam3(X11,X12,X13) \n')
ml_wrapper.write('\n\n')
ml_wrapper.write('static struct custom_operations default_custom_ops = {\n')
ml_wrapper.write(' (char*) "default handling",\n')
ml_wrapper.write(' custom_finalize_default,\n')
ml_wrapper.write(' custom_compare_default,\n')
ml_wrapper.write(' custom_hash_default,\n')
ml_wrapper.write(' custom_serialize_default,\n')
ml_wrapper.write(' custom_deserialize_default\n')
ml_wrapper.write('};\n\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('extern "C" {\n')
ml_wrapper.write('#endif\n\n')
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_is_null(value p) {\n')
ml_wrapper.write(' void * t = * (void**) Data_custom_val(p);\n')
ml_wrapper.write(' return Val_bool(t == 0);\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_mk_null( void ) {\n')
ml_wrapper.write(' CAMLparam0();\n')
ml_wrapper.write(' CAMLlocal1(result);\n')
ml_wrapper.write(' void * z3_result = 0;\n')
ml_wrapper.write(' result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1);\n')
ml_wrapper.write(' memcpy( Data_custom_val(result), &z3_result, sizeof(void*));\n')
ml_wrapper.write(' CAMLreturn (result);\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('void MLErrorHandler(Z3_context c, Z3_error_code e)\n')
ml_wrapper.write('{\n')
ml_wrapper.write(' // Internal do-nothing error handler. This is required to avoid that Z3 calls exit()\n')
ml_wrapper.write(' // upon errors, but the actual error handling is done by throwing exceptions in the\n')
ml_wrapper.write(' // wrappers below.\n')
ml_wrapper.write('}\n\n')
ml_wrapper.write('void DLL_PUBLIC n_set_internal_error_handler(value a0)\n')
ml_wrapper.write('{\n')
ml_wrapper.write(' Z3_context _a0 = * (Z3_context*) Data_custom_val(a0);\n')
ml_wrapper.write(' Z3_set_error_handler(_a0, MLErrorHandler);\n')
ml_wrapper.write('}\n\n')
ml_pref = open(os.path.join(ml_dir, 'z3native_stubs.c.pre'), 'r')
for s in ml_pref:
ml_wrapper.write(s);
ml_pref.close()
for name, result, params in _dotnet_decls:
ip = inparams(params)
op = outparams(params)
@ -1410,7 +1416,7 @@ def mk_ml():
for p in params:
if is_out_param(p) or is_array_param(p):
c = c + 1
ml_wrapper.write(' CAMLlocal%s(result, res_val' % (c+2))
ml_wrapper.write(' CAMLlocal%s(result, z3rv_val' % (c+2))
for p in params:
if is_out_param(p) or is_array_param(p):
ml_wrapper.write(', _a%s_val' % i)
@ -1423,45 +1429,63 @@ def mk_ml():
# declare locals, preprocess arrays, strings, in/out arguments
i = 0
for param in params:
k = param_kind(param)
if k == OUT_ARRAY:
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
if param_type(param) == CONTEXT and i == 0:
ml_wrapper.write(' Z3_context_plus * ctx_p = (Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
ml_wrapper.write(' Z3_context _a0 = ctx_p->ctx;\n')
else:
k = param_kind(param)
if k == OUT_ARRAY:
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
type2str(param_type(param)),
i,
type2str(param_type(param)),
type2str(param_type(param)),
param_array_capacity_pos(param)))
elif k == OUT_MANAGED_ARRAY:
ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param)))
elif k == IN:
t = param_type(param)
ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i))))
elif k == OUT:
ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
elif k == INOUT:
ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i))
elif k == OUT_MANAGED_ARRAY:
ml_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param)))
elif k == IN:
t = param_type(param)
ml_wrapper.write(' %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i))))
elif k == OUT:
ml_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
elif k == INOUT:
ml_wrapper.write(' %s _a%s = a%s;\n' % (type2str(param_type(param)), i, i))
i = i + 1
if result != VOID:
ml_wrapper.write(' %s z3_result;\n' % type2str(result))
i = 0
for param in params:
k = param_kind(param)
if k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { _a%s[_i] = %s; }\n' % (param_array_capacity_pos(param), i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', _i)')))
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(param))
ml_wrapper.write(' _a%s[_i] = %s;\n' % (i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', _i)')))
ml_wrapper.write(' }\n')
i = i + 1
# invoke procedure
ml_wrapper.write(' ')
need_closing_paren = False
if result != VOID:
ml_wrapper.write('z3_result = ')
ts = type2str(result)
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
ml_wrapper.write('result = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (ml_plus_ops_type(ts), pts))
if ts == 'Z3_context':
ml_wrapper.write(' %s z3rv = %s_mk(' % (pts, pts))
else:
ml_wrapper.write(' %s z3rv = %s_mk(ctx_p, (%s) ' % (pts, pts, ml_minus_type(ts)))
need_closing_paren = True
else:
ml_wrapper.write('result = caml_alloc(%s, 0);\n' % ret_size)
ml_wrapper.write(' %s z3rv = ' % ts)
elif len(op) != 0:
ml_wrapper.write('result = caml_alloc(%s, 0);\n ' % ret_size)
# invoke procedure
ml_wrapper.write('%s(' % name)
i = 0
first = True
@ -1476,31 +1500,51 @@ def mk_ml():
else:
ml_wrapper.write('_a%i' % i)
i = i + 1
ml_wrapper.write(');\n')
ml_wrapper.write(')')
if need_closing_paren:
ml_wrapper.write(')');
ml_wrapper.write(';\n')
# convert output params
if len(op) > 0:
if result != VOID:
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "res_val", "z3_result"))
i = 0
for p in params:
if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
ml_wrapper.write(' _a%s_val = caml_alloc(_a%s, 0);\n' % (i, param_array_capacity_pos(p)))
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) { value t; %s Store_field(_a%s_val, _i, t); }\n' % (param_array_capacity_pos(p), ml_set_wrap(param_type(p), 't', '_a' + str(i) + '[_i]'), i))
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(p))
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
ml_wrapper.write(' value t;\n')
ml_wrapper.write(' t = caml_alloc_custom(&%s, sizeof(%s), 0, 1);\n' % (ml_plus_ops_type(ts), pts))
ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i]);\n' % (pts, i, pts, ml_minus_type(ts), i))
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), 't', '_a%dp' % i))
else:
ml_wrapper.write(' value t;\n')
ml_wrapper.write(' t = caml_alloc_custom(&default_custom_ops, sizeof(%s), 0, 1);\n' % (ts))
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), 't', '_a%d[_i]' % i))
ml_wrapper.write(' Store_field(_a%s_val, _i, t);\n' % i)
ml_wrapper.write(' }\n')
elif param_kind(p) == OUT_MANAGED_ARRAY:
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), '_a%d_val' % i, '_a%d' % i))
elif is_out_param(p):
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
pt = param_type(p)
ts = type2str(pt)
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (pts, i, pts, ml_minus_type(ts), i))
ml_wrapper.write(' %s\n' % ml_set_wrap(pt, '_a%d_val' % i, '_a%dp' % i))
else:
ml_wrapper.write(' %s\n' % ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i))
i = i + 1
# return tuples
if len(op) == 0:
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3_result"))
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "result", "z3rv"))
else:
ml_wrapper.write(' result = caml_alloc(%s, 0);\n' % ret_size)
i = j = 0
if result != VOID:
ml_wrapper.write(' Store_field(result, 0, res_val);\n')
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "z3rv_val", "z3rv"))
ml_wrapper.write(' Store_field(result, 0, z3rv_val);\n')
j = j + 1
for p in params:
if is_out_param(p):
@ -1535,7 +1579,17 @@ def mk_ml():
ml_wrapper.write('}\n')
ml_wrapper.write('#endif\n')
if is_verbose():
print ('Generated "%s"' % ml_nativef)
print ('Generated "%s"' % ml_wrapperf)
def mk_ml():
global Type2Str
if not is_ml_enabled():
return
ml_dir = get_component('ml').src_dir
mk_z3native_ml(ml_dir)
mk_z3native_stubs_c(ml_dir)
# Collect API(...) commands from
def def_APIs():

3558
src/api/ml/z3.ml
View file

File diff suppressed because it is too large Load diff

54
src/api/ml/z3.mli
View file

@ -244,33 +244,12 @@ sig
(** Translates (copies) the AST to another context.
@return A copy of the AST which is associated with the other context. *)
val translate : ast -> context -> ast
(** Unwraps an AST.
This function is used for transitions between native and
managed objects. It returns the native pointer to the AST. Note that
AST objects are reference counted and unwrapping an AST disables automatic
reference counting, i.e., all references to the IntPtr that is returned
must be handled externally and through native calls (see e.g.,
[Z3native.inc_ref]).
{!wrap_ast} *)
val unwrap_ast : ast -> Z3native.ptr
(** Wraps an AST.
This function is used for transitions between native and
managed objects. Note that the native ast that is passed must be a
native object obtained from Z3 (e.g., through {!unwrap_ast})
and that it must have a correct reference count (see e.g.,
[Z3native.inc_ref]). *)
val wrap_ast : context -> Z3native.z3_ast -> ast
end
(** The Sort module implements type information for ASTs *)
and Sort :
sig
type sort = Sort of AST.ast
val ast_of_sort : sort -> AST.ast
type sort
(** Comparison operator.
@return True if the two sorts are from the same context
@ -299,9 +278,7 @@ end
(** Function declarations *)
and FuncDecl :
sig
type func_decl = FuncDecl of AST.ast
val ast_of_func_decl : FuncDecl.func_decl -> AST.ast
type func_decl
(** Parameters of Func_Decls *)
module Parameter :
@ -473,7 +450,7 @@ end
(** General Expressions (terms) *)
and Expr :
sig
type expr = Expr of AST.ast
type expr
val ast_of_expr : Expr.expr -> AST.ast
val expr_of_ast : AST.ast -> Expr.expr
@ -662,7 +639,7 @@ end
(** Quantifier expressions *)
module Quantifier :
sig
type quantifier = Quantifier of Expr.expr
type quantifier
val expr_of_quantifier : quantifier -> Expr.expr
val quantifier_of_expr : Expr.expr -> quantifier
@ -674,10 +651,7 @@ sig
also called a multi-pattern. *)
module Pattern :
sig
type pattern = Pattern of AST.ast
val ast_of_pattern : pattern -> AST.ast
val pattern_of_ast : AST.ast -> pattern
type pattern
(** The number of terms in the pattern. *)
val get_num_terms : pattern -> int
@ -1078,7 +1052,6 @@ sig
(** Create mutually recursive data-types. *)
val mk_sorts_s : context -> string list -> Constructor.constructor list list -> Sort.sort list
(** The number of constructors of the datatype sort. *)
val get_num_constructors : Sort.sort -> int
@ -3241,8 +3214,7 @@ end
module Optimize :
sig
type optimize
type handle
type handle
(** Create a Optimize context. *)
val mk_opt : context -> optimize
@ -3250,31 +3222,25 @@ sig
(** A string that describes all available optimize solver parameters. *)
val get_help : optimize -> string
(** Sets the optimize solver parameters. *)
val set_parameters : optimize -> Params.params -> unit
(** Retrieves parameter descriptions for Optimize solver. *)
val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs
(** Assert a constraints into the optimize solver. *)
val add : optimize -> Expr.expr list -> unit
(** Asssert a soft constraint.
Supply integer weight and string that identifies a group
of soft constraints.
*)
val add_soft : optimize -> Expr.expr -> string -> Symbol.symbol -> handle
(** Add maximization objective.
*)
val maximize : optimize -> Expr.expr -> handle
(** Add minimization objective.
*)
val minimize : optimize -> Expr.expr -> handle
@ -3283,38 +3249,30 @@ sig
*)
val check : optimize -> Solver.status
(** Retrieve model from satisfiable context *)
val get_model : optimize -> Model.model option
(** Retrieve lower bound in current model for handle *)
val get_lower : handle -> int -> Expr.expr
(** Retrieve upper bound in current model for handle *)
val get_upper : handle -> int -> Expr.expr
(** Creates a backtracking point.
{!pop} *)
val push : optimize -> unit
(** Backtrack one backtracking point.
Note that an exception is thrown if Pop is called without a corresponding [Push]
{!push} *)
val pop : optimize -> unit
(** Retrieve explanation why optimize engine returned status Unknown. *)
val get_reason_unknown : optimize -> string
(** Retrieve SMT-LIB string representation of optimize object. *)
val to_string : optimize -> string
(** Retrieve statistics information from the last call to check *)
val get_statistics : optimize -> Statistics.statistics
end

107
src/api/ml/z3native.ml.pre Normal file
View file

@ -0,0 +1,107 @@
(** The native (raw) interface to the dynamic Z3 library. *)
open Z3enums
(**/**)
type ptr
and symbol = ptr
and config = ptr
and context = ptr
and ast = ptr
and app = ast
and sort = ast
and func_decl = ast
and pattern = ast
and model = ptr
and literals = ptr
and constructor = ptr
and constructor_list = ptr
and solver = ptr
and goal = ptr
and tactic = ptr
and params = ptr
and probe = ptr
and stats = ptr
and ast_vector = ptr
and ast_map = ptr
and apply_result = ptr
and func_interp = ptr
and func_entry = ptr
and fixedpoint = ptr
and optimize = ptr
and param_descrs = ptr
and rcf_num = ptr
external is_null : ptr -> bool
= "n_is_null"
external mk_null : unit -> ptr
= "n_mk_null"
external set_internal_error_handler : ptr -> unit
= "n_set_internal_error_handler"
external context_of_symbol : symbol -> context
= "n_context_of_symbol"
external context_of_constructor : constructor -> context
= "n_context_of_constructor"
external context_of_constructor_list : constructor_list -> context
= "n_context_of_constructor_list"
external context_of_rcf_num : rcf_num -> context
= "n_context_of_rcf_num"
external context_of_ast : ast -> context
= "n_context_of_ast"
external context_of_params : params -> context
= "n_context_of_params"
external context_of_param_descrs : param_descrs -> context
= "n_context_of_param_descrs"
external context_of_model : model -> context
= "n_context_of_model"
external context_of_func_interp : func_interp -> context
= "n_context_of_func_interp"
external context_of_func_entry : func_entry -> context
= "n_context_of_func_entry"
external context_of_goal : goal -> context
= "n_context_of_goal"
external context_of_tactic : tactic -> context
= "n_context_of_tactic"
external context_of_probe : probe -> context
= "n_context_of_probe"
external context_of_apply_result : apply_result -> context
= "n_context_of_apply_result"
external context_of_solver : solver -> context
= "n_context_of_solver"
external context_of_stats : stats -> context
= "n_context_of_stats"
external context_of_ast_vector : ast_vector -> context
= "n_context_of_ast_vector"
external context_of_ast_map : ast_map -> context
= "n_context_of_ast_map"
external context_of_fixedpoint : fixedpoint -> context
= "n_context_of_fixedpoint"
external context_of_optimize : optimize -> context
= "n_context_of_optimize"
exception Exception of string

384
src/api/ml/z3native_stubs.c.pre Normal file
View file

@ -0,0 +1,384 @@
#include <stddef.h>
#include <string.h>
#include <assert.h>
#ifdef __cplusplus
extern "C" {
#endif
#include <caml/mlvalues.h>
#include <caml/memory.h>
#include <caml/alloc.h>
#include <caml/fail.h>
#include <caml/callback.h>
#ifdef Custom_tag
#include <caml/custom.h>
#include <caml/bigarray.h>
#endif
#ifdef __cplusplus
}
#endif
#include <z3.h>
#include <z3native_stubs.h>
#define CAMLlocal6(X1,X2,X3,X4,X5,X6) \
CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal1(X6)
#define CAMLlocal7(X1,X2,X3,X4,X5,X6,X7) \
CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal2(X6,X7)
#define CAMLlocal8(X1,X2,X3,X4,X5,X6,X7,X8) \
CAMLlocal5(X1,X2,X3,X4,X5); \
CAMLlocal3(X6,X7,X8)
#define CAMLparam7(X1,X2,X3,X4,X5,X6,X7) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam2(X6,X7)
#define CAMLparam8(X1,X2,X3,X4,X5,X6,X7,X8) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam3(X6,X7,X8)
#define CAMLparam9(X1,X2,X3,X4,X5,X6,X7,X8,X9) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam4(X6,X7,X8,X9)
#define CAMLparam12(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam2(X11,X12)
#define CAMLparam13(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13) \
CAMLparam5(X1,X2,X3,X4,X5); \
CAMLxparam5(X6,X7,X8,X9,X10); \
CAMLxparam3(X11,X12,X13)
static struct custom_operations default_custom_ops = {
(char*) "default handling",
custom_finalize_default,
custom_compare_default,
custom_hash_default,
custom_serialize_default,
custom_deserialize_default,
custom_compare_ext_default,
};
#define MK_CTX_OF(X) \
Z3_context_plus * n_context_of_ ## X(Z3_ ## X ## _plus * p) { return p->cp; }
// Context objects
typedef struct {
Z3_context ctx;
unsigned long ast_count;
} Z3_context_plus;
Z3_context_plus Z3_context_plus_mk(Z3_context c) {
Z3_context_plus r;
r.ctx = c;
r.ast_count = 0;
printf("ctx++\n");
return r;
}
Z3_context Z3_context_plus_raw(Z3_context_plus * cp) {
return cp->ctx;
}
void Z3_context_finalize(value v) {
Z3_context_plus * cp = (Z3_context_plus*)Data_custom_val(v);
printf("ctx--; cnt=%lu\n", cp->ast_count);
Z3_del_context(cp->ctx);
}
static struct custom_operations Z3_context_plus_custom_ops = {
(char*) "Z3_context ops",
Z3_context_finalize,
custom_compare_default,
custom_hash_default,
custom_serialize_default,
custom_deserialize_default,
custom_compare_ext_default,
};
// Symbol objects
typedef struct {
Z3_context_plus * cp;
Z3_symbol s;
} Z3_symbol_plus;
Z3_symbol_plus Z3_symbol_plus_mk(Z3_context_plus * cp, Z3_symbol s) {
Z3_symbol_plus r;
r.cp = cp;
r.s = s;
return r;
}
Z3_symbol Z3_symbol_plus_raw(Z3_symbol_plus * sp) {
return sp->s;
}
static struct custom_operations Z3_symbol_plus_custom_ops = {
(char*) "Z3_symbol ops",
custom_finalize_default,
custom_compare_default,
custom_hash_default,
custom_serialize_default,
custom_deserialize_default,
custom_compare_ext_default,
};
MK_CTX_OF(symbol)
// AST objects
typedef struct {
Z3_context_plus * cp;
Z3_ast a;
} Z3_ast_plus;
Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus * cp, Z3_ast a) {
Z3_ast_plus r;
r.cp = cp;
r.a = a;
printf("++\n");
Z3_inc_ref(cp->ctx, a);
cp->ast_count++;
return r;
}
Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) {
return ap->a;
}
void Z3_ast_finalize(value v) {
printf("--\n");
Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v));
Z3_dec_ref(ap->cp->ctx, ap->a);
ap->cp->ast_count--;
}
int Z3_ast_compare(value v1, value v2) {
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
Z3_ast_plus * a2 = (Z3_ast_plus*)Data_custom_val(v2);
assert(a1->cp->ctx == a2->cp->ctx);
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->a);
unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->a);
if (id1 == id2)
return 0;
else if (id1 < id2)
return -1;
else
return +1;
}
int Z3_ast_compare_ext(value v1, value v2) {
Z3_ast_plus * a1 = (Z3_ast_plus*)Data_custom_val(v1);
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->a);
int id2 = Val_int(v2);
if (id1 == id2)
return 0;
else if (id1 < id2)
return -1;
else
return +1;
}
intnat Z3_ast_hash(value v) {
Z3_ast_plus * ap = (Z3_ast_plus*)Data_custom_val(v);
return Z3_get_ast_hash(ap->cp->ctx, ap->a);
}
static struct custom_operations Z3_ast_plus_custom_ops = {
(char*) "Z3_ast ops",
Z3_ast_finalize,
Z3_ast_compare,
Z3_ast_hash,
custom_serialize_default,
custom_deserialize_default,
Z3_ast_compare_ext
};
MK_CTX_OF(ast)
// Constructor objects
typedef struct {
Z3_context_plus * cp;
Z3_constructor c;
} Z3_constructor_plus;
Z3_constructor_plus Z3_constructor_plus_mk(Z3_context_plus * cp, Z3_constructor c) {
Z3_constructor_plus r;
r.cp = cp;
r.c = c;
return r;
}
Z3_constructor Z3_constructor_plus_raw(Z3_constructor_plus * cp) {
return cp->c;
}
static struct custom_operations Z3_constructor_plus_custom_ops = {
(char*) "Z3_constructor ops",
custom_finalize_default,
custom_compare_default,
custom_hash_default,
custom_serialize_default,
custom_deserialize_default,
custom_compare_ext_default,
};
MK_CTX_OF(constructor)
// constructor_list objects
typedef struct {
Z3_context_plus * cp;
Z3_constructor_list c;
} Z3_constructor_list_plus;
Z3_constructor_list_plus Z3_constructor_list_plus_mk(Z3_context_plus * cp, Z3_constructor_list c) {
Z3_constructor_list_plus r;
r.cp = cp;
r.c = c;
return r;
}
Z3_constructor_list Z3_constructor_list_plus_raw(Z3_constructor_list_plus * cp) {
return cp->c;
}
static struct custom_operations Z3_constructor_list_plus_custom_ops = {
(char*) "Z3_constructor_list ops",
custom_finalize_default,
custom_compare_default,
custom_hash_default,
custom_serialize_default,
custom_deserialize_default,
custom_compare_ext_default,
};
MK_CTX_OF(constructor_list)
// rcf_num objects
typedef struct {
Z3_context_plus * cp;
Z3_rcf_num c;
} Z3_rcf_num_plus;
Z3_rcf_num_plus Z3_rcf_num_plus_mk(Z3_context_plus * cp, Z3_rcf_num c) {
Z3_rcf_num_plus r;
r.cp = cp;
r.c = c;
return r;
}
Z3_rcf_num Z3_rcf_num_plus_raw(Z3_rcf_num_plus * cp) {
return cp->c;
}
static struct custom_operations Z3_rcf_num_plus_custom_ops = {
(char*) "Z3_rcf_num ops",
custom_finalize_default,
custom_compare_default,
custom_hash_default,
custom_serialize_default,
custom_deserialize_default,
custom_compare_ext_default,
};
MK_CTX_OF(rcf_num)
#define MK_PLUS_OBJ(X) \
typedef struct { \
Z3_context_plus * cp; \
Z3_ ## X p; \
} Z3_ ## X ## _plus; \
\
Z3_ ## X ## _plus Z3_ ## X ## _plus_mk(Z3_context_plus * cp, Z3_ ## X p) { \
Z3_ ## X ## _plus r; \
r.cp = cp; \
r.p = p; \
Z3_ ## X ## _inc_ref(cp->ctx, p); \
return r; \
} \
\
Z3_ ## X Z3_ ## X ## _plus_raw(Z3_ ## X ## _plus * pp) { \
return pp->p; \
} \
\
void Z3_ ## X ## _finalize(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \
} \
\
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \
custom_compare_default, \
custom_hash_default, \
custom_serialize_default, \
custom_deserialize_default, \
custom_compare_ext_default, \
}; \
\
MK_CTX_OF(X)
MK_PLUS_OBJ(params)
MK_PLUS_OBJ(param_descrs)
MK_PLUS_OBJ(model)
MK_PLUS_OBJ(func_interp)
MK_PLUS_OBJ(func_entry)
MK_PLUS_OBJ(goal)
MK_PLUS_OBJ(tactic)
MK_PLUS_OBJ(probe)
MK_PLUS_OBJ(apply_result)
MK_PLUS_OBJ(solver)
MK_PLUS_OBJ(stats)
MK_PLUS_OBJ(ast_map)
MK_PLUS_OBJ(ast_vector)
MK_PLUS_OBJ(fixedpoint)
MK_PLUS_OBJ(optimize)
#ifdef __cplusplus
extern "C" {
#endif
CAMLprim DLL_PUBLIC value n_is_null(value p) {
void * t = * (void**) Data_custom_val(p);
return Val_bool(t == 0);
}
CAMLprim DLL_PUBLIC value n_mk_null( void ) {
CAMLparam0();
CAMLlocal1(result);
void * z3_result = 0;
result = caml_alloc_custom(&default_custom_ops, sizeof(void*), 0, 1);
memcpy( Data_custom_val(result), &z3_result, sizeof(void*));
CAMLreturn (result);
}
void MLErrorHandler(Z3_context c, Z3_error_code e)
{
// Internal do-nothing error handler. This is required to avoid that Z3 calls exit()
// upon errors, but the actual error handling is done by throwing exceptions in the
// wrappers below.
}
void DLL_PUBLIC n_set_internal_error_handler(value a0)
{
Z3_context _a0 = * (Z3_context*) Data_custom_val(a0);
Z3_set_error_handler(_a0, MLErrorHandler);
}