Boolean Vectors

[SSoelvsten]

By placing BDDs (or ZDDs) in a vector of length b we can represent a b-bit binary integer. These can be used to implement the logic for boolean vectors in an SMT solver. The following description is based off the implementation for unsigned boolean vectors in the BDD library BuDDy; it would also be of interest to have signed boolean vectors with two's complement.

We can allow the user to choose whether to use BDDs or ZDDs to represent each bit by templating the bvec class and all the functions. If they choose to use ZDDs, then we do need to have the domain defined to make bitwise negation make any sense. It might make sense to start with BDDs only and then template it later.

Constructors

We want to be able to construct a bvec in a few ways

• [ ] bvec_true(), and bvec_false() for the all-1 and all-0 vectors.
• [ ] bvec_const(i) to construct a bvec that represents the constant integer i
• [ ] bvec_vars(vs) to construct a bvec where the ith bit is the ith variable in vs. Alternatively, vs can be a function index -> variable label.

Operators

The following functions return a new bvec.

• [ ] Bit-wise operations such as bit-wise AND, OR, and XOR are quite easy to implement, since one merely needs to apply that operator per index.

  bvec_and(x,y) (x & y), bvec_or(x,y) (x | y), bvec_xor(x,y) (x ^ y), bvec_not(x) (~ y)

• [ ] Much more intersting are arithmetic operations, since the output bits are dependant on multiple input bits.

  • With Decision Diagrams on either side:

    bvec_add(x,y) (x + y), bvec_sub(x,y) (x - y), bvec_mul(x,y) (x * y), bvec_div(x,y) (x / y), bvec_shr(x,y) (x >> y), bvec_shl(x,y) (x << y)

  • Where the latter value i is a fixed b-bit number:

    bvec_mulfixed(x,i) (x * i and i * x), bvec_divfixed(x,i) (x / i), bvec_shrfixed(x,i) (x >> i), bvec_shlfixed(x,i) (x << i)

• [ ] We would also want some extra functions:

  • bvec_truncate(x,b) or bdd_coerce(x,b) to change x to be b bits. If it is made longer, then it is padded with extra zeros.

Comparators

The following functions return a single decision diagram (not a vector of decision diagrams) which contains the desired result of a comparison of two bvecs. The type is either a bdd or zdd depending on what was the templated value underneath.

• [ ] bvec_eq(x,y) and bvec_neq(x,y)
• [ ] bvec_lt(x,y), bvec_le(x,y), bvec_gt(x,y), and bvec_ge(x,y).