z3 - z3 中的 DPLL(T) 式 SMT 求解是否记录了线性实数运算？

Question

我正在尝试设计方法来提高 z3 在我的问题上的性能。我知道 CAV'06论文和技术报告。z3 v4.3.1 的相关部分是否与这些文档中描述的内容不同，如果不同，有何不同？此外，z3 中默认遵循的策略是什么，用于决定何时检查线性实数算术中与已决定（和传播）命题文字相对应的理论原子的一致性？

Answer 1

线性算术在src/smt/theory_arith*. 见http://z3.codeplex.com/SourceControl/latest#src/smt/theory_arith_core.h

关于您指出的论文，这些想法已用于实施。然而，实际代码包含许多线性整数、非线性算术和证明生成的扩展。如果你只关心线性实数算术，你应该只关注theory_arith.h, theory_arith_core.h。该文件theory_arith_aux.h还包含有用的功能。