При использовании массивов SMTLIB я заметил разницу между пониманием теории Z3 и моим.Я использую теорию массива SMTLIB [0], которую можно найти на официальном сайте [1].
Я думаю, что мою проблему лучше всего проиллюстрировать простым примером.
(store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0)
(store (store ((as const (Array Int Int)) 0) 0 1) 1 2)
первый массив должен возвращать 2 по индексу 1 и 0 для всех других индексов, второй должен возвращать 1 по индексу 0, 2 по индексу 1 и 0 для всех остальных индексов.Вызов select по индексу 0, кажется, подтверждает это:
(assert
(=
(select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0)
0
)
)
(assert
(=
1
(select (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0)
)
)
Z3 возвращает sat для обоих.
(assert
(=
(select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0)
(select (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0)
)
)
Как и ожидалось, Z3 (в случае, если это важно, яиспользуя версию 3.2 на linux-amd64) в этом случае отвечает unsat.Далее, давайте сравним эти два массива:
(assert
(=
(store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0)
(store (store ((as const (Array Int Int)) 0) 0 1) 1 2)
)
)
Z3 сообщает мне sat, что я интерпретирую как «эти два массива сравниваются равными».Тем не менее, я ожидал бы, что эти массивы не будут сравниваться.Я основываю это на теории массива SMTLIB, которая гласит:
- (forall ((a (Array s1 s2)) (b (Array s1 s2)))
(=> (forall ((i s1)) (= (select a i) (select b i)))
(= a b)))
Итак, на простом английском языке это будет означать что-то вроде «Два массива будут сравниваться равными, если и только если они равны для всех индексов».Кто-нибудь может мне это объяснить?Я что-то упускаю или неправильно понимаю теорию?Буду признателен за любые мысли по этому вопросу.
С наилучшими пожеланиями, Леон
[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 [1] http://smtlib.org