如何在z3的Python API中實現位向量數組

Question

我是z3py的新手，正在通過the Z3 API in Python，但無法弄清楚如何定義一個位向量數組。

我想是這樣的：

DOT__mem[16] = BitVec('DOT__mem[16]', 8) 

但是這句法沒有工作，即使是在教程中實踐面板上。

有人可以幫助正確的語法嗎？

Answer 1

以下示例說明如何創建Z3位向量的「向量」（Python列表）。 該示例也可在線獲取rise4fun。

# Create a Bitvector of size 8 
a = BitVec('a', 8) 

# Create a "vector" (list) with 16 Bit-vectors of size 8 
DomVect = [ BitVec('DomVect_%s' % i, 8) for i in range(16) ] 
print DomVect 
print DomVect[15] 

def BitVecVector(prefix, sz, N): 
    """Create a vector with N Bit-Vectors of size sz""" 
    return [ BitVec('%s__%s' % (prefix, i), sz) for i in range(N) ] 

# The function BitVecVector is similar to the functions IntVector and RealVector in Z3Py. 

# Create a vector with 32 Bit-vectors of size 8. 
print BitVecVector("A", 8, 32)