Wir haben ein .NET-Projekt mit Z3 API v4.0. Wir möchten das Projekt auf Mono kompilieren und ausführen können.
Das Projekt wurde mit MonoDevelop zusammengestellt. Wenn wir das Programm ausführen oder debuggten, trat jedoch die folgende Ausnahme auf
%Vor%Wir haben Mac OS X und Mono 3.0.2 / MonoDevelop 3.0.5 verwendet, wenn das wichtig ist.
Hat jemand Erfahrung mit Z3 API auf Mono?
Es klingt wie eine seltsame Idee, aber unsere Situation wird wie folgt beschrieben. Wir haben einen Kurs mit Z3 und alle Laborcomputer haben Windows und .NET Framework installiert. Einige Studenten, die auf ihren eigenen Computern (Linux, Mac) arbeiten, sollten jedoch in der Lage sein, das Projekt zu kompilieren und auszuführen.
Zusammenfassung:
Dank @ Leos Vorschlag kann ich das Projekt unter MonoDevelop mit ein paar Änderungen ausführen:
1) Erstellen Sie eine App.config -Datei und fügen Sie folgende Informationen unter configuration tag:
2) Kopieren Sie libz3.dylib aus der Mac OS X-Distribution (oder erstellen Sie aus der Quelle für neuere Versionen) und stellen Sie sicher, dass die gemeinsam genutzte Bibliothek und Microsoft.Z3.dll beim Kompilieren in den Ausgabeordner ( bin/Debug in Debug mode) kopiert werden das Projekt. Zu diesem Zweck fügen wir dem ItemGroup -Tag in der Projektdatei manuell hinzu:
Der Prozess sollte für libz3.so unter Linux ähnlich sein.
Wir haben verschiedene Beispiele mit verschiedenen Theorien ausprobiert. Bisher ist kein Fehler oder Ausnahme aufgetreten.
Wir haben dieses Szenario nie in Betracht gezogen. Normalerweise teilen wir Linux / OSX-Benutzern mit, dass sie die anderen APIs verwenden: C / C ++, Python, OCaml oder Java. Die Java API ist noch nicht Teil der offiziellen Version, aber sie wird in Version 4.3.2 sein. Es ist der .NET API sehr ähnlich. Wenn sie C # -Code schreiben, sollte es einfach sein, zur Java-API zu wechseln. Sie können den Quellcode des aktuellen Release-Kandidaten mit
abrufen %Vor%Es ist ziemlich stabil. Um es zu kompilieren, verwenden wir
%Vor% Wenn Sie F # verwenden, können Sie auch die neue OCaml-API in Betracht ziehen, die Christoph entwickelt (Zweig ml-ng bei Ссылка ). Es ist schön wie die. NET API.
Eine kompliziertere Option ist das Hacken / Ändern des Z3-Generators für Make-Dateien ( scripts/mk_util.py ), um die .Net-APIs unter Linux und OSX zu erstellen. Ich bin mit Mono nicht vertraut, aber es sollte möglich sein. Ich schätze, Sie müssen die gleichen Tricks verwenden, die in der Z3 Java API verwendet werden. Eine Sache, die geändert werden muss, ist die gemeinsam zu ladende Bibliothek ( libz3.so auf Linux und libz3.dylib auf OSX) anstelle der Z3-DLL.