Solving bitvectors with MCSAT: explanations from bits and pieces (long version)

TL;DR

This paper introduces a decision procedure for fixed-sized bitvectors within the MCSAT framework, utilizing BDDs and specialized interpolations, implemented in Yices 2, with experimental validation.

Contribution

It develops a novel decision procedure for bitvectors using BDDs and interpolation in MCSAT, extending SMT solving capabilities beyond traditional methods.

Findings

Effective conflict explanation via word-level interpolation

Successful implementation in Yices 2 SMT solver

Competitive experimental results demonstrating practicality

Abstract

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.