SMT解空间度量工具包

多面体预处理加速

针对SMT(LA)公式的解空间度量任务，通过新型多面体预处理技术显著提升体积计算与格点计数的效率。

Ge, Cunjing

Frontiers of Computer Science 2025

技术优势

预处理显著减少求解负担

论文提出一系列新型多面体预处理技术，在体积计算和格点计数前对公式进行简化，从而提升后续计算的效率。

应用实例上效果尤其明显

实验结果表明，这些预处理技术在来源于实际应用的实例上更加有效，说明它们针对现实约束结构做了优化。

应用场景

• 静态分析工具：静态分析中需要度量代码可达路径或参数空间体积，SharpSMT直接提供解空间体积计算与格点计数，替代手写专用程序。
• 软件测试：测试数据生成时可用SharpSMT量化输入域的体积或样本点数量，帮助评估测试覆盖率和生成均匀分布的测试用例。
• 约束求解：约束求解器常用于计数解的数量，SharpSMT集成格点计数近似算法，能在可接受精度下快速估计线性算术约束的解个数。
• 自动推理：在自动推理中，对逻辑公式的解空间进行度量可用于概率推理或模型计数，SharpSMT提供可扩展工具支持。