More ML API:

Fixes in native layer.
Added symbols.
Prepared code for automatic documentation.

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

examples/ml/ml_example.ml

@@ -4,6 +4,7 @@
 *)
 
 open Z3
+open Z3.Context
 
 exception ExampleException of string
 
@@ -15,6 +16,10 @@ let _ =
       Printf.printf "Running Z3 version %s\n" Version.to_string ;
       let cfg = [("model", "true"); ("proof", "false")] in
       let ctx = (new context cfg) in
+      let is = (mk_symbol_int ctx 42) in
+      let ss = (mk_symbol_string ctx "mySymbol") in
+      Printf.printf "int symbol: %s\n" (Symbol.to_string (is :> symbol));
+      Printf.printf "string symbol: %s\n" (Symbol.to_string (ss :> symbol));
       Printf.printf "Disposing...\n";
       ctx#dispose (* can do, but we'd rather let it go out of scope *) ;
     );

scripts/mk_util.py

@@ -2777,99 +2777,12 @@ def mk_z3consts_ml(api_files):
                             efile.write('  | %s \n' % k[3:]) # strip Z3_
                         efile.write('\n')
                         efile.write('(** Convert %s to int*)\n' % name[3:])
-                        efile.write('let int_of_%s x : int =\n' % (name[3:])) # strip Z3_
-                        efile.write('  match x with\n')
-                        for k, i in decls.iteritems():
-                            efile.write('  | %s -> %d\n' % (k[3:], i))
-                        efile.write('\n')
-                        efile.write('(** Convert int to %s*)\n' % name[3:])
-                        efile.write('let %s_of_int x : %s =\n' % (name[3:],name[3:])) # strip Z3_
-                        efile.write('  match x with\n')
-                        for k, i in decls.iteritems():
-                            efile.write('  | %d -> %s\n' % (i, k[3:]))
-                        # use Z3.Exception?
-                        efile.write('  | _ -> raise (Failure "undefined enum value")\n\n')
-                    mode = SEARCHING
-                else:
-                    if words[2] != '':
-                        if len(words[2]) > 1 and words[2][1] == 'x':
-                            idx = int(words[2], 16)
-                        else:
-                            idx = int(words[2])
-                    decls[words[1]] = idx
-                    idx = idx + 1
-            linenum = linenum + 1
-    if VERBOSE:
-        print "Generated '%s/z3enums.ml'" % ('%s' % gendir)
-    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.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)
-
-        api = open(api_file, 'r')
-
-        SEARCHING  = 0
-        FOUND_ENUM = 1
-        IN_ENUM    = 2
-
-        mode    = SEARCHING
-        decls   = {}
-        idx     = 0
-
-        linenum = 1
-        for line in api:
-            m1 = blank_pat.match(line)
-            m2 = comment_pat.match(line)
-            if m1 or m2:
-                # skip blank lines and comments
-                linenum = linenum + 1 
-            elif mode == SEARCHING:
-                m = typedef_pat.match(line)
-                if m:
-                    mode = FOUND_ENUM
-                m = typedef2_pat.match(line)
-                if m:
-                    mode = IN_ENUM
-                    decls = {}
-                    idx   = 0
-            elif mode == FOUND_ENUM:
-                m = openbrace_pat.match(line)
-                if m:
-                    mode  = IN_ENUM
-                    decls = {}
-                    idx   = 0
-                else:
-                    assert False, "Invalid %s, line: %s" % (api_file, linenum)
-            else:
-                assert mode == IN_ENUM
-                words = re.split('[^\-a-zA-Z0-9_]+', line)
-                m = closebrace_pat.match(line)
-                if m:
-                    name = words[1]
-                    if name not in DeprecatedEnums:
-                        efile.write('(** %s *)\n' % name[3:])
-                        efile.write('type %s =\n' % name[3:]) # strip Z3_
-                        for k, i in decls.iteritems():
-                            efile.write('  | %s \n' % k[3:]) # strip Z3_
-                        efile.write('\n')
-                        efile.write('(** Convert %s to int*)\n' % name[3:])
-                        efile.write('val int_of_%s : %s -> int\n' % (name[3:], name[3:])) # strip Z3_
-                        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)
-                        efile.write('type %s =\n' % name[3:]) # strip Z3_
-                        for k, i in decls.iteritems():
-                            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')
                         for k, i in decls.iteritems():
                             efile.write('  | %s -> %d\n' % (k[3:], i))
                         efile.write('\n')
+                        efile.write('(** Convert int to %s*)\n' % name[3:])
                         efile.write('let int2%s x : %s =\n' % (name[3:],name[3:])) # strip Z3_
                         efile.write('  match x with\n')
                         for k, i in decls.iteritems():

scripts/update_api.py

@@ -1106,26 +1106,26 @@ def arrayparams(params):
     return op
 
 
-def ml_unwrap(t):
+def ml_unwrap(t, ts, s):
     if t == STRING:
-        return 'String_val'
+        return '(' + ts + ') String_val(' + s + ')'
-    elif t == BOOL or t == INT or PRINT_MODE or ERROR_CODE:
+    elif t == BOOL or t == INT or t == PRINT_MODE or t == ERROR_CODE:
-        return 'Int_val'
+        return '(' + ts + ') Int_val(' + s + ')'
     elif t == UINT:
-        return 'Unsigned_int_val'
+        return '(' + ts + ') Unsigned_int_val(' + s + ')'
     elif t == INT64:
-        return 'Long_val'
+        return '(' + ts + ') Long_val(' + s + ')'
     elif t == UINT64:
-        return 'Unsigned_long_val'
+        return '(' + ts + ') Unsigned_long_val(' + s + ')'
     elif t == DOUBLE:
-        return 'Double_val'
+        return '(' + ts + ') Double_val(' + s + ')'
     else:
-        return 'Data_custom_val'
+        return '* (' + ts + '*) Data_custom_val(' + s + ')'
 
 def ml_set_wrap(t, d, n):
     if t == VOID:
         return d + ' = Val_unit;'
-    elif t == BOOL or t == INT or t == UINT or PRINT_MODE or ERROR_CODE:
+    elif t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE:
         return d + ' = Val_int(' + n + ');'
     elif t == INT64 or t == UINT64:
         return d + ' = Val_long(' + n + ');'
@@ -1135,7 +1135,7 @@ def ml_set_wrap(t, d, n):
         return d + ' = caml_copy_string((const char*) ' + n + ');'
     else:
         ts = type2str(t)
-        return d + ' = caml_alloc_custom(0, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));'
+        return d + ' = caml_alloc_custom(&default_custom_ops, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));'
 
 def mk_ml():
     global Type2Str
@@ -1146,7 +1146,9 @@ def mk_ml():
     ml_wrapperf = os.path.join(ml_dir, 'z3native.c')
     ml_native   = open(ml_nativef, 'w')
     ml_native.write('(* Automatically generated file *)\n\n')
+    ml_native.write('(** The native (raw) interface to the dynamic Z3 library. *)\n\n')
     ml_native.write('open Z3enums\n\n')
+    ml_native.write('(**/**)\n')
     ml_native.write('type ptr\n')
     ml_native.write('and z3_symbol = ptr\n')
     for k, v in Type2Str.iteritems():
@@ -1226,6 +1228,7 @@ def mk_ml():
         else:
             ml_native.write('        res\n')
         ml_native.write('\n')
+    ml_native.write('(**/**)\n')
 
     # C interface
     ml_wrapper = open(ml_wrapperf, 'w')
@@ -1276,6 +1279,14 @@ def mk_ml():
     ml_wrapper.write('  CAMLxparam5(X6,X7,X8,X9,X10);                                     \\\n')
     ml_wrapper.write('  CAMLxparam3(X11,X12,X13);                                           \n')
     ml_wrapper.write('\n\n')
+    ml_wrapper.write('static struct custom_operations default_custom_ops = {\n')
+    ml_wrapper.write('  identifier: "default handling",\n')
+    ml_wrapper.write('  finalize:    custom_finalize_default,\n')
+    ml_wrapper.write('  compare:     custom_compare_default,\n')
+    ml_wrapper.write('  hash:        custom_hash_default,\n')
+    ml_wrapper.write('  serialize:   custom_serialize_default,\n')
+    ml_wrapper.write('  deserialize: custom_deserialize_default\n')
+    ml_wrapper.write('};\n\n')
     ml_wrapper.write('#ifdef __cplusplus\n')
     ml_wrapper.write('extern "C" {\n')
     ml_wrapper.write('#endif\n\n')
@@ -1342,10 +1353,10 @@ def mk_ml():
                 t = param_type(param)
                 ts = type2str(t)
                 ml_wrapper.write('  %s * _a%s = (%s*) malloc(sizeof(%s) * a%s);\n' % (ts, i, ts, ts, param_array_capacity_pos(param)))
-                ml_wrapper.write('  for (unsigned i = 0; i < a%s; i++) _a%s[i] = (%s) %s(Field(a%s, i));\n' % (param_array_capacity_pos(param), i, ts, ml_unwrap(t), i))
+                ml_wrapper.write('  for (unsigned i = 0; i < _a%s; i++) _a%s[i] = %s;\n' % (param_array_capacity_pos(param), i, ml_unwrap(t, ts, 'Field(a' + str(i) + ', i)')))
             elif k == IN:
                 t = param_type(param)
-                ml_wrapper.write('  %s _a%s = (%s) %s(a%s);\n' % (type2str(t), i, type2str(t), ml_unwrap(t), i))
+                ml_wrapper.write('  %s _a%s = %s;\n' % (type2str(t), i, ml_unwrap(t, type2str(t), 'a' + str(i))))
             elif k == OUT:
                 ml_wrapper.write('  %s _a%s;\n' % (type2str(param_type(param)), i))
             elif k == INOUT:

src/api/ml/z3.ml

@@ -1,33 +1,17 @@
-(* 
+(**
+   The Z3 ML/Ocaml Interface.
+
    Copyright (C) 2012 Microsoft Corporation
-   Author: CM Wintersteiger (cwinter) 2012-12-17
+   @author CM Wintersteiger (cwinter) 2012-12-17
 *)
 
 open Z3enums
 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
-end
 
-module Version =
+(* Object definitions. These are internal and should be interacted 
-struct
+   with only via the corresponding functions from modules. *)
-  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 = 
-    let (mj, mn, bld, rev) = get_version in
-    string_of_int mj ^ "." ^
-      string_of_int mn ^ "." ^
-      string_of_int bld ^ "." ^
-      string_of_int rev ^ "."
-end
 
 class virtual idisposable = 
 object
@@ -61,7 +45,7 @@ object (self)
 
   method sub_one_ctx_obj = m_refCount <- m_refCount - 1
   method add_one_ctx_obj = m_refCount <- m_refCount + 1
-  method get_native = m_n_ctx
+  method gno = m_n_ctx
 end
 
 class virtual z3object ctx_init obj_init =
@@ -91,9 +75,9 @@ object (self)
       | None -> ()
     ); 
 
-  method get_native_object = m_n_obj
+  method gno = m_n_obj
 
-  method set_native_object x =
+  method sno x =
     (match x with
       | Some(x) -> self#incref x
       | None -> ()
@@ -105,11 +89,11 @@ object (self)
     m_n_obj <- x
 
   method get_context = m_ctx
-  method get_native_context = m_ctx#get_native
+  method gnc = m_ctx#gno
 
 (*
   method array_to_native a =
-    let f e = e#get_native_object in 
+    let f e = e#gno in 
     (Array.map f a) 
 
   method array_length a =
@@ -120,61 +104,145 @@ object (self)
 
 end
 
-class symbol ctx_init obj_init = 
+class symbol ctx obj = 
 object (self)
-  inherit z3object ctx_init obj_init
+  inherit z3object ctx obj
 
   method incref o = ()
   method decref o = ()
 end
 
-class int_symbol ctx_init obj_init  = 
+class int_symbol ctx = 
 object(self)
-  inherit symbol ctx_init obj_init
+  inherit symbol ctx None
+  method cnstr_obj obj = (self#sno obj) ; self
+  method cnstr_int i = (self#sno (Some (mk_int_symbol ctx#gno i))) ; self
 end
 
-class string_symbol ctx_init obj_init = 
+class string_symbol ctx = 
 object(self)
-  inherit symbol ctx_init obj_init
+  inherit symbol ctx None
+  method cnstr_obj obj = (self#sno obj) ; self
+  method cnstr_string name = (self#sno (Some (mk_string_symbol ctx#gno name))) ; self
 end
 
+(**/**)
+
+(** Interaction logging for Z3.
+    Note that this is a global, static log and if multiple Context 
+    objects are created, it logs the interaction with all of them. *)
+module Log = 
+struct
+  (** Open an interaction log file. 
+      @param filename the name of the file to open.
+      @return True if opening the log file succeeds, false otherwise.
+  *)
+  (* CMW: "open" seems to be a reserved keyword? *)
+  let open_ filename = ((int2lbool (open_log filename)) == L_TRUE)
+
+  (** Closes the interaction log. *)
+  let close = close_log
+
+  (** Appends a user-provided string to the interaction log.
+      @param s the string to append*)
+  let append s = append_log s
+end
+
+(** Version information. *)
+module Version =
+struct
+  (** The major version. *)
+  let major = let (x, _, _, _) = get_version in x
+
+  (** The minor version. *)
+  let minor = let (_, x, _, _) = get_version in x
+
+  (** The build version. *)
+  let build = let (_, _, x, _) = get_version in x
+
+  (** The revision. *)
+  let revision = let (_, _, _, x) = get_version in x
+
+  (** A string representation of the version information. *)
+  let to_string = 
+    let (mj, mn, bld, rev) = get_version in
+    string_of_int mj ^ "." ^
+      string_of_int mn ^ "." ^
+      string_of_int bld ^ "." ^
+      string_of_int rev ^ "."
+end
+
+(** Symbols are used to name several term and type constructors. *)
 module Symbol =
 struct
+(**/**)
   let create ctx obj =
     match obj with 
       | Some(x) -> (
-	match (int2symbol_kind (get_symbol_kind ctx#get_native x)) with
+	match (int2symbol_kind (get_symbol_kind ctx#gno x)) with
-	  | INT_SYMBOL -> (new int_symbol ctx obj :> symbol)
+	  | INT_SYMBOL -> (((new int_symbol ctx)#cnstr_obj obj) :> symbol)
-          | STRING_SYMBOL -> (new string_symbol ctx obj :> symbol)
+          | STRING_SYMBOL -> (((new string_symbol ctx)#cnstr_obj obj) :> symbol)
       )
       | None -> raise (Exception "Can't create null objects")
+(**/**)
 
-  let kind o = match o#m_n_obj with
+  (** The kind of the symbol (int or string) *)
-    | Some(x) -> (int2symbol_kind (get_symbol_kind o#get_native_context x))
+  let kind (o : symbol) = match o#gno with
+    | Some(x) -> (int2symbol_kind (get_symbol_kind o#gnc x))
     | _ -> raise (Exception "Underlying object lost")
 
-  let is_int_symbol o = match o#m_n_obj with
+  (** Indicates whether the symbol is of Int kind *)
-    | Some(x) -> x#kind == INT_SYMBOL
+  let is_int_symbol (o : symbol) = match o#gno with
+    | Some(x) -> (kind o) == INT_SYMBOL
     | _ -> false
 
-  let is_string_symbol o = match o#m_n_obj with
+  (** Indicates whether the symbol is of string kind. *)
-    | Some(x) -> x#kind == STRING_SYMBOL
+  let is_string_symbol (o : symbol) = match o#gno with
+    | Some(x) -> (kind o) == STRING_SYMBOL
     | _ -> false
 
-  let get_int o = match o#m_n_obj with
+  (** The int value of the symbol. *)
-    | Some(x) -> (get_symbol_int o#get_native_context x)
+  let get_int (o : int_symbol) = match o#gno with
+    | Some(x) -> (get_symbol_int o#gnc x)
     | None -> 0
 
-  let get_string o = match o#m_n_obj with
+  (** The string value of the symbol. *)
-    | Some(x) -> (get_symbol_string o#get_native_context x)
+  let get_string (o : string_symbol) = match o#gno with
+    | Some(x) -> (get_symbol_string o#gnc x)
     | None -> ""
 
-  let to_string o = match o#m_n_obj with
+  (** A string representation of the symbol. *)
+  let to_string (o : symbol) = match o#gno with
     | Some(x) -> 
       (
 	match (kind o) with
-	  | INT_SYMBOL -> (string_of_int (get_symbol_int o#get_native_context x))
+	  | INT_SYMBOL -> (string_of_int (get_symbol_int o#gnc x))
-	  | STRING_SYMBOL -> (get_symbol_string o#get_native_context x)
+	  | STRING_SYMBOL -> (get_symbol_string o#gnc x)
       )
     | None -> ""
 end
+
+(** The main interaction with Z3 happens via the Context. *)
+module Context =
+struct
+  (**
+     Creates a new symbol using an integer.
+     
+     Not all integers can be passed to this function.
+     The legal range of unsigned integers is 0 to 2^30-1.
+  *)
+  let mk_symbol_int ctx i = 
+    (new int_symbol ctx)#cnstr_int i
+    
+  (** Creates a new symbol using a string. *)
+  let mk_symbol_string ctx s =
+    (new string_symbol ctx)#cnstr_string s
+
+  (**
+     Create an array of symbols.
+  *)
+  let mk_symbols ctx names =
+    let f elem = mk_symbol_string ctx elem in
+    (Array.map f names)
+      
+end