mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +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 70f0d2f423
commit 03a5c88ded
3 changed files with 164 additions and 53 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
.gitignore vendored
View file

@ -67,3 +67,6 @@ src/api/java/enumerations/*.java
*.bak *.bak
doc/api doc/api
doc/code doc/code
src/api/ml/z3_native.c
src/api/ml/z3_native.ml
src/api/ml/z3_enums.ml

89
scripts/mk_util.py
View file

@ -49,6 +49,7 @@ UTIL_COMPONENT='util'
API_COMPONENT='api' API_COMPONENT='api'
DOTNET_COMPONENT='dotnet' DOTNET_COMPONENT='dotnet'
JAVA_COMPONENT='java' JAVA_COMPONENT='java'
ML_COMPONENT='ml'
CPP_COMPONENT='cpp' CPP_COMPONENT='cpp'
##################### #####################
IS_WINDOWS=False IS_WINDOWS=False
@ -2230,6 +2231,8 @@ def mk_bindings(api_files):
if is_java_enabled(): if is_java_enabled():
check_java() check_java()
mk_z3consts_java(api_files) mk_z3consts_java(api_files)
if is_ml_enabled():
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()
@ -2503,6 +2506,92 @@ def mk_z3consts_java(api_files):
if VERBOSE: if VERBOSE:
print("Generated '%s'" % ('%s' % gendir)) print("Generated '%s'" % ('%s' % gendir))
# Extract enumeration types from z3_api.h, and add ML definitions
def mk_z3consts_ml(api_files):
blank_pat = re.compile("^ *$")
comment_pat = re.compile("^ *//.*$")
typedef_pat = re.compile("typedef enum *")
typedef2_pat = re.compile("typedef enum { *")
openbrace_pat = re.compile("{ *")
closebrace_pat = re.compile("}.*;")
ml = get_component(ML_COMPONENT)
DeprecatedEnums = [ 'Z3_search_failure' ]
gendir = ml.src_dir
if not os.path.exists(gendir):
os.mkdir(gendir)
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');
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')
SEARCHING = 0
FOUND_ENUM = 1
IN_ENUM = 2
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('\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_
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
efile.write('\n')
# efile.write'end\n');
if VERBOSE:
print "Generated '%s/z3_enums.ml'" % ('%s' % gendir)
def mk_gui_str(id): def mk_gui_str(id):
return '4D2F40D8-E5F9-473B-B548-%012d' % id return '4D2F40D8-E5F9-473B-B548-%012d' % id

125
scripts/update_api.py
View file

@ -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'} BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint'}
# Mapping to ML types # Mapping to ML types
Type2ML = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double', Type2ML = { VOID : 'unit', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
STRING : 'char*', STRING_PTR : 'char**', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'boolean', SYMBOL : 'long', 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
@ -332,13 +332,13 @@ def param2ml(p):
elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID: elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID:
return "long*" return "long*"
elif param_type(p) == STRING: elif param_type(p) == STRING:
return "char*" return "string"
else: else:
print "ERROR: unreachable code" print "ERROR: unreachable code"
assert(False) assert(False)
exit(1) exit(1)
if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s[]" % type2ml(param_type(p)) return "%s array" % type2ml(param_type(p))
else: else:
return type2ml(param_type(p)) return type2ml(param_type(p))
@ -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')