More ML API

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

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)
 

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')

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