從Z3Py模型中檢索陣列

Question

我知道有一個similar question for Z3 C++ API，但我找不到Z3Py的相應信息。我試圖從Z3找到的模型中檢索數組，以便我可以使用索引訪問數組的值。舉例來說，如果我有

>>> b = Array('b', IntSort(), BitVecSort(8)) 
>>> s = Solver() 
>>> s.add(b[0] == 0) 
>>> s.check() 
sat 

話，我想這樣做

>>> s.model()[b][0] 
0 

，但我目前得到：

>>> s.model()[b][0] 
Traceback (most recent call last): 
    File "<stdin>", line 1, in <module> 
TypeError: 'FuncInterp' object does not support indexing 

從C++的回答來看，它似乎像我不得不使用我從模型中得到的一些值來聲明一個新函數，但是我不能很好地將它適用於Z3Py。

Answer 1

通過構建對關聯數組模型函數的調用，可以讓模型評估（eval(...)）特定點處的數組。下面是一個例子：

b = Array('b', IntSort(), BitVecSort(8)) 
s = Solver() 
s.add(b[0] == 21) 
s.add(b[1] == 47) 
s.check() 

m = s.model() 
print(m[b]) 

print(m.eval(b[0])) 
print(m.eval(b[1])) 

產生

[1 -> 47, 0 -> 21, else -> 47] 
21 
47