Lesen einer Z3-Datei

Question

Mein Programm erstellt ein Protokoll aller z3-Interaktionen mit Z3_open_log(). Dann habe ich es in einem anderen Programm mit Z3_parse_z3_file() gelesen. Es gibt mir die Zusammenfassung aller an der Eingabe gemachten Behauptungen. Sagen wir, ich habe zwei Behauptungen: a1 und a2. Dann durch Parsen der z3-Datei bekomme ich (und a1 a2).

Ich möchte (und (nicht a1) a2) testen. Wie kann ich das tun, vorausgesetzt, ich bekomme nur die Verbindung der beiden Behauptungen, nicht ein Paar Behauptungen? Ich konnte keine Funktion in der API finden, die mir erlaubt, in eine AST zu navigieren, zu sehen, ob es eine Konjunktion ist und darüber zu iterieren.

Wenn es nicht der Weg ist, den ich gehen sollte, welchen Weg würden Sie empfehlen?

Vielen Dank im Voraus,

AG.

Answer 1

Wie bereits im obigen Kommentar beschrieben, können Sie mit der API Z3-ASTs durchlaufen. Das gesagt, ich habe ein paar Kommentare.

Die Protokollierung ist für Debugging-Zwecke gedacht. Sie werden hauptsächlich verwendet, um problematische Spuren zu melden. Wir haben einen neuen Protokollierungsmechanismus in Z3 4.0. Es zeichnet alle APIs auf und ermöglicht uns eine getreue Wiedergabe der Interaktion zwischen der Host-Anwendung und Z3.

Die Formate Z3 Low Level und Simplify sind in Z3 4.0 veraltet. Z3 haben immer noch eine begrenzte Unterstützung für sie.

Z3 4.0 hat neue C-, C++ -, .NET- und Python-APIs. Die C-API ist abwärtskompatibel, aber ich habe mehrere Prozeduren als veraltet markiert. Es ist viel einfacher, ASTs mit den neuen APIs zu durchlaufen und zu manipulieren. Python-API ist bereits online verfügbar. Hier ein Beispiel:

http://rise4fun.com/Z3Py/Cp

Hier ist ein weiteres Beispiel, das (and a1 a2), extrahiert jeweils Kinder baut und baut (and (not a1) a2).

http://rise4fun.com/Z3Py/8h

Das folgende Tutorial umfasst die neue Z3 API:

http://rise4fun.com/Z3Py/tutorial/guide

Z3 4.0 wird in Kürze freigegeben werden.