О теории массивов в Z3

Я хочу знать, могу ли я заставить Z3 «запомнить» обновление массива.

Например, следующий ввод допустим:

(declare-const x Int)
(declare-const a1 (Array Int Int))
(assert  (= (select (store a1 x 2) x) 2))
(assert (not (= (select a1 x) 2)))
(check-sat)

«Хранилище» в первом утверждении не влияет на второе утверждение. Могу ли я сделать операцию сохранения в массиве, что приведет к вечным изменениям в массиве? Я имею в виду, что если я использую хранилище для массива, то массив изменяется навсегда. например, если после того, как я использую «(сохранить a1 x 2)», то каждый раз (выберите a1 x) равно 2. Кто-нибудь знает это? Спасибо.


arrays z3
person Student Popper    schedule 21.09.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Выражение (= (select (store a1 x 2) x) 2) эквивалентно true. Это бессодержательное утверждение, поскольку одна из аксиом теории массивов — forall a,i,v: select(store(a,i,v), i) = v. Таким образом, это выражение является лишь экземпляром аксиомы (встроенной в Z3), и по этой причине оно избыточно.

Возможно, вы намеревались утверждать (assert (= (select a1 x) 2)). Это утверждение говорит, что значение массива в позиции x равно 2. То есть любое решение, созданное Z3, должно будет присвоить 2 этой позиции массива a1.

Обратите внимание, что в Z3 нет понятия «до» и «после» утверждения или побочных эффектов. Например, выражение a = a + 1 эквивалентно false в Z3. Один общий метод, используемый для кодирования назначений языка программирования в Z3, использует несколько переменных для каждой переменной программы. Одна переменная для каждого «местоположения программы». Например, кодовый блок a = a + 1; b = 2*a; a = b + 1 кодируется как a_1 = a_0 + 1 and b_1 = 2*a_0 and a_2 = b_1 + 1. Следующая статья содержит больше примеров/деталей: http://dl.acm.org/citation.cfm?id=1995394

Если вы собираетесь кодировать обновление массива, используемое в программе, у вас должен быть один массив a1, представляющий массив до обновления, и один массив a2, представляющий массив после обновления. То есть пишем: (assert (= a2 (store a1 x 2))), а последнее утверждение заменяем на (assert (not (= (select a2 x) 2)))

person Leonardo de Moura    schedule 21.09.2012