From 2dde851ed7ec60719efb3290999d0fb41a45e3c8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 19 Dec 2012 08:06:10 +0000 Subject: [PATCH] More ML API Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_util.py | 5 ++- scripts/update_api.py | 58 +++++++++---------------------- src/api/ml/z3.ml | 80 +++++++++++++++++++++++++++++++++++++++++-- 3 files changed, 96 insertions(+), 47 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 962f15670..c17df82e6 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -458,7 +458,8 @@ def display_help(exit_code): if IS_WINDOWS: print(" -n, --nodotnet do not generate Microsoft.Z3.dll make rules.") print(" -j, --java generate Java bindings.") - print(" --staticlib build Z3 static library.") + print(" --ml generate Ocaml bindinds.") + print(" --staticlib build Z3 static library.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") print(" --gprof enable gprof") @@ -2546,7 +2547,6 @@ def mk_z3consts_ml(api_files): efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w') efile.write('(* Automatically generated file *)\n\n') - efile.write('module Z3enums = struct\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) @@ -2617,7 +2617,6 @@ def mk_z3consts_ml(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 - efile.write('end\n') if VERBOSE: print "Generated '%s/enumerations.ml'" % ('%s' % gendir) diff --git a/scripts/update_api.py b/scripts/update_api.py index b613ce79d..9eb7d1405 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -158,7 +158,7 @@ Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', I # Mapping to ML types Type2ML = { VOID : 'unit', VOID_PTR : 'VOIDP', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', STRING : 'string', STRING_PTR : 'char**', - BOOL : 'int', SYMBOL : 'symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' } + BOOL : 'int', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int' } next_type_id = FIRST_OBJ_ID @@ -182,6 +182,7 @@ def def_Types(): v = Type2Str[k] if is_obj(k): Type2Dotnet[k] = v + Type2ML[k] = v.lower() def type2str(ty): global Type2Str @@ -211,10 +212,7 @@ def type2javaw(ty): def type2ml(ty): global Type2ML - if (ty >= FIRST_OBJ_ID): - return 'int' - else: - return Type2ML[ty] + return Type2ML[ty] def _in(ty): return (IN, ty); @@ -327,17 +325,11 @@ def param2pystr(p): def param2ml(p): k = param_kind(p) if k == OUT: - if param_type(p) == INT or param_type(p) == UINT: - 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: + if param_type(p) == STRING: return "string" else: - print "ERROR: unreachable code" - assert(False) - exit(1) - if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + return "ptr" + elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s array" % type2ml(param_type(p)) else: return type2ml(param_type(p)) @@ -1104,6 +1096,7 @@ def is_array_param(p): return False def mk_ml(): + global Type2Str if not is_ml_enabled(): return ml_dir = get_component('ml').src_dir @@ -1112,29 +1105,12 @@ def mk_ml(): ml_native = open(ml_nativef, 'w') ml_native.write('(* Automatically generated file *)\n\n') ml_native.write('open Z3enums\n\n') - ml_native.write('module Z3native = 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\n') - ml_native.write(' exception Exception of string\n\n') + ml_native.write('type ptr\n') + ml_native.write('and z3_symbol = ptr\n') + for k, v in Type2Str.iteritems(): + if is_obj(k): + ml_native.write('and %s = ptr\n' % v.lower()) + ml_native.write('\nexception Exception of string\n\n') # ML declarations ml_native.write(' module ML2C = struct\n\n') @@ -1190,9 +1166,9 @@ def mk_ml(): i = i + 1 ml_native.write(') in\n') if len(params) > 0 and param_type(params[0]) == CONTEXT: - ml_native.write(' let err = (Z3enums.int2error_code (ML2C.n_get_error_code a0)) in \n') - ml_native.write(' if err <> Z3enums.OK then\n') - ml_native.write(' raise (Exception (ML2C.n_get_error_msg_ex a0 (Z3enums.error_code2int err)))\n') + ml_native.write(' let err = (int2error_code (ML2C.n_get_error_code a0)) in \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(' else\n') if result == VOID: ml_native.write(' ()\n') @@ -1200,8 +1176,6 @@ def mk_ml(): ml_native.write(' res\n') ml_native.write('\n') - ml_native.write('end\n') - # C interface ml_wrapper = open(ml_wrapperf, 'w') ml_wrapper.write('// Automatically generated file\n\n') diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 61ac503a0..b00569da1 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -3388,12 +3388,88 @@ end (* Author: CM Wintersteiger (C) Microsoft Research, 2012 -*) + *) open Z3enums open Z3native -module Z3 = struct +class context = + object (self) + val m_n_ctx : Z3native.z3_context option = None + val mutable m_refCount : int = 0 + initializer Gc.finalise (fun self -> self#dispose ()) self + method dispose () = + Printf.printf "Disposing %d \n" (Oo.id self) ; + match m_n_ctx with + | Some(x) -> (del_context x) + | None -> () + method sub_one_ctx_obj = m_refCount <- m_refCount - 1 + method add_one_ctx_obj = m_refCount <- m_refCount + 1 + end +class virtual z3object ctx_init obj_init = + object (self) + val mutable m_ctx : context option = ctx_init + val mutable m_n_obj : Z3native.ptr option = obj_init + + initializer + (match m_n_obj with + | Some (x) -> self#incref x; + (match m_ctx with + | Some(x) -> x#add_one_ctx_obj + | None -> () + ) + | None -> () + ); + Gc.finalise (fun self -> self#dispose ()) self + + method virtual incref : Z3native.ptr -> unit + method virtual decref : Z3native.ptr -> unit + + (* + Disposes of the underlying native Z3 object. + *) + method dispose () = + Printf.printf "Disposing %d \n" (Oo.id self) ; + (match m_n_obj with + | Some (x) -> self#decref x; m_n_obj <- None + | None -> () + ); + (match m_ctx with + | Some (x) -> x#sub_one_ctx_obj + | None -> () + ); + m_ctx <- None + + + method get_native_object = m_n_obj + + method set_native_object x = + (match x with + | Some(x) -> self#incref x + | None -> () + ); + (match m_n_obj with + | Some(x) -> self#decref x + | None -> () + ); + m_n_obj <- x + + method get_context = m_ctx + + method array_to_native a = + let f e = e#get_native_object in + (Array.map f a) + + method array_length a = + match a with + | Some(x) -> (Array.length x) + | None -> 0 + + end + +<<<<<<< HEAD end >>>>>>> More new ML API. +======= +>>>>>>> More ML API