z3 - z3 数值约束：哪个更好？

Question

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

(assert (=> (and (<= 0.0009765625 value) (< value 0.001953125)) (= new-value 0.0009765625)))

                                     OR

(assert (=> (and (<= (/1.0 1024.0) value) (< value (/1.0 512.0))) (= new-value (/1.0 1024.0))))

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

Answer 1

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