z3 数值约束 : which is better?

Question

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

(断言(=>(和(<= 0.0009765625 值)(< 值 0.001953125))(= 新值 0.0009765625)))

                                     OR

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

请注意，我们这里有 2 的幂的倒数(并且有许多此类约束涉及较小和较大的数字)。

Answer 1

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