证明 2 个公式在某些条件下等价? [英] Prove 2 formulas equivalent under some conditions?
问题描述
如果a == 0
,两个公式a1 == a + b
和a1 == b
是等价的.我想用 Z3 python 找到这个必需的条件(a == 0
).我写了下面的代码:
Two formulas a1 == a + b
and a1 == b
are equivalent if a == 0
. I want to find this required condition (a == 0
) with Z3 python. I wrote the code below:
from z3 import *
def equivalence(F, G):
s = Solver()
s.add(Not(F == G))
r = s.check()
if r == unsat:
print 'Equ'
print s.model()
else:
print 'Not Equ'
a, b = BitVecs('a b', 32)
g = True
tmp = BitVec('tmp', 32)
g = And(g, tmp == a)
tmp1 = BitVec('tmp1', 32)
g = And(g, tmp1 == b)
tmp2 = BitVec('tmp2', 32)
g = And(g, tmp2 == (tmp1 + tmp))
a1 = BitVec('a1', 32)
g = And(g, a1 == tmp2)
f = True
f = And(f, a1 == b)
equivalence(Exists([a], g), f)
然而,上面的代码总是返回 "Not Equ"
作为输出.然后显然我无法将模型 (a === 0
) 作为 "f"
和 "g"
的条件等效,
However, the above code always returns "Not Equ"
as the output. Then obviously I cannot get the model (a === 0
) as the condition for "f"
and "g"
to be equivalent, either.
知道代码哪里出错了,以及如何修复它吗?非常感谢!
Any idea on where the code is wrong, and how to fix it? Thanks so much!
推荐答案
帖子中的代码与提出的问题不符.在 smt-lib 邮件列表中提出并回答了类似的问题.
The code in the post does not correspond to the question that is asked. A similar question was asked and answered on the smt-lib mailing list.
这篇关于证明 2 个公式在某些条件下等价?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!