Bitvectors

SMTLIB2 standard The Theory of fixed sized bit-vectors

Modern CPUs and main-stream programming languages use arithmetic over fixed-size bit-vectors. The theory of bit-vectors allows modeling the precise semantics of unsigned and of signed two-complements arithmetic. There are a large number of supported functions and relations over bit-vectors. They are summarized on Z3's documentation link. We will not try to give a comprehensive overview here, but touch on some of the main features.

In contrast to programming languages, such as C, C++, C#, Java, there is no distinction between signed and unsigned bit-vectors as numbers. Instead, the theory of bit-vectors provides special signed versions of arithmetical operations where it makes a difference whether the bit-vector is treated as signed or unsigned.

Z3 supports Bitvectors of arbitrary size. (_ BitVec n) is the sort of bitvectors whose length is n. Bitvector literals may be defined using binary, decimal and hexadecimal notation. In the binary and hexadecimal cases, the bitvector size is inferred from the number of characters. For example, the bitvector literal #b010 in binary format is a bitvector of size 3, and the bitvector literal #x0a0 in hexadecimal format is a bitvector of size 12. The size must be specified for bitvector literals in decimal format. For example, (_ bv10 32) is a bitvector of size 32 that represents the numeral 10. By default, Z3 display bitvectors in hexadecimal format if the bitvector size is a multiple of 4, and in binary otherwise. The command (set-option pp.bv-literals false) can be used to force Z3 to display bitvector literals in decimal format.

Basic Bitvector Arithmetic

Bitwise Operations

We can prove a bitwise version of deMorgan's law

Let us illustrate a simple property of bit-wise arithmetic. There is a fast way to check that fixed size numbers are powers of two. It turns out that a bit-vector x is a power of two or zero if and only if x & (x - 1) is zero, where & represents the bitwise and. We check this for four bits below.

Word operations

Predicates over Bitvectors

Signed comparison, such as bvsle, takes the sign bit of bitvectors into account for comparison, while unsigned comparison treats the bitvector as unsigned (treats the bitvector as a natural number).

BitVectors and Integers

You can mix integers and bit-vectors. Note that reasoning in the combination has significant overhead so you will be better off if you can model your problems entirely only using bit-vectors or entirely using integers (reals). In the conversion function from bit-vectors to integers, bit-vectors correspond to non-negative integers. For the conversion function that maps integers to bit-vectors you have to supply the bit-width $n$. Then the bit-vector corresponding to the integer argument represents the unsigned number obtained by taking the modulus with respect to $2^n$.

Pop-count

We claim that the following program computes the number of bits that are set in $v$:

int popcount32 (unsigned int v) { 
  v = v - ((v >> 1) & 0x55555555); 
  v = (v & 0x33333333) + ((v >> 2) & 0x33333333); 
  v = ((v + (v >> 4) & 0xF0F0F0F) * 0x1010101) >> 24; 
  return(v); 
} 

To check this claim, let us first reformulate popcount32 using definitions in SMTLIB2

The brute force way to compute a popcount is to add all bits together. We can define the brute-force method for 4, 8 and 16 bits before writing down the 32 bit version.