z3 - Z3 中带有量词的函数

Question

我对量词有疑问。

设 a(0) = 0，a(n+1) 将是 a(n)+1 或 a(n)+2，具体取决于 x(n) 的值。我们可能期望对于任何类型的 x(.) 和所有 n，a(n) <= n*2。

这是 Z3 的代码:

(declare-fun a (Int) Int)
(declare-fun x (Int) Int)
(declare-fun N () Int)
(assert (forall 
    ((n Int))
    (=> (>= n 0)
        (= (a (+ n 1))
            (ite (> (x n) 0)
            (+ (a n) 1)
            (+ (a n) 2)
            )
        )
    )
))
(assert (= (a 0) 0))
(assert (> (a N) (+ N N)))

(check-sat)
(get-model)

我希望 Z3 可以返回“unsat”，而它总是“超时”。我想知道 Z3 是否可以处理这种量词，是否有人可以提供一些建议。

谢谢。

Answer 1

公式是SAT，对于N < 0，a的图是underspecified的。但是默认量词实例化引擎无法确定这一点。您可以利用您定义的递归函数来执行不同的引擎。

;(declare-fun a (Int) Int)
 (declare-fun x (Int) Int)
 (declare-fun y (Int) Int)
 (declare-fun N () Int)
 (define-fun-rec a ((n Int)) Int
   (if (> n 0) (if (> (x (- n 1)) 0) (+ (a (- n 1)) 1) (+ (a (- n 1)) 2)) (y n)))
(assert (= (a 0) 0))
(assert (> (a N) (+ N N)))

(check-sat)
(get-model)

正如 Malte 所写，不支持对此类公式进行归纳，因此不要指望 Z3 会产生归纳证明。它确实找到了一类 Horn 子句公式的归纳不变量，但它需要转换才能将任意公式转换为这种格式。