Я ищу некоторые примеры кода, использующие теорию массивов в Z3 python, но не могу их найти.
пожалуйста, может ли кто-нибудь привести несколько примеров кода?
Благодарность!
Я ищу некоторые примеры кода, использующие теорию массивов в Z3 python, но не могу их найти.
пожалуйста, может ли кто-нибудь привести несколько примеров кода?
Благодарность!
Вот пример, показывающий объявления массивов и доступ к элементам по индексам 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», чтобы получить дополнительную информацию.