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 

這裏是關於陣列理論http://rise4fun.com/Z3Py/2CAn使用Select和Store另一個例子：

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」關鍵字在網站上搜索以獲取更多信息。