1

给定c == a + 4和t == c + b，如果b == -4，那么t == a。我试图做相反的事情，这意味着给定上述 2 个等式和t == a，我试图找到 的值b。

这与相关问题非常相似，但这次我只切换aand b，我真的很困惑代码返回不同的结果。

按照上面链接中发布的代码，我有以下代码（类似，仅a和b切换）：

#!/usr/bin/python
from z3 import *

a, b, c, t = BitVecs('a b c t', 32)

g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))

s = Solver()
s.add(ForAll([t, a, c], Implies(t == a, g)))
if s.check() == sat:
    print s.model()[b]
else:
    print 'Unsat'

但是，在 Ubuntu 上，运行上述代码会返回意外结果Unsat，但不会返回值-4（或0xfffffffc）

知道为什么这是错误的吗？

非常感谢。

4

1 回答 1

1

Z3实际上正在回归unknown。该方法check返回sat：unsat或unknown。这是一个自定义策略，表明该公式确实不饱和。

#!/usr/bin/python
from z3 import *
a, b, c, t = BitVecs('a b c t', 32)

g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))

s = Goal()
s.add(ForAll([t, a, c], Implies(t == a, g)))

T = Then("simplify", "der", "distribute-forall")
# print the simplified formula. Note that it is unsat
print T(s)

# Create a solver using the tactic above and qe

s = Then("simplify", "der", "distribute-forall", "qe", "smt").solver()
s.add(ForAll([t, a, c], Implies(t == a, g)))
print s.check()

更新 公式的形式是

forall t, a, c: t == a ==> c == (a + 4) and t == (c + b).

这个公式在逻辑上等价于：

forall a, c: c == (a + 4) and a == (c + b).

这在逻辑上等价于

(forall a, c: c == (a + 4)) and (forall a, c: a == (c + b)).

这两个子公式在逻辑上都等价于假。这就是公式不可满足的原因。

您写的评论表明您认为您创建的公式略有不同

forall t, a, c: t == a ==> c == (a + 4) ==> t == (c + b).

这个公式是sat。要创建这个公式，我们必须替换

g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))

和

g = Implies(c == (a + 4), t == (c + b))

更新的示例可在此处获得。

于 2013-07-05T19:31:30.437 回答