Invariante Induktion über Hornsätze mit Z3py

Question

Ich verwende Z3py, um einige Invarianten abzuleiten, die als eine Konjunktion von Hornsätzen kodiert sind, während sie auch eine Vorlage für die Invariante liefern. Ich fange zuerst mit einem einfachen Beispiel an, wenn Sie das Code-Snippet unten sehen.

x = 0; 
while(x < 5){ 
    x += 1 
} 
assert(x == 5) 

Dies schlägt sich in den Horn-Klauseln

x = 0 => Inv (x)

x < 5/\ Inv (x) => Inv (x +1)

Nicht (x < 5)/\ Inv (x) => x = 5

Die hier unveränderlich ist x < = 5.

Ich habe eine Vorlage für die Invariante der Form a * x + b < = c zur Verfügung gestellt, so dass der Löser nur eine Menge von Werten für a, b und c erraten muss, die auf x < = 5 reduziert werden kann

Aber wenn ich es kodiere, werde ich immer ungeeignet. Wenn ich versuche, Nicht (x == 5) zu bestätigen, bekomme ich a = 2, b = 1/8 und c = 2, was für mich als Gegenbeispiel wenig Sinn macht.

Ich stelle meinen Code zur Verfügung und wäre dankbar für jede Hilfe bei der Korrektur meiner Codierung.

x = Real('x') 
x_2 = Real('x_2') 
a = Real('a') 
b = Real('b') 
c = Real('c') 
s = Solver() 
s.add(ForAll([x],And(
Implies(x == 0 , a*x + b <= c), 
Implies(And(x_2 == x + 1, x < 5, a*x + b <= c), a*x_2 + b <= c), 
Implies(And(a*x + b <= c, Not(x < 5)), x==5) 
))) 
if (s.check() == sat): 
    print(s.model()) 

Edit: es wird für mich Fremder. Wenn ich die x_2-Definition entferne und einfach x_2 durch (x + 1) in der zweiten horn-Klausel ersetze sowie x_2 = x_2 + 1 lösche, werde ich ungeeignet, ob ich Not (x == 5) oder x == 5 schreibe in der letzten Hornklausel.

Answer 1

gab es zwei Dinge, die Ihre ursprüngliche Codierung von Arbeits verhindern:

1) Es ist nicht möglich, alle für einen einzigen Wert von x_2x erfüllen x_2 == x + 1 für. Wenn Sie also x_2 == x + 1 schreiben wollen, müssen sowohl x als auch universell quantifiziert werden.

2) Etwas überraschend, dieses Problem ist befriedigend in den ganzen Zahlen, aber nicht in den Realwerten. Sie können das Problem mit der Klausel x < 5 /\ Inv(x) => Inv(x + 1) sehen. Wenn x eine Ganzzahl ist, dann wird dies durch x <= 5 erfüllt. Wenn x jedoch ein realer Wert sein darf, dann können Sie x == 4.5 haben, was sowohl x < 5 als auch x <= 5 erfüllt, aber nicht x + 1 <= 5, so dass Inv(x) = (x <= 5) dieses Problem in den Reals nicht erfüllt.

Auch können Sie es hilfreich finden, Inv(x) zu definieren, es räumt den Code ziemlich ein bisschen auf. Hier ist die Codierung Ihres Problems mit diesen Änderungen:

from z3 import * 

# Changing these from 'Int' to 'Real' changes the problem from sat to unsat. 
x = Int('x') 
x_2 = Int('x_2') 
a = Int('a') 
b = Int('b') 
c = Int('c') 

def Inv(x): 
    return a*x + b <= c 

s = Solver() 

# I think this is the simplest encoding for your problem. 
clause1 = Implies(x == 0 , Inv(x)) 
clause2 = Implies(And(x < 5, Inv(x)), Inv(x + 1)) 
clause3 = Implies(And(Inv(x), Not(x < 5)), x == 5) 
s.add(ForAll([x], And(clause1, clause2, clause3))) 

# Alternatively, if clause2 is specified with x_2, then x_2 needs to be 
# universally quantified. Note the ForAll([x, x_2]... 
#clause2 = Implies(And(x_2 == x + 1, x < 5, Inv(x)), Inv(x_2)) 
#s.add(ForAll([x, x_2], And(clause1, clause2, clause3))) 

# Print result all the time, to avoid confusing unknown with unsat. 
result = s.check() 
print result 
if (result == sat): 
    print(s.model()) 

Eine weitere Sache: es ist ein bisschen seltsam für mich a*x + b <= c als Vorlage zu schreiben, da dies das gleiche wie a*x <= d für eine ganze Zahl d ist.