Logo image
Back
Bit-Precise Reasoning with Parametric Bit-Vectors
Conference proceeding   Open access

Bit-Precise Reasoning with Parametric Bit-Vectors

Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett and Cesare Tinelli
28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, Vol.341, 4
08/07/2025
DOI: 10.4230/LIPIcs.SAT.2025.4
url
https://doi.org/10.4230/LIPIcs.SAT.2025.4View
Published (Version of record) Open Access

Abstract

The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one.
 Bit-precise Reasoning Parametric Bit-vectors Satisfiability Modulo Theories

Details

Metrics

43 Record Views
Logo image