Проблема определения метода вставки списка в z3 - PullRequest
Новая
       24

Проблема определения метода вставки списка в z3

0 голосов
/ 03 марта 2020

Я разрабатываю метод вставки в 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)
      )
    )
  )
)

1 Ответ

1 голос
/ 03 марта 2020

Вы не показали нам свое определение len, и в вашем коде есть куча ошибок syntacti c. Но вы, кажется, на правильном пути. Я бы закодировал вашу spe c следующим образом: 

(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-решатели обычно не выполняют индукцию. По крайней мере, не из коробки без большого количества поворотов с тактикой и тому подобным. Желаем удачи!

...