mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-05-03 11:09:14 -07:00
parent 91af947863 cf34a2b1d9
commit 52e367417f
8 changed files with 2878 additions and 3411 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
examples/ml/ml_example.ml
View file

@ -190,9 +190,10 @@ let basic_tests ( ctx : context ) =
(* Error handling test. *)
try (
let i = Integer.mk_numeral_s ctx "1/2" in
raise (TestFailedException (numeral_to_string i)) (* unreachable *)
Printf.printf "%s\n" (Expr.to_string i) ;
raise (TestFailedException "check")
)
with Z3native.Exception(_) -> (
with Z3.Error(_) -> (
Printf.printf "Exception caught, OK.\n"
)
@ -342,7 +343,7 @@ let _ =
);
Printf.printf "Exiting.\n" ;
exit 0
) with Z3native.Exception(msg) -> (
) with Error(msg) -> (
Printf.printf "Z3 EXCEPTION: %s\n" msg ;
exit 1
)

2
scripts/mk_make.py
View file

@ -19,5 +19,3 @@ mk_bindings(API_files)
mk_vs_proj('z3', ['shell'])
mk_vs_proj_dll('libz3', ['api_dll'])
mk_makefile()

209
scripts/mk_util.py
View file

@ -69,6 +69,7 @@ IS_LINUX=False
IS_OSX=False
IS_FREEBSD=False
IS_OPENBSD=False
IS_CYGWIN=False
VERBOSE=True
DEBUG_MODE=False
SHOW_CPPS = True
@ -139,6 +140,9 @@ def is_openbsd():
def is_osx():
return IS_OSX
def is_cygwin():
return IS_CYGWIN
def norm_path(p):
# We use '/' on mk_project for convenience
return os.path.join(*(p.split('/')))
@ -591,6 +595,8 @@ elif os.name == 'posix':
IS_FREEBSD=True
elif os.uname()[0] == 'OpenBSD':
IS_OPENBSD=True
elif os.uname()[0][:6] == 'CYGWIN':
IS_CYGWIN=True
def display_help(exit_code):
print("mk_make.py: Z3 Makefile generator\n")
@ -1691,6 +1697,8 @@ class JavaDLLComponent(Component):
t = t.replace('PLATFORM', 'freebsd')
elif IS_OPENBSD:
t = t.replace('PLATFORM', 'openbsd')
elif IS_CYGWIN:
t = t.replace('PLATFORM', 'cygwin')
else:
t = t.replace('PLATFORM', 'win32')
out.write(t)
@ -1808,6 +1816,16 @@ class MLComponent(Component):
def mk_makefile(self, out):
if is_ml_enabled():
CP_CMD = 'cp'
if IS_WINDOWS:
CP_CMD='copy'
OCAML_FLAGS = ''
if DEBUG_MODE:
OCAML_FLAGS += '-g'
OCAMLCF = OCAMLC + ' ' + OCAML_FLAGS
OCAMLOPTF = OCAMLOPT + ' ' + OCAML_FLAGS
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
@ -1824,51 +1842,52 @@ 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)'
out.write('%s: %s %s\n' % (stubso, stubsc, z3dllso))
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
(OCAMLCF, OCAML_LIB, api_src, src_dir, stubso, stubsc))
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' % (OCAMLCF, self.sub_dir, ml, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, self.sub_dir, cmi, mli))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLCF, 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('\t%s -I %s -o %s -c %s\n' % (OCAMLOPT, self.sub_dir, ft, ff))
out.write('%s: %s %s\n' % (ft, ff, cmos))
out.write('\t%s -I %s -o %s -c %s\n' % (OCAMLOPTF, self.sub_dir, ft, ff))
cmxs = cmxs + ' ' + ft
OCAMLMKLIB = 'ocamlmklib'
LIBZ3 = '-L. -lz3'
if is_cygwin():
# Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
LIBZ3 = 'libz3.dll'
elif DEBUG_MODE:
OCAMLMKLIB += ' -g'
z3mls = os.path.join(self.sub_dir, 'z3ml')
out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmos))
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
out.write('%s.cmxa: %s %s %s\n' % (z3mls, cmxs, stubso, z3dllso))
out.write('\tocamlmklib -o %s -I %s %s %s -L. -lz3\n' % (z3mls, self.sub_dir, stubso, cmxs))
out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmxs, LIBZ3))
out.write('%s.cmxs: %s.cmxa\n' % (z3mls, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPT, z3mls, self.sub_dir, z3mls))
out.write('\t%s -shared -o %s.cmxs -I %s %s.cmxa\n' % (OCAMLOPTF, z3mls, self.sub_dir, z3mls))
out.write('\n')
out.write('ml: %s.cma %s.cmxa %s.cmxs\n' % (z3mls, z3mls, z3mls))
@ -1911,7 +1930,11 @@ class MLComponent(Component):
metafile=os.path.join(self.sub_dir, 'META')))
for m in self.modules:
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(' ' + os.path.join(self.sub_dir, m) + '.cmx')
out.write(' %s' % ((os.path.join(self.sub_dir, 'libz3ml$(LIB_EXT)'))))
@ -2863,78 +2886,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

455
scripts/update_api.py
View file

@ -141,7 +141,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)
@ -261,9 +265,9 @@ def param2ml(p):
else:
return "ptr"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s array" % type2ml(param_type(p))
return "%s list" % type2ml(param_type(p))
elif k == OUT_MANAGED_ARRAY:
return "%s array" % type2ml(param_type(p))
return "%s list" % type2ml(param_type(p))
else:
return type2ml(param_type(p))
@ -385,7 +389,7 @@ def mk_dotnet(dotnet):
dotnet.write(' }\n')
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ]
Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
def mk_dotnet_wrappers(dotnet):
@ -1039,11 +1043,115 @@ def arrayparams(params):
op.append(param)
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'
if ts == 'Z3_ast_plus' or ts == 'Z3_sort_plus' or ts == 'Z3_func_decl_plus' or ts == 'Z3_app_plus' or ts == 'Z3_pattern_plus':
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 '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 + ')'
elif t == BOOL:
elif t == BOOL or (type2str(t) == 'Z3_bool'):
return '(' + ts + ') Bool_val(' + s + ')'
elif t == INT or t == PRINT_MODE or t == ERROR_CODE:
return '(' + ts + ') Int_val(' + s + ')'
@ -1055,232 +1163,105 @@ 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:
return d + ' = Val_unit;'
elif t == BOOL:
elif t == BOOL or (type2str(t) == 'Z3_bool'):
return d + ' = Val_bool(' + n + ');'
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE:
return d + ' = Val_int(' + n + ');'
elif t == INT64 or t == UINT64:
return d + ' = Val_long(' + n + ');'
elif t == DOUBLE:
return 'Store_double_val(' + d + ', ' + n + ');'
return d + '= caml_copy_double(' + n + ');'
elif t == STRING:
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(type2str(t))
return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';'
def ml_alloc_and_store(t, lhs, rhs):
if t == VOID or t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == INT64 or t == UINT64 or t == DOUBLE or t == STRING or (type2str(t) == 'Z3_bool'):
return ml_set_wrap(t, lhs, rhs)
else:
pts = ml_plus_type(type2str(t))
pops = ml_plus_ops_type(type2str(t))
alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts)
return alloc_str + ml_set_wrap(t, lhs, rhs)
def mk_ml(ml_dir):
global Type2Str
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_native.write('module ML2C = struct\n\n')
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('\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))
ml_native.write('external %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))
ml_native.write(' = "n_%s_bytecode" "n_%s"\n' % (ml_method_name(name), ml_method_name(name)))
else:
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:
ip = inparams(params)
op = outparams(params)
ml_native.write(' let %s ' % ml_method_name(name))
# null pointer helpers
for type_id in Type2Str:
type_name = Type2Str[type_id]
if ml_has_plus_type(type_name) and not type_name in ['Z3_context', 'Z3_sort', 'Z3_func_decl', 'Z3_app', 'Z3_pattern']:
ml_name = type2ml(type_id)
ml_native.write('external context_of_%s : %s -> context = "n_context_of_%s"\n' % (ml_name, ml_name, ml_name))
ml_native.write('external is_null_%s : %s -> bool = "n_is_null_%s"\n' % (ml_name, ml_name, ml_name))
ml_native.write('external mk_null_%s : context -> %s = "n_mk_null_%s"\n\n' % (ml_name, ml_name, ml_name))
first = True
i = 0
for p in params:
if is_in_param(p):
if first:
first = False
else:
ml_native.write(' ')
ml_native.write('a%d' % i)
i = i + 1
if len(ip) == 0:
ml_native.write('()')
ml_native.write(' = \n')
ml_native.write(' ')
if result == VOID and len(op) == 0:
ml_native.write('let _ = ')
else:
ml_native.write('let res = ')
ml_native.write('(ML2C.n_%s' % (ml_method_name(name)))
if len(ip) == 0:
ml_native.write(' ()')
first = True
i = 0
for p in params:
if is_in_param(p):
ml_native.write(' a%d' % i)
i = i + 1
ml_native.write(') in\n')
if name not in Unwrapped and len(params) > 0 and param_type(params[0]) == CONTEXT:
ml_native.write(' let err = (error_code_of_int (ML2C.n_get_error_code a0)) in \n')
ml_native.write(' if err <> OK then\n')
ml_native.write(' raise (Exception (ML2C.n_get_error_msg a0 (int_of_error_code err)))\n')
ml_native.write(' else\n')
if result == VOID and len(op) == 0:
ml_native.write(' ()\n')
else:
ml_native.write(' res\n')
ml_native.write('\n')
ml_native.write('(**/**)\n')
ml_native.close()
# C interface
if mk_util.is_verbose():
print ('Generated "%s"' % ml_nativef)
mk_z3native_stubs_c(ml_dir)
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)
@ -1319,22 +1300,39 @@ def mk_ml(ml_dir):
ml_wrapper.write(' CAMLlocal1(result);\n')
else:
c = 0
needs_tmp_value = False
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))
needs_tmp_value = needs_tmp_value or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY
if needs_tmp_value:
c = c + 1
if len(ap) > 0:
c = c + 1
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)
i = i + 1
if needs_tmp_value:
ml_wrapper.write(', tmp_val')
if len(ap) != 0:
ml_wrapper.write(', _iter');
ml_wrapper.write(');\n')
if len(ap) != 0:
if len(ap) > 0:
ml_wrapper.write(' unsigned _i;\n')
# declare locals, preprocess arrays, strings, in/out arguments
have_context = False
i = 0
for param in params:
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')
have_context = True
else:
k = param_kind(param)
if k == OUT_ARRAY:
ml_wrapper.write(' %s * _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
@ -1358,22 +1356,30 @@ def mk_ml(ml_dir):
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(' _iter = a' + str(i) + ';\n')
ml_wrapper.write(' for (_i = 0; _i < _a%s; _i++) {\n' % param_array_capacity_pos(param))
ml_wrapper.write(' assert(_iter != Val_emptylist);\n')
ml_wrapper.write(' _a%s[_i] = %s;\n' % (i, ml_unwrap(t, ts, 'Field(_iter, 0)')))
ml_wrapper.write(' _iter = Field(_iter, 1);\n')
ml_wrapper.write(' }\n')
ml_wrapper.write(' assert(_iter == Val_emptylist);\n\n')
i = i + 1
# invoke procedure
ml_wrapper.write(' ')
ml_wrapper.write('\n /* invoke Z3 function */\n ')
if result != VOID:
ml_wrapper.write('z3_result = ')
ts = type2str(result)
if ml_has_plus_type(ts):
ml_wrapper.write('%s z3rv_m = ' % ts)
else:
ml_wrapper.write('%s z3rv = ' % ts)
# invoke procedure
ml_wrapper.write('%s(' % name)
i = 0
first = True
@ -1390,37 +1396,84 @@ def mk_ml(ml_dir):
i = i + 1
ml_wrapper.write(');\n')
if have_context and name not in Unwrapped:
ml_wrapper.write(' int ec = Z3_get_error_code(ctx_p->ctx);\n')
ml_wrapper.write(' if (ec != 0) {\n')
ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n')
ml_wrapper.write(' caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), msg);\n')
ml_wrapper.write(' }\n')
if result != VOID:
ts = type2str(result)
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
if name in NULLWrapped:
ml_wrapper.write(' %s z3rv = %s_mk(z3rv_m);\n' % (pts, pts))
else:
ml_wrapper.write(' %s z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, pts, ml_minus_type(ts)))
# convert output params
if len(op) > 0:
if result != VOID:
ml_wrapper.write(' %s\n' % ml_set_wrap(result, "res_val", "z3_result"))
# we have output parameters (i.e. call-by-reference arguments to the Z3 native
# code function). Hence, the value returned by the OCaml native wrapper is a tuple
# which contains the Z3 native function's return value (if it is non-void) in its
# first and the output parameters in the following components.
ml_wrapper.write('\n /* construct return tuple */\n')
ml_wrapper.write(' result = caml_alloc(%s, 0);\n' % ret_size)
i = 0
for p in params:
pt = param_type(p)
ts = type2str(pt)
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))
# convert a C-array into an OCaml list and return it
ml_wrapper.write('\n _a%s_val = Val_emptylist;\n' % i)
ml_wrapper.write(' for (_i = _a%s; _i > 0; _i--) {\n' % param_array_capacity_pos(p))
pts = ml_plus_type(ts)
pops = ml_plus_ops_type(ts)
if ml_has_plus_type(ts):
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_alloc_and_store(pt, 'tmp_val', '_a%dp' % i))
else:
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%d[_i]' % i))
ml_wrapper.write(' _iter = caml_alloc(2,0);\n')
ml_wrapper.write(' Store_field(_iter, 0, tmp_val);\n')
ml_wrapper.write(' Store_field(_iter, 1, _a%s_val);\n' % i)
ml_wrapper.write(' _a%s_val = _iter;\n' % i)
ml_wrapper.write(' }\n\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) ))
wrp = ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i)
wrp = wrp.replace('*)', '**)')
wrp = wrp.replace('_plus', '')
ml_wrapper.write(' %s\n' % wrp)
elif is_out_param(p):
ml_wrapper.write(' %s\n' % ml_set_wrap(param_type(p), "_a" + str(i) + "_val", "_a" + str(i) ))
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_alloc_and_store(pt, '_a%d_val' % i, '_a%dp' % i))
else:
ml_wrapper.write(' %s\n' % ml_alloc_and_store(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"))
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' % ml_alloc_and_store(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):
ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i))
j = j + 1
i = i + 1
else:
# As we have no output parameters, we simply return the result
ml_wrapper.write('\n /* construct simple return value */\n')
ml_wrapper.write(' %s' % ml_alloc_and_store(result, "result", "z3rv"))
# local array cleanup
ml_wrapper.write('\n /* cleanup and return */\n')
i = 0
for p in params:
k = param_kind(p)
@ -1446,8 +1499,9 @@ def mk_ml(ml_dir):
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('}\n')
ml_wrapper.write('#endif\n')
if mk_util.is_verbose():
print ('Generated "%s"' % ml_nativef)
print ('Generated "%s"' % ml_wrapperf)
# Collect API(...) commands from
def def_APIs(api_files):
@ -1636,6 +1690,7 @@ def generate_files(api_files,
if java_output_dir:
mk_java(java_output_dir, java_package_name)
if ml_output_dir:
mk_ml(ml_output_dir)

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

File diff suppressed because it is too large Load diff

55
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
@ -3243,38 +3216,31 @@ sig
type optimize
type handle
(** Create a Optimize context. *)
val mk_opt : context -> optimize
(** 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
@ -3474,6 +3432,3 @@ val enable_trace : string -> unit
Remarks: It is a NOOP otherwise.
*)
val disable_trace : string -> unit

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

@ -0,0 +1,36 @@
(** 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 set_internal_error_handler : ptr -> unit
= "n_set_internal_error_handler"

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

@ -0,0 +1,445 @@
#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,
};
int compare_pointers(void* pt1, void* pt2) {
if (pt1 == pt2)
return 0;
else if ((intnat)pt1 < (intnat)pt2)
return -1;
else
return +1;
}
#define MK_CTX_OF(X) \
CAMLprim DLL_PUBLIC value n_context_of_ ## X(value v) { \
CAMLparam1(v); \
CAMLlocal1(result); \
Z3_context_plus cp; \
Z3_ ## X ## _plus * p = (Z3_ ## X ## _plus *) Data_custom_val(v); \
cp = p->cp; \
result = caml_alloc_custom(&Z3_context_plus_custom_ops, sizeof(Z3_context_plus), 0, 1); \
*(Z3_context_plus *)Data_custom_val(result) = cp; \
/* We increment the usage counter of the context, as we just \
created a second custom block holding that context */ \
cp->obj_count++; \
CAMLreturn(result); \
} \
\
CAMLprim value DLL_PUBLIC n_is_null_ ## X (value v) { \
CAMLparam1(v); \
Z3_ ## X ## _plus* pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
CAMLreturn(Val_bool(pp->p == NULL)); \
} \
\
CAMLprim value DLL_PUBLIC n_mk_null_ ## X (value v) { \
CAMLparam1(v); \
CAMLlocal1(result); \
Z3_context_plus cp = *(Z3_context_plus*)(Data_custom_val(v)); \
Z3_ ## X ## _plus a = Z3_ ## X ## _plus_mk(cp, NULL); \
result = caml_alloc_custom(&Z3_ ## X ## _plus_custom_ops, sizeof(Z3_ ## X ## _plus), 0, 1); \
*(Z3_ ## X ## _plus*)(Data_custom_val(result)) = a; \
CAMLreturn(result); \
}
/* Context objects */
/* The Z3context_plus_data exists exactly once for each context,
no matter how many custom blocks for that context exist.
Each custom block only stores a pointer to the corresponding
Z3_context_plus_data. This ensures that the reference counting
is performed at exactly one place and not within the custom
blocks that get copied. */
typedef struct {
Z3_context ctx;
unsigned long obj_count;
} Z3_context_plus_data;
/* A context is wrapped to an OCaml value by storing a pointer
to its associated Z3_context_plus_data instance.
This instance gets created in mk_context and is deleted
together with the Z3 context instance in try_to_delete_context
whenever the obj_count field is zero. */
typedef Z3_context_plus_data* Z3_context_plus;
Z3_context_plus Z3_context_plus_mk(Z3_context c) {
Z3_context_plus r = (Z3_context_plus)malloc(sizeof(Z3_context_plus_data));
r->ctx = c;
/* The context created here will be wrapped into a custom block.
We regard custom blocks that point to a Z3_context_plus structure
as a usage of this structure. Hence, we assign it a counter of one. */
r->obj_count = 1;
return r;
}
Z3_context Z3_context_plus_raw(Z3_context_plus * cp) {
return (*cp)->ctx;
}
void try_to_delete_context(Z3_context_plus cp) {
if (cp->obj_count == 0) {
/* printf("try_to_delete_context: Deleting context %p(%p) with cnt=0.\n", cp, cp->ctx); */
Z3_del_context(cp->ctx);
free(cp);
}
/*
else if (cp->obj_count > 0)
printf("try_to_delete_context: Not deleting context %p(%p) with cnt=%lu.\n", cp, cp->ctx, cp->obj_count);
else if (cp->obj_count < 0)
printf("try_to_delete_context: ERROR, found context %p(%p) with negative cnt=%lu.\n", cp, cp->ctx, cp->obj_count);
*/
}
void Z3_context_finalize(value v) {
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
cp->obj_count--;
try_to_delete_context(cp);
}
int Z3_context_compare(value v1, value v2) {
/* As each context created within the OCaml bindings has a unique
Z3_context_plus_data allocated to store the handle and the ref counters,
we can just compare pointers here. This suffices to test for (in)equality
and induces an arbitrary (but fixed) ordering. */
Z3_context_plus cp1 = *(Z3_context_plus*)Data_custom_val(v1);
Z3_context_plus cp2 = *(Z3_context_plus*)Data_custom_val(v2);
return compare_pointers(cp1, cp2);
}
int Z3_context_compare_ext(value v1, value v2) {
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v1);
return compare_pointers(cp, (void*)Val_int(v2));
}
/* We use the pointer to the Z3_context_plus_data structure as
a hash value; it is unique, at least. */
intnat Z3_context_hash(value v) {
/* We use the address of the context's Z3_context_plus_data structure
as a hash value */
Z3_context_plus cp = *(Z3_context_plus*)Data_custom_val(v);
return (intnat)cp;
}
static struct custom_operations Z3_context_plus_custom_ops = {
(char*) "Z3_context ops",
Z3_context_finalize,
Z3_context_compare,
Z3_context_hash,
custom_serialize_default,
custom_deserialize_default,
Z3_context_compare_ext
};
/* AST objects */
typedef struct {
Z3_context_plus cp;
Z3_ast p;
} Z3_ast_plus;
Z3_ast_plus Z3_ast_plus_mk(Z3_context_plus cp, Z3_ast p) {
Z3_ast_plus r;
r.cp = cp;
r.p = p;
/* printf("++\n"); */
cp->obj_count++;
if (p != NULL)
Z3_inc_ref(cp->ctx, p);
return r;
}
Z3_ast Z3_ast_plus_raw(Z3_ast_plus * ap) {
return ap->p;
}
void Z3_ast_finalize(value v) {
/* printf("--\n"); */
Z3_ast_plus * ap = (Z3_ast_plus*)(Data_custom_val(v));
if (ap->p != NULL)
Z3_dec_ref(ap->cp->ctx, ap->p);
ap->cp->obj_count--;
try_to_delete_context(ap->cp);
}
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);
/* if the two ASTs belong to different contexts, we take
their contexts' addresses to order them (arbitrarily, but fixed) */
if (a1->cp->ctx != a2->cp->ctx)
return compare_pointers(a1->cp->ctx, a2->cp->ctx);
/* handling of NULL pointers */
if (a1->p == NULL && a2->p == NULL)
return 0;
if (a1->p == NULL)
return -1;
if (a2->p == NULL)
return +1;
/* Comparison according to AST ids. */
unsigned id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
unsigned id2 = Z3_get_ast_id(a2->cp->ctx, a2->p);
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;
int id2 = Val_int(v2);
if (a1->p == NULL && id2 == 0)
return 0;
if (a1->p == NULL)
return -1;
if (id2 == 0)
return +1;
id1 = Z3_get_ast_id(a1->cp->ctx, a1->p);
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);
if (ap->p == NULL)
return 0;
else
return Z3_get_ast_hash(ap->cp->ctx, ap->p);
}
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)
#define MK_PLUS_OBJ_NO_REF(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; \
r.cp->obj_count++; \
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); \
pp->cp->obj_count--; \
try_to_delete_context(pp->cp); \
} \
\
int Z3_ ## X ## _compare(value v1, value v2) { \
Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \
if (pp1->cp != pp2->cp) \
return compare_pointers(pp1->cp, pp2->cp); \
else \
return compare_pointers(pp1->p, pp2->p); \
} \
\
intnat Z3_ ## X ## _hash(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
return (intnat)pp->p; \
} \
\
int Z3_ ## X ## _compare_ext(value v1, value v2) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
return compare_pointers(pp->p, (void*)Val_int(v2)); \
} \
\
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \
Z3_ ## X ## _compare, \
Z3_ ## X ## _hash, \
custom_serialize_default, \
custom_deserialize_default, \
Z3_ ## X ## _compare_ext \
}; \
\
MK_CTX_OF(X)
#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; \
r.cp->obj_count++; \
if (p != NULL) \
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); \
if (pp->p != NULL) \
Z3_ ## X ## _dec_ref(pp->cp->ctx, pp->p); \
pp->cp->obj_count--; \
try_to_delete_context(pp->cp); \
} \
\
int Z3_ ## X ## _compare(value v1, value v2) { \
Z3_ ## X ## _plus * pp1 = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
Z3_ ## X ## _plus * pp2 = (Z3_ ## X ## _plus*)Data_custom_val(v2); \
if (pp1->cp != pp2->cp) \
return compare_pointers(pp1->cp, pp2->cp); \
else \
return compare_pointers(pp1->p, pp2->p); \
} \
\
intnat Z3_ ## X ## _hash(value v) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v); \
return (intnat)pp->p; \
} \
\
int Z3_ ## X ## _compare_ext(value v1, value v2) { \
Z3_ ## X ## _plus * pp = (Z3_ ## X ## _plus*)Data_custom_val(v1); \
return compare_pointers(pp->p, (void*)Val_int(v2)); \
} \
\
static struct custom_operations Z3_ ## X ## _plus_custom_ops = { \
(char*) "Z3_" #X " ops", \
Z3_ ## X ## _finalize, \
Z3_ ## X ## _compare, \
Z3_ ## X ## _hash, \
custom_serialize_default, \
custom_deserialize_default, \
Z3_ ## X ## _compare_ext \
}; \
\
MK_CTX_OF(X)
MK_PLUS_OBJ_NO_REF(symbol)
MK_PLUS_OBJ_NO_REF(constructor)
MK_PLUS_OBJ_NO_REF(constructor_list)
MK_PLUS_OBJ_NO_REF(rcf_num)
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
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
n_* wrapper functions. */
}
CAMLprim value DLL_PUBLIC n_set_internal_error_handler(value ctx_v)
{
CAMLparam1(ctx_v);
Z3_context_plus ctx_p = *(Z3_context_plus*) Data_custom_val(ctx_v);
Z3_set_error_handler(ctx_p->ctx, MLErrorHandler);
CAMLreturn(Val_unit);
}