2

我想用 Z3 python 证明两个公式 'f' 和 'g' 的等价性。在下面的代码中，基本上 'g' 是 'f' 并添加了一些随机代码。我用 Exists 限定符忽略了 'g' 中的所有随机代码，所以 'f' 和 'g' 实际上是等价的。

MI = BitVecSort(32)
MV = BitVecSort(8)
Mem = Array('Mem', MI, MV)

def equivalence(F, G):
    s = Solver()
    s.add(Not(F == G))
    if s.check() == unsat:
        print "Equivalence"
    else:
        print "Inequivalence"

def Select2(M, I): 
    return Concat(Select(M, I+1), Select(M, I))

x, y = BitVecs('x y', 32)

g = True
t = BitVec('t', 32)
g = And(g, t == y)
t2 = BitVec('t2', 16)
g = And(g, t2 == Select2(Mem, t))
t3 = BitVec('t3', 32)
g = And(g, t3 == (t + 2))
y1 = BitVec('y1', 32)
g = And(g, y1 == t)
x1 = BitVec('x1', 32)
g = And(g, x1 == 0)

f = True
x1 = BitVec('x1', 32)
f = And(f, x1 == 0)

equivalence(Exists([t3, t2, t, y, y1, x], g), f)

但是，此脚本返回“不等价”而不是预期的“等价”。实际上，仔细观察，等价中的 s.check() 返回“未知”。

我希望 Z3 能够轻松解决这个小问题，但似乎 Z3 在这里做错了什么。任何想法？

非常感谢。

4

1 回答 1

2

你得到unknown是因为量词。您可以通过应用量词消除来获得预期的答案。我们可以创建一个使用qe和求解器的smt求解器。我们只需要更换

   s = Solver()

和

   s = Then('qe', 'smt').solver()

Then是一个组合器，它构建一个应用qe（量词消除）的策略，然后调用通用 SMT 求解器smt。该方法.solver()将策略转换为求解器。

我们可以在这里测试它。

于 2013-04-11T16:35:23.693 回答