10

Z3APIv4.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

重要な場合は、MacOSXとMono3.0.2/MonoDevelop3.0.5を使用しました。

MonoでZ3APIを使用した経験のある人はいますか？

奇妙な考えのように聞こえますが、私たちの状況は次のように説明されています。Z3を使用するコースがあり、すべてのラボコンピューターにWindowsと.NETFrameworkがインストールされています。ただし、自分のコンピューター（Linux、Mac）で作業している一部の学生は、プロジェクトをコンパイルして実行できるはずです。

概要：

@Leoの提案のおかげで、いくつかの変更を加えて、MonoDevelopでプロジェクトを実行できます。

1）App.configファイルを作成し、configurationタグの下に次の情報を追加します。

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

2）libz3.dylibMac OS Xディストリビューションからコピー（または新しいバージョンの場合はソースからビルド）し、プロジェクトのコンパイル時に共有ライブラリMicrosoft.Z3.dllが出力フォルダー（モード）にコピーされていることを確認bin/Debugします。Debugこの目的のためItemGroupに、プロジェクトファイルのタグに手動で追加します。

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

libz3.soこのプロセスは、Linuxでも同様である必要があります。

さまざまな理論でさまざまな例を試しました。これまでのところ、エラーや例外は発生していません。

4

1 に答える 1

5

このシナリオを検討したことはありません。通常、Linux / OSXユーザーには、C / C ++、Python、OCaml、Javaなどの他のAPIを使用するように指示します。Java APIはまだ公式リリースの一部ではありませんが、v4.3.2に含まれる予定です。これは、.NetAPIと非常によく似ています。彼らがC＃コードを書いているのであれば、JavaAPIに簡単に移行できるはずです。現在のリリース候補のソースコードは、次を使用して取得できます。

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

かなり安定しています。それをコンパイルするために、私たちは使用しています

cd z3
python scripts/mk_make.py
cd build
make

F＃を使用している場合は、Christophが開発している新しいOCaml APIを検討することもできます（http://z3.codeplex.comml-ngのブランチ）。.NetAPIとしては素晴らしいです。

より複雑なオプションは、Z3 makeファイルジェネレーター（scripts/mk_util.py）をハック/変更して、LinuxおよびOSXで.NetAPIを構築することです。私はMonoに精通していませんが、可能であるはずです。Z3JavaAPIで使用されているのと同じトリックを使用する必要があると思います。変更する必要があるのは、Z3 DLLの代わりにロードする共有ライブラリ（ libz3.soLinuxおよびOSX）です。libz3.dylib

于 2013-01-13T19:52:22.677 に答える