최상의 배열 조작 API

Question

SMT-LIB 2.0 어레이 초기화 및 조작은 약간 번잡합니다. 다음 코드는 http://rise4fun.com/Z3/kxmrd에 대해 설명합니다.

SMT-LIB 2.0보다 Python/C/C++ /. Net API를 사용하여 배열을 초기화하거나 조작하는 멋진 방법이 있습니까?

Answer 1

당신은 당신이 원하는 것을 달성하기 위해 같은 for i in range(n) 같은 일반 파이썬 구조를 사용할 수 있습니다 온라인 here

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

실행을.

s.add(a == xs) 또는 s.add(a.startsWith(xs))과 같은 것을 쓸 수 있으면 좋겠지 만 그럴 수 있는지는 알 수 없습니다.