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