An MCSAT treatment of Bit-Vectors (preliminary report)

We propose a general scheme for treating the theory of bit-vectors (BV) in the MCSAT framework, complementing the approach by Zeljic, Wintersteiger, and Rummer. MCSAT assigns values to first-order variables. In order to keep track of the set of feasible values for a given bit-vector variable, we propose the use of Binary Decision Diagram. This allows an assignment mechanism that is generic for BV. When a conflict arises, involving some of the constraints and some of the assignments made so far, MCSAT must produce an explanation for the conflict. This mechanism can be specialized according to the constraints involved in the conflict. We propose an explanation mechanism that applies when these constraints are in the core fragment of BV, based on slicing and equality reasoning. We plan to add support for more BV fragments in the future.