PolySAT: Word-level Bit-vector Reasoning in Z3
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916279516921856 |
|---|---|
| author | Rath, Jakob Eisenhofer, Clemens Kaufmann, Daniela Bjørner, Nikolaj Kovács, Laura |
| author_facet | Rath, Jakob Eisenhofer, Clemens Kaufmann, Daniela Bjørner, Nikolaj Kovács, Laura |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_04696 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | PolySAT: Word-level Bit-vector Reasoning in Z3 Rath, Jakob Eisenhofer, Clemens Kaufmann, Daniela Bjørner, Nikolaj Kovács, Laura Logic in Computer Science 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. |
| title | PolySAT: Word-level Bit-vector Reasoning in Z3 |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2406.04696 |