∃-Abfragen und ∀-Abfragen mit Z3-Fixpunkt-Engine

Question

Ich bin verwirrt und zu verstehen, wie zwei verschiedene Eingabeformate für Z3-Fixpunkt-Engine verwandt sind. Kurzes Beispiel: Angenommen, ich möchte die Existenz negativer Zahlen beweisen. Ich deklariere eine Funktion, die 1 für nichtnegative Zahlen und 0 für negative zurückgibt und anschließend Solver fehlschlägt, wenn es Argumente gibt, für die Funktion 0 zurückgibt. Es gibt jedoch eine Einschränkung: Ich möchte Solver antworten sat, wenn mindestens eine vorhanden ist negative Zahl und unsat, wenn alle Zahlen nicht negativ sind.

Es ist trivialerweise mit der Verwendung von declare-rel und query Format:

(declare-rel f (Int Int)) 
(declare-rel fail()) 
(declare-var n Int) 
(declare-var m Int) 

(rule (=> (< n 0) (f n 0))) 
(rule (=> (>= n 0) (f n 1))) 

(rule (=> (and (f n m) (= m 0)) fail)) 
(query fail) 

Aber es wird heikel, während reines Format SMT-LIB2 Verwendung (mit forall). Zum Beispiel gibt

(set-logic HORN) 
(declare-fun f (Int Int) Bool) 
(declare-fun fail() Bool) 

(assert (forall ((n Int)) 
    (=> (< n 0) (f n 0)))) 
(assert (forall ((n Int)) 
    (=> (>= n 0) (f n 1)))) 

(assert (forall ((n Int) (m Int)) 
    (=> (and (f n m) (= m 0)) fail))) 
(assert (not fail)) 

(check-sat) 

unsat zurück. Es überrascht nicht, dass das Ändern von (= m 0) zu (= m 1) dasselbe ergibt. Wir können sat nur implizieren fail von (= m 2). Das Problem ist, dass ich nicht verstehen kann, , wie Solver mit diesem Format zu fragen.

Wie ich es im Moment bin zu verstehen, während forall -Form mit können wir fragen nur ∀-Lösungen zu finden, dh die Antwort sat bedeutet, dass Solver (oder invariant) satisfiying alle Behauptungen für alle finden Interpretation verwaltet Werte und unsat bedeutet, dass es keine solchen Funktionen gibt. Mit anderen Worten, es versucht beweisen, setzen Sie den "Beweis" (die Invariante) in das Modell (offensichtlich, wenn sat).

Im Gegenteil, wenn query die Lösung in dem declare-rel Format Solver ing sucht die Lösung für einig Variablen, wie nur die Einschränkungen unter dem ∃-Quantor sind. Mit anderen Worten gibt es das Gegenbeispiel. Es kann nur die Invariante im Fall von unsat drucken.

Ich habe ein paar Fragen:

1. Bin Verständnis ich es richtig? Ich habe das Gefühl, dass ich einige Schlüsselideen vermisse. Zum Beispiel wird eine allgemeine Idee, wie (query ...) in Bezug auf (assert (forall ...)) ausgedrückt wird wirklich hilfreich sein (und Frage 2 automatisch beantworten).
2. Gibt es eine Möglichkeit, solche ∃-Einschränkungen (Ausgabe sat, wenn Gegenbeispiel gefunden wurde) mit reinem SMT-LIB2-Format zu lösen? Wenn ja, wie?

Answer 1

Zunächst ist das Format, das "declare-rel", "declare-var", "rule" und "query" verwendet, eine benutzerdefinierte Erweiterung von SMT-LIB2. Die "declare-var" -Funktion ist praktisch, um gebundene Variablen aus mehreren Regeln zu entfernen. Es erlaubt auch Datalog-Regeln mit stratifizierter Negation zu formulieren und die Semantik dafür ist das, was Sie von stratifizierter Negation erwarten sollten. Laut Konvention verwendet "sat", um anzugeben, dass eine Abfrage eine Ableitung hat, und "unzufrieden", dass für eine Abfrage keine Ableitung existiert.

Es stellt sich heraus, dass Standard-SMT-LIB2 ziemlich viel ausdrücken kann, was Sie für Hornklauseln ohne Negation wollen.Regeln werden zu Implikationen und Abfragen sind Implikationen des Formulars: (=> query false) oder wie du es geschrieben hast (nicht query). Eine Ableitung im benutzerdefinierten Format entspricht einem Beweis der leeren Klausel (z. B. Beweis von "Abfrage", die dann "falsch" erweist). Die Existenz einer Ableitung bedeutet also, dass die SMT-LIB2-Behauptungen "ungeeignet" sind. Umgekehrt, wenn es eine Interpretation (ein Modell) für die Horn-Klauseln gibt, dann stellt ein solches Modell fest, dass es keine Ableitung gibt. Die Klauseln sind "sat".

Mit anderen Worten:

"sat" for datalog extension <=> "unsat" for SMT-LIB2 formulation 
"unsat" for datalog extension <=> "sat" for SMT-LIB2 formulation 

Der Vorteil der reinen SMT-LIB2-Format, wenn es gilt, ist, dass gibt es keine spezielle Syntax-Erweiterungen. Dies sind einfache SMT-Formeln und andere, die diese Klasse von Formeln lösen möchten, müssen nicht spezielle Erweiterungen schreiben, sie müssen nur sicherstellen, dass die Solver, die auf Horn-Klauseln abgestimmt sind, die entsprechende Klasse von Formeln erkennen. (Z3s Implementierung des HORN-Fragments erlaubt eine gewisse Flexibilität beim Niederschreiben von Horn-Klauseln. Sie können Disjunktionen in den Körpern haben und Sie können Curry-Implikationen haben).

Es gibt einen Nachteil bei der Verwendung des SMT-LIB2-Formats, das das regelbasierte Format unterstützt: Wenn eine Ableitung der Abfrage vorhanden ist, verfügt das regelbasierte Format über Pragmas zum Drucken von Elementen eines Tupels. Beachten Sie, dass die Abfragerelation im Allgemeinen Argumente annehmen kann. Diese Funktion ist nützlich für endliche Domänenbeziehungen. Ihr Beispiel oben verwendet Integer, so dass die Relationen keine endliche Domäne sind, aber Beispiele im Online-Tutorial enthalten endliche Domain-Instanzen. Nun entspricht eine Ableitung einer Abfrage auch einem Auflösungsnachweis. Sie können einen Entlastungsbeweis aus dem SMT-LIB2-Fall extrahieren, aber ich muss sagen, es ist eher verschachtelt und ich habe keinen Weg gefunden, es effektiv zu verwenden. Die "Dualität" -Maschine für Horn-Klauseln erzeugt Ableitungen in einem zugänglicheren Format als das Standardbeweisformat von Z3. In jedem Fall ist es wahrscheinlich, dass Benutzer auf Hindernisse stossen, wenn sie versuchen, mit den Proof-Zertifikaten zu arbeiten, weil sie selten verwendet werden. Das regelbasierte Format verfügt über ein weiteres Feature, das eine Gruppe von Prädikaten mit Instanzen zusammenstellt, die einer Ableitung entsprechen. Es ist einfacher, diese Ausgabe zu betrachten.