We present a decision procedure for the theory of fixed-sized bitvectors in the MCSAT framework. MCSAT is an alternative to CDCL(T) for SMT solving and can be seen as an extension of CDCL to domains other than the Booleans. Our procedure uses BDDs to record and update the sets of feasible values of bitvector variables. For explaining conflicts and propagations, we develop specialized word-level interpolation for two common fragments of the theory. For full generality, explaining conflicts outside of the covered fragments resorts to local bitblasting. The approach is implemented in the Yices 2 SMT solver and we present experimental results.
CITATION STYLE
Graham-Lengrand, S., Jovanović, D., & Dutertre, B. (2020). Solving Bitvectors with MCSAT: Explanations from Bits and Pieces. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12166 LNAI, pp. 103–121). Springer. https://doi.org/10.1007/978-3-030-51074-9_7
Mendeley helps you to discover research relevant for your work.