z3 ocaml绑定不起作用（windows 7）

Question

我没有得到在windows 7上工作的z3 ocaml绑定。 这是我遵循的过程。

1. 安装的目的CAML版本3.11.0（微软工具链）
2. 安装camlidl-1.05
3. 安装z3-3.0
4. （使用Microsoft Visual Studio 2008 + cygwin的它还内置）内置Z3的OCaml通过结合运行“build.cmd”。构建成功。
5. 复制从Z3/ocaml的到ObjectiveCaml/lib目录

6. 通过 “build.cmd” 生成的文件推出ocaml的互动，并加载 “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 
   

可有人请给我一些提示？

编辑1： 建立 “\例子Z3-3.0 \ ocaml的” 的例子：

摘自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 

我得到了下面的错误上执行build.cmd in Visual Studio 2008命令提示符

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

关于删除-ccopt "%XCFLAGS%"，它工作正常。生成的exe也按预期执行。 （请注意，我在PATH中有flexdll）。任何想法为什么这可能会发生？

Answer 1

OCaml版本3.11及更高版本通过flexdll调用链接器，该链接器不需要或不知道“/ nologo/MT/DWIN32”标志。 ocaml \ build.cmd脚本测试ocaml版本并适当地设置XCFLAGS。我想应该改变examples \ ocaml \ build.cmd来做同样的事情。

如果我通过在Z3 ocaml绑定目录中执行'ocamlmktop -o ocamlz3 z3.cma'来创建一个自定义顶层，那么从顶层使用Z3对我有用。

Answer 2

这里是为我工作（视窗7）：

1. 下载并安装ocaml的3.08+
2. 下载并安装Visual Studio C++
3. 下载并解压缩CamlIDL
4. 下载并安装cygwin，在安装时选择使得包以及你最喜欢的linux编辑器包在“Select pa ckage“窗口。
5. 打开cygwin的
6. Cygwin中去CamlIDL根目录
7. 重命名config/Makefile.win32到config/Makefile
8. 打开config/Makefile用编辑器
9. 编辑BINLIB和OCAMLLIB变量 保存退出对于cygwin的
10. 设置C编译器：从CamlIDL根目录Invoking cl.exe (MSVC compiler) in Cygwin shell
11. 运行make all
12. 运行make install
13. 退出cygwin的
14. 下载并安装Z3
15. 下载并安装FlexDLL：http://alain.frisch.fr/flexdll.html
16. 单击开始，指向我的电脑，单击鼠标右键，点属性，指向系统保护，选择高级选项卡，指向环境值...
17. 添加C:\Program Files\flexdll\和C:\Program Files\Microsoft Research\Z3-<version-number>\bin\ Path变量
18. 单击开始，指向所有程序，指向Microsoft Visual Studio，指向Visual Studio工具，然后单击Visual Studio命令提示符。
19. 在Visual Studio命令提示符转到C:\Program Files\Microsoft Research\Z3-<version-number>\ocaml
20. 打开build.cmd用编辑器
21. 从最后两个命令
22. 保存并关闭build.cmd
删除 %CD%变量
23. 运行build.cmd
24. 复制z3 *并通过build.cmd从产生到z3/ocaml%OCAMLLIB%
25. 运行ocamlmktop -o ocamlz3 z3.cma %OCAMLLIB%\libcamlidl.lib ole32.lib
26. 运行ocamlz3.exe
27. 类型#use "../examples/ocaml/test_mlapi.ml";;

28. libz3.lib文件尝试simple_example();;​

29. 最后步骤应该从Z3产生有效的输出。

对于Debian/Ubuntu的：

1. （来自的Mickaël德拉哈耶）安装ocaml的3.09+ 1. sudo apt-get install camlidl​
2. git clone git://github.com/polazarus/z3-installer.git
3. cd z3-installer
4. make＃下载Z3和建设OCaml的库（本地和字节）
5. sudo make install＃安装Z3二进制，DLL和OCaml的库
6. sudo cp z3/lib/libz3.so /usr/lib/
7. cd z3/ocaml
8. ocamlmktop -o ocamlz3 z3.cma
9. 。 /ocamlz3
10. 尝试下面的代码片段：

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();;​