diff --git a/examples/ml/README b/examples/ml/README index a83400e99..3e1eb0d1c 100644 --- a/examples/ml/README +++ b/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, -which can be run on Windows via -ocaml -I . MLExample +It will create ml_example in the build directory, +which can be run in the build directory via +LD_LIBRARY_PATH=. ./ml_example +or +LD_LIBRARY_PATH=. ./ml_example.byte +for the byte-code version. -On Linux and FreeBSD, we must use -?? - diff --git a/examples/ml/ml_example.ml b/examples/ml/ml_example.ml new file mode 100644 index 000000000..9c704e4d0 --- /dev/null +++ b/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"; +;; diff --git a/examples/ml/mlexample.ml b/examples/ml/mlexample.ml deleted file mode 100644 index 8cc248206..000000000 --- a/examples/ml/mlexample.ml +++ /dev/null @@ -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 -;; diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 27913ab62..da7d22d54 100644 --- a/scripts/mk_util.py +++ b/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('\tcp api/ml/z3.cmxa .\n') + 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('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('\tcp api/ml/z3.cma .\n') + 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('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) - deps = '' + out.write('ml_example.byte: z3.cma ') 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)) + out.write(' %s' % os.path.join(self.to_ex_dir, mlfile)) + out.write('\n') + out.write('\tocamlc -g -o ml_example.byte -I . z3.cma -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('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): diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index fb8121c79..71e16898e 100644 --- a/src/api/ml/z3.ml +++ b/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 -> ()