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.

翻译：PolySAT是一种支持对具有大规模位向量运算的多项式算术进行比特精确SMT推理的字级决策过程。PolySAT演算通过两个关键组件扩展了冲突驱动子句学习模理论：(i) 等式图的位向量插件，以及 (ii) 支持非线性多项式的位向量算术理论求解器。PolySAT实现了专用过程，用于从多项式不等式中提取位向量区间。为了进行冲突分析与消解，PolySAT配备了基于非线性位向量算术的按需引理生成机制。PolySAT已集成至SMT求解器Z3中，在模型检测和智能合约验证等领域具有潜在应用价值，这些领域中针对乘法器/除法器的比特爆破技术难以扩展。