Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PolySAT: Word-level Bit-vector Reasoning in Z3

Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann, Nikolaj Bjørner, Laura Kovács

TL;DR

PolySAT addresses the scalability of bit-vector reasoning for large widths by enabling word-level, non-linear reasoning integrated into Z3. It combines a bit-vector e-graph plugin with a theory solver that translates constraints into primitive forms, tracks viable values via forbidden intervals, and learns non-linear lemmas on demand, all within a CDCL(T) framework. Key contributions include interval-based viable-value tracking, incremental linearization rules, on-demand non-linear lemmas, and a selective bit-blasting fallback, validated through experiments showing complementary strengths to existing solvers. The approach enables efficient, scalable reasoning for bit-vector problems in model checking and smart-contract verification, where traditional bit-blasting struggles.

Abstract

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.

PolySAT: Word-level Bit-vector Reasoning in Z3

TL;DR

PolySAT addresses the scalability of bit-vector reasoning for large widths by enabling word-level, non-linear reasoning integrated into Z3. It combines a bit-vector e-graph plugin with a theory solver that translates constraints into primitive forms, tracks viable values via forbidden intervals, and learns non-linear lemmas on demand, all within a CDCL(T) framework. Key contributions include interval-based viable-value tracking, incremental linearization rules, on-demand non-linear lemmas, and a selective bit-blasting fallback, validated through experiments showing complementary strengths to existing solvers. The approach enables efficient, scalable reasoning for bit-vector problems in model checking and smart-contract verification, where traditional bit-blasting struggles.

Abstract

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.
Paper Structure (21 sections, 13 theorems, 23 equations, 4 figures, 1 table, 1 algorithm)

This paper contains 21 sections, 13 theorems, 23 equations, 4 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. PolySAT in a Nutshell
  4. E-graph Plugin
  5. Theory Solver
  6. Tracking Viable Values
  7. Value Propagation
  8. Viable Value Query
  9. Interval Conflict
  10. Computing Intervals
  11. Fixed Bits
  12. Linear Inequality with Equal Coefficients
  13. Linear Inequality with Different Coefficients
  14. Projecting intervals to sub-slices
  15. Non-Linear Conflicts
  16. ...and 6 more sections

Key Result

Lemma 1

In case no fixed value is known for the other sub-slice, it is possible to learn an interval as long as $\mathopen[{l};{h}\mathclose[$ is big enough. where $l_y \coloneqq \lceil \frac{l}{2^v} \rceil \operatorname{mod} 2^v$, $h_y \coloneqq \lfloor \frac{h}{2^v} \rfloor$, $l_z \coloneqq l \operatorname{mod} 2^v$, and $h_z \coloneqq h \operatorname{mod} 2^v$.

Figures (4)

  • Figure 1: PolySAT Integration
  • Figure 2: Primitive Constraints
  • Figure 3: Derived Constraints ($w = \lvert p \rvert = \lvert q \rvert$)
  • Figure 4: Example for extracting intervals from an inequality constraint $px+q \leq_\mathsf{u} rx+s$ with different variable coefficients. The blue dashed line plots $\widehat{p}x+\widehat{q}$, and the red continuous line is $\widehat{r}x+\widehat{s}$.

Theorems & Definitions (15)

  • Example 1
  • Lemma 1: General Intervals
  • Lemma 2: Specific Intervals
  • Example 2
  • Lemma 3: Saturation Modulo Multiplication Inequalities
  • Lemma 4: Overflow Saturation
  • Lemma 5: Saturation Modulo Equalities
  • Lemma 6: Parity Saturation
  • Lemma 7: Incremental Linearization
  • Lemma 8: $x \coloneqq p \mathbin{\&} q$
  • ...and 5 more