在z3中定义列表的插入方法的问题

Question

我正在Z3中为列表开发一个插入方法。但是，我必须满足一些要求：

• 未插入该项目，如果它已经在列表中

• 未插入项目，如果列表（集合）已满

  首先，我定义数据类型：

(declare-datatypes (T) ((Lst nil (cons (hd T) (tl Lst)))))

我定义函数isFull来知道列表是否超过最大容量，而IsMember则知道列表是否包含数字。

(define-fun isFull  ((l (Lst Int))) Bool
  (ite
    (<= (len l) 10)
    false
    true
  )
)
(define-fun-rec isMember((i Int) (l (Lst Int))) Bool 
  (ite
    (= l nil)
    false
    (or (= i (hd l)) (isMember i (tl l)))
  )
)

然后我试图定义一个插入方法，但是出了点问题：

(define-fun insert ((i Int) (l (Lst Int))) (l (Lst Int))
  (ite (= false (isMember i l )  )
    (ite (= false (isFull l ))
      (ite(= l nil)
          (= (hd l) i)
      )
    )
  )
)

Answer 1

您尚未向我们显示您对len的定义，并且您的代码中存在许多语法错误。但是您似乎走上了正确的道路。我会将您的规范编写如下：

(declare-datatypes (T) ((Lst nil (cons (hd T) (tl Lst)))))

(define-fun-rec len ((l (Lst Int))) Int
   (ite (= l nil) 0 (+ 1 (len (tl l)))))

(define-fun isFull  ((l (Lst Int))) Bool
  (> (len l) 10))

(define-fun-rec isMember ((i Int) (l (Lst Int))) Bool
  (and (distinct l nil)
       (or (= i (hd l))
           (isMember i (tl l)))))

(define-fun funnyInsert ((i Int) (l (Lst Int))) (Lst Int)
  (ite (or (isMember i l) (isFull l))
       l
       (cons i l)))

我称呼您的插入funnyInsert，因为它的作用很有趣。

[请注意，尽管z3将按原样接受此程序，但是使用这些定义不太可能证明任何有趣的事情。递归函数的属性通常使用归纳证明，而SMT求解器通常不执行归纳。至少在没有大量修改策略之类的情况下，不要开箱即用。祝你好运！