Список «содержит» функцию в Z3 - PullRequest
Новая
       5

Список «содержит» функцию в Z3

0 голосов
/ 23 мая 2018

С учетом типичного типа списка: 

(declare-datatypes (X)(
  (Lst
    (nil)
    (insert
      (head X)
      (tail Lst)))))

Я пытаюсь создать функцию, которая возвращает, находится ли данный элемент в данном списке.Похоже, я должен использовать неинтерпретированную функцию.Я пробовал разные подходы без успеха.Например: 

(declare-fun is-in-lst ((Int)(Lst Int)) Bool)

(assert (forall((elem Int)(lst (Lst Int)))
  (=
    (is-in-lst elem lst)
    (and
      (is-insert lst)
      (or
        (= elem (head lst))
        (is-in-lst elem (tail lst)))))))

(declare-const l1 (Lst Int))

(assert (is-in-lst 6 l1))
(assert (is-in-lst 5 l1))

Это возможно в Z3?Если это так, что будет лучшим способом решения проблемы?Спасибо

1 Ответ

0 голосов
/ 23 мая 2018

Последний стандарт SMTLib допускает рекурсивные определения.Также List предопределено в Z3, поэтому вам не нужно определять его самостоятельно.Вы можете закодировать свою функцию как: 

(define-fun-rec elem ((e Int) (l (List Int))) Bool
   (ite (= l nil) false (or (= e (head l)) (elem e (tail l)))))

(declare-const l1 (List Int))
(assert (elem 6 l1))
(assert (elem 5 l1))

(check-sat)
(get-value (l1))

. Для этого z3 отвечает: 

sat
((l1 (let ((a!1 (insert 6 (insert 4 (insert 7 (insert 5 nil))))))
  (insert 0 (insert 1 (insert 3 (insert 2 a!1)))))))

. Возможно, вам потребуется получить последнюю версию Z3 из их ночных сборок, как поддержку рекурсивного-functions является довольно новым, и поэтому последний официальный выпуск (4.6.0) может или не может работать с этим.(Вы можете получить ночные сборки от https://github.com/Z3Prover/bin/tree/master/nightly.)

...