Кодирование частичных карт в Z3 - PullRequest
Новая
       7

Кодирование частичных карт в Z3

0 голосов
/ 02 октября 2018

Я хотел закодировать частичные карты в Z3, с поддержкой вопроса о том, определена ли карта для определенного ключа.

Он также должен поддерживать операцию (update_map m1 m2), которая обновляет m1 с отображениямив m2 таким образом, что сопоставления m2 переопределяют сопоставления m1.

. Я попытался закодировать его, используя массивы и пользовательский тип данных option, и аксиоматически указал функцию update_map.,Тем не менее, похоже, что Z3 не может даже справиться с моей спецификацией update_map: он возвращает unknown для следующего кода: 

(declare-datatypes (T) ((option None (Some (option-value T)))))
(define-sort map (K V) (Array K (option V)))

(declare-sort V)
(declare-sort K)

(define-const empty_map (map K V)
  ((as const (Array K (option V))) None))

(define-fun get ((m (map K V)) (k K)) (option V)
  (select m k))

(define-fun put ((m (map K V)) (k K) (v V)) (map K V)
  (store m k (Some v)))

(declare-fun update_map ((map K V) (map K V)) (map K V))

(assert (forall ((m1 (map K V)) (m2 (map K V)) (k K))
    (=> (= (get m2 k) None)
        (= (get (update_map m1 m2) k) (get m1 k)))))
(assert (forall ((m1 (map K V)) (m2 (map K V)) (k K) (v V))
    (=> (= (get m2 k) (Some v))
        (= (get (update_map m1 m2) k) (Some v)))))

(check-sat)

Так что у меня есть два вопроса:

  1. Есть ли лучший способ кодировать карты, который позволил бы мне доказать факты о update_map?
  2. Может кто-нибудь поделиться какой-то интуицией о том, почему Z3 не понимает эту спецификацию?Как, в чем заключается «основная особенность», усложняющая Z3?[Я уже знаю, что кванторы считаются сложными, а логика первого порядка неразрешимой, я ищу что-то более конкретное; -)]

1 Ответ

0 голосов
/ 02 октября 2018

Z3 не может доказать выполнимость, то есть он не может построить модель для вашей формулы.К сожалению, я не знаю более точной причины этого - возможно, это ограничение возможностей поиска моделей Z3 для массивов, квантификаторов или их комбинации.

Если вы в конечном счете не заинтересованы в поиске моделей, а скорееконтрпримеры (ненасыщенные ядра), затем добавьте неудовлетворительную формулу и попробуйте получить ненасыщенные.Т.е. попробуйте что-то вроде следующего (заявление об отказе: я на самом деле не пробовал, но я уверен, что вы поняли идею): 

(assert (not
  (=
    (get
      (update_map
        (put empty_map 2 -2)
        (put empty_map 1 -1))
      -1))))

В качестве альтернативы аксиоматизирующим карт поверх массивов, естьпосмотрите на Аксиоматизация карты Дафни .Аксиомы представлены на языке буги, но перевод на Z3 обычно прост.

...