论文标题
用MCSAT求解BitVector：零碎的解释（长版）
Solving bitvectors with MCSAT: explanations from bits and pieces (long version)
论文作者
论文摘要
我们为MCSAT框架中固定尺寸的比特向量理论提供了决策程序。 MCSAT是SMT求解的CDCL（t）的替代方法，可以看作是CDCL向布尔值以外的其他域的扩展。我们的过程使用BDD来记录和更新BitVector变量的可行值集。为了解释冲突和传播，我们为该理论的两个共同片段开发了专门的单词级插值。为了充分的一般性，解释了在覆盖片段之外的冲突，以供局部替代品。该方法是在YICES 2 SMT求解器中实现的，我们提出了实验结果。
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.
