最佳陣列操作API

Question

SMT-LIB 2.0陣列的初始化和操作有點麻煩。如下面的代碼所解釋的，http://rise4fun.com/Z3/kxmrd。

是否有任何優雅的方式來初始化或操作數組，使用Python/C/C++/.Net API比SMT-LIB 2.0？

Answer 1

你可以使用常規的Python結構，如for i in range(n)達到你想要的東西：

s = Solver() 
a = Array('a', IntSort(), IntSort()) 
xs = [20, 23, 27, 12, 19, 31, 41, 7] 

for i in range(len(xs)): 
    s.add(Select(a, i) == xs[i]) 

a1 = Array('a1', IntSort(), IntSort()) 

s.add(a1 == Store(a, 3,9)) 

print s.check() 

m = s.model() 
for d in m.decls(): 
    print "%s = %s" % (d.name(), m[d]) 

運行它的在線here。

如果你可以寫一些像s.add(a == xs)或s.add(a.startsWith(xs))這將是很好的，但我不知道這是否可能。