mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

ML API: basic structure and interface

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-02-19 19:49:27 +00:00
parent 34a72942bf
commit 23febf13c4
4 changed files with 1380 additions and 1447 deletions
Download patch file Download diff file Expand all files Collapse all files

81
scripts/mk_util.py
View file

@ -1340,10 +1340,17 @@ class MLComponent(Component):
shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f)) shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f))
for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)): for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)):
shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f)) shutil.copyfile(os.path.join(self.src_dir, f), os.path.join(BUILD_DIR, sub_dir, f))
cmis = '%s/z3enums.cmi %s/z3native.cmi %s/z3.cmi' % (src_dir,src_dir,src_dir)
out.write('%s/z3enums.cmi: %s/z3enums.mli\n' % (src_dir,src_dir))
out.write('\t%s -I %s -c %s/z3enums.mli\n' % (OCAMLC,src_dir,src_dir))
out.write('%s/z3native.cmi: %s/z3native.mli\n' % (src_dir,src_dir))
out.write('\t%s -I %s -c %s/z3native.mli\n' % (OCAMLC,src_dir,src_dir))
out.write('%s/z3.cmi: %s/z3.mli\n' % (src_dir,src_dir))
out.write('\t%s -I %s -c %s/z3.mli\n' % (OCAMLC,src_dir,src_dir))
out.write('api/ml/libz3ml$(LIB_EXT): %s$(SO_EXT)\n' % get_component(Z3_DLL_COMPONENT).dll_name) out.write('api/ml/libz3ml$(LIB_EXT): %s$(SO_EXT)\n' % get_component(Z3_DLL_COMPONENT).dll_name)
out.write('\t$(CXX) $(CXXFLAGS) -I %s -I %s %s/z3native.c $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT)\n' % (OCAML_LIB, api_src, src_dir)) out.write('\t$(CXX) $(CXXFLAGS) -I %s -I %s %s/z3native.c $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT)\n' % (OCAML_LIB, api_src, src_dir))
out.write('\t$(AR) $(AR_FLAGS) $(AR_OUTFLAG)api/ml/libz3ml$(LIB_EXT) api/ml/z3native$(OBJ_EXT)\n') out.write('\t$(AR) $(AR_FLAGS) $(AR_OUTFLAG)api/ml/libz3ml$(LIB_EXT) api/ml/z3native$(OBJ_EXT)\n')
out.write('api/ml/z3.cmxa: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT)' % get_component(Z3_DLL_COMPONENT).dll_name) out.write('api/ml/z3.cmxa: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (get_component(Z3_DLL_COMPONENT).dll_name, cmis))
for mlfile in get_ml_files(self.src_dir): for mlfile in get_ml_files(self.src_dir):
out.write(' %s' % os.path.join(src_dir, mlfile)) out.write(' %s' % os.path.join(src_dir, mlfile))
out.write('\n') out.write('\n')
@ -1351,7 +1358,7 @@ class MLComponent(Component):
if DEBUG_MODE: if DEBUG_MODE:
out.write('-g ') out.write('-g ')
out.write('-ccopt "-I../../%s" -cclib "-L../.. -lz3ml" -I %s %s/z3enums.ml %s/z3native.ml %s/z3.ml -a -o api/ml/z3.cmxa -linkall\n' % (api_src,src_dir,src_dir,src_dir,src_dir)) out.write('-ccopt "-I../../%s" -cclib "-L../.. -lz3ml" -I %s %s/z3enums.ml %s/z3native.ml %s/z3.ml -a -o api/ml/z3.cmxa -linkall\n' % (api_src,src_dir,src_dir,src_dir,src_dir))
out.write('api/ml/z3.cma: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT)' % get_component(Z3_DLL_COMPONENT).dll_name) out.write('api/ml/z3.cma: api/ml/libz3ml$(LIB_EXT) %s$(SO_EXT) %s' % (get_component(Z3_DLL_COMPONENT).dll_name, cmis))
for mlfile in get_ml_files(self.src_dir): for mlfile in get_ml_files(self.src_dir):
out.write(' %s' % os.path.join(self.to_src_dir, mlfile)) out.write(' %s' % os.path.join(self.to_src_dir, mlfile))
out.write('\n') out.write('\n')
@ -2716,6 +2723,76 @@ def mk_z3consts_ml(api_files):
linenum = linenum + 1 linenum = linenum + 1
if VERBOSE: if VERBOSE:
print "Generated '%s/z3enums.ml'" % ('%s' % gendir) 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)
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('(** %s *)\n' % name[3:])
efile.write('type %s =\n' % name[3:]) # strip Z3_
for k, i in decls.iteritems():
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
if VERBOSE:
print "Generated '%s/z3enums.mli'" % ('%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

26
scripts/update_api.py
View file

@ -1147,49 +1147,66 @@ def mk_ml():
return return
ml_dir = get_component('ml').src_dir ml_dir = get_component('ml').src_dir
ml_nativef = os.path.join(ml_dir, 'z3native.ml') 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.c') ml_wrapperf = os.path.join(ml_dir, 'z3native.c')
ml_native = open(ml_nativef, 'w') ml_native = open(ml_nativef, 'w')
ml_i = open(ml_nativefi, 'w')
ml_native.write('(* Automatically generated file *)\n\n') ml_native.write('(* Automatically generated file *)\n\n')
ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\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_native.write('open Z3enums\n\n') ml_native.write('open Z3enums\n\n')
ml_native.write('(**/**)\n') ml_native.write('(**/**)\n')
ml_native.write('type ptr\n') ml_native.write('type ptr\n')
ml_i.write('type ptr\n')
ml_native.write('and z3_symbol = ptr\n') ml_native.write('and z3_symbol = ptr\n')
ml_i.write('and z3_symbol = ptr\n')
for k, v in Type2Str.iteritems(): for k, v in Type2Str.iteritems():
if is_obj(k): if is_obj(k):
ml_native.write('and %s = ptr\n' % v.lower()) ml_native.write('and %s = ptr\n' % v.lower())
ml_i.write('and %s = ptr\n' % v.lower())
ml_native.write('\n') ml_native.write('\n')
ml_native.write('external is_null : ptr -> bool\n') ml_i.write('\n')
ml_native.write(' = "n_is_null"\n\n') ml_native.write('external is_null : ptr -> bool\n = "n_is_null"\n\n')
ml_native.write('external mk_null : unit -> ptr\n') ml_native.write('external mk_null : unit -> ptr\n = "n_mk_null"\n\n')
ml_native.write(' = "n_mk_null"\n\n')
ml_native.write('exception Exception of string\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('exception Exception of string\n\n')
# ML declarations # ML declarations
ml_native.write('module ML2C = struct\n\n') ml_native.write('module ML2C = struct\n\n')
for name, result, params in _dotnet_decls: for name, result, params in _dotnet_decls:
ml_native.write(' external n_%s : ' % ml_method_name(name)) ml_native.write(' external n_%s : ' % ml_method_name(name))
ml_i.write('val %s : ' % ml_method_name(name))
ip = inparams(params) ip = inparams(params)
op = outparams(params) op = outparams(params)
if len(ip) == 0: if len(ip) == 0:
ml_native.write(' unit -> ') ml_native.write(' unit -> ')
for p in ip: for p in ip:
ml_native.write('%s -> ' % param2ml(p)) ml_native.write('%s -> ' % param2ml(p))
ml_i.write('%s -> ' % param2ml(p))
if len(op) > 0: if len(op) > 0:
ml_native.write('(') ml_native.write('(')
ml_i.write('(')
first = True first = True
if result != VOID or len(op) == 0: if result != VOID or len(op) == 0:
ml_native.write('%s' % type2ml(result)) ml_native.write('%s' % type2ml(result))
ml_i.write('%s' % type2ml(result))
first = False first = False
for p in op: for p in op:
if first: if first:
first = False first = False
else: else:
ml_native.write(' * ') ml_native.write(' * ')
ml_i.write(' * ')
ml_native.write('%s' % param2ml(p)) ml_native.write('%s' % param2ml(p))
ml_i.write('%s' % param2ml(p))
if len(op) > 0: if len(op) > 0:
ml_native.write(')') ml_native.write(')')
ml_i.write(')')
ml_native.write('\n') ml_native.write('\n')
ml_i.write('\n')
ml_native.write(' = "n_%s"\n' % ml_method_name(name)) ml_native.write(' = "n_%s"\n' % ml_method_name(name))
if len(ip) > 5: if len(ip) > 5:
ml_native.write(' "n_%s_bytecode"\n' % ml_method_name(name)) ml_native.write(' "n_%s_bytecode"\n' % ml_method_name(name))
@ -1201,6 +1218,7 @@ def mk_ml():
ip = inparams(params) ip = inparams(params)
op = outparams(params) op = outparams(params)
ml_native.write(' let %s ' % ml_method_name(name)) ml_native.write(' let %s ' % ml_method_name(name))
first = True first = True
i = 0; i = 0;
for p in params: for p in params:

2
src/api/ml/Makefile
View file

@ -7,4 +7,4 @@ all:
doc: *.ml doc: *.ml
mkdir -p doc mkdir -p doc
ocamldoc -html -d doc -I ../../../bld_dbg/api/ml -sort *.ml -hide Z3 ocamldoc -html -d doc -I ../../../bld_dbg/api/ml -sort *.mli -hide Z3

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

File diff suppressed because it is too large Load diff