We have a .NET project using Z3 API v4.0. We would like to be able to compile and run the project on Mono.
The project compiled fine with MonoDevelop. However, when we run or debugged the program, the following exception occurred
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
We used Mac OS X and Mono 3.0.2/MonoDevelop 3.0.5 if that matters.
Has anyone had experience using Z3 API on Mono?
It sounds like a weird idea, but our situation is described as follows. We have a course using Z3 and all lab computers have Windows and .NET framework installed. However, some students working on their own computers (Linux, Mac) should be able to compile and run the project.
Summary:
Thanks to @Leo's suggestion, I am able to run the project under MonoDevelop with a few changes:
1) Create an App.config
file and add the following information under configuration
tag:
<dllmap dll="z3.dll" target="libz3.dylib" os="osx" cpu="x86"/>
2) Copy libz3.dylib
from Mac OS X distribution (or build from source for newer versions) and make sure the shared library and Microsoft.Z3.dll
are copied to output folder (bin/Debug
on Debug
mode) when compiling the project. For this purpose, we manually add to ItemGroup
tag in the project file:
<None Include="libz3.dylib">
<CopyToOutputDirectory>Always</CopyToOutputDirectory>
<Visible>False</Visible>
</None>
The process should be similar for libz3.so
on Linux.
We have tried various examples with different theories. There is no error or exception occurring so far.
We never considered this scenario. We usually tell Linux/OSX users to use the other APIs: C/C++, Python, OCaml or Java. The Java API is not part of the official release yet, but it will be in v4.3.2. It is very similar to the .Net API. If they are writing C# code, it should be easy to move to the Java API. You can get the source code of the current release candidate using
git clone https://git01.codeplex.com/z3 -b rc
It is quite stable. To compile it, we have use
cd z3
python scripts/mk_make.py
cd build
make
If you are using F#, you may also consider the new OCaml API that Christoph is developing (branch ml-ng
at http://z3.codeplex.com). It is nice as the .Net API.
A more complicated option is to hack/modify the Z3 make file generator (scripts/mk_util.py
) to build the .Net APIs on Linux and OSX. I'm not familiar with Mono, but it should be possible. I guess you have to use the same tricks used in the Z3 Java API. One thing that needs to be changed is the shared library to be loaded (libz3.so
on Linux and libz3.dylib
on OSX) instead of the Z3 DLL.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With