Относно теорията на масивите в 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)

„Съхранението“ в първото твърдение не засяга второто твърдение. Мога ли да направя операцията за съхраняване на масива, което води до вечна промяна на масива? Искам да кажа, че ако използвам store върху масив, тогава масивът се променя завинаги. например, ако след като използвам „(съхранява 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