More ML API

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

src/api/ml/z3.ml

@@ -1,118 +1,118 @@
 (* 
    Copyright (C) 2012 Microsoft Corporation
    Author: CM Wintersteiger (cwinter) 2012-12-17
- *)
+*)
 
 open Z3enums
 open Z3native
 
 module Log = 
-  struct
+struct
-    let m_is_open = false
+  let m_is_open = false
-(* CMW: "open" seems to be an invalid function name*)
+    (* CMW: "open" seems to be an invalid function name*)
-    let open_ fn = int2lbool(open_log fn) == L_TRUE
+  let open_ fn = int2lbool(open_log fn) == L_TRUE
-    let close = (close_log)
+  let close = (close_log)
-    let append s = (append_log s)
+  let append s = (append_log s)
-  end
+end
   
 class virtual idisposable = 
-  object
+object
-    method virtual dispose : unit
+  method virtual dispose : unit
-  end
+end
 
 class context settings  =
-  object (self)
+object (self)
-    inherit idisposable
+  inherit idisposable
-    val mutable m_n_ctx : Z3native.z3_context option = None
+  val mutable m_n_ctx : Z3native.z3_context option = None
-    val mutable m_refCount : int = 0
+  val mutable m_refCount : int = 0
     
-    initializer 
+  initializer 
-      let cfg = mk_config() in
+  let cfg = mk_config() in
-      (match settings with
+  (match settings with
-      | Some(x) -> 
+    | Some(x) -> 
-	  let f e = (set_param_value cfg (fst e) (snd e)) in
+      let f e = (set_param_value cfg (fst e) (snd e)) in
-	  (List.iter f x)
+      (List.iter f x)
-      | _ -> ()	    
+    | _ -> ()	    
-      ) ;
+  ) ;
-      m_n_ctx <- Some (mk_context_rc cfg) ;
+  m_n_ctx <- Some (mk_context_rc cfg) ;
-      del_config(cfg) ;
+  del_config(cfg) ;
-      Gc.finalise (fun self -> self#dispose) self
+  Gc.finalise (fun self -> self#dispose) self
     
-    method dispose : unit = 
+  method dispose : unit = 
-      if m_refCount == 0 then (
+    if m_refCount == 0 then (
-	Printf.printf "Disposing %d \n" (Oo.id self) ;
+      Printf.printf "Disposing %d \n" (Oo.id self) ;
-	match m_n_ctx with
+      match m_n_ctx with
 	| Some(x) -> (del_context x)
 	| None -> ()
-       ) else (
+    ) else (
-	(* re-queue for finalization? *)
+       (* re-queue for finalization? *)
-       )
+    )
 
-    method sub_one_ctx_obj = m_refCount <- m_refCount - 1
+  method sub_one_ctx_obj = m_refCount <- m_refCount - 1
-    method add_one_ctx_obj = m_refCount <- m_refCount + 1
+  method add_one_ctx_obj = m_refCount <- m_refCount + 1
-  end
+end
 
 class virtual z3object ctx_init obj_init =
-  object (self)
+object (self)
-    inherit idisposable
+  inherit idisposable
-    val mutable m_ctx : context option = ctx_init
+  val mutable m_ctx : context option = ctx_init
-    val mutable m_n_obj : Z3native.ptr option = obj_init
+  val mutable m_n_obj : Z3native.ptr option = obj_init
     
-    initializer 
+  initializer 
-      (match m_n_obj with 
+    (match m_n_obj with 
       | Some (x) -> self#incref x;
-	  (match m_ctx with
+	(match m_ctx with
 	  | Some(x) -> x#add_one_ctx_obj
 	  | None -> ()
-	  )
+	)
       | None -> ()
-      );
+    );
-      Gc.finalise (fun self -> self#dispose) self
+    Gc.finalise (fun self -> self#dispose) self
 
-    method virtual incref : Z3native.ptr -> unit
+  method virtual incref : Z3native.ptr -> unit
-    method virtual decref : Z3native.ptr -> unit
+  method virtual decref : Z3native.ptr -> unit
     
-        (* 
+    (* 
-	   Disposes of the underlying native Z3 object. 
+       Disposes of the underlying native Z3 object. 
-	 *)
+    *)
-    method dispose =
+  method dispose =
-      Printf.printf "Disposing %d \n" (Oo.id self) ;
+    Printf.printf "Disposing %d \n" (Oo.id self) ;
-      (match m_n_obj with
+    (match m_n_obj with
       | Some (x) -> self#decref x; m_n_obj <- None
       | None -> ()
-      ); 
+    ); 
-      (match m_ctx with
+    (match m_ctx with
       | Some (x) -> x#sub_one_ctx_obj
       | None -> ()
-      );
+    );
-      m_ctx <- None
+    m_ctx <- None
 
 
-    method get_native_object = m_n_obj
+  method get_native_object = m_n_obj
 
-    method set_native_object x =
+  method set_native_object x =
-      (match x with
+    (match x with
       | Some(x) -> self#incref x
       | None -> ()
-      );
+    );
-      (match m_n_obj with
+    (match m_n_obj with
       | Some(x) -> self#decref x
       | None -> ()
-      );
+    );
-      m_n_obj <- x
+    m_n_obj <- x
 
-    method get_context = m_ctx
+  method get_context = m_ctx
 
-(*
+  (*
     method array_to_native a =
-      let f e = e#get_native_object in 
+    let f e = e#get_native_object in 
-      (Array.map f a) 
+    (Array.map f a) 
 
     method array_length a =
-      match a with
+    match a with
-      | Some(x) -> (Array.length x)
+    | Some(x) -> (Array.length x)
-      | None -> 0
+    | None -> 0
-*)
+  *)
 
-  end
+end