mirror of
https://github.com/Z3Prover/z3
synced 2025-11-03 21:09:11 +00:00
More ML API
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
f5a0520b83
commit
65ddf2be49
3 changed files with 65 additions and 41 deletions
5
.gitignore
vendored
5
.gitignore
vendored
|
|
@ -9,6 +9,7 @@ callgrind.out.*
|
|||
# OCaml generated files
|
||||
*.a
|
||||
*.cma
|
||||
*.cmo
|
||||
*.cmi
|
||||
*.cmxa
|
||||
ocamlz3
|
||||
|
|
@ -71,5 +72,5 @@ doc/code
|
|||
src/api/ml/z3_native.c
|
||||
src/api/ml/z3_native.ml
|
||||
src/api/ml/native.c
|
||||
src/api/ml/Z3.ml
|
||||
src/api/ml/z3_enums.ml
|
||||
src/api/ml/z3.ml
|
||||
src/api/ml/enumerations.ml
|
||||
|
|
|
|||
|
|
@ -672,6 +672,9 @@ def get_cs_files(path):
|
|||
def get_java_files(path):
|
||||
return filter(lambda f: f.endswith('.java'), os.listdir(path))
|
||||
|
||||
def get_ml_files(path):
|
||||
return filter(lambda f: f.endswith('.ml'), os.listdir(path))
|
||||
|
||||
def find_all_deps(name, deps):
|
||||
new_deps = []
|
||||
for dep in deps:
|
||||
|
|
@ -1284,9 +1287,17 @@ class MLComponent(Component):
|
|||
|
||||
def mk_makefile(self, out):
|
||||
if is_ml_enabled():
|
||||
mk_dir(os.path.join(BUILD_DIR, 'api', 'ml'))
|
||||
bld_dir = os.path.join(BUILD_DIR, 'api', 'ml')
|
||||
mk_dir(bld_dir)
|
||||
libfile = '%s$(LIB_EXT)' % self.lib_name
|
||||
out.write('%s: libz3$(SO_EXT) %s\n' % (libfile, os.path.join(self.to_src_dir, 'native.c')))
|
||||
for mlfile in get_ml_files(self.src_dir):
|
||||
out.write('%si: %s\n' % (os.path.join('api', 'ml', mlfile),os.path.join(self.to_src_dir, mlfile)))
|
||||
out.write('\tocamlopt -I %s -i %s > %si\n' % (os.path.join('api', 'ml'), os.path.join(self.to_src_dir, mlfile), os.path.join('api', 'ml', mlfile)))
|
||||
out.write('\tocamlopt -I %s -c %si \n' % (os.path.join('api', 'ml'), os.path.join('api','ml', mlfile)))
|
||||
out.write('%s: libz3$(SO_EXT) %s' % (libfile, os.path.join(self.to_src_dir, 'native.c')))
|
||||
for mlfile in get_ml_files(self.src_dir):
|
||||
out.write(' %si' % os.path.join('api','ml', mlfile))
|
||||
out.write('\n')
|
||||
out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3_native$(OBJ_EXT) -I%s %s/native.c\n' % (get_component(API_COMPONENT).to_src_dir, self.to_src_dir))
|
||||
out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3ml$(LIB_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'ml', 'native'))
|
||||
out.write('ml: %s\n' % libfile)
|
||||
|
|
@ -2522,11 +2533,9 @@ def mk_z3consts_ml(api_files):
|
|||
if not os.path.exists(gendir):
|
||||
os.mkdir(gendir)
|
||||
|
||||
efile = open('%s.ml' % os.path.join(gendir, "z3_enums"), 'w')
|
||||
efile = open('%s.ml' % os.path.join(gendir, "enumerations"), 'w')
|
||||
efile.write('(* Automatically generated file *)\n\n')
|
||||
# efile.write('module z3_enums = struct\n\n');
|
||||
|
||||
|
||||
efile.write('module Enumerations = struct\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)
|
||||
|
|
@ -2572,11 +2581,21 @@ def mk_z3consts_ml(api_files):
|
|||
if m:
|
||||
name = words[1]
|
||||
if name not in DeprecatedEnums:
|
||||
efile.write('\n(* %s *)\n' % name)
|
||||
efile.write('type %s =\n' % name[3:]) # strip Z3_
|
||||
efile.write
|
||||
for k, i in decls.iteritems():
|
||||
efile.write(' | %s \n' % k[3:]) # strip Z3_
|
||||
efile.write(' | %s \n' % k[3:]) # strip Z3_
|
||||
efile.write('\n')
|
||||
efile.write('let %s2int x : int =\n' % (name[3:])) # strip Z3_
|
||||
efile.write(' match x with\n')
|
||||
for k, i in decls.iteritems():
|
||||
efile.write(' | %s -> %d\n' % (k[3:], i))
|
||||
efile.write('\n')
|
||||
efile.write('let int2%s x : %s =\n' % (name[3:],name[3:])) # strip Z3_
|
||||
efile.write(' match x with\n')
|
||||
for k, i in decls.iteritems():
|
||||
efile.write(' | %d -> %s\n' % (i, k[3:]))
|
||||
# use Z3.Exception?
|
||||
efile.write(' | _ -> raise (Failure "undefined enum value")\n\n')
|
||||
mode = SEARCHING
|
||||
else:
|
||||
if words[2] != '':
|
||||
|
|
@ -2587,10 +2606,9 @@ def mk_z3consts_ml(api_files):
|
|||
decls[words[1]] = idx
|
||||
idx = idx + 1
|
||||
linenum = linenum + 1
|
||||
efile.write('\n')
|
||||
# efile.write'end\n');
|
||||
efile.write('end\n')
|
||||
if VERBOSE:
|
||||
print "Generated '%s/z3_enums.ml'" % ('%s' % gendir)
|
||||
print "Generated '%s/enumerations.ml'" % ('%s' % gendir)
|
||||
|
||||
def mk_gui_str(id):
|
||||
return '4D2F40D8-E5F9-473B-B548-%012d' % id
|
||||
|
|
|
|||
|
|
@ -156,9 +156,9 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I
|
|||
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'}
|
||||
|
||||
# Mapping to ML types
|
||||
Type2ML = { VOID : 'unit', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
|
||||
STRING : 'string', STRING_PTR : 'char**',
|
||||
BOOL : 'lbool', SYMBOL : 'symbol', PRINT_MODE : 'ast_print_mode', ERROR_CODE : 'error_code' }
|
||||
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float',
|
||||
STRING : 'string', STRING_PTR : 'char**',
|
||||
BOOL : 'int', SYMBOL : 'symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' }
|
||||
|
||||
next_type_id = FIRST_OBJ_ID
|
||||
|
||||
|
|
@ -212,7 +212,7 @@ def type2javaw(ty):
|
|||
def type2ml(ty):
|
||||
global Type2ML
|
||||
if (ty >= FIRST_OBJ_ID):
|
||||
return 'long'
|
||||
return 'int'
|
||||
else:
|
||||
return Type2ML[ty]
|
||||
|
||||
|
|
@ -328,9 +328,9 @@ def param2ml(p):
|
|||
k = param_kind(p)
|
||||
if k == OUT:
|
||||
if param_type(p) == INT or param_type(p) == UINT:
|
||||
return "int*"
|
||||
return "int"
|
||||
elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID:
|
||||
return "long*"
|
||||
return "int"
|
||||
elif param_type(p) == STRING:
|
||||
return "string"
|
||||
else:
|
||||
|
|
@ -1075,12 +1075,12 @@ def mk_ml():
|
|||
if not is_ml_enabled():
|
||||
return
|
||||
ml_dir = get_component('ml').src_dir
|
||||
ml_nativef = os.path.join(ml_dir, 'Z3.ml')
|
||||
ml_nativef = os.path.join(ml_dir, 'z3.ml')
|
||||
ml_wrapperf = os.path.join(ml_dir, 'native.c')
|
||||
ml_native = open(ml_nativef, 'w')
|
||||
ml_native.write('(* Automatically generated file *)\n')
|
||||
ml_native.write('\n')
|
||||
ml_native.write('module Z3Native = struct\n\n')
|
||||
ml_native.write('(* Automatically generated file *)\n\n')
|
||||
ml_native.write('open Enumerations\n\n')
|
||||
ml_native.write('module Z3 = struct\n\n')
|
||||
ml_native.write('type context\n')
|
||||
ml_native.write('and symbol\n')
|
||||
ml_native.write('and ast\n')
|
||||
|
|
@ -1103,15 +1103,17 @@ def mk_ml():
|
|||
ml_native.write('and solver\n')
|
||||
ml_native.write('and stats\n')
|
||||
ml_native.write('\n')
|
||||
ml_native.write(' exception Z3Exception of string\n\n')
|
||||
ml_native.write(' exception Exception of string\n\n')
|
||||
for name, result, params in _dotnet_decls:
|
||||
ml_native.write(' external native_%s : ' % ml_method_name(name))
|
||||
ml_native.write(' external n_%s : ' % ml_method_name(name))
|
||||
i = 0;
|
||||
for param in params:
|
||||
ml_native.write('%s -> ' % param2ml(param))
|
||||
i = i + 1
|
||||
if len(params) == 0:
|
||||
ml_native.write(' unit -> ')
|
||||
ml_native.write('%s\n' % (type2ml(result)))
|
||||
ml_native.write(' = "Native_Z3_%s"\n\n' % ml_method_name(name))
|
||||
ml_native.write(' = "n_%s"\n\n' % ml_method_name(name))
|
||||
# Exception wrappers
|
||||
for name, result, params in _dotnet_decls:
|
||||
ml_native.write(' let %s ' % ml_method_name(name))
|
||||
|
|
@ -1128,25 +1130,28 @@ def mk_ml():
|
|||
ml_native.write(' ')
|
||||
if result != VOID:
|
||||
ml_native.write('let res = ')
|
||||
ml_native.write('n_%s(' % (ml_method_name(name)))
|
||||
first = True
|
||||
i = 0;
|
||||
for param in params:
|
||||
if first:
|
||||
first = False
|
||||
else:
|
||||
ml_native.write(', ')
|
||||
ml_native.write('a%d' % i)
|
||||
i = i + 1
|
||||
ml_native.write(')')
|
||||
if len(params) == 0:
|
||||
ml_native.write('n_%s()' % (ml_method_name(name)))
|
||||
else:
|
||||
ml_native.write('(n_%s ' % (ml_method_name(name)))
|
||||
first = True
|
||||
i = 0;
|
||||
for param in params:
|
||||
if first:
|
||||
first = False
|
||||
else:
|
||||
ml_native.write(' ')
|
||||
ml_native.write('a%d' % i)
|
||||
i = i + 1
|
||||
ml_native.write(')')
|
||||
if result != VOID:
|
||||
ml_native.write(' in\n')
|
||||
else:
|
||||
ml_native.write(';\n')
|
||||
if len(params) > 0 and param_type(params[0]) == CONTEXT:
|
||||
ml_native.write(' let err = error_code.fromInt(n_get_error_code(a0)) in \n')
|
||||
ml_native.write(' if err <> Z3_enums.OK then\n')
|
||||
ml_native.write(' raise (z3_exception n_get_error_msg_ex(a0, err.toInt()))\n')
|
||||
ml_native.write(' let err = (Enumerations.int2error_code (n_get_error_code a0)) in \n')
|
||||
ml_native.write(' if err <> Enumerations.OK then\n')
|
||||
ml_native.write(' raise (Exception (n_get_error_msg_ex a0 (error_code2int err)))\n')
|
||||
ml_native.write(' else\n')
|
||||
if result == VOID:
|
||||
ml_native.write(' ()\n')
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue