logic - Z3py对号角子句的不变感应

我目前正在使用Z3py来推导一些不变量，这些不变量被编码为号角句的连词，同时还提供了不变量的模板。如果您看到下面的代码段，那么我首先从一个简单的示例开始。

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

这转化为horn子句

x = 0 => Inv(x)

x Inv(x +1)

不是(x x = 5

这里的不变量是x
我提供了a * x + b 因此，求解器要做的就是猜测a，b和c的一组值，这些值可以减少到x
但是，当我对其进行编码时，我总是感到不安。如果尝试断言Not(x == 5)，我得到a = 2，b = 1/8和c = 2，这对我来说毫无意义。

我在下面提供了我的代码，对于纠正我的编码方面的帮助将不胜感激。

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())

编辑:它对我来说很陌生。如果删除x_2定义并在第二个horn子句中将x_2替换为(x + 1)并删除x_2 = x_2 + 1，则无论写Not(x == 5)还是x == 5，我都会感到不满意在最后的号角条款中。

最佳答案

有两件事使您的原始编码无法正常工作:

1)对于单个x_2 == x + 1值，不可能对所有x都满足x_2。因此，如果您要编写x_2 == x + 1，则必须统一量化x和x_2。

2)有点令人惊讶的是，这个问题在整数中是可以满足的，但在实数中是不能满足的。您可以看到子句x < 5 /\ Inv(x) => Inv(x + 1)的问题。如果x是整数，则x <= 5可以满足要求。但是，如果x允许为任何实际值，那么您可以拥有x == 4.5，它同时满足x < 5和x <= 5，但不能满足x + 1 <= 5，因此Inv(x) = (x <= 5)实际上无法满足此问题。

另外，您可能会发现定义Inv(x)会有所帮助，它可以使代码清理很多。这是这些更改所引起的问题的编码:

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())

还有一件事:将a*x + b <= c编写为模板对我来说有点奇怪，因为这与某些整数a*x <= d的d相同。

inv

logic - Z3py对号角子句的不变感应