在 z3 中列出 concat

Question

有没有办法在 z3 中连接两个列表？类似于 ML 中的 @ 运算符？我正在考虑自己定义它，但我认为 z3 不支持递归函数定义，即

define-fun concat ( (List l1) (List l2) List 
   (ite (isNil l1) (l2) (concat (tail l1) (insert (head l1) l2)) )
)

Answer 1

2021 年更新

以下答案写于 2012 年； 9年前。它在很大程度上仍然是正确的；除了 SMTLib 现在通过 define-fun-rec 构造明确允许递归函数定义。然而，求解器的支持仍然很弱，关于这些函数的大多数感兴趣的属性仍然不能被证明是开箱即用的。底线仍然是这样的递归定义会导致归纳证明，而 SMT 求解器根本不具备进行归纳的能力。也许再过 9 年他们就能做到这一点，大概允许用户指定他们自己的不变量。目前，Isabelle、Coq、ACL2、HOL、Lean 等定理证明器仍然是处理这类问题的最佳工具。

2012 年的回答

您是正确的，SMT-Lib2 不允许递归函数定义。 （在 SMT-Lib2 中，函数定义更像宏，它们适合缩写。）

通常的技巧是将这些符号声明为未解释的函数，然后将定义方程断言为量化的公理。当然，一旦量词发挥作用，求解器就可以开始为“困难”查询返回unknown 或timeout。但是，Z3 非常擅长于典型软件验证任务产生的许多目标，因此它应该能够证明许多感兴趣的属性。

这是一个示例，说明如何在列表上定义len 和append，然后证明它们的一些定理。请注意，如果证明需要归纳，则 Z3 可能会超时（如下面的第二个示例所示），但 Z3 的未来版本可能也能够处理归纳证明。

如果您想试一试，这里是 Z3 网站上此示例的永久链接：http://rise4fun.com/Z3/RYmx

; declare len as an uninterpreted function
(declare-fun len ((List Int)) Int)

; assert defining equations for len as an axiom
(assert (forall ((xs (List Int)))
          (ite (= nil xs)
               (= 0                     (len xs))
               (= (+ 1 (len (tail xs))) (len xs)))))

; declare append as an uninterpreted function
(declare-fun append ((List Int) (List Int)) (List Int))

; assert defining equations for append as an axiom
(assert (forall ((xs (List Int)) (ys (List Int)))
            (ite (= nil xs)
                 (= (append xs ys) ys)
                 (= (append xs ys) (insert (head xs) (append (tail xs) ys))))))

; declare some existential constants
(declare-fun x () Int)
(declare-fun xs () (List Int))
(declare-fun ys () (List Int))

; prove len (insert x xs) = 1 + len xs
; note that we assert the negation, so unsat means the theorem is valid
(push)
(assert (not (= (+ 1 (len xs)) (len (insert x xs)))))
(check-sat)
(pop)

; prove (len (append xs ys)) = len xs + len ys
; note that Z3 will time out since this proof requires induction
; future versions might very well be able to deal with it..
(push)
(assert (not (= (len (append xs ys)) (+ (len xs) (len ys)))))
(check-sat)
(pop)

Answer 2

虽然 Levent 的代码有效，但如果您愿意为递归深度设置一个界限，那么 Z3 的断言问题通常会少得多。您甚至不需要依赖 MBQI，这通常需要花费太多时间才能实用。从概念上讲，您需要这样做：

; the macro finder can figure out when universal declarations are macros
(set-option :macro-finder true)

(declare-fun len0 ((List Int)) Int)
(assert (forall ((xs (List Int))) (= (len0 xs) 0)))

(declare-fun len1 ((List Int)) Int)
(assert (forall ((xs (List Int))) (ite (= xs nil)
                                       0
                                       (+ 1 (len0 (tail xs))))))

(declare-fun len2 ((List Int)) Int)
(assert (forall ((xs (List Int))) (ite (= xs nil)
                                       0
                                       (+ 1 (len1 (tail xs))))))

... 等等。手动写下所有这些可能会很痛苦，所以我建议使用编程 API。 （无耻的插头：我一直在工作 Racket bindings 和 here's how 你会在那里做的。）