Fehler mit rekursiven Funktionen?

Question

Ich versuche rekursive Funktionen in z3, und ich bin gespannt, ob es einen Fehler bei der Modellkonstruktion gibt. Bedenken Sie:

(define-fun-rec f ((x Int)) Int 
        (ite (> x 1) 
         (f (- x 1)) 
         1)) 
(check-sat) 
(get-value ((f 0))) 

Hier f ist eigentlich die konstante Funktion 1, nur in einer dummen Weise definiert. Für diesen Eingang, z3 druckt:

sat 
(((f 0) 0)) 

Dies scheint falsch, da f 01 sollte gleich.

Was interessant ist, wenn ich behaupten, was z3 als Ergebnis schlägt, dann bekomme ich die richtige unsat Antwort:

(define-fun-rec f ((x Int)) Int 
        (ite (> x 1) 
         (f (- x 1)) 
         1)) 
(assert (= (f 0) 0)) 
(check-sat) 

ich:

unsat 

Also, es sieht aus wie z3 tatsächlich tut jetzt, dass f 0 nicht 0 sein kann; obwohl es im vorherigen Fall genau dieses Modell hervorgebracht hat.

Gehen wir noch einen Schritt weiter, wenn ich Ausgabe:

(define-fun-rec f ((x Int)) Int 
        (ite (> x 1) 
         (f (- x 1)) 
         1)) 
(assert (= (f 0) 1)) 
(check-sat) 
(get-model) 

Dann antwortet z3:

sat 
(model 
    (define-fun f ((x!0 Int)) Int 
    1) 
) 

, die ist in der Tat eine vernünftige Antwort.

Also scheint es vielleicht einen Bug mit rekursiven Funktionsmodellen unter bestimmten Bedingungen zu geben?

Answer 1

Die verwendeten Modelle spiegeln nicht den Graph der rekursiven Funktionsdefinitionen wider. Wenn also rekursive Funktionen auf Werte ausgewertet werden, die beim Lösen nicht gesehen wurden, kann dies zu willkürlichen Ergebnissen führen. Dieses Verhalten wird jetzt geändert, da die rekursiven Definitionen in Modellen enthalten sind.