测试一个常量是否匹配一个区间

Question

给定以下简单示例：

s = Solver()

Z = IntSort()
a = Const('a', Z)

s.add(a >= 0)
s.add(a < 10)

print(s.check(a > 5)) # sat

直到最后一行，a 的隐含范围是 0 <= a < 10 - a > 5 不满足 。但是，.check() 告诉 z3 “这是真的”——这不是我想要的。

有没有办法让 z3 测试是否 a > 5 给定现有的一组约束，并让 z3 将其解释为“根据我们对 a 的所有其他了解，确保这是真的"?

编辑：好的，我想我明白了。由于 z3 试图找到满足所有约束的模型，因此我应该检查 inverse 以查看它是否找到解决方案 - 在这种情况下，我的检查将不成立。

在这种情况下，我的“测试”功能将变为：

def test(s, expr):
    return s.check(Not(expr)) == unsat

因此...

s = Solver()

Z = IntSort()
a = Const('a', Z)

s.add(a >= 0)
s.add(a < 10)

print(s.check(a > 5)) # sat

print(s.check(Not(a > 5)) == unsat) # false, test failed
s.add(a > 8)

print(s.check(Not(a > 5)) == unsat) # true, test passed

对吗？

Answer 1

你所做的基本上是正确的，尽管不是惯用的。当您发出 s.check(formula) 时，您是在告诉 z3 显示您 add 编辑的所有其他约束以及 formula 的可满足性；即，它们的连词。因此，按照您的设置方式，它会为您提供正确的结果。

这里有更多细节。因为你想证明的是这样的：

Implies(And(lower, upper), required)

这样做的典型方法是断言它的否定，然后检查它是否可满足。也就是说，您将检查是否：

Not(Implies(And(lower, upper), required))

是可以满足的。回想一下 Implies(a, b) 等同于 Or(Not(a), b)，所以一点布尔逻辑将上面的转换为：

And(And(lower, upper), Not(required))

你正在做的是 add 上面的第一个合取（即 And(lower, upper)）到求解器本身，然后使用第二个合取 Not(required) 作为参数来检查看看你是否得到 unsat。如果这样做，那么您将获得 required 始终成立的“证明”。否则你会得到一个反例。

不过，我应该补充一点，这不是 z3py 的惯用用法，而是使用公式调用 check。后者通常与假设列表一起使用，并通过调用 get-unsat-assumptions 来确定其中的哪个子集是不可满足的。这些应用程序通常来自 model-checking 个问题。有关详细信息，请参阅 https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf 的第 4.2.5 节，其中讨论了 check-sat-assuming 的语义，它是 SMTLib 等价于使用额外假设调用 check。

要在更惯用的 z3 中解决您的问题，可以这样写：

from z3 import *

s = Solver()
a = Int('a')

lower    = a >= 0
upper    = a < 10
required = a > 5

formula = Implies(And(lower, upper), required)

# assert the negation
s.add(Not(formula))
r = s.check()
if r == sat:
    print("Not valid, counterexample:")
    print(s.model())
elif r == unsat:
    print("Valid!")
else:
    print("Solver said:", r)

这会打印：

Not valid, counterexample:
[a = 0]

如果您更改为 lower = a >= 8，它将打印：

Valid!

最重要的是，您所做的是正确的，但对 check-sat-assuming 来说不是很地道的用法。一种更简单的方法是简单地断言您的 lower/upper 边界暗示所需的不等式的含义的否定，并检查结果是否为 unsat。

测试一个常量是否匹配一个区间

Testing that a constant matches an interval

smt

z3