|
Solving Bit-Vector Equations of Fixed and Non-Fixed Size
M. Oliver Möller 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. |