(Z3Py) Конкат, квантификаторы и битовые векторы

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__'

Я попытался добавить простой __len__ метод в BitVecRef но возникли дальнейшие проблемы.

Без 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)))