z3 ocaml binding not working (windows 7)

Question

I am not getting the z3 ocaml binding working on windows 7. Here is the process I followed.

1. Installed Objective Caml version 3.11.0 (Microsoft toolchain)
2. Installed camlidl-1.05 (built it using Microsoft Visual Studio 2008 + cygwin)
3. Installed z3-3.0
4. Built z3 ocaml binding by running "build.cmd".The build was successful.
5. Copied the files generated by "build.cmd" from z3/ocaml to ObjectiveCaml/lib

6. Launched ocaml interactive and loaded "z3.cma"

   # #load "z3.cma";;
   Characters -1--1:
     #load "z3.cma";;
   
   Error: The external function `get_theory_callbacks' is not available
   
   # Z3.mk_context;;
   Characters -1--1:
     Z3.mk_context;;
   
   Error: The external function `camlidl_z3_Z3_mk_context' is not available
   

Can someone please give me some hints?

EDIT 1: Building the example in "Z3-3.0\examples\ocaml":

Excerpt from build.cmd

set XCFLAGS=/nologo /MT /DWIN32
ocamlopt -ccopt "%XCFLAGS%" -o test_mlapi.exe -I ..\..\ocaml ole32.lib %OCAMLLIB%\libcamlidl.lib z3.cmxa test_mlapi.ml

I got the following error on executing build.cmd in the Visual Studio 2008 Command Prompt

** Fatal error: Cannot find file "/nologo"
File "caml_startup", line 1, characters 0-1:
Error: Error during linking

On removing the -ccopt "%XCFLAGS%", it works fine. The generated exe also executes as expected. ( Note that I have flexdll in PATH ). Any idea why this might be happening?

Answer 1

OCaml version 3.11 and later call the linker through flexdll, which does not need or know about the "/nologo /MT /DWIN32" flags. The ocaml\build.cmd script tests the ocaml version and sets XCFLAGS appropriately. I guess that examples\ocaml\build.cmd should be changed to do the same.

Using Z3 from the toplevel works for me if I create a custom toplevel by executing 'ocamlmktop -o ocamlz3 z3.cma' from Z3 ocaml bindings directory.

Answer 2

Here is what worked for me (Windows 7):

1. Download and install Ocaml 3.08+ ​
2. Download and install Visual Studio C++ ​
3. Download and extract CamlIDL ​
4. Download and install cygwin, while installing choose the make package as well as your favorite linux editor package in a "Select package" window. ​
5. Open cygwin ​
6. In cygwin go to CamlIDL root directory ​
7. Rename config/Makefile.win32 to config/Makefile ​
8. Open config/Makefile with an editor ​
9. Edit BINLIB and OCAMLLIB variables ​​
10. Save and exit the Makefile ​
11. Setup c compiler for cygwin: Invoking cl.exe (MSVC compiler) in Cygwin shell ​
12. Run make all from CamlIDL root directory ​
13. Run make install ​
14. Exit cygwin ​
15. Download and install Z3 ​
16. Download and install FlexDLL: http://alain.frisch.fr/flexdll.html ​
17. Click Start, point to My Computer, right click, point to Properties, point to System Protection, choose Advanced Tab, point to Environment values... ​
18. Add C:\Program Files\flexdll\ and C:\Program Files\Microsoft Research\Z3-<version-number>\bin\ to the Path variable ​
19. Click Start, point to All Programs, point to Microsoft Visual Studio, point to Visual Studio Tools, and then click Visual Studio Command Prompt. ​
20. In Visual Studio Command Prompt go to C:\Program Files\Microsoft Research\Z3-<version-number>\ocaml ​​
21. Open build.cmd with an editor ​
22. Remove %CD% variable from the last two commands ​
23. Save and close build.cmd ​
24. Run build.cmd ​
25. Copy z3* and libz3.lib files generated by build.cmd from z3/ocaml to %OCAMLLIB% ​
26. Run ocamlmktop -o ocamlz3 z3.cma %OCAMLLIB%\libcamlidl.lib ole32.lib ​
27. Run ocamlz3.exe ​
28. Type #use "../examples/ocaml/test_mlapi.ml";; ​

29. Try simple_example();;​

30. The last step should produce a valid output from Z3.

​
For Debian/Ubuntu:

1. Install Ocaml 3.09+ ​ 1. sudo apt-get install camlidl​
2. git clone git://github.com/polazarus/z3-installer.git (from Mickaël Delahaye)
3. cd z3-installer
4. make # download Z3 AND build the Ocaml library (native and byte)
5. sudo make install # install Z3 binary, DLL and the Ocaml library
6. sudo cp z3/lib/libz3.so /usr/lib/
7. cd z3/ocaml
8. ocamlmktop -o ocamlz3 z3.cma
9. ./ocamlz3
10. Try the following snippet:

let simple_example() =
begin
Printf.printf "\nsimple_example\n";
let ctx = Z3.mk_context_x (Array.append [|("MODEL", "true")|] [||]) in
Printf.printf "CONTEXT:\n%sEND OF CONTEXT\n" (Z3.context_to_string ctx); Z3.del_context ctx;
end;;
simple_example();;​