From f7b3529f0166facc8b94b6becbe97b56e4abc54d Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 19 Dec 2012 16:33:51 +0000
Subject: [PATCH] More ML API

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
---
 examples/ml/MLExample.ml | 12 ++++++++
 scripts/mk_util.py       |  9 +++++-
 src/api/ml/README        |  3 --
 src/api/ml/z3.ml         | 59 ++++++++++++++++++++++++++++++++--------
 4 files changed, 67 insertions(+), 16 deletions(-)
 create mode 100644 examples/ml/MLExample.ml

diff --git a/examples/ml/MLExample.ml b/examples/ml/MLExample.ml
new file mode 100644
index 000000000..8cc248206
--- /dev/null
+++ b/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
+;;
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 2c525861c..40828f8c3 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1597,7 +1597,14 @@ class MLExampleComponent(ExampleComponent):
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s/%s' % (self.to_ex_dir, mlfile))
             out.write('\n')
-            out.write('_ex_%s: ml_example.byte ml_example$(EXE_EXT)\n\n' % self.name)
+            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):
diff --git a/src/api/ml/README b/src/api/ml/README
index f8984c79e..36f903925 100644
--- a/src/api/ml/README
+++ b/src/api/ml/README
@@ -1,11 +1,8 @@
 This directory is work in progress.
 
 We are currently working on a brand new ML API.
-<<<<<<< HEAD
 
 On Windows, there are no less than four different ports of OCaml. The Z3 build 
 system assumes that either the win32 or the win64 port is installed. This means
 that OCaml will use `cl' as the underlying C compiler and not the cygwin or
 mingw compilers. 
-=======
->>>>>>> Beginnings of a new ML API
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index a6a388aa7..0329402dd 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -1,27 +1,60 @@
 (* 
-   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
 	
@@ -34,7 +67,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
@@ -42,7 +75,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
@@ -70,6 +103,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) 
@@ -78,6 +112,7 @@ class virtual z3object ctx_init obj_init =
       match a with
       | Some(x) -> (Array.length x)
       | None -> 0
+*)
 
   end