mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

More new ML API

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-12-11 15:07:33 +00:00
parent 90cb046684
commit 1579da02b0
3 changed files with 99 additions and 56 deletions
Download patch file Download diff file Expand all files Collapse all files

9
.gitignore vendored
View file

@ -1,8 +1,5 @@
*~ *~
*.pyc *.pyc
*.pyo
# Ignore callgrind files
callgrind.out.*
# .hpp files are automatically generated # .hpp files are automatically generated
*.hpp *.hpp
.z3-trace .z3-trace
@ -45,6 +42,7 @@ bld_rel_x64/*
# Auto generated files. # Auto generated files.
config.log config.log
config.status config.status
configure
install_tactic.cpp install_tactic.cpp
mem_initializer.cpp mem_initializer.cpp
gparams_register_modules.cpp gparams_register_modules.cpp
@ -56,8 +54,6 @@ src/api/api_log_macros.cpp
src/api/dll/api_dll.def src/api/dll/api_dll.def
src/api/dotnet/Enumerations.cs src/api/dotnet/Enumerations.cs
src/api/dotnet/Native.cs src/api/dotnet/Native.cs
src/api/dotnet/Properties/AssemblyInfo.cs
src/api/dotnet/Microsoft.Z3.xml
src/api/python/z3consts.py src/api/python/z3consts.py
src/api/python/z3core.py src/api/python/z3core.py
src/ast/pattern/database.h src/ast/pattern/database.h
@ -78,3 +74,6 @@ src/api/ml/z3native_stubs.c
src/api/ml/z3native.ml src/api/ml/z3native.ml
src/api/ml/z3enums.ml src/api/ml/z3enums.ml
src/api/ml/z3.mllib src/api/ml/z3.mllib
src/api/ml/z3_native.c
src/api/ml/z3_native.ml
src/api/ml/z3_enums.ml

25
scripts/mk_util.py
View file

@ -2431,6 +2431,8 @@ def mk_bindings(api_files):
mk_z3consts_ml(api_files) mk_z3consts_ml(api_files)
_execfile(os.path.join('scripts', 'update_api.py'), g) # HACK _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK
cp_z3py_to_build() cp_z3py_to_build()
if is_ml_enabled():
mk_z3consts_ml(api_files)
# Extract enumeration types from API files, and add python definitions. # Extract enumeration types from API files, and add python definitions.
def mk_z3consts_py(api_files): def mk_z3consts_py(api_files):
@ -2718,6 +2720,7 @@ def mk_z3consts_ml(api_files):
if not os.path.exists(gendir): if not os.path.exists(gendir):
os.mkdir(gendir) os.mkdir(gendir)
<<<<<<< HEAD
efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w') efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w')
efile.write('(* Automatically generated file *)\n\n') efile.write('(* Automatically generated file *)\n\n')
efile.write('(** The enumeration types of Z3. *)\n\n') efile.write('(** The enumeration types of Z3. *)\n\n')
@ -2799,6 +2802,13 @@ def mk_z3consts_ml(api_files):
efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w') efile = open('%s.mli' % os.path.join(gendir, "z3enums"), 'w')
efile.write('(* Automatically generated file *)\n\n') efile.write('(* Automatically generated file *)\n\n')
efile.write('(** The enumeration types of Z3. *)\n\n') efile.write('(** The enumeration types of Z3. *)\n\n')
=======
efile = open('%s.ml' % os.path.join(gendir, "z3_enums"), 'w')
efile.write('(* Automatically generated file *)\n\n')
# efile.write('module z3_enums = struct\n\n');
>>>>>>> More new ML API
for api_file in api_files: for api_file in api_files:
api_file_c = ml.find_file(api_file, ml.name) api_file_c = ml.find_file(api_file, ml.name)
api_file = os.path.join(api_file_c.src_dir, api_file) api_file = os.path.join(api_file_c.src_dir, api_file)
@ -2844,6 +2854,7 @@ def mk_z3consts_ml(api_files):
if m: if m:
name = words[1] name = words[1]
if name not in DeprecatedEnums: if name not in DeprecatedEnums:
<<<<<<< HEAD
efile.write('(** %s *)\n' % name[3:]) efile.write('(** %s *)\n' % name[3:])
efile.write('type %s =\n' % name[3:]) # strip Z3_ efile.write('type %s =\n' % name[3:]) # strip Z3_
for k, i in decls.iteritems(): for k, i in decls.iteritems():
@ -2854,6 +2865,13 @@ def mk_z3consts_ml(api_files):
efile.write('(** Convert int to %s*)\n' % name[3:]) 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('val %s_of_int : int -> %s\n' % (name[3:],name[3:])) # strip Z3_
efile.write('\n') efile.write('\n')
=======
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_
>>>>>>> More new ML API
mode = SEARCHING mode = SEARCHING
else: else:
if words[2] != '': if words[2] != '':
@ -2864,8 +2882,15 @@ def mk_z3consts_ml(api_files):
decls[words[1]] = idx decls[words[1]] = idx
idx = idx + 1 idx = idx + 1
linenum = linenum + 1 linenum = linenum + 1
<<<<<<< HEAD
if VERBOSE: if VERBOSE:
print "Generated '%s/z3enums.mli'" % ('%s' % gendir) print "Generated '%s/z3enums.mli'" % ('%s' % gendir)
=======
efile.write('\n')
# efile.write'end\n');
if VERBOSE:
print "Generated '%s/z3_enums.ml'" % ('%s' % gendir)
>>>>>>> More new ML API
def mk_gui_str(id): def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id return '4D2F40D8-E5F9-473B-B548-%012d' % id

119
scripts/update_api.py
View file

@ -157,9 +157,9 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'} BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'}
# Mapping to ML types # Mapping to ML types
Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', Type2ML = { VOID : 'unit', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
STRING : 'string', STRING_PTR : 'char**', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' } BOOL : 'lbool', SYMBOL : 'symbol', PRINT_MODE : 'ast_print_mode', ERROR_CODE : 'error_code' }
next_type_id = FIRST_OBJ_ID next_type_id = FIRST_OBJ_ID
@ -1069,9 +1069,7 @@ def mk_bindings():
exe_c.write("}\n") exe_c.write("}\n")
def ml_method_name(name): def ml_method_name(name):
result = '' return name[3:] # Remove Z3_
name = name[3:] # Remove Z3_
return result
def mk_ml(): def mk_ml():
if not is_ml_enabled(): if not is_ml_enabled():
@ -1080,10 +1078,57 @@ def mk_ml():
ml_nativef = os.path.join(ml_dir, 'z3_native.ml') ml_nativef = os.path.join(ml_dir, 'z3_native.ml')
ml_wrapperf = os.path.join(ml_dir, 'z3_native.c') ml_wrapperf = os.path.join(ml_dir, 'z3_native.c')
ml_native = open(ml_nativef, 'w') ml_native = open(ml_nativef, 'w')
ml_native.write('// Automatically generated file\n') ml_native.write('(* Automatically generated file *)\n')
ml_native.write('\n') ml_native.write('\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')
ml_native.write('and sort = private ast\n')
ml_native.write('and func_decl = private ast\n')
ml_native.write('and app = private ast\n')
ml_native.write('and pattern = private ast\n')
ml_native.write('and params\n')
ml_native.write('and param_descrs\n')
ml_native.write('and model\n')
ml_native.write('and func_interp\n')
ml_native.write('and func_entry\n')
ml_native.write('and fixedpoint\n')
ml_native.write('and ast_vector\n')
ml_native.write('and ast_map\n')
ml_native.write('and goal\n')
ml_native.write('and tactic\n')
ml_native.write('and probe\n')
ml_native.write('and apply_result\n')
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')
for name, result, params in _dotnet_decls: for name, result, params in _dotnet_decls:
ml_native.write(' external %s : (' % ml_method_name(name)) ml_native.write(' external native_%s : ' % ml_method_name(name))
i = 0;
for param in params:
ml_native.write('%s -> ' % param2ml(param))
i = i + 1
ml_native.write('%s\n' % (type2ml(result)))
ml_native.write(' = "Native_Z3_%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))
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(' = \n')
ml_native.write(' ')
if result != VOID:
ml_native.write('let res = ')
ml_native.write('n_%s(' % (ml_method_name(name)))
first = True first = True
i = 0; i = 0;
for param in params: for param in params:
@ -1091,50 +1136,24 @@ def mk_ml():
first = False first = False
else: else:
ml_native.write(', ') ml_native.write(', ')
ml_native.write('%s a%d' % (param2ml(param), i)) ml_native.write('a%d' % i)
i = i + 1 i = i + 1
ml_native.write('%s)\n' % (type2ml(result))) ml_native.write(')')
# ml_native.write(' = "NATIVE_%s"' % ml_method_name(name)) if result != VOID:
# ml_native.write('\n\n') ml_native.write(' in\n')
# # Exception wrappers else:
# for name, result, params in _dotnet_decls: ml_native.write(';\n')
# java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name))) if len(params) > 0 and param_type(params[0]) == CONTEXT:
# first = True ml_native.write(' let err = error_code.fromInt(n_get_error_code(a0)) in \n')
# i = 0; ml_native.write(' if err <> Z3_enums.OK then\n')
# for param in params: ml_native.write(' raise (z3_exception n_get_error_msg_ex(a0, err.toInt()))\n')
# if first: ml_native.write(' else\n')
# first = False if result == VOID:
# else: ml_native.write(' ()\n')
# java_native.write(', ') else:
# java_native.write('%s a%d' % (param2java(param), i)) ml_native.write(' res\n')
# i = i + 1 ml_native.write('\n')
# java_native.write(')') ml_native.write('\nend\n')
# if len(params) > 0 and param_type(params[0]) == CONTEXT:
# java_native.write(' throws Z3Exception')
# java_native.write('\n')
# java_native.write(' {\n')
# java_native.write(' ')
# if result != VOID:
# java_native.write('%s res = ' % type2java(result))
# java_native.write('INTERNAL%s(' % (java_method_name(name)))
# first = True
# i = 0;
# for param in params:
# if first:
# first = False
# else:
# java_native.write(', ')
# java_native.write('a%d' % i)
# i = i + 1
# java_native.write(');\n')
# if len(params) > 0 and param_type(params[0]) == CONTEXT:
# java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
# java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
# java_native.write(' throw new Z3Exception(INTERNALgetErrorMsgEx(a0, err.toInt()));\n')
# if result != VOID:
# java_native.write(' return res;\n')
# java_native.write(' }\n\n')
# java_native.write('}\n')
ml_wrapper = open(ml_wrapperf, 'w') ml_wrapper = open(ml_wrapperf, 'w')
ml_wrapper.write('// Automatically generated file\n\n') ml_wrapper.write('// Automatically generated file\n\n')
ml_wrapper.write('#include <stddef.h>\n') ml_wrapper.write('#include <stddef.h>\n')