From 3e336592a290c07b2937c84ce415776b3563240d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 4 Jun 2013 18:00:48 +0100 Subject: [PATCH] ML API: bug and build fixes Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 28 ++++++++++++++++------------ scripts/update_api.py | 5 ++++- src/api/ml/z3.ml | 27 +++++++++++++++++---------- src/api/ml/z3.mli | 6 +++--- 4 files changed, 40 insertions(+), 26 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a30e074b0..f46339f5c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1340,26 +1340,30 @@ class MLComponent(Component): mk_dir(os.path.join(BUILD_DIR, sub_dir)) api_src = get_component(API_COMPONENT).to_src_dir for f in filter(lambda f: f.endswith('.ml'), os.listdir(self.src_dir)): - out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f)) - str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f) - if IS_WINDOWS: str = str.replace('/','\\') + out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f))) + str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f)) + out.write(str) + for f in filter(lambda f: f.endswith('.mli'), os.listdir(self.src_dir)): + out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f))) + str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f)) out.write(str) for f in filter(lambda f: f.endswith('.c'), os.listdir(self.src_dir)): - out.write('%s/%s: %s/%s\n' % (sub_dir,f,src_dir,f)) - str = '\t%s %s/%s %s/%s\n' % (CP_CMD,src_dir,f,sub_dir,f) - if IS_WINDOWS: str = str.replace('/','\\') + out.write('%s: %s\n' % (os.path.join(sub_dir,f),os.path.join(src_dir,f))) + str = '\t%s %s %s\n' % (CP_CMD,os.path.join(src_dir,f),os.path.join(sub_dir,f)) out.write(str) modules = ["z3enums", "z3native", "z3"] # dependencies in this order! prev = '' for m in modules: - out.write('%s/%s.mli: %s/%s.ml %s\n' % (sub_dir,m,sub_dir,m,prev)) - out.write('\t%s -I %s -i -c %s/%s.ml > %s/%s.mli\n' % (OCAMLC,sub_dir,sub_dir,m,sub_dir,m)) - prev = prev + ' ' + sub_dir + '/' + m + '.mli' + fn = os.path.join(self.src_dir, ('%s.mli' % m)) + if not os.path.exists(fn): + out.write('%s.mli: %s.ml %s\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m),prev)) + out.write('\t%s -I %s -i -c %s.ml > %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir, m),os.path.join(sub_dir, m))) + prev = prev + ' ' + os.path.join(sub_dir, m) + '.mli' cmis = '' for m in modules: - out.write('%s/%s.cmi: %s/%s.mli\n' % (sub_dir,m,sub_dir,m)) - out.write('\t%s -I %s -c %s/%s.mli\n' % (OCAMLC,sub_dir,sub_dir,m)) - cmis = cmis + ' ' + sub_dir + '/' + m + '.cmi' + out.write('%s.cmi: %s.mli\n' % (os.path.join(sub_dir,m),os.path.join(sub_dir,m))) + out.write('\t%s -I %s -c %s.mli\n' % (OCAMLC,sub_dir,os.path.join(sub_dir,m))) + cmis = cmis + ' ' + os.path.join(sub_dir,m) + '.cmi' out.write('api/ml/libz3ml$(LIB_EXT): api/ml/z3native.c %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, sub_dir)) out.write('\t$(AR) $(AR_FLAGS) $(AR_OUTFLAG)api/ml/libz3ml$(LIB_EXT) api/ml/z3native$(OBJ_EXT)\n') diff --git a/scripts/update_api.py b/scripts/update_api.py index 44d871348..77a5bf7f2 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1185,7 +1185,8 @@ def mk_ml(): ip = inparams(params) op = outparams(params) if len(ip) == 0: - ml_native.write(' unit -> ') + ml_native.write(' unit -> ') + ml_i.write(' unit -> ') for p in ip: ml_native.write('%s -> ' % param2ml(p)) ml_i.write('%s -> ' % param2ml(p)) @@ -1233,6 +1234,8 @@ def mk_ml(): 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: diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 081433f1f..8b783d25d 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -34,7 +34,7 @@ struct ) let create_context settings = - let cfg = Z3native.mk_config in + let cfg = Z3native.mk_config () in let f e = (Z3native.set_param_value cfg (fst e) (snd e)) in (List.iter f settings) ; let v = Z3native.mk_context_rc cfg in @@ -101,12 +101,12 @@ end module Version = struct - let major = let (x, _, _, _) = Z3native.get_version in x - let minor = let (_, x, _, _) = Z3native.get_version in x - let build = let (_, _, x, _) = Z3native.get_version in x - let revision = let (_, _, _, x) = Z3native.get_version in x + let major = let (x, _, _, _) = Z3native.get_version () in x + let minor = let (_, x, _, _) = Z3native.get_version () in x + let build = let (_, _, x, _) = Z3native.get_version () in x + let revision = let (_, _, _, x) = Z3native.get_version () in x let to_string = - let (mj, mn, bld, rev) = Z3native.get_version in + let (mj, mn, bld, rev) = Z3native.get_version () in string_of_int mj ^ "." ^ string_of_int mn ^ "." ^ string_of_int bld ^ "." ^ @@ -609,6 +609,10 @@ sig val add_symbol : params -> Symbol.symbol -> Symbol.symbol -> unit val mk_params : context -> params val to_string : params -> string + + val update_param_value : context -> string -> string -> unit + val get_param_value : context -> string -> string option + val set_print_mode : context -> Z3enums.ast_print_mode -> unit end = struct type params = z3_native_object @@ -1099,7 +1103,7 @@ struct end -module Array = +module Z3Array = struct let mk_sort ( ctx : context ) ( domain : sort ) ( range : sort ) = sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range)) @@ -1382,7 +1386,7 @@ struct end -module List = +module Z3List = struct let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : sort ) = let (r, _, _, _, _, _, _) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) (Sort.gno elem_sort)) in @@ -2038,7 +2042,7 @@ struct if not r then None else - expr_of_ptr (z3obj_gc x) v + Some(expr_of_ptr (z3obj_gc x) v) let evaluate ( x : model ) ( t : expr ) ( completion : bool ) = eval x t completion @@ -2331,7 +2335,7 @@ struct if (Z3native.stats_is_uint (z3obj_gnc x) (z3obj_gno x) i) then (Entry.create_si k (Z3native.stats_get_uint_value (z3obj_gnc x) (z3obj_gno x) i)) else - (Entry.create_sd k (Z3native.stats_get_float_value (z3obj_gnc x) (z3obj_gno x) i)) + (Entry.create_sd k (Z3native.stats_get_double_value (z3obj_gnc x) (z3obj_gno x) i)) ) in mk_list f n @@ -2667,3 +2671,6 @@ let global_param_reset_all = let toggle_warning_messages ( enabled: bool ) = Z3native.toggle_warning_messages enabled + +module Array = Z3Array +module List = Z3List diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 570ff8717..3f83ef6b2 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -8,7 +8,7 @@ (** General Z3 exceptions Many functions in this API may throw an exception; if they do, it is this one.*) -exception Error +exception Error of string (** Context objects. @@ -55,11 +55,11 @@ module Log : sig (** Open an interaction log file. @return True if opening the log file succeeds, false otherwise. *) - (* CMW: "open" seems to be a reserved keyword? *) + (* CMW: "open" is a reserved keyword. *) val open_ : string -> bool (** Closes the interaction log. *) - val close : unit + val close : unit -> unit (** Appends a user-provided string to the interaction log. *) val append : string -> unit