z3 数值约束：哪个更好？

【问题标题】：z3 numerical constraints: which is better?z3 数值约束：哪个更好？
【发布时间】：2013-07-22 18:48:26
【问题描述】：

在使用 z3 求解整数实数约束时，以下两种编写（等效）约束的方式中哪一种更可取（在性能方面）？

(assert (=> (and (

OR

(assert (=> (and (

请注意，我们这里有 2 的幂的倒数（并且这种类型的约束有很多，涉及更小和更大的数字）。

【问题讨论】：

标签： z3

【解决方案1】：

在内部，Z3 将所有十进制数字转换为分数。在解析公式时执行此转换。无论如何，我们不希望在这两种编码之间看到任何大的性能差异。 Z3 中的解析时间通常是微不足道的（与求解时间相比）。

【讨论】：