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

Question

我无法在 Windows 7 上使用 z3 ocaml 绑定。 这是我遵循的过程。

1. 安装 Objective Caml 版本 3.11.0（Microsoft 工具链）
2. 安装 camlidl-1.05（使用 Microsoft Visual Studio 2008 + cygwin 构建）
3. 安装 z3-3.0
4. 通过运行“build.cmd”构建 z3 ocaml 绑定。构建成功。
5. 将“build.cmd”生成的文件从 z3/ocaml 复制到 ObjectiveCaml/lib

6. 启动 ocaml 交互并加载“z3.cma”

   # #load "z3.cma";;
   字符-1--1：
     #加载“z3.cma”;;
   
   错误：外部函数“get_theory_callbacks”不可用
   
   # Z3.mk_context;;
   字符-1--1：
     Z3.mk_context;;
   
   错误：外部函数“camlidl_z3_Z3_mk_context”不可用
   

有人能给我一些提示吗？

编辑1： 在“Z3-3.0\examples\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时遇到以下错误在 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。我想应该更改 example\ocaml\build.cmd 来执行相同的操作。

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

Answer 2

以下是对我有用的方法（Windows 7）：

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

29. 尝试 simple_example();;

30. 最后一步应从 Z3 产生有效输出。

对于 Debian/Ubuntu：

1. 安装 Ocaml 3.09+
   1. sudo apt-get install camlidl
2. git clone git://github.com/polazarus/z3-installer.git （来自 Mickaël Delahaye）
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() =
开始
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;
结束;;
simple_example();;