Лучший манипулятор массива 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)), но я не знаю, возможно ли это.