arith.nl.rounds 和 final-checks 之间的关系答案

【问题标题】：Relation between arith.nl.rounds and final-checksarith.nl.rounds 和 final-checks 之间的关系
【发布时间】：2015-01-22 14:22:12
【问题描述】：

配置选项smt.arith.nl.rounds和统计值final-checks之间是否有关系（或者说前者的描述中提到“最终检查”只是巧合）？

我在 SMTLIB 程序上运行了 Z3 4.3.2（官方下载）和 Z3 4.4 0ab54b9e0c33 的 Windows x64 版本，在这两种情况下，final-checks 的报告数量（大约 10,000）似乎都不受我的值的影响选择smt.arith.nl.rounds（我尝试了 1、64、128、...、1024 和 4096）。

【问题讨论】：

标签： configuration z3 usage-statistics

【解决方案1】：

所有理论都有最终检查，但smt.arith.nl.rounds 仅适用于非线性算术求解器（旧的；不是 NLSAT）。可能有很多最终检查，其中没有任何涉及任何非线性算术，或者他们使用其他方法来解决这些部分。

【讨论】：