Solving Bit-Vector Equations of Fixed and Non-Fixed Size

M. Oliver Möller
Harald Rueß

June 1999

Abstract:

This report is concerned with solving equations on fixed and non-fixed size bit-vector terms. We define an equational transformation system for solving equations on terms where all sizes of bit-vectors and extraction positions are known. This transformation system suggests a generalization for dealing with bit-vectors of unknown size and unknown extraction positions. Both solvers adhere to the principle of splitting bit-vectors only on demand, thereby making them quite effective in practice

Available as PostScript, PDF, DVI.