Z3 - 假设如何运作

Question

我在 Z3py 中有以下代码

    import z3
    x = z3.BitVec('x', 32)
    a = z3.BitVec('a', 32)
    solver=z3.Solver()
    solver.set(unsat_core=True)
    d=z3.Bool('d')
    solver.assert_and_track(x!=a,d)
    solver.add(x==a)
    print solver.check(d)
    print solver.check(z3.Not(d))

我希望它打印 unsat 和 sat。但是它总是打印 unsat。调用 solver.check(z3.Not(d)) 是否应该有效地禁用断言 x!=a？

Answer 1

assert_and_track 只是将 answer-literal d 与示例中的公式 x!=a 相关联。由于上下文同时包含x==a和x!=a，所以是unsat。没有假设会使它令人满意。

但我同意这非常令人困惑。我认为问题可以追溯到 assert_and_track 而不是 真正用于您正在尝试做的事情的事实，而只是为了使 unsat-core-extraction 成为可能。请参阅此处的讨论：

要真正实现你想要的，只需自己断言含义即可。即使用：

solver.add(Implies(d, x!=a))

例如下面的脚本：

from z3 import *

x = z3.BitVec('x', 32)
a = z3.BitVec('a', 32)

solver=z3.Solver()
solver.set(unsat_core=True)
d=z3.Bool('d')

solver.add(Implies(d, x!=a))
solver.add(x==a)

print solver.check(d)
print solver.unsat_core()
print solver.check(z3.Not(d))
print solver.model()

产生：

unsat
[d]
sat
[a = 0, d = False, x = 0]

我相信这就是你想要达到的目标。

Z3 - 假设如何运作

Z3 - how assumptions works

z3

z3py