Z3:证明两个公式相等时的错误结果。Z3错误？
Z3:证明两个公式相等时的错误结果。Z3错误？
提问于 2013-04-11 18:03:05
我想用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)然而，此脚本返回‘Inequivalence’而不是预期的‘Equivalence’。实际上，仔细观察，Equivalence中的s.check()返回“未知”。
我原以为Z3能轻松解决这个微不足道的问题，但看起来Z3在这里做错了什么。有什么想法吗？
非常感谢。
回答 1
Stack Overflow用户
回答已采纳
发布于 2013-04-12 00:35:24
因为有了量词，你才会得到unknown。您可以通过应用量词消除来获得预期的结果。我们可以创建一个使用qe和smt求解器的求解器。我们只需要替换掉
s = Solver()使用
s = Then('qe', 'smt').solver()Then是一个组合器，它构建了一个应用qe (量词消除)的策略，然后调用通用的smt求解器。.solver()方法将策略转换为求解器。
我们可以通过here来测试它。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/15945931
复制相关文章
相似问题
腾讯云开发者
