ML API and example compilation.

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

examples/ml/README

@@ -5,10 +5,10 @@ To build the example execute
    make examples
 in the build directory.
 
-It will create MLExample in the build directory,
+It will create ml_example in the build directory,
-which can be run on Windows via 
+which can be run in the build directory via 
-ocaml -I . MLExample
+LD_LIBRARY_PATH=. ./ml_example
-
+or
-On Linux and FreeBSD, we must use
+LD_LIBRARY_PATH=. ./ml_example.byte
-?? 
+for the byte-code version.
 

examples/ml/ml_example.ml

@@ -0,0 +1,14 @@
+(* 
+   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
+  Printf.printf "Disposing...\n";
+  ctx#dispose ;
+  Printf.printf "Exiting.\n";
+;;

examples/ml/mlexample.ml

@@ -1,12 +0,0 @@
-(* 
-   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
-;;

scripts/mk_util.py

@@ -1296,10 +1296,6 @@ class MLComponent(Component):
             bld_dir = os.path.join(BUILD_DIR, 'api', 'ml')
             mk_dir(bld_dir)
             libfile = '%s$(SO_EXT)' % self.lib_name
-            # for mlfile in get_ml_files(self.src_dir):
-            #     out.write('%si: libz3$(SO_EXT) %s\n' % (os.path.join('api', 'ml', mlfile),os.path.join(self.to_src_dir, mlfile)))
-            #     out.write('\tocamlopt -I %s -i %s > %si\n' % (os.path.join('api', 'ml'), os.path.join(self.to_src_dir, mlfile), os.path.join('api', 'ml', mlfile)))
-            #     out.write('\tocamlopt -I %s -c %si \n' % (os.path.join('api', 'ml'), os.path.join('api','ml', mlfile)))
             out.write('%s: libz3$(SO_EXT) %s' % (libfile, os.path.join(self.to_src_dir, 'z3native.c')))
             for mlfile in get_ml_files(self.src_dir):
                 out.write(' %s' % os.path.join(self.to_src_dir, mlfile))
@@ -1307,11 +1303,9 @@ class MLComponent(Component):
             out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/ml/z3native$(OBJ_EXT) -I%s %s/z3native.c\n' % (get_component(API_COMPONENT).to_src_dir, self.to_src_dir))
             out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %  (libfile, os.path.join('api', 'ml', 'z3native')))
             out.write('z3.cmxa: %s\n' % libfile)
-            out.write('\tcd %s && ocamlbuild -lflags -cclib,../../../%s/libz3ml.so,-cclib,../../../%s/libz3.so -build-dir ../../../%s/api/ml z3.cmxa && cd -\n' % (self.to_src_dir,BUILD_DIR,BUILD_DIR,BUILD_DIR))
+            out.write('\tcd %s && ocamlbuild -cflags \'-g\' -lflags -cclib,-L../..,-cclib,-lz3,-cclib,-lz3ml,-linkall -build-dir ../../../%s/api/ml z3.cmxa z3native$(OBJ_EXT) && cd -\n' % (self.to_src_dir,BUILD_DIR))
-            out.write('\tcp api/ml/z3.cmxa .\n')
             out.write('z3.cma: %s\n' % libfile)
-            out.write('\tcd %s && ocamlbuild -lflags -custom,-cclib,../../../%s/libz3ml.so,-cclib,../../../%s/libz3.so -build-dir ../../../%s/api/ml z3.cma && cd -\n' % (self.to_src_dir,BUILD_DIR,BUILD_DIR,BUILD_DIR))
+            out.write('\tcd %s && ocamlbuild -cflags \'-g\' -lflags -custom,-cclib,-L../..,-cclib,-lz3,-cclib,-lz3ml,-linkall -build-dir ../../../%s/api/ml z3native$(OBJ_EXT) z3.cma && cd -\n' % (self.to_src_dir,BUILD_DIR))
-            out.write('\tcp api/ml/z3.cma .\n')
             out.write('ml: z3.cmxa z3.cma\n')
             out.write('\n')
     
@@ -1436,14 +1430,23 @@ class MLExampleComponent(ExampleComponent):
 
     def mk_makefile(self, out):
         if ML_ENABLED:
-            out.write('_ex_%s: z3.cmxa' % self.name)
+            out.write('ml_example.byte: z3.cma ')
-            deps = ''
             for mlfile in get_ml_files(self.ex_dir):
                 out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))                
-            if IS_WINDOWS:
+            out.write('\n')
-                deps = deps.replace('/', '\\')
+            out.write('\tocamlc -g -o ml_example.byte -I . z3.cma -I api/ml')
-            out.write('%s\n' % deps)
+            for mlfile in get_ml_files(self.ex_dir):
-            out.write('\tcd %s && ocamlbuild -build-dir ../../%s -lib z3 MLExample.native && cd -\n\n' % (self.to_src_dir, BUILD_DIR))
+                out.write(' %s/%s' % (self.to_ex_dir, mlfile))
+            out.write('\n')
+            out.write('ml_example($EXE_EXT): z3.cmxa ')
+            for mlfile in get_ml_files(self.ex_dir):
+                out.write(' %s' % os.path.join(self.to_ex_dir, mlfile))                
+            out.write('\n')
+            out.write('\tocamlopt -g -o ml_example -I . z3.cmxa -I api/ml')
+            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)
 
 class PythonExampleComponent(ExampleComponent):
     def __init__(self, name, path):

src/api/ml/z3.ml

@@ -3463,7 +3463,7 @@ object (self)
        Disposes of the underlying native Z3 object. 
     *)
   method dispose =
-    Printf.printf "Disposing %d \n" (Oo.id self) ;
+    Printf.printf "Disposing z3object %d \n" (Oo.id self) ;
     (match m_n_obj with
       | Some (x) -> self#decref x; m_n_obj <- None
       | None -> ()