CODEWITHSUNDEEP
pythonz3bitvector
SuperLative
SuperLative

Reputation: 13

(Z3Py) Concat, quantifiers and bit-vectors

Is it possible to make use of quantifiers with bit-vectors and concatenations? To illustrate, running the following code in the newest Z3:

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

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

produces the following error:

BitVecRef instance has no attribute '__len__'

I have tried adding a simple __len__ method in BitVecRef but further problems arose.

Without the Concat, the code works as expected. For example:

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

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

outputs the correct: proved

Upvotes: 1

Views: 1724

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Your example defines the value b as shorthand for a concatenation. It gets passed as the bound variable to the quantifier Exists(b, a == b). Quantifiers expect a list of basic constants, such as a, b, c below, but not compound expressions, such as d. Below is a version of your puzzle that gets processed:

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

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

Upvotes: 3

Related Questions