3

我在我的 Mac OSX（Mountain Lion、JDK 7、Scala 2.10、Z3 4.3）上成功安装了 Scala^Z3（如下： http: //lara.epfl.ch/w/ScalaZ3）。一切都很好，除了我无法从这个网站（http://lara.epfl.ch/w/jniz3-scala-examples）运行任何示例而不会得到这个讨厌的错误：

java.lang.NoClassDefFoundError: scala/reflect/ClassManifest
    at .<init>(<console>:8)
    at .<clinit>(<console>)
    at .<init>(<console>:7)
        ...
Caused by: java.lang.ClassNotFoundException: scala.reflect.ClassManifest
    at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
    at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
    at java.security.AccessController.doPrivileged(Native Method)
    at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
    ... 29 more

我认为这是因为 Scala 2.9.x 和 2.10.x 在处理反射方面不兼容。因为我能够在 Scala 2.9.x 下运行相同的示例集。我的问题是，有没有办法解决这个问题并在 Scala 2.10 下运行 Scala^Z3？

4

3 回答 3

5

通过查看项目属性和构建文件（https://github.com/psuter/ScalaZ3/blob/master/project/build.properties和https://github.com/psuter/ScalaZ3/blob/master/project/ build/scalaZ3.scala ) 我推断 scalaZ3 目前仅提供给 scala 2.9.2。目前没有跨版本支持。

在“build.properties”文件中将版本更改为 scala 2.10.0 后，您可能会尝试获取代码并自行编译。有关如何编译它的说明，请参阅此页面：https ://github.com/psuter/ScalaZ3 。如果幸运的话，代码将在 scala 2.10 下编译。如果你不是，可能需要做一些小的修复。交叉你的手指。

如果你不着急，你也可以给 Scala^Z3 的作者发错误，并要求他们提供 scala 2.10 版本的库。

于 2013-03-05T13:12:00.333 回答
3

我正在复制我在 GitHub 上对您的问题的回复中的说明，因为它可能会在将来对某人有所帮助。

当前状态是旧的 sbt 项目似乎与 Scala 2.10 不能很好地融合。以下是针对 Linux 的项目“手动”编译的说明。这适用于 Z3 4.3（从Z3 git repo获取）和 Scala 2.10。按照原始说明安装 Z3 后：

首先编译Java文件：

$ mkdir bin
$ find src/main -name '*.java' -exec javac -d bin {} +

然后编译 C 文件。为此，您需要先生成 JNI 标头，然后编译共享库。以下命令中的选项适用于 Linux。为了找到 JNI 标头的位置，我(new java.io.File(System.getProperty("java.home")).getParent在 Scala 控制台中运行（并添加/include到结果中）。

$ javah -classpath bin -d src/c z3.Z3Wrapper
$ gcc -o lib-bin/libscalaz3.so -shared -Wl,-soname,libscalaz3.so \
        -I/usr/lib/jvm/java-6-sun-1.6.0.26/include \
        -I/usr/lib/jvm/java-6-sun-1.6.0.26/include/linux \
        -Iz3/4.3/include -Lz3/4.3/lib \
        -g -lc -Wl,--no-as-needed -Wl,--copy-dt-needed -lz3 -fPIC -O2 -fopenmp \
        src/c/*.[ch]

现在编译 Scala 文件：

$ find src/main -name '*.scala' -exec scalac -classpath bin -d bin {} +

您将收到“功能警告”，这是迁移到 2.10 时的典型情况，以及另一个关于非详尽模式匹配的警告。

现在让我们用所有东西制作一个jar文件......

$ cd bin
$ jar cvf scalaz3.jar z3
$ cd ..
$ jar uf bin/scalaz3.jar lib-bin/libscalaz3.so

...现在你应该已经bin/scalaz3.jar包含了你需要的一切。让我们试一试：

$ export LD_LIBRARY_PATH=z3/4.3/lib
$ scala -cp bin/scalaz3.jar
scala> z3.scala.version

希望这可以帮助！

于 2013-03-06T16:28:19.990 回答
1

这并不能直接回答问题，但可能会帮助其他尝试scalaz3使用scala 2.10.

我ScalaZ3用Scala 2.10.1和Z3 4.3.0建立Windows 7。我用http://lara.epfl.ch/w/jniz3-scala-examplesinteger constraints上的示例对其进行了测试，它工作正常。

Z3楼

在 codeplex的Z3 4.3.0下载不包括libZ3.lib文件。所以我不得不下载源代码并在我的机器上构建它。构建过程非常简单。

构建 ScalaZ3

目前，build.properties有 sbt 版本0.7.4和 scala 版本2.9.2。这很好。（我不得不对文件进行一些小修改。在任务中build.scala修改z3LibPath(z3VN).absolutePath为。）z3LibPath(z3VN).absolutePath + "\\libz3.lib"gcc

现在，如果我将 scala 版本更改为2.10.1in build.properties，我会"Error compiling sbt component 'compiler-interface'"在启动 sbt 时出错。我不知道为什么会这样。

然后我将 sbt 版本更改为0.12.2scala 版本2.10.1，并从新的源代码开始。我还在build.sbt项目根文件夹中添加了包含scalaVersion := "2.10.1". 这是必需的，因为在 sbt 中0.12.2，该文件build.properties应该仅用于指定sbt版本。有关 sbt 版本差异的更多信息（https://github.com/harrah/xsbt/wiki/Migrating-from-SBT-0.7.x-to-0.10.x）。

我得到错误Z3Wrapper.java:27: cannot find symbol LibraryChecksum。发生这种情况是因为没有生成LibraryChecksum.java应该由 build ( project\build\build.scala) 生成的文件。看起来该package任务没有执行 ( project\build\build.scala) 中的任务。任务compute-checksum、javah和gcc未执行。这可能是因为 sbt0.12.2期望build.scala文件直接位于project文件夹下。

然后我复制了LibraryChecksum.java从以前的构建生成的，然后构建通过。生成的 jar 文件不包含scalaz3.dll.

然后我手动执行javah和任务。gcc这些任务的命令可以从成功构建的日志中复制scala 2.9.2（我对 scala 的命令进行了适当的修改2.10.1）。在这里，我也不得不做一些改变。我必须明确添加任务的scala-library.jar 类路径的完整路径。javah

然后我将 .jar 添加lib-bin\scalaz3.dll到 jar 文件中jar uf target\scala-2.10\scalaz3.jar lib-bin/scalaz3.dll。

于 2013-06-08T13:39:34.273 回答