问线性实算法的DPLL(T)-style SMT解在z3中有记录吗？
EN

Stack Overflow用户

提问于 2014-01-17 22:47:59

回答 1查看 219关注 0票数 1

我正在设法改进z3在我的问题上的性能。我知道CAV'06 纸和技术报告。z3 v4.3.1的相关部分是否与这些文档中所描述的不同，如果是的话，在哪些方面？另外，在z3中默认采用什么策略来决定何时检查线性实算法的一致性，以及对应于已确定的(和传播的)命题的理论原子？

回答已采纳

发布于 2014-01-17 23:29:13

在src/smt/theory_arith*的文件中实现了线性算法。请参阅core.h

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

票数 2

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/21197400

复制

相似问题

问线性实算法的DPLL(T)-style SMT解在z3中有记录吗？EN