Drucken interner Solverformeln in z3

Question

Das Theorembeweiswerkzeug z3 benötigt viel Zeit, um eine Formel zu lösen, von der ich glaube, dass sie leicht zu handhaben ist. Um dies besser zu verstehen und möglicherweise meinen Input für z3 zu optimieren, wollte ich die internen Constraints sehen, die z3 als Teil seines Lösungsprozesses generiert. Wie drucke ich die Formel, die z3 für seine Back-End-Solver erstellt, wenn Sie z3 über die Befehlszeile verwenden?

Answer 1

Das Befehlszeilentool Z3 verfügt nicht über diese Option. Außerdem enthält Z3 mehrere Löser und Vorverarbeitungsschritte. Es ist unklar, welcher Schritt für Sie nützlich wäre. Der Z3-Quellcode ist verfügbar unter https://github.com/Z3Prover/z3. Wenn Z3 im Debug-Modus kompiliert wird, bietet es eine zusätzliche Befehlszeilenoption -tr:<tag>. Diese Option kann zum selektiven Ausgeben von Informationen verwendet werden. Zum Beispiel enthält die Quelldatei nlsat_solver.cpp die folgende Anweisung:

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
       tout << "\nvar order:\n"; 
       display_vars(tout);); 

die Kommandozeilenoption -tr:nlsat wird anweisen Z3 die Anweisung oben auszuführen. tout ist der Ablaufverfolgungs-Ausgabestream. Es wird in der Datei .z3-trace gespeichert. Die Z3-Quelle ist voll von diesen TRACE Befehlen. Da der Code verfügbar ist, können wir auch eigene Trace-Befehle im Code hinzufügen.

Wenn Sie Ihr Beispiel veröffentlichen, kann ich Ihnen sagen, welche Z3-Komponenten verwendet werden, um es vorzuverarbeiten und zu lösen. Dann können wir auswählen, welche "Tags" wir für die Ablaufverfolgung aktivieren sollen.

EDIT (nach dem constraints gebucht wurden): Ihr Beispiel ist in der gemischten ganzzahligen & realen nichtlinearen Arithmetik. Der neue nichtlineare arithmetische Solver (nlsat) in Z3 unterstützt to_int nicht. So wird der Allzwecklöser Z3 verwendet, um Ihr Problem zu lösen. Obwohl dieser Löser fast alles akzeptiert, ist er für nichtlineare reelle Arithmetik noch nicht vollständig. Die nichtlineare Unterstützung dieses Solvers basiert auf: Intervallanalyse und Grobner-Basisberechnungen. Dieser Solver ist im Ordner src/smt (in der unstable branch) implementiert. Das Arithmetikmodul ist in den Dateien theory_arith* implementiert. Eine gute Tracing-Befehlszeilenoption ist -tr:after_reduce. Nach der Vorverarbeitung wird der Satz von Bedingungen angezeigt. Der Engpass ist das arithmetische Modul (theory_arith*).

Zusätzliche Bemerkungen:

• Das Problem ist in einem Fragmente unentscheidbare: Misch integer & reale nicht-lineare Arithmetik. Das heißt, es ist unmöglich, einen Ton und einen vollständigen Löser für dieses Fragment zu schreiben. Natürlich können wir einen Solver schreiben, der Instanzen löst, die wir in der Praxis finden. Ich glaube, es ist möglich, nlsat zu erweitern, um die to_int zu behandeln. Wenn Sie to_int vermeiden, können Sie nlsat verwenden. Das Problem wird in dem nichtlinearen realen arithmetischen Fragment liegen. Ich verstehe, dass dies schwierig sein kann, da die to_int eine Schlüsselrolle in Ihrer Codierung scheint.

• Der Code im Zweig "unstable" unter z3.codeplex.com ist viel besser organisiert als die offizielle Version im Zweig "master". Ich werde es bald mit der "Master" Filiale zusammenführen.Sie können den Zweig "Unstable" abrufen, wenn Sie mit dem Quellcode spielen möchten.

• Der Zweig "unstable" verwendet ein neues Build-System. Sie können die Release-Version mit Tracing-Unterstützung erstellen. Sie müssen nur die Option -t beim Generieren des Makefile verwenden.

Python-Skripte/mk_make.py -t

• Wenn Z3 im Debug-Modus kompiliert wird, die Option AUTO_CONFIG=false standardmäßig. Um das Verhalten des "Freigabemodus" zu reproduzieren, müssen Sie daher die Befehlszeilenoption AUTO_CONFIG=true angeben.