Annahmen in Z3 oder Z3Py

Question

Gibt es eine Möglichkeit, Annahmen in Z3 (ich benutze die Z3Py-Bibliothek) so auszudrücken, dass die Engine ihre Gültigkeit nicht überprüft, sondern sie als zugrundeliegende Theorien nimmt, genau wie im Theorembeweis?

Zum Beispiel sagen wir, dass ich zwei unäre Funktionen mit einem Argument vom Typ Real habe. Ich möchte der Z3-Engine mitteilen, dass für alle Eingabewerte f1 (t) gleich f2 (t) ist.

in Z3Py codiert, die in etwa wie folgt aussehen:
t = Real ("t")
assumption1 = ForAll (t, f1 (t) = f2 (t)).

Das Problem mit dem vorgestellten Code ist, dass mein Assertion-Set ziemlich groß ist und ich Quantoren verwende (ich versuche die Erfüllbarkeit eines Echtzeitsystems zu beweisen). Wenn ich die obige Behauptung zu der Menge der anderen Assertionen hinzufüge, wird die Überprüfungsprozedur nicht beendet.

Answer 1

Ja, das ist möglich, genau wie du es beschreibst, aber du wirst mit Quantifizierern enden, was natürlich bedeutet, dass du ein schwierigeres Problem löst und Z3 sich anders verhält (es ist möglich, dass du ganz andere Löser verwendest) die nicht viel Quellcode teilen).

Für das gegebene Beispiel ist es möglich, den Quantifizierer billig zu eliminieren, da er die Form einer Funktionsdefinition hat (ForAll x. F (x) = ...), dh wir können einfach alle Vorkommen von f ersetzen mit der rechten Seite und dann ist der Quantifikator trivial zufrieden. In Z3 geschieht dies durch den Makrofinder, der als Taktik (mit dem Namen "Makrofinder") angewendet werden kann, oder wenn Sie die Taktik "smt" verwenden (implizit über andere oder direkt), dann können Sie einstellen smt.macro_finder = wahr.

Answer 2

Gibt es eine Möglichkeit, Annahmen in Z3 (ich benutze die Z3Py-Bibliothek) so auszudrücken, dass die Engine ihre Gültigkeit nicht überprüft, sondern sie als zugrundeliegende Theorien nimmt, genau wie im Theorembeweis?

Tatsächlich werden alle Assertionen, die Sie zu Z3 hinzufügen, als Annahmen behandelt, die Sie nennen. Z3 prüft die Erfüllbarkeit der Assertionen, prüft nicht die Gültigkeit. Um die Gültigkeit einer Formel F zu überprüfen, wird (nicht F) bestätigt und auf Erfüllbarkeit von (nicht F) geprüft. Wenn (nicht F) ungesättigt ist, dann ist F gültig. Wenn Sie Hintergrundaxiome haben, überprüfen Sie im Wesentlichen die Gültigkeit von Hintergrund => F, so dass Sie die Erfüllbarkeit von Hintergrund & (nicht F) prüfen können.

Ob Z3 bei Ihrer Abfrage endet, hängt davon ab, welche Kombination von Theorien und Quantifikatoren Sie verwenden. Je mehr Funktionen Ihre Abfragen kombinieren, desto schwieriger wird es. Für Formeln über reine lineare arithmetische oder polynomiale reelle Arithmetik, werden diese in der SMT-LIB-Klassifikation als LRA, LIA und NRA bezeichnet (siehe smtlib.org). Z3 verwendet spezialisierte Entscheidungsprozeduren, die kürzlich hinzugefügt wurden.