我试图证明 Z3（Microsoft 的 SMT 求解器）中的一个归纳事实。我知道 Z3 通常不提供此功能，如Z3 指南（第 8 节：数据类型）中所述，但是当我们限制要证明事实的域时，这似乎是可能的。考虑以下示例：
(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。
我觉得这很奇怪，因为 Z3 解决原来的问题并没有花很长时间，但是当我们将上限增加 1 时，它突然变得不可能。我试图向量词添加一个模式，如下所示：
(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 来证明这样的事实，或者我是否错误地表述了我的问题？
Z3 使用许多启发式方法来控制量词实例化。其中之一是基于“实例化深度”。Z3 用“深度”属性标记每个表达式。所有用户提供的断言都被标记为深度 0。当一个量词被实例化时，新表达式的深度会发生碰撞。Z3 不会使用深度大于预定义阈值的表达式来实例化量词。在您的问题中，达到了阈值：(p 40)深度为 0、(p 39)深度为 1、(p 38)深度为 2 等。
要增加阈值，您应该使用以下选项：
(set-option :qi-eager-threshold 100)
这是带有此选项的示例：http : //rise4fun.com/Z3/ZdxO。
当然，使用这个设置，Z3 会超时，例如对于(p 110).
未来，Z3将对“有界量化”有更好的支持。在大多数情况下，处理这种量词的最佳方法是对其进行扩展。使用编程 API，我们可以在将表达式发送到 Z3 之前轻松地“实例化”它们。这是 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在求解前对公式进行了预处理。然后，大多数包含算术符号的模式将永远不会匹配。有关如何有效使用模式/触发器的更多信息，请参阅此文章。作者还提供了幻灯片。