z3py: как представить массив целых чисел или символов в z3py

Question

Я новичок в z3py и SMT, и я не нашел хорошего учебника о z3py.

Вот моя постановка задачи:

Учитывая входной целочисленный массив I = [1,2,3,4,5], а выходной массив целых чисел O = [1,2,4,5].

Я хочу, чтобы вывести к для оператора Delete, которая удаляет элемент в позиции к в массиве, где

Delete(I,O) =  (ForAll 0<=x<k, O[x] = I[x]) and (ForAll k<=x<length(I)-1, O[x] = I[x+1]) is true 

Должен ли я использовать массив или IntVector, или что-нибудь еще, чтобы представить выходной массив/вход ?

Edit:

Мой код выглядит следующим образом:

from z3 import * 

k=Int('k') 
s=Solver() 

x = Int('x') 
y = Int('y') 

s.add(k >= 0) 
s.add(k < 4)  
s.add(x >= 0) 
s.add(x < k) 
s.add(y >= k) 
s.add(y < 4) 

I = Array('I',IntSort(),IntSort()) 
O = Array('O',IntSort(),IntSort()) 
Store(I, 0, 1) 
Store(I, 1, 2) 
Store(I, 2, 3) 
Store(I, 3, 4) 
Store(I, 4, 5) 

Store(O, 0, 1) 
Store(O, 1, 2) 
Store(O, 2, 4) 
Store(O, 3, 5) 

s.add(And(ForAll(x,Select(O,x) == Select(I,x)),ForAll(y,Select(O,y) == Select(I,y+1)))) 
print s.check() 
print s.model() 

возвращает

sat 
[I = [2 -> 2, else -> 2], 
O = [2 -> 2, else -> 2], 
y = 1, 
k = 1, 
x = 0, 
elem!0 = 2, 
elem!1 = 2, 
k!4 = [2 -> 2, else -> 2]] 

Я не понимаю, что я, О, элем 0, элем! 1 и k! 4, и это явно не то, что я ожидал.

Answer 1

Отказ от ответственности: Я почти никогда не использовал Z3py раньше, но я использовал Z3 совсем немного.

У меня такое ощущение, что вы несколько новичок в кодировании логических проблем - может быть? В вашей проблеме происходит несколько (странных) вещей.

1. Вы ставите ограничения на x и y, но вы на самом деле никогда не использовать их - вместо этого, вы связываете другуюx и y в своих количественных утверждений. Последние два могут иметь одинаковые имена, но они полностью не связаны с x и y, которые вы ограничили (поскольку каждый forall связывает свою собственную переменную, вы также можете использовать x в обоих). Следовательно, ваши квантифицированные x и y располагаются на всем Int, тогда как вы, вероятно, хотите ограничить их интервалом [0..4). Для этого используйте значение внутри forall.

2. Согласно документации, Store(a, i, v)возвращает новый массив a', который идентичен a, за исключением того, что x[i] == v. То есть вам нужно позвонить I = Store(I, 0, 1) и т. Д., Чтобы наконец получить массив I, в котором хранятся ваши нужные значения.

3. Поскольку вы этого не делаете, Z3 может выбрать модель, которая удовлетворяет вашим ограничениям. Как вы можете видеть на выходе, модель для I составляет [2 -> 2, else -> 2], в которой говорится, что I[2] == 2 и I[i] == 2 для любых i != 2. Я не знаю, почему Z3 выбрал эту конкретную модель, но она (вместе с моделью для O) удовлетворяет вашим требованиям.

4. Возможно, вы проигнорируете elem!0, elem!1 и k!4, они являются внутренне сгенерированными символами.

5. Вот уменьшенная версия вашего примера, не проверяет:

   x = Int('x')   
   I = Array('O',IntSort(),IntSort()) 
   O = Array('O',IntSort(),IntSort()) 
   
   I = Store(I, 0, 1) 
   I = Store(I, 1, 2) 
   
   s.add(
       And(
       ForAll(x, Select(O,x) == Select(I,x)), 
       ForAll(x, Select(O,x) == Select(I,x+1)))) 
   
   print s.check() # UNSAT 
   

   Причина, почему это невыполнимо, что I[0] == 1 && I[1] == 2, что противоречит вашему foralls. Если вы создаете экземпляр как квантифицированный x с 0, вы получаете O[0] == I[0] && O[0] == I[1] - ограничение, которое не может быть выполнено, т. Е. Нет модели для O, которая ее удовлетворяет.

Редактировать (обратиться комментарий):

Если вы озадачены, почему, учитывая сниппет, такие как

I = Array('O',IntSort(),IntSort()) 
I = Store(I, 0, 1) 
I = Store(I, 1, 2) 
# print(I) 
s.check() 
s.model() 

Z3 сообщает sat и возвращает модель, в которой I = [], затем вспомните, что каждый Store(...) возвращает новое выражение Z3, которое представляет операцию хранилища, каждый из которых, в свою очередь, возвращает новый массив (который равен начальному, m удалять обновление). Как показывает print, конечным значением I является выражение Store(Store(I, 0, 1), 1, 2). Поэтому достаточно, чтобы I был пустым массивом, то есть I - обновления (Store s) будут давать свежий массив (думаю, и I2 в этом случае), но поскольку они безымянные, они не будут (или по крайней мере, не обязательно) отображаться в модели.

Если вы хотите явно увидеть «окончательные» значения вашего массива в модели, вы можете добиться этого, давая имя массива, который создается последним Store, например

I = Array('I',IntSort(),IntSort()) 
I = Store(I, 0, 1) 
I = Store(I, 1, 2) 

II = Array('II',IntSort(),IntSort()) 
s.add(I == II) 

s.check() 
s.model() # includes II = [1 -> 2, 0 -> 1, else -> 3] 

Answer 2

Это правильный ответ на мой вопрос:

from z3 import * 

x = Int('x') 
y = Int('y') 
k = Int('k') 

s = Solver() 

I = Array('I',IntSort(),IntSort()) 
O = Array('O',IntSort(),IntSort()) 
I = Store(I, 0, 1) 
I = Store(I, 1, 2) 
I = Store(I, 2, 3) 
I = Store(I, 3, 4) 
I = Store(I, 4, 5) 

O = Store(O, 0, 1) 
O = Store(O, 1, 2) 
O = Store(O, 2, 4) 
O = Store(O, 3, 5) 

s.add(k >= 0) 
s.add(k < 4) 
s.add(And(ForAll([x],Implies(And(x>=0,x<k),Select(O,x) == Select(I,x))),ForAll([y],Implies(And(y>=k,y<4),Select(O,y) == Select(I,y+1))))) 
print s.check() 
if s.check() == z3.sat: 
    print s.model() 

ответ

sat 
[I = [2 -> 2, else -> 2], 
k = 2, 
O = [2 -> 2, else -> 2], 
k!17 = [2 -> 2, else -> 2]]