匹配位向量公式中的乘法运算
计算机科学中的逻辑
2016-12-13 v2
摘要
由硬件验证问题产生的位向量公式通常包含字级算术运算。经验证据表明，最先进的 SMT 求解器在推理含有乘法的位向量公式时效率不高。当乘法运算符在公式中被分解并以替代方式表示时，情况尤其如此。我们提出了一种预处理启发式方法，用于识别特定类型的分解乘法器，并向输入公式中添加特殊断言，以编码子项与字级乘法的等价性。预处理后的公式随后使用 SMT 求解器求解。我们使用三个 SMT 求解器进行的实验表明，我们的启发式方法使得多个公式能够被快速求解，而相同的公式在没有预处理步骤的情况下会超时。
引用
@article{arxiv.1611.10146,
title = {Matching Multiplications in Bit-Vector Formulas},
author = {Supratik Chakraborty and Ashutosh Gupta and Rahul Jain},
journal= {arXiv preprint arXiv:1611.10146},
year = {2016}
}
备注
Accepted in VMCAI 2017