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

  • M. Oliver Möller
  • Harald Ruess

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.
Published
1999-01-18
How to Cite
Möller, M. O., & Ruess, H. (1999). Solving Bit-Vector Equations of Fixed and Non-Fixed Size. BRICS Report Series, 6(18). https://doi.org/10.7146/brics.v6i18.20075