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

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-05-04 11:17:18 -07:00
parent 044e08a114 d11d9bd1de
commit 9e4b9ea98b
13 changed files with 2931 additions and 3429 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()

211
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:
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(' ' + 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

525
scripts/update_api.py
View file

@ -78,7 +78,7 @@ Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint',
# Mapping to Java types
Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr',
FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr',
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int'}
Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
@ -87,7 +87,7 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I
# Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
next_type_id = FIRST_OBJ_ID
@ -95,7 +95,7 @@ next_type_id = FIRST_OBJ_ID
def def_Type(var, c_type, py_type):
global next_type_id
exec('%s = %s' % (var, next_type_id), globals())
Type2Str[next_type_id] = c_type
Type2Str[next_type_id] = c_type
Type2PyStr[next_type_id] = py_type
next_type_id = next_type_id + 1
@ -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):
@ -633,18 +637,18 @@ def mk_java(java_dir, package_name):
elif k == IN_ARRAY or k == INOUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT:
java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
else:
else:
java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
elif k == OUT_ARRAY:
java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)),
i,
type2str(param_type(param)),
param_array_capacity_pos(param),
java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)),
i,
type2str(param_type(param)),
param_array_capacity_pos(param),
type2str(param_type(param))))
if param_type(param) == INT or param_type(param) == UINT:
java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
else:
java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
elif k == IN and param_type(param) == STRING:
java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i))
elif k == OUT_MANAGED_ARRAY:
@ -675,7 +679,7 @@ def mk_java(java_dir, package_name):
java_wrapper.write('(%s)a%i' % (param2str(param), i))
i = i + 1
java_wrapper.write(');\n')
# cleanup
# cleanup
i = 0
for param in params:
k = param_kind(param)
@ -711,7 +715,7 @@ def mk_java(java_dir, package_name):
if result == STRING:
java_wrapper.write(' return jenv->NewStringUTF(result);\n')
elif result != VOID:
java_wrapper.write(' return (%s) result;\n' % type2javaw(result))
java_wrapper.write(' return (%s) result;\n' % type2javaw(result))
java_wrapper.write('}\n')
java_wrapper.write('#ifdef __cplusplus\n')
java_wrapper.write('}\n')
@ -941,7 +945,7 @@ def def_API(name, result, params):
error ("unsupported parameter for %s, %s" % (ty, name, p))
elif kind == OUT_ARRAY:
sz = param_array_capacity_pos(p)
sz_p = params[sz]
sz_p = params[sz]
sz_p_k = param_kind(sz_p)
tstr = type2str(ty)
if sz_p_k == OUT or sz_p_k == INOUT:
@ -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_%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)
@ -1288,16 +1269,16 @@ def mk_ml(ml_dir):
ret_size = len(op)
if result != VOID:
ret_size = ret_size + 1
# Setup frame
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s(' % ml_method_name(name))
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s(' % ml_method_name(name))
first = True
i = 0
for p in params:
if is_in_param(p):
if first:
first = False
else:
else:
ml_wrapper.write(', ')
ml_wrapper.write('value a%d' % i)
i = i + 1
@ -1319,61 +1300,86 @@ 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:
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')
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' % (
type2str(param_type(param)),
i,
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(' _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)
# return tuples
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)
@ -1432,7 +1485,7 @@ def mk_ml(ml_dir):
ml_wrapper.write(' CAMLreturn(result);\n')
ml_wrapper.write('}\n\n')
if len(ip) > 5:
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name))
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name))
ml_wrapper.write(' return n_%s(' % ml_method_name(name))
i = 0
while i < len(ip):
@ -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)

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

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

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);
}

8
src/sat/sat_clause_set.cpp
View file

@ -35,6 +35,8 @@ namespace sat {
unsigned id = c.id();
if (id >= m_id2pos.size())
return;
if (empty())
return;
unsigned pos = m_id2pos[id];
if (pos == UINT_MAX)
return;
@ -52,7 +54,11 @@ namespace sat {
clause & clause_set::erase() {
SASSERT(!empty());
clause & c = *m_set.back();
m_id2pos[c.id()] = UINT_MAX;
SASSERT(c.id() < m_id2pos.size());
SASSERT(m_id2pos[c.id()] == m_set.size()-1);
if (c.id() < m_id2pos.size()) {
m_id2pos[c.id()] = UINT_MAX;
}
m_set.pop_back();
return c;
}

26
src/smt/theory_arith_core.h
View file

@ -1866,7 +1866,7 @@ namespace smt {
template<typename Ext>
template<bool Lazy>
void theory_arith<Ext>::pivot(theory_var x_i, theory_var x_j, numeral const & a_ij, bool apply_gcd_test) {
TRACE("arith_pivot", tout << "pivoting: v" << x_i << ", v" << x_j << "\n";);
TRACE("arith_pivoting", tout << "pivoting: v" << x_i << ", v" << x_j << "\n";);
m_stats.m_pivots++;
SASSERT(is_base(x_i) || is_quasi_base(x_i));
SASSERT(x_i != x_j);
@ -2067,14 +2067,14 @@ namespace smt {
theory_var max = get_num_vars();
theory_var result = max;
row const & r = m_rows[get_var_row(x_i)];
int n;
int best_col_sz = INT_MAX;
int best_so_far = INT_MAX;
typename vector<row_entry>::const_iterator it = r.begin_entries();
int n = 0;
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
for (; it != end; ++it) {
if (!it->is_dead()) {
theory_var x_j = it->m_var;
numeral const & a_ij = it->m_coeff;
@ -2090,14 +2090,14 @@ namespace smt {
best_so_far = num;
best_col_sz = col_sz;
n = 1;
}
}
else if (num == best_so_far && col_sz == best_col_sz) {
n++;
if (m_random()%n == 0) {
result = x_j;
out_a_ij = a_ij;
}
}
}
}
}
}
@ -2174,6 +2174,7 @@ namespace smt {
inf_numeral curr_error;
typename var_heap::iterator it = m_to_patch.begin();
typename var_heap::iterator end = m_to_patch.end();
//unsigned n = 0;
for (; it != end; ++it) {
theory_var v = *it;
if (below_lower(v))
@ -2188,7 +2189,16 @@ namespace smt {
<< ", best_error: " << best_error << ", curr_error: " << curr_error << "\n";);
best = v;
best_error = curr_error;
//n = 2;
}
#if 0
else if (false && n > 0 && curr_error == best_error) {
n++;
if (m_random()%n == 0) {
best = v;
}
}
#endif
}
if (best == null_theory_var)
m_to_patch.clear(); // all variables are satisfied

6
src/smt/theory_seq.cpp
View file

@ -2380,7 +2380,7 @@ void theory_seq::init_model(expr_ref_vector const& es) {
}
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(), get_family_id());
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory);
for (unsigned j = 0; j < m_nqs.size(); ++j) {
ne const& n = m_nqs[j];
@ -2469,7 +2469,9 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
for (unsigned i = 0; i < concats.size(); ++i) {
expr* c = concats[i], *c1;
if (m_util.str.is_unit(c, c1)) {
sv->add_dependency(ctx.get_enode(c1));
if (ctx.e_internalized(c1)) {
sv->add_dependency(ctx.get_enode(c1));
}
}
else if (m_util.str.is_string(c)) {
sv->add_string(c);

25
src/smt/theory_seq_empty.h
View file

@ -25,6 +25,7 @@ Revision History:
namespace smt {
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
proto_model& m_model;
ast_manager& m;
seq_util u;
symbol_set m_strings;
@ -34,8 +35,9 @@ namespace smt {
expr_ref_vector m_trail;
public:
seq_factory(ast_manager & m, family_id fid):
seq_factory(ast_manager & m, family_id fid, proto_model& md):
value_factory(m, fid),
m_model(md),
m(m),
u(m),
m_next(0),
@ -78,6 +80,17 @@ namespace smt {
v2 = u.str.mk_string(symbol("b"));
return true;
}
sort* ch;
if (u.is_seq(s, ch)) {
if (m_model.get_some_values(ch, v1, v2)) {
v1 = u.str.mk_unit(v1);
v2 = u.str.mk_unit(v2);
return true;
}
else {
return false;
}
}
NOT_IMPLEMENTED_YET();
return false;
}
@ -92,7 +105,7 @@ namespace smt {
return u.str.mk_string(sym);
}
}
sort* seq = 0;
sort* seq = 0, *ch = 0;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
@ -102,7 +115,11 @@ namespace smt {
//return u.str.mk_char(zstring(s), 0);
return u.str.mk_char(zstring("a"), 0);
}
NOT_IMPLEMENTED_YET();
if (u.is_seq(s, ch)) {
expr* v = m_model.get_fresh_value(ch);
return u.str.mk_unit(v);
}
UNREACHABLE();
return 0;
}
virtual void register_value(expr* n) {
@ -126,7 +143,7 @@ namespace smt {
public:
theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
virtual void init_model(model_generator & mg) {
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id()));
mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
}
};

6
src/util/mpf.cpp
View file

@ -1231,9 +1231,9 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
else if (is_zero(x))
set(o, x);
else {
// This is a generalized version of the algorithm for FPREM1 in the `Intel
// 64 and IA-32 Architectures Software Developer’s Manual',
// Section 3-402 Vol. 2A `FPREM1-Partial Remainder'.
// This is a generalized version of the algorithm for FPREM1 in the Intel
// 64 and IA-32 Architectures Software Developer's Manual',
// Section 3-402 Vol. 2A FPREM1-Partial Remainder'.
scoped_mpf ST0(*this), ST1(*this);
set(ST0, x);
set(ST1, y);