Z3Py: Warum sind die folgenden Annahmen nicht erfüllbar?

Question

Dies mag eine naive Frage sein, aber warum führt das Folgende nicht zu einer erfüllbaren Menge von Annahmen?

Folgt nicht die letzte Annahme direkt aus den Annahmen 2 und 3?

import z3 

# Initialize variables 
t = z3.Int('t') 
z = z3.Real("z") 
y = z3.Real("y") 
M = z3.Real("M") 
x = z3.Function("x", z3.IntSort(), z3.RealSort()) 
f = z3.Function("f", z3.RealSort(), z3.RealSort()) 
d_f1 = z3.Function("d_f1", z3.RealSort(), z3.RealSort()) 

# Add assumptions 
s = z3.Solver() 

s.add(f(y) == f(z) + d_f1(z) *(y-z)) 
s.add(d_f1(z) < M) 
s.add(f(x(t+1)) == f(x(t)) + d_f1(x(t)) *(x(t+1)-x(t))) 

s.add(f(x(t+1)) < f(x(t)) + M *(x(t+1)-x(t))) 

# Check if assumptions are satisfiable 
s.check() 

Das Ergebnis, das ich bekommen ist,

unknown 

Gibt es eine Möglichkeit, eine ähnliche Reihe von Annahmen zu kodieren, die als erfüllbar vom Solver bestimmt werden?

Danke!

Answer 1

Z3 gibt "unbekannt" zurück, was bedeutet, dass kein Modell für die Assertions gefunden werden kann. Der Hintergrund ist, dass Ihre Integritätsregeln nichtlineare Arithmetik über freie Funktionen (und Integer) verwenden. Z3 bietet keine Entscheidungsprozedur für das Fragment, in dem sich Ihre Formel befindet. Stattdessen versucht es eine unvollständige Suchprozedur und kommt auf einen Zustand, in dem es die Behauptungen weder aufstellen noch widerlegen kann.