在 Windows 上编译 Scala^Z3答案

【问题标题】：Compiling Scala^Z3 on Windows在 Windows 上编译 Scala^Z3
【发布时间】：2011-09-12 13:16:47
【问题描述】：

我尝试使用 Cygwin 和 JDK 1.7.0 在 Win XP 上编译 Scala^Z3，但没有达到预期的效果。

我做了以下事情： - 使用 SBT 0.7.4 - 使用来自 github 的当前 Scala^Z3 修订版 - 使用 Cygwin 及其 gcc - 使用 JDK 1.7.0 (javac)

“sbt 更新”成功。 “sbt package”最终会出现几个错误，说明未定义的引用，如下所示：

\psuter-ScalaZ3-35cb691\src\c/z3_Z3Wrapper.c:10：未定义对`_Z3_mk_config'的引用

为了让它工作，我将 ....\PSuterScalaZ3\psuter-ScalaZ3-35cb691\project\build\scalaz3.scala 第 74 行更改为：

lazy val gcc : ManagedTask = if(isUnix || is32bit) {

在主页上声明它也应该适用于 Windows。有吗？有预编译的jar吗？

我在这里看到了一个 z3.jar：http://lara.epfl.ch/~psuter/jniz3/z3.jar 这也是一个Linux版本，我猜？因为它对我也不起作用......

Scala^Z3 是一段非常好的代码（如果我能让它工作的话；））

【问题讨论】：

标签： scala z3

【解决方案1】：

很抱歉，sbt 脚本目前确实只适用于 Linux（从绝对路径可以看出，我们还不太习惯有外部用户）。

下面是我在 Windows 下编译它的步骤：

用 javac 编译所有 Java 源代码（没有依赖关系）
使用 javah 生成头文件
使用 scalac 编译所有 Scala 源代码（仅使用 Java .class 文件作为依赖项）
使用 Visual Studio 编译 .c + .h 文件
手动创建包含所有内容的 jar 文件

一旦我们使 Scala^Z3 适应 Z3 3.1 中的新变化，我们还希望发布带有 Linux 和 Windows 共享库的预编译 .jar 文件。

编辑 GitHub 存储库现在包含为 Scala 2.9.1 和 Z3 3.2 准备的预编译 .jar 文件。它适用于 Windows 和 Linux（32 位）。该存储库还包含有关如何在 Windows 中使用 MinGW 而不是 Visual Studio 编译共享库的更详细说明（因此无需 VS 运行时库）。

【讨论】：

一个预编译的 .jar (Z3 3.1) 会很棒......你认为它什么时候可以使用？这是因为我们需要 .parseSmtlib2String() 方法。
我使用了预编译的 .jar（版本 1.1 和 z3.dll 2.19），但它指出：“警告：分配的虚拟内存不足。无法分配大小为 1561721928 的对象。当前分配大小：142676。 High watermark: 0" 当从 Scala^Z3 主页上的 ppt 幻灯片中定义一个小术语时。有什么问题？它真的需要那么多内存吗？错误的 DLL？
希望在下周末之前。内存问题可能来自于最新的 Z3 有两种管理内存的方式；手动或自动。我不确定使用针对旧 Z3 编译的共享库如何与该方面进行交互。
期待它；）感谢您的快速回答！
我已将预编译版本添加到 GitHub。（包括对 parseSMTLIB2String 和 parseSMTLIB2File 的支持。）我自己在 Windows 和 Linux（32 位）下对其进行了测试。您可以从存储库本身（在 jar-releases/32/scala-2.9.1/scalaz3-3.2.a.jar 中）或从 GitHub 作为“包下载”获取它。热这有帮助。我还将尝试自动化该过程，以便可以从 Windows 中的 sbt 访问它。目前不是。

【解决方案2】：

几个月前我遇到了类似的问题，这就是我必须做的才能用 Visual Studio 2010 编译它。我不确定它是否仍然相关，因为 Scala^Z3 和 Z3 本身发生了很大变化，但我希望它仍然有用。

创建了一个新的 Visual C++ Win32 项目 (.NET Framework 4) 创建 DLL。
在 src/c/ 目录中添加了所有 .h 和 .c 文件。 VC不知何故抱怨“内联”修饰符，一位同事建议删除它们，我这样做了。
从 Z3 2.19 添加了 z3.h，不接受 Z3 2.16。还添加了对应的z3.lib（x86，还没试过x64）。 VC不接受 z3.dll 和有关文件损坏的投诉。不知道为什么，Z3 它本身对我来说很好。
项目编译时出现 13 个警告，并创建了一个 dll 显然必须命名为 scalaz3.dll。
sbt 编译，将 scalaz3.dll 添加到 lib-bin，jar 整个一起到scalaz3.jar
'scala -classpath scalaz3.jar test.scala' 带有 scalaz3.jar 和 z3.dll 在当前文件夹中工作

【讨论】：

感谢您提供这些详细步骤。 .dll 确实必须称为 scalaz3.dll。当您运行 Scala^Z3 时，它会要求系统尝试加载具有该确切名称的库。如果失败，它会在 .jar 中查找该名称的文件，将其复制到临时目录并从那里加载。（临时目录名称包含当前版本的 Scala^Z3 的哈希以避免冲突。）在 *nix 系统上，该名称也必须是 libscalaz3.so，在 MacOSX 上可能是 libscalaz3.jnilib，如果该平台支持 Z3 .
我终于知道了如何只使用MinGW编译共享库，所以现在z3.dll之外不再有依赖了。