（Z3Py）Concat，量詞和位向量

Question

是否可以使用位向量和連接的量詞？爲了說明，在最新的運行Z3以下代碼：

a = BitVec('a', 8) 
b = Concat(BitVec('b', 4), BitVec('c', 4)) 

prove(ForAll(a, Exists(b, a == b))) 

產生以下錯誤：

BitVecRef instance has no attribute '__len__' 

我曾嘗試在BitVecRef添加一個簡單的方法__len__但進一步的問題出現了。

沒有Concat，代碼按預期工作。例如：

a = BitVec('a', 8) 
b = BitVec('b', 8) 

prove(ForAll(a, Exists(b, a == b))) 

輸出正確：proved

Answer 1

你的示例的值定義B中簡寫的級聯。 它作爲綁定變量傳遞給量詞Exists（b，a == b）。量詞期望列表的基本常量，如下面的a，b，c，但不包括複合表達式，如d。下面是你的拼圖得到處理的版本：

a = BitVec('a', 8) 
b = BitVec('b', 4) 
c = BitVec('c', 4) 
d = Concat(b, c) 

prove(ForAll(a, Exists(b, a == d)))