证明 Z3 中的归纳事实 [英] Proving inductive facts in Z3

问题描述

我正在尝试证明 Z3(Microsoft 的 SMT 求解器)中的一个归纳事实.我知道 Z3 通常不提供此功能，如 Z3 指南(第 8 节: 数据类型)，但是当我们限制要证明事实的域时，这似乎是可能的.考虑以下示例:

I am trying to prove an inductive fact in Z3, an SMT solver by Microsoft. I know that Z3 does not provide this functionality in general, as explained in the Z3 guide (section 8: Datatypes), but it looks like this is possible when we constrain the domain over which we want to prove the fact. Consider the following example:

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (=> 
    (and (> x 0) (<= x 20))
    (= (p (- x 1)) (p x) ))))
(assert (not (p 20)))

(check-sat)

求解器正确响应 unsat，这意味着 (p 20) 是有效的.问题是，当我们进一步放松这个约束时(我们用任何大于 20 的整数替换前面例子中的 20)，求解器会以 unknown 响应.

The solver responds correctly with unsat, which means that (p 20) is valid. The problem is that when we relax this constraint any further (we replace 20 in the previous example by any integer greater than 20), the solver responds with unknown.

我觉得这很奇怪，因为解决原来的问题不需要Z3很长时间，但是当我们将上限增加1时，它突然变得不可能了.我尝试向量词添加一个模式，如下所示:

I find this strange because it does not take Z3 long to solve the original problem, but when we increase the upper limit by one it becomes suddenly impossible. I have tried to add a pattern to the quantifier as follows:

(declare-fun p (Int) Bool)
(assert (p 0))

(assert (forall ((x Int)) 
    (! (=> 
    (and (> x 0) (<= x 40))
    (= (p (- x 1)) (p x) )) :pattern ((<= x 40)))))
(assert (not (p 40)))

(check-sat)

哪个看起来效果更好，但现在上限是 40.这是否意味着我最好不要使用 Z3 来证明这些事实，还是我的问题表述有误?

Which seems to work better, but now the upper limit is 40. Does this mean that I can better not use Z3 to prove such facts, or am I formulating my problem incorrectly?

推荐答案

Z3 使用许多启发式方法来控制量词实例化.其中之一是基于实例化深度".Z3 用深度"属性标记每个表达式.所有用户提供的断言都被标记为深度 0.当一个量词被实例化时，新表达式的深度会发生碰撞.Z3 不会使用深度大于预定义阈值的表达式来实例化量词.在您的问题中，达到了阈值:(p 40) 是深度 0，(p 39) 是深度 1，(p 38)是深度2等

Z3 uses many heuristics to control quantifier instantiation. One one them is based on the "instantiation depth". Z3 tags every expression with a "depth" attribute. All user supplied assertions are tagged with depth 0. When a quantifier is instantiated, the depth of the new expressions is bumped. Z3 will not instantiate quantifiers using expressions tagged with a depth greater than a pre-defined threshold. In your problem, the threshold is reached: (p 40) is depth 0, (p 39) is depth 1, (p 38) is depth 2, etc.

要增加阈值，您应该使用以下选项:

To increase the threshold, you should use the option:

(set-option :qi-eager-threshold 100)

以下是此选项的示例:http://rise4fun.com/Z3/ZdxO.

Here is the example with this option: http://rise4fun.com/Z3/ZdxO.

当然，使用这个设置，Z3会超时，例如对于(p 110).

Of course, using this setting, Z3 will timeout, for example, for (p 110).

未来Z3会更好的支持有界量化".在大多数情况下，处理这种量词的最佳方法是对其进行扩展.使用编程 API，我们可以在将表达式发送到 Z3 之前轻松地实例化"它们.这是 Python 中的一个示例(http://rise4fun.com/Z3Py/44lE):

In the future, Z3 will have better support for "bounded quantification". In most cases, the best approach for handling this kind of quantifier is to expand it. With the programmatic API, we can easily "instantiate" expressions before we send them to Z3. Here is an example in Python (http://rise4fun.com/Z3Py/44lE):

p = Function('p', IntSort(), BoolSort())

s = Solver()

s.add(p(0))
s.add([ p(x+1) == p(x) for x in range(40)])
s.add(Not(p(40)))

print s.check()

最后，在 Z3 中，包含算术符号的模式不是很有效.问题是Z3在求解前对公式进行了预处理.然后，大多数包含算术符号的模式将永远不会匹配.有关如何有效使用模式/触发器的详细信息，请参阅 这篇文章.作者还提供了一个幻灯片组.

Finally, in Z3, patterns containing arithmetic symbols are not very effective. The problem is that Z3 preprocess the formula before solving. Then, most patterns containing arithmetic symbols will never match. For more information on how to use patterns/triggers effectively, see this article. The author also provides a slide deck.

这篇关于证明 Z3 中的归纳事实的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！