我试图在 Microsoft 的 SMT 求解器 Z3 中证明一个归纳事实。我知道 Z3 一般不提供此功能,如Z3 guide http://rise4fun.com/z3/tutorial/guide(第 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 http://rise4fun.com/Z3/ZdxO.
当然,使用这个设置,Z3会超时,例如(p 110)
.
未来Z3将对“有界量化”有更好的支持。在大多数情况下,处理此类量词的最佳方法是对其进行扩展。
通过编程 API,我们可以在将表达式发送到 Z3 之前轻松“实例化”它们。
这是 Python 中的一个示例(http://rise4fun.com/Z3Py/44lE 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在求解之前对公式进行了预处理。那么,大多数包含算术符号的模式将永远不会匹配。有关如何有效使用模式/触发器的更多信息,请参阅本文 http://research.microsoft.com/en-us/um/people/moskal/pdf/prtrig.pdf。作者还提供了一个幻灯片 http://research.microsoft.com/en-us/um/people/moskal/pdf/prtrig-slides.pdf.
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)