Meilleure manipulation de la matrice API

Question

L'initialisation et la manipulation de la baie SMT-LIB 2.0 sont un peu lourdes. Comme le code suivant l'explique, http://rise4fun.com/Z3/kxmrd.

Existe-t-il un moyen élégant d'initialiser ou de manipuler des tableaux, en utilisant Python/C/C++ /. Net API que SMT-LIB 2.0?

Answer 1

Vous pouvez utiliser des constructions Python réguliers tels que for i in range(n) pour obtenir ce que vous voulez:

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]) 

Run en ligne here.

Ce serait bien si vous pouviez écrire quelque chose comme s.add(a == xs) ou s.add(a.startsWith(xs)), mais je ne sais pas si c'est possible.