(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解决原始问题并不需要很长时间,但当我们将上限增加一时,它突然变得不可能。我尝试添加一个量词模式,如下所示:
(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来证明这些事实,还是我的问题表述有误?