10

我们有一个使用 Z3 API v4.0 的 .NET 项目。我们希望能够在 Mono 上编译和运行该项目。

该项目使用 MonoDevelop 编译得很好。但是，当我们运行或调试程序时，出现如下异常

System.DllNotFoundException: z3.dll
  at (wrapper managed-to-native) Microsoft.Z3.Native/LIB:Z3_mk_context_rc (intptr)
  at Microsoft.Z3.Native.Z3_mk_context_rc (IntPtr a0) [0x00000] in <filename unknown>:0
  at Microsoft.Z3.Context..ctor () [0x00000] in <filename unknown>:0
  at <StartupCode$Nqueens>.$Nqueens..cctor () [0x00000] in /path/to/file:15

如果重要的话，我们使用 Mac OS X 和 Mono 3.0.2/MonoDevelop 3.0.5。

有人有在 Mono 上使用 Z3 API 的经验吗？

这听起来像是一个奇怪的想法，但我们的情况描述如下。我们有一门使用 Z3 的课程，所有实验室计算机都安装了 Windows 和 .NET 框架。但是，一些在自己的计算机（Linux、Mac）上工作的学生应该能够编译和运行该项目。

概括：

感谢@Leo 的建议，我可以在 MonoDevelop 下运行该项目，只需进行一些更改：

1）创建一个文件并在标签App.config下添加以下信息：configuration

<dllmap dll="z3.dll" target="libz3.dylib" os="osx" cpu="x86"/>

2）libz3.dylib从 Mac OS X 发行版复制（或从源代码构建新版本）并确保在编译项目时将共享库和Microsoft.Z3.dll复制到输出文件夹（bin/Debug打开模式）。Debug为此，我们ItemGroup在项目文件中手动添加到标记：

<None Include="libz3.dylib">
  <CopyToOutputDirectory>Always</CopyToOutputDirectory>
  <Visible>False</Visible>
</None>

libz3.soLinux 上的过程应该类似。

我们用不同的理论尝试了各种例子。到目前为止没有发生错误或异常。

4

1 回答 1

5

我们从未考虑过这种情况。我们通常告诉 Linux/OSX 用户使用其他 API：C/C++、Python、OCaml 或 Java。Java API 还不是正式版本的一部分，但它会在 v4.3.2 中。它与 .Net API 非常相似。如果他们正在编写 C# 代码，那么迁移到 Java API 应该很容易。您可以使用以下方式获取当前候选版本的源代码

git clone https://git01.codeplex.com/z3 -b rc

它相当稳定。为了编译它，我们使用

cd z3
python scripts/mk_make.py
cd build
make

如果您使用 F#，您还可以考虑 Christoph 正在开发的新 OCaml API（ml-ng位于http://z3.codeplex.com的分支）。它与 .Net API 一样好。

一个更复杂的选择是破解/修改 Z3 make 文件生成器 ( scripts/mk_util.py) 以在 Linux 和 OSX 上构建 .Net API。我对 Mono 不熟悉，但应该可以。我猜你必须使用在 Z3 Java API 中使用的相同技巧。需要更改的一件事是要加载的共享库（libz3.so在 Linux 和libz3.dylibOSX 上）而不是 Z3 DLL。

于 2013-01-13T19:52:22.677 回答