More ML API

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

examples/ml/MLExample.ml

@@ -0,0 +1,12 @@
+(* 
+   Copyright (C) 2012 Microsoft Corporation
+   Author: CM Wintersteiger (cwinter) 2012-12-17
+ *)
+   
+   open Z3
+   
+   let _ = ignore(Log.open_ "z3.log") ;
+let cfg = Some [("model", "true"); ("proof", "false")] in
+let ctx = (new context cfg) in
+ctx#dispose
+;;

examples/ml/README

@@ -0,0 +1,14 @@
+### This is work-in-progress and does not work yet.
+
+Small example using the Z3 ML bindings.
+To build the example execute
+   make examples
+in the build directory.
+
+It will create MLExample in the build directory,
+which can be run on Windows via 
+ocaml -I . MLExample
+
+On Linux and FreeBSD, we must use
+?? 
+   

scripts/mk_project.py

@@ -98,6 +98,7 @@ def init_project_def():
     add_c_example('maxsat')
     add_dotnet_example('dotnet_example', 'dotnet')
     add_java_example('java_example', 'java')
+    add_ml_example('ml_example', 'ml')
     add_z3py_example('py_example', 'python')
     return API_files
 

scripts/mk_util.py

@@ -1427,6 +1427,24 @@ class JavaExampleComponent(ExampleComponent):
             out.write(' -d .\n')
             out.write('_ex_%s: JavaExample.class\n\n' % (self.name))
 
+class MLExampleComponent(ExampleComponent):
+    def __init__(self, name, path):
+        ExampleComponent.__init__(self, name, path)
+
+    def is_example(self):
+        return ML_ENABLED
+
+    def mk_makefile(self, out):
+        if ML_ENABLED:
+            out.write('_ex_%s: z3.cmxa' % self.name)
+            deps = ''
+            for mlfile in get_ml_files(self.ex_dir):
+                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))
+            if IS_WINDOWS:
+                deps = deps.replace('/', '\\')
+            out.write('%s\n' % deps)
+            out.write('\tcd %s && ocamlbuild -build-dir ../../%s -lib z3 MLExample.native && cd -\n\n' % (self.to_src_dir, BUILD_DIR))
+
 class PythonExampleComponent(ExampleComponent):
     def __init__(self, name, path):
         ExampleComponent.__init__(self, name, path)
@@ -1500,6 +1518,10 @@ def add_java_example(name, path=None):
     c = JavaExampleComponent(name, path)
     reg_component(name, c)
 
+def add_ml_example(name, path=None):
+    c = MLExampleComponent(name, path)
+    reg_component(name, c)
+
 def add_z3py_example(name, path=None):
     c = PythonExampleComponent(name, path)
     reg_component(name, c)

src/api/ml/z3.ml

@@ -3386,29 +3386,62 @@ end
 
 =======
 (* 
-   Author: CM Wintersteiger
-   (C) Microsoft Research, 2012
+   Copyright (C) 2012 Microsoft Corporation
+   Author: CM Wintersteiger (cwinter) 2012-12-17
  *)
 
 open Z3enums
 open Z3native
 
-class context =
+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
+    
+class virtual idisposable = 
+  object
+    method virtual dispose : unit
+  end
+
+class context settings  =
   object (self)
-    val m_n_ctx : Z3native.z3_context option = None
+    inherit idisposable
+    val mutable 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 -> ()
+	
+    initializer 
+      let cfg = mk_config() in
+      (match settings with
+      | Some(x) -> 
+	  let f e = (set_param_value cfg (fst e) (snd e)) in
+	  (List.iter f x)
+      | _ -> ()	    
+      ) ;
+      m_n_ctx <- Some (mk_context_rc cfg) ;
+      del_config(cfg) ;
+      Gc.finalise (fun self -> self#dispose) self
+	
+    method dispose : unit = 
+      if m_refCount == 0 then (
+	Printf.printf "Disposing %d \n" (Oo.id self) ;
+	match m_n_ctx with
+	| Some(x) -> (del_context x)
+	| None -> ()
+       ) else (
+	(* re-queue for finalization? *)
+       )
+
     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)
+    inherit idisposable
     val mutable m_ctx : context option = ctx_init
     val mutable m_n_obj : Z3native.ptr option = obj_init
 	
@@ -3421,7 +3454,7 @@ class virtual z3object ctx_init obj_init =
 	  )
       | None -> ()
       );
-      Gc.finalise (fun self -> self#dispose ()) self
+      Gc.finalise (fun self -> self#dispose) self
 
     method virtual incref : Z3native.ptr -> unit
     method virtual decref : Z3native.ptr -> unit
@@ -3429,7 +3462,7 @@ class virtual z3object ctx_init obj_init =
         (* 
 	   Disposes of the underlying native Z3 object. 
 	 *)
-    method dispose () =
+    method dispose =
       Printf.printf "Disposing %d \n" (Oo.id self) ;
       (match m_n_obj with
       | Some (x) -> self#decref x; m_n_obj <- None
@@ -3457,6 +3490,7 @@ class virtual z3object ctx_init obj_init =
 
     method get_context = m_ctx
 
+(*
     method array_to_native a =
       let f e = e#get_native_object in 
       (Array.map f a) 
@@ -3465,6 +3499,7 @@ class virtual z3object ctx_init obj_init =
       match a with
       | Some(x) -> (Array.length x)
       | None -> 0
+*)
 
   end