diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml index 9c704e4d0..c79b3cdaa 100644 --- a/examples/ml/ml_example.ml +++ b/examples/ml/ml_example.ml @@ -4,11 +4,19 @@ *) open Z3 - -let _ = ignore(Log.open_ "z3.log") ; - let cfg = Some [("model", "true"); ("proof", "false")] in - let ctx = (new context cfg) in - Printf.printf "Disposing...\n"; - ctx#dispose ; + +exception ExampleException of string + +let _ = + if not (Log.open_ "z3.log") then + raise (ExampleException "Log couldn't be opened.") + else + ( + Printf.printf "Running Z3 version %s\n" Version.to_string ; + let cfg = [("model", "true"); ("proof", "false")] in + let ctx = (new context cfg) in + Printf.printf "Disposing...\n"; + ctx#dispose (* can do, but we'd rather let it go out of scope *) ; + ); Printf.printf "Exiting.\n"; ;; diff --git a/scripts/update_api.py b/scripts/update_api.py index a586ad6e3..25adce2af 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1,4 +1,3 @@ - ############################################ # Copyright (c) 2012 Microsoft Corporation # @@ -328,16 +327,12 @@ def param2ml(p): if k == OUT: if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64: return "int" - elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID: - return "int" elif param_type(p) == STRING: return "string" else: return "ptr" elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s array" % type2ml(param_type(p)) - elif k == OUT_MANAGED_ARRAY: - return "%s array" % type2ml(param_type(p)); else: return type2ml(param_type(p)) @@ -1131,9 +1126,16 @@ def mk_ml(): ml_native.write('%s -> ' % param2ml(p)) if len(op) > 0: ml_native.write('(') - ml_native.write('%s' % type2ml(result)) + first = True + if result != VOID or len(op) == 0: + ml_native.write('%s' % type2ml(result)) + first = False for p in op: - ml_native.write(' * %s' % param2ml(p)) + if first: + first = False + else: + ml_native.write(' * ') + ml_native.write('%s' % param2ml(p)) if len(op) > 0: ml_native.write(')') ml_native.write('\n') @@ -1160,11 +1162,13 @@ def mk_ml(): i = i + 1 ml_native.write(' = \n') ml_native.write(' ') - if result == VOID: + if result == VOID and len(op) == 0: ml_native.write('let _ = ') else: ml_native.write('let res = ') ml_native.write('(ML2C.n_%s' % (ml_method_name(name))) + if len(ip) == 0: + ml_native.write(' ()') first = True i = 0; for p in params: @@ -1177,7 +1181,7 @@ def mk_ml(): ml_native.write(' if err <> OK then\n') ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (error_code2int err)))\n') ml_native.write(' else\n') - if result == VOID: + if result == VOID and len(op) == 0: ml_native.write(' ()\n') else: ml_native.write(' res\n') diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 9812bd790..31bb7e5fc 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -9,12 +9,27 @@ open Z3native module Log = struct let m_is_open = false - (* CMW: "open" seems to be an invalid function name*) - let open_ fn = int2lbool(open_log fn) == L_TRUE - let close = (close_log) - let append s = (append_log s) + (* CMW: "open" seems to be an invalid function name*) + let open_ fn = let rv = (open_log fn) in + Printf.printf "ol returned %d\n" rv ; + ((int2lbool rv) == L_TRUE) + let close = close_log + let append s = append_log s end - + +module Version = +struct + let major = let (x, _, _, _) = get_version in x + let minor = let (_, x, _, _) = get_version in x + let build = let (_, _, x, _) = get_version in x + let revision = let (_, _, _, x) = get_version in x + let to_string = + string_of_int major ^ "." ^ + string_of_int minor ^ "." ^ + string_of_int build ^ "." ^ + string_of_int revision ^ "." +end + class virtual idisposable = object method virtual dispose : unit @@ -25,7 +40,7 @@ object (self) inherit idisposable val mutable m_n_ctx : Z3native.z3_context = - let cfg = mk_config() in + let cfg = mk_config in let f e = (set_param_value cfg (fst e) (snd e)) in (List.iter f settings) ; let v = mk_context_rc cfg in @@ -34,14 +49,15 @@ object (self) val mutable m_refCount : int = 0 - initializer Gc.finalise (fun self -> self#dispose) self + initializer + Gc.finalise (fun self -> self#dispose) self method dispose : unit = if m_refCount == 0 then ( Printf.printf "Disposing %d \n" (Oo.id self) ; (del_context m_n_ctx) ) else ( - (* re-queue for finalization? *) + (* re-queue for finalization? *) ) method sub_one_ctx_obj = m_refCount <- m_refCount - 1 @@ -66,9 +82,9 @@ object (self) method virtual incref : Z3native.ptr -> unit method virtual decref : Z3native.ptr -> unit - (* - Disposes of the underlying native Z3 object. - *) + (* + Disposes of the underlying native Z3 object. + *) method dispose = Printf.printf "Disposing z3object %d \n" (Oo.id self) ; (match m_n_obj with @@ -92,16 +108,17 @@ object (self) method get_context = m_ctx method get_native_context = m_ctx#get_native - (* - method array_to_native a = +(* + method array_to_native a = let f e = e#get_native_object in (Array.map f a) - method array_length a = + method array_length a = match a with - | Some(x) -> (Array.length x) - | None -> 0 - *) + | Some(x) -> (Array.length x) + | None -> 0 +*) + end class symbol ctx_init obj_init = @@ -110,49 +127,55 @@ object (self) method incref o = () method decref o = () +end - method kind = match m_n_obj with - | Some(x) -> (int2symbol_kind (get_symbol_kind self#get_native_context x)) - | _ -> raise (Exception "Underlying object lost") +class int_symbol ctx_init obj_init = +object(self) + inherit symbol ctx_init obj_init +end - method is_int_symbol = match m_n_obj with - | Some(x) -> self#kind == INT_SYMBOL - | _ -> false +class string_symbol ctx_init obj_init = +object(self) + inherit symbol ctx_init obj_init +end - method is_string_symbol = match m_n_obj with - | Some(x) -> self#kind == STRING_SYMBOL - | _ -> false - - method to_string = match m_n_obj with - | Some(x) -> - ( - match self#kind with - | INT_SYMBOL -> (string_of_int (get_symbol_int self#get_native_context x)) - | STRING_SYMBOL -> (get_symbol_string self#get_native_context x) - ) - | None -> "" - - method create ctx obj = +module Symbol = +struct + let create ctx obj = match obj with | Some(x) -> ( match (int2symbol_kind (get_symbol_kind ctx#get_native x)) with - | INT_SYMBOL -> (new intsymbol ctx obj :> symbol) - | STRING_SYMBOL -> (new stringsymbol ctx obj :> symbol) + | INT_SYMBOL -> (new int_symbol ctx obj :> symbol) + | STRING_SYMBOL -> (new string_symbol ctx obj :> symbol) ) | None -> raise (Exception "Can't create null objects") -end + let kind o = match o#m_n_obj with + | Some(x) -> (int2symbol_kind (get_symbol_kind o#get_native_context x)) + | _ -> raise (Exception "Underlying object lost") -and intsymbol ctx_init obj_init = -object(self) - inherit symbol ctx_init obj_init + let is_int_symbol o = match o#m_n_obj with + | Some(x) -> x#kind == INT_SYMBOL + | _ -> false - method get_int = match m_n_obj with - | Some(x) -> (get_symbol_int m_ctx#get_native x) + let is_string_symbol o = match o#m_n_obj with + | Some(x) -> x#kind == STRING_SYMBOL + | _ -> false + + let get_int o = match o#m_n_obj with + | Some(x) -> (get_symbol_int o#get_native_context x) | None -> 0 -end -and stringsymbol ctx_init obj_init = -object(self) - inherit symbol ctx_init obj_init + let get_string o = match o#m_n_obj with + | Some(x) -> (get_symbol_string o#get_native_context x) + | None -> "" + + let to_string o = match o#m_n_obj with + | Some(x) -> + ( + match (kind o) with + | INT_SYMBOL -> (string_of_int (get_symbol_int o#get_native_context x)) + | STRING_SYMBOL -> (get_symbol_string o#get_native_context x) + ) + | None -> "" end