Ich habe mehrere SMT-Löser (CVC3, CVC4 und Z3) für den folgenden scheinbar trivialen Benchmark ausprobiert:
%Vor%Die Löser kehren alle unbekannt zurück. Ich verstehe, dass dies ein unentscheidbares Fragment ist (gut nicht-linear), aber ich hatte erwartet, dass es einige einfache Instanziierungs-Heuristiken geben würde, die es lösen könnten. Ich habe auch versucht, einige zusätzliche Behauptungen mit Konstanten hinzuzufügen, aber es hat nicht geholfen.
Gibt es eine Möglichkeit, diese Probleme anzugehen, und wo liegen die Grenzen der Argumentation in der quantifizierten Arithmetik in SMT?
Pad ist korrekt, der qe Präprozessor kann ziemlich teuer sein. Darüber hinaus ist es in Formeln, die von Software-Verifikations-Tools wie VCC , Dafny , VeriFast , Why3 und ESCJava2 . Es ist nicht effektiv, da die von diesen Anwendungen erzeugten Formeln auch nicht interpretierte Funktionen, Arrays usw. enthalten.
As Pad's Antwort schlägt vor, Z3 ist eine Sammlung von Motoren. Es bietet APIs und Befehle, mit denen Benutzer auswählen können, welche Engine (oder Kombination von Engines) zur Lösung eines Problems verwendet wird. Wenn der Benutzer nur sagt (check-sat) versucht zu erraten, was die beste Engine zum Lösen der Eingabeformel ist. Die Schätzung basiert auf der Struktur der Eingabeformel und Anmerkungen, die vom Benutzer bereitgestellt werden (Beispiel: der Befehl set-logic ). Wir erweitern ständig die Menge der Fragmente, die automatisch erkannt werden, und die Menge der von uns bereitgestellten Engines.
Es ist peinlich, dass Z3 ein Fragment wie LIA verpasst hat und die Prozedur qe nicht automatisch angewendet hat. Für LIA -Formeln ist qe normalerweise die beste Option. Alternativen, die auf E-Matching oder MBQI basieren, sind nicht effektiv, da sie für völlig unterschiedliche Fragmente gedacht sind.
Ich habe nur festgeschriebenen Code , der LIA erkennt (auch wenn set-logic nicht verwendet wird). Die Änderung ist bereits im Zweig unstable (Working-in-Progress) verfügbar. Es wird morgen in den nächtlichen Builds und in der nächsten offiziellen Version verfügbar sein.
Ihr Beispiel gehört zur Kategorie "Linear Integer Arithmetic" (LIA).
LIA dh Presburger Arithmetik räumt Quantifier-Eliminierung (qe) ein, obwohl die Zeitkomplexität von qe-Prozeduren prohibitiv hoch ist.
>Ich bin mir nicht sicher, ob CVC3 und CVC4 die Eliminierung von Quantifizierern für LIA unterstützen, aber in Z3 können Sie
tun %Vor% Von der Rise4Fun-Ausführung habe ich unsat result.
Hier ist die qe -Taktik ein Vorverarbeitungsschritt, bevor die Endspiel-Taktik smt angewendet wird.