diff --git a/ml/msbuild.proj b/ml/msbuild.proj deleted file mode 100644 index ee2a6915e..000000000 --- a/ml/msbuild.proj +++ /dev/null @@ -1,72 +0,0 @@ - - - - - - - - - - - - - - - - - - - - diff --git a/ml/readme.txt b/ml/readme.txt deleted file mode 100644 index 71b2ab56d..000000000 --- a/ml/readme.txt +++ /dev/null @@ -1,144 +0,0 @@ -Z3 - JakobL@2011-12-20 - -============================================================================== - -What: - -Z3 is a high-performance theorem prover being developed at Microsoft -Research by Nikolaj Bjørner (NBjorner) and Leonardo de Moura -(Leonardo). - -This folder contains the Z3 ML module used by the SLAM verification -engine. The Z3 ML module provides a complete ML interface to the Z3 -x86 native library. - -============================================================================== - -Multiple source depots: - -This folder is hosted in two separate source depots: -* SDT (sdport=BGIT-SDTVMDEPOT:5010): //depot/src/z3_2/ml/ -* SLAM (SDPort=BGIT-SDSLAM:7021): //depot/src/main/slam/engine/slam2/z3/ - -Goal is to have identical contents in both source depots. Reason for -hosting in SDT source depot: to allow for testing of the Z3 ML module -'close' to Z3. Reason for maintaining in SLAM source depot: to allow -for building SLAM without access to SDT. - -Discrepancy between usage and files in the two source depots are in -the following marked with [SDT] or [SLAM]. - -============================================================================== - -How to use the Z3 ML Module: - -* doc\index.html: Reference documentation of the ML interface. Notice: - This is generated during build and hence first available afterwards. - -* z3.mli: Provides the actual Z3 ML Signature, generated at build - time. The Reference documentation is built from this file. - -* test_mlapi.ml: Sample program that demonstrate how to use the Z3 ML library. - -* queen.ml: Sample program that demonstrate how to use the Z3 ML library. - -* import\z3.exe: Z3 shell: Useful for trying out queries. ([SDT]: in - %SDTROOT%\release_mt\z3.exe) - -============================================================================== - -Building and linking: - -Z3 ML is used as any other ML library. - -Prerequisites: - -* [SLAM]: Just a standard 'SDV Build Environment'. - -* [SDT]: NB. Make sure to use an x86 build window. - -1. Install OCaml: - * Install from: \\sdv-fs.ntdev.corp.microsoft.com\software\3rdParty\ocaml-3.07pl2-win-msvc.exe - Or from z3_2\tools - * Install to: C:\ocaml - -2. Install CamlIDL: - * Install from: \\sdv-fs.ntdev.corp.microsoft.com\software\Installers\camlidl-1.04-2.exe - Or from z3_2\tools - * Install to: C:\ocaml - -3. Build z3.sln's configuration 'release_mt': - cd %SDTROOT%\src\z3_2 - msbuild /target:lib /p:configuration=release_mt - msbuild /target:shell /p:configuration=release_mt - -To build and run regressions: -* [SLAM]: mb -* [SDT]: build - -To clean: -* [SLAM]: mc -* [SDT]: clean - -To link with your favorite app: -* [SLAM]: Reference z3.proj from your msbuild.proj file: - - -* [SDT]: Link the Z3 ML library as well as supporting libraries: - ocamlopt -ccopt "/MT /nologo /DWIN32" ole32.lib %OCAMLLIB%\libcamlidl.lib -I %SDTROOT%\src\z3_2\ml %SDTROOT%\src\z3_2\ml\z3.cmxa -o queen.exe queen.ml -============================================================================== - -Files: - -* readme.txt: This file -* build.cmd: Build script [SDT]: invoke directly; [SLAM]: invoked automatically -* clean.cmd: [SDT]: Script for cleaning; [SLAM]: use mc for cleaning -* regress.cmd: Script for updating regressions. Not for regular users. -* build.sed, update-ml-doc.cmd: Supporting scripts for building. -* diff.exe.exe: Supporting tool for building. Obtained from [SLAM] from //depot/src/main/tools/Win32/UnxUtils.zip. -* sed.exe: Supporting tool for building. Obtained from http://sed.sourceforge.net/ -> "super sed v3.59 for Windows by Paolo Bonzini" -> sed-3.59.zip -> sed-3.59.exe. See http://www.pement.org/sed/ for a good overview of sed for Windows. -* msbuild.proj: [SLAM only]: Used by mb and mc -* z3.proj: [SLAM only]: Project file for consumers of the Z3 module -* import.cmd: [SLAM only]: Script to import files from SDT. -* z3.idl,z3_api.idl: Interface definition files, z3_api.idl is autogenerated during build. -* z3.h: Supporting header file for z3.idl -* x3.{mli,ml}: Module X3 contains Z3 ML specific extensions. Do not use directly, included in Z3 during build. -* queen.ml: Z3 ML test program. -* test_mlapi.ml: Z3 ML test program. -* z3_theory_stubs.c and test_theory.ml: Theory plugin and test. - -*.regress.*: Regression files, used by build. - -[SLAM only]: -* import\z3lib.lib: Z3 C library. -* import\msbig_rational.lib: Supporting C library. -* import\test_capi.c: Z3 C test program. -* import\{z3.h,z3_api.h,z3_macros.h}: Z3 C header files. -* import\{mldoc_footer.html,tabs.css,test_mlapi_header.html,z3.png,z3_ml.css,z3_mlapi_header.html}: Files for automated documentation generation. - -============================================================================== - -Import from MSR: - -Certain files are imported from MSR. See above list for details as -well as import.cmd script. To determine the version of z3.exe you are -using, a bit of investigate work will lead you to exact build: - -Run import\z3.exe -version. This will generate: - Version (major minor build revision): 0 1 0 0 -Or: - Version (major minor build revision): 0 1 10828 7 - -The first example indicate a private drop imported with something like -'import.cmd J:\SD\other\sdt1\src\z3_2'. The second example indicate -drop 10828 from risebuild imported with something like 'import.cmd -\\risebuild\drops\z32\2.0.51220.7'. - -TODO: Update following: Look at -http://pexbuild3/ccnet/ViewFarmReport.aspx -> View All Builds -> -10828. This will give you the SD change number. Voila! - -============================================================================== - -Known issues: -* warning LNK4099: This message is shown when linking. Please ignore. diff --git a/ml/regress.cmd b/ml/regress.cmd deleted file mode 100644 index be610a403..000000000 --- a/ml/regress.cmd +++ /dev/null @@ -1,10 +0,0 @@ -@echo off -call .\build.cmd -sd edit test_capi.regress.txt test_capi.regress.err test_mlapi.regress.txt test_mlapi.regress.err queen.regress.txt queen.regress.err -move test_capi.txt test_capi.regress.txt -move test_capi.err test_capi.regress.err -move test_mlapi.txt test_mlapi.regress.txt -move test_mlapi.err test_mlapi.regress.err -move queen.txt queen.regress.txt -move queen.err queen.regress.err -sd revert -a test_capi.regress.txt test_capi.regress.err test_mlapi.regress.txt test_mlapi.regress.err queen.regress.txt queen.regress.err diff --git a/ml/z3.proj b/ml/z3.proj deleted file mode 100644 index 44ea4947d..000000000 --- a/ml/z3.proj +++ /dev/null @@ -1,11 +0,0 @@ - - - - - - - - $(MLFlags) -I $(SLAMSRC)\slam\engine\slam2\z3 - - -