在 z3 中列出 concat [英] list concat in z3

问题描述

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

Is there a way to concat two lists in z3? Similar to the @ operator in ML? I was thinking of defining it myself but I don't think z3 supports recursive function definitions, i.e.,

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

推荐答案

2021 更新

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

2021 Update

Below answer was written in 2012; 9 years ago. It largely remains still correct; except SMTLib now explicitly allows for recursive-function definitions, via define-fun-rec construct. However, solver support is still very weak, and most properties of interest regarding such functions can still not be proven out-of-the-box. Bottom line remains that such recursive definitions lead to inductive proofs, and SMT-solvers are simply not equipped to do induction. Perhaps in another 9 years they will be able to do so, presumably allowing users to specify their own invariants. For the time being, theorem-provers such as Isabelle, Coq, ACL2, HOL, Lean, etc., remain the best tools to handle these sorts of problems.

您是对的，SMT-Lib2 不允许递归函数定义.(在 SMT-Lib2 中，函数定义更像是宏，它们适合缩写.)

You are correct that SMT-Lib2 does not allow recursive function definitions. (In SMT-Lib2, function definitions are more like macros, they are good for abbreviations.)

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

The usual trick is to declare such symbols as uninterpreted functions, and then assert the defining equations as quantified axioms. Of course, as soon as quantifiers come into play the solver can start returning unknown or timeout for "difficult" queries. However, Z3 is pretty good at many goals arising from typical software verification tasks, so it should be able to prove many properties of interest.

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

Here's an example illustrating how you can define len and append over lists, and then prove some theorems about them. Note that if a proof requires induction, then Z3 is likely to time-out (as in the second example below), but future versions of Z3 might be able to handle inductive proofs as well.

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

Here's the permalink for this example on the Z3 web-site if you'd like to play around: 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)

这篇关于在 z3 中列出 concat的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！