diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 33129f555..2c525861c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1866,11 +1866,7 @@ def mk_config(): if GPROF: print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) -<<<<<<< HEAD print('ML API: %s' % is_ml_enabled()) -======= - print 'ML API: %s' % is_ml_enabled() ->>>>>>> Beginnings of a new ML API if is_java_enabled(): print('JNI Bindings: %s' % JNI_HOME) print('Java Compiler: %s' % JAVAC) @@ -2738,9 +2734,6 @@ def mk_z3consts_ml(api_files): if not os.path.exists(gendir): os.mkdir(gendir) -<<<<<<< HEAD -<<<<<<< HEAD -<<<<<<< HEAD efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w') efile.write('(* Automatically generated file *)\n\n') efile.write('(** The enumeration types of Z3. *)\n\n') @@ -2822,23 +2815,7 @@ def mk_z3consts_ml(api_files): 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') -======= - efile = open('%s.ml' % os.path.join(gendir, "z3_enums"), 'w') - efile.write('(* Automatically generated file *)\n\n') - # efile.write('module z3_enums = struct\n\n'); - - ->>>>>>> More new ML API -======= - efile = open('%s.ml' % os.path.join(gendir, "enumerations"), 'w') - efile.write('(* Automatically generated file *)\n\n') - efile.write('module Enumerations = struct\n') ->>>>>>> More ML API -======= - efile = open('%s.ml' % os.path.join(gendir, "z3enums"), 'w') - efile.write('(* Automatically generated file *)\n\n') efile.write('module Z3enums = struct\n') ->>>>>>> New native ML API layer. 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) @@ -2884,8 +2861,6 @@ def mk_z3consts_ml(api_files): if m: name = words[1] if name not in DeprecatedEnums: -<<<<<<< HEAD -<<<<<<< HEAD efile.write('(** %s *)\n' % name[3:]) efile.write('type %s =\n' % name[3:]) # strip Z3_ for k, i in decls.iteritems(): @@ -2896,17 +2871,10 @@ def mk_z3consts_ml(api_files): 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') -======= efile.write('\n(* %s *)\n' % name) -======= ->>>>>>> More ML API efile.write('type %s =\n' % name[3:]) # strip Z3_ for k, i in decls.iteritems(): -<<<<<<< HEAD efile.write(' | %s \n' % k[3:]) # strip Z3_ ->>>>>>> More new ML API -======= - efile.write(' | %s \n' % k[3:]) # strip Z3_ efile.write('\n') efile.write('let %s2int x : int =\n' % (name[3:])) # strip Z3_ efile.write(' match x with\n') @@ -2919,7 +2887,6 @@ def mk_z3consts_ml(api_files): efile.write(' | %d -> %s\n' % (i, k[3:])) # use Z3.Exception? efile.write(' | _ -> raise (Failure "undefined enum value")\n\n') ->>>>>>> More ML API mode = SEARCHING else: if words[2] != '': @@ -2930,21 +2897,9 @@ def mk_z3consts_ml(api_files): decls[words[1]] = idx idx = idx + 1 linenum = linenum + 1 -<<<<<<< HEAD -<<<<<<< HEAD - if VERBOSE: - print "Generated '%s/z3enums.mli'" % ('%s' % gendir) -======= - efile.write('\n') - # efile.write'end\n'); - if VERBOSE: - print "Generated '%s/z3_enums.ml'" % ('%s' % gendir) ->>>>>>> More new ML API -======= efile.write('end\n') if VERBOSE: print "Generated '%s/enumerations.ml'" % ('%s' % gendir) ->>>>>>> More ML API def mk_gui_str(id): return '4D2F40D8-E5F9-473B-B548-%012d' % id diff --git a/scripts/update_api.py b/scripts/update_api.py index f142c8ec1..a586ad6e3 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -159,7 +159,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 @@ -213,10 +213,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); @@ -1106,6 +1103,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 @@ -1114,29 +1112,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') @@ -1192,9 +1173,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') @@ -1202,8 +1183,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 5251a8767..a6a388aa7 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -1,11 +1,83 @@ (* 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 -end