Ändern der Reihenfolge der Z3 fixepoint Abfragen ändert das Ergebnis

Question

Ich versuche, herauszufinden, warum Abfrage Aufträge Swapping kann die Antwort von Z3 FixedPoint Motor ändern:

(declare-rel fib (Int Int)) 
(declare-rel q1()) 
(declare-rel q2()) 
(declare-var n Int) 
(declare-var tmp1 Int) 
(declare-var tmp2 Int) 

(rule (=> (< n 2) (fib n 1))) 
(rule (=> (and (>= n 2) 
       (fib (- n 1) tmp1) 
       (fib (- n 2) tmp2)) 
     (fib n (+ tmp1 tmp2)))) 

(rule (=> (< n 2) q1)) 
(rule (=> (and (fib n tmp1) (<= tmp1 0)) q2)) 

(query q1) 
(query q2) 

erste Abfrage q1 ist ein Dummy ein, nur Motor zu fragen über etwas. Die zweite Abfrage q2 widerspricht mit infered Invariant, dass Fibonacci-Zahlen immer positiv sind.

Wenn die Reihenfolge der Anfragen ist

(query q2) 
(query q1) 

alles funktioniert, sind richtige Antworten gegeben. Aber tauschen sie den nächsten Fehler gibt, während q2 Abfrage:

(smt.diff_logic: non-diff logic expression (+ fib_1_1 fib_1_0 (* (- 1) fib_1_n))) 
unknown 

Kann jemand den Grund erklären? Ist es Z3 Problem oder mache ich etwas falsch? Als erstes werden irgendwelche Vorschläge zur Bearbeitung (ich verwende .NET API) sehr geschätzt. Vielen Dank!

Answer 1

Es ist ein wenig aggressiv unter der Annahme, dass alle Einschränkungen UTVPI (Einheit zwei Variable pro Ungleichung) sind. Der UTVPI-Modus ist oft schneller als allgemeine lineare Arithmetik. Es schneidet den Suchraum nach Kandidaten-Invarianten bis zu UTVPI-Formeln ab und verwendet flussbasierte Entscheidungsprozeduren für Constraints. Auf der anderen Seite kann es Invarianten vermissen, die nicht in dem UTVPI-Fragment ausgedrückt werden können. Standardmäßig überprüft die PDR-Engine, ob die Formeln alle zu UTVPI gehören, in dem Fall in den UTVPI-Modus wechselt.

Sie können den UTVPI-Modus deaktivieren, indem Sie die Option verwenden.

fixedpoint.pdr.utvpi = false

Ich werde versuchen, den Schalter anmutiger zu machen. Danke für das Beispiel.