I am currently using Z3py to to deduce some invariants which are encoded as a conjunction of horn-clauses whilst also providing a template for the invariant. I'm starting with a simple example first if you see the code snippet below.
x = 0;
while(x < 5){
x += 1
}
assert(x == 5)
This translates into the horn clauses
x = 0 => Inv(x)
x < 5 /\ Inv(x) => Inv(x +1)
Not( x < 5) /\ Inv(x) => x = 5
The invariant here is x <= 5.
I have provided a template for the invariant of the form a*x + b <= c so that all the solver has to do is guess a set of values for a,b and c that can reduce to x <= 5.
However when I encode it up I keep getting unsat. If try to assert Not (x==5) I get a=2 , b = 1/8 and c = 2 which makes little sense to me as a counterexample.
I provide my code below and would be grateful for any help on correcting my encoding.
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: it gets stranger for me. If I remove the x_2 definition and just replace x_2 with (x + 1) in the second horn clause as well as delete the x_2 = x_2 + 1, I get unsat whether I write Not( x==5) or x==5 in the final horn clause.
There were two things preventing your original encoding from working:
1) It's not possible to satisfy x_2 == x + 1 for all x for a single value of x_2. Thus, if you're going to write x_2 == x + 1, both x and x_2 need to be universally quantified.
2) Somewhat surprisingly, this problem is satisfiable in the integers but not in the reals. You can see the problem with the clause x < 5 /\ Inv(x) => Inv(x + 1). If x is an integer, then this is satisfied by x <= 5. However, if x is allowed to be any real value, then you could have x == 4.5, which satisfies both x < 5 and x <= 5, but not x + 1 <= 5, so Inv(x) = (x <= 5) does not satisfy this problem in the reals.
Also, you might find it helpful to define Inv(x), it cleans up the code quite a bit. Here is the encoding of your problem with those changes:
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())
One more thing: it's a bit strange to me to write a*x + b <= c as a template, because this is the same as a*x <= d for some integer d.