在Mono上使用Z3托管API

Question

我们有一个使用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.so在Linux上,该过程应该类似.

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

Answer 1

我们从未考虑过这种情况。我们通常会告诉 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＃，你也可以考虑新的OCaml的API，克里斯托夫正在开发（分公司ml-ng在http://z3.codeplex.com）。它与 .Net API 一样好。

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