Z3Python: пример массива?

Question

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

Пожалуйста, может ли кто-нибудь привести примеры кода?

спасибо!

Answer 1

Вот пример, показывающий объявления массива и доступа к пунктам по индексам http://rise4fun.com/Z3Py/7jAj:

x = Int('x') 
a = Array('a', IntSort(), BoolSort()) 
b = Array('b', IntSort(), BoolSort()) 
c = Array('c', BoolSort(), BoolSort()) 

e = ForAll(x, Or(Not(a[x]), c[b[x]])) 
print e 

solver = Solver() 
solver.add(e) 
c = solver.check() 
print c 

Вот еще один пример использования Select и Store по теории массива http://rise4fun.com/Z3Py/2CAn:

x = Int('x') 
y = Int('y') 
a = Array('a', IntSort(), IntSort()) 

s = Solver() 
s.add(Select(a, x) == x, Store(a, x, y) == a) 
print s.check() 
print s.model() 

Это говорит, есть несколько примеров массивов, плавающих вокруг StackOverflow. Вы можете попробовать выполнить поиск на сайте с использованием ключевого слова «z3py array» для получения дополнительной информации.