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可以return"unsat"，而它总是"timeout"。不知道Z3能不能处理这种量词，有没有大佬给点建议。

谢谢。

Answer 1

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

;(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 子句公式的 class 上找到归纳不变量，但它需要转换才能将任意公式转换为这种格式。

Answer 2

谢谢，Malte 和 Nikolaj。变量 N 应该是有界的：

(assert (> N 0))
(assert (< N 10000))

我替换

(assert (> (a N) (+ N N)))

和

(assert (and
 (not (> (a N) (+ N N)))
 (> (a (+ N 1)) (+ (+ N 1) (+ N 1)))
))

并且它适用于 a(n) 的两个定义。这是不是你说的那种归纳证明？

这是两个代码块，它们都是 return "unsat":

(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 (> N 0))
(assert (< N 10000))
;(assert (> (a N) (+ N N)))
(assert (and
  (not (> (a N) (+ N N)))
  (> (a (+ N 1)) (+ (+ N 1) (+ N 1)))
))
(check-sat)
;(get-model)

和

(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 (> N 0))
(assert (< N 10000))
;(assert (> (a N) (+ N N)))
(assert (and
  (not (> (a N) (+ N N)))
  (> (a (+ N 1)) (+ (+ N 1) (+ N 1)))
))
(check-sat)
;(get-model)

Z3 中带有量词的函数

function with quantifier in Z3

z3