mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

ML API bugfixes

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2012-12-20 04:10:38 +00:00
parent 50560ba791
commit 1685e3dd6f
3 changed files with 99 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
examples/ml/ml_example.ml
View file

@ -4,11 +4,19 @@
*) *)
open Z3 open Z3
let _ = ignore(Log.open_ "z3.log") ; exception ExampleException of string
let cfg = Some [("model", "true"); ("proof", "false")] in
let ctx = (new context cfg) in let _ =
Printf.printf "Disposing...\n"; if not (Log.open_ "z3.log") then
ctx#dispose ; 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"; Printf.printf "Exiting.\n";
;; ;;

22
scripts/update_api.py
View file

@ -1,4 +1,3 @@
############################################ ############################################
# Copyright (c) 2012 Microsoft Corporation # Copyright (c) 2012 Microsoft Corporation
# #
@ -328,16 +327,12 @@ def param2ml(p):
if k == OUT: if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64: if param_type(p) == INT or param_type(p) == UINT or param_type(p) == INT64 or param_type(p) == UINT64:
return "int" 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: elif param_type(p) == STRING:
return "string" return "string"
else: else:
return "ptr" return "ptr"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s array" % type2ml(param_type(p)) return "%s array" % type2ml(param_type(p))
elif k == OUT_MANAGED_ARRAY:
return "%s array" % type2ml(param_type(p));
else: else:
return type2ml(param_type(p)) return type2ml(param_type(p))
@ -1131,9 +1126,16 @@ def mk_ml():
ml_native.write('%s -> ' % param2ml(p)) ml_native.write('%s -> ' % param2ml(p))
if len(op) > 0: if len(op) > 0:
ml_native.write('(') 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: 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: if len(op) > 0:
ml_native.write(')') ml_native.write(')')
ml_native.write('\n') ml_native.write('\n')
@ -1160,11 +1162,13 @@ def mk_ml():
i = i + 1 i = i + 1
ml_native.write(' = \n') ml_native.write(' = \n')
ml_native.write(' ') ml_native.write(' ')
if result == VOID: if result == VOID and len(op) == 0:
ml_native.write('let _ = ') ml_native.write('let _ = ')
else: else:
ml_native.write('let res = ') ml_native.write('let res = ')
ml_native.write('(ML2C.n_%s' % (ml_method_name(name))) ml_native.write('(ML2C.n_%s' % (ml_method_name(name)))
if len(ip) == 0:
ml_native.write(' ()')
first = True first = True
i = 0; i = 0;
for p in params: for p in params:
@ -1177,7 +1181,7 @@ def mk_ml():
ml_native.write(' if err <> OK then\n') 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(' raise (Exception (ML2C.n_get_error_msg_ex a0 (error_code2int err)))\n')
ml_native.write(' else\n') ml_native.write(' else\n')
if result == VOID: if result == VOID and len(op) == 0:
ml_native.write(' ()\n') ml_native.write(' ()\n')
else: else:
ml_native.write(' res\n') ml_native.write(' res\n')

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

@ -9,12 +9,27 @@ open Z3native
module Log = module Log =
struct struct
let m_is_open = false let m_is_open = false
(* CMW: "open" seems to be an invalid function name*) (* CMW: "open" seems to be an invalid function name*)
let open_ fn = int2lbool(open_log fn) == L_TRUE let open_ fn = let rv = (open_log fn) in
let close = (close_log) Printf.printf "ol returned %d\n" rv ;
let append s = (append_log s) ((int2lbool rv) == L_TRUE)
let close = close_log
let append s = append_log s
end 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 = class virtual idisposable =
object object
method virtual dispose : unit method virtual dispose : unit
@ -25,7 +40,7 @@ object (self)
inherit idisposable inherit idisposable
val mutable m_n_ctx : Z3native.z3_context = 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 let f e = (set_param_value cfg (fst e) (snd e)) in
(List.iter f settings) ; (List.iter f settings) ;
let v = mk_context_rc cfg in let v = mk_context_rc cfg in
@ -34,14 +49,15 @@ object (self)
val mutable m_refCount : int = 0 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 = method dispose : unit =
if m_refCount == 0 then ( if m_refCount == 0 then (
Printf.printf "Disposing %d \n" (Oo.id self) ; Printf.printf "Disposing %d \n" (Oo.id self) ;
(del_context m_n_ctx) (del_context m_n_ctx)
) else ( ) else (
(* re-queue for finalization? *) (* re-queue for finalization? *)
) )
method sub_one_ctx_obj = m_refCount <- m_refCount - 1 method sub_one_ctx_obj = m_refCount <- m_refCount - 1
@ -66,9 +82,9 @@ object (self)
method virtual incref : Z3native.ptr -> unit method virtual incref : Z3native.ptr -> unit
method virtual decref : 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 = method dispose =
Printf.printf "Disposing z3object %d \n" (Oo.id self) ; Printf.printf "Disposing z3object %d \n" (Oo.id self) ;
(match m_n_obj with (match m_n_obj with
@ -92,16 +108,17 @@ object (self)
method get_context = m_ctx method get_context = m_ctx
method get_native_context = m_ctx#get_native 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 let f e = e#get_native_object in
(Array.map f a) (Array.map f a)
method array_length a = method array_length a =
match a with match a with
| Some(x) -> (Array.length x) | Some(x) -> (Array.length x)
| None -> 0 | None -> 0
*) *)
end end
class symbol ctx_init obj_init = class symbol ctx_init obj_init =
@ -110,49 +127,55 @@ object (self)
method incref o = () method incref o = ()
method decref o = () method decref o = ()
end
method kind = match m_n_obj with class int_symbol ctx_init obj_init =
| Some(x) -> (int2symbol_kind (get_symbol_kind self#get_native_context x)) object(self)
| _ -> raise (Exception "Underlying object lost") inherit symbol ctx_init obj_init
end
method is_int_symbol = match m_n_obj with class string_symbol ctx_init obj_init =
| Some(x) -> self#kind == INT_SYMBOL object(self)
| _ -> false inherit symbol ctx_init obj_init
end
method is_string_symbol = match m_n_obj with module Symbol =
| Some(x) -> self#kind == STRING_SYMBOL struct
| _ -> false let create ctx obj =
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 =
match obj with match obj with
| Some(x) -> ( | Some(x) -> (
match (int2symbol_kind (get_symbol_kind ctx#get_native x)) with match (int2symbol_kind (get_symbol_kind ctx#get_native x)) with
| INT_SYMBOL -> (new intsymbol ctx obj :> symbol) | INT_SYMBOL -> (new int_symbol ctx obj :> symbol)
| STRING_SYMBOL -> (new stringsymbol ctx obj :> symbol) | STRING_SYMBOL -> (new string_symbol ctx obj :> symbol)
) )
| None -> raise (Exception "Can't create null objects") | 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 = let is_int_symbol o = match o#m_n_obj with
object(self) | Some(x) -> x#kind == INT_SYMBOL
inherit symbol ctx_init obj_init | _ -> false
method get_int = match m_n_obj with let is_string_symbol o = match o#m_n_obj with
| Some(x) -> (get_symbol_int m_ctx#get_native x) | 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 | None -> 0
end
and stringsymbol ctx_init obj_init = let get_string o = match o#m_n_obj with
object(self) | Some(x) -> (get_symbol_string o#get_native_context x)
inherit symbol ctx_init obj_init | 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 end