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

Question

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

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";;
   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\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

在Visual Studio 2008 命令提示符中执行build.cmd时出现以下错误

** 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