z3 - 我们可以通过分子/分母表示来限制 z3 实项的值吗？

Question

在 z3 中，实数项的值由两个整数的除法表示:分子和分母。我经常找到具有非常大的分子和分母的真实值(作为我的 z3 问题的解决方案)，如下所示:

29176049827299110215982818410792217459/804618286561124267999713087296957062500-556895298158182412321541102649719164259083/4272120792496289300944476637003193523343750

在具有较小分子和分母的替代解决方案(对同一问题)的情况下，这些实变量通常有其他分配。我只是想知道我是否可以限制分子和分母(例如，关于位数)。实际上，我正在为此目的寻找 z3 功能。预先感谢您的回答。

Answer 1

Z3 中的实数通常不表示为分子与分母的比值。这会将 Z3 限制为有理数。对于 Z3 返回无理数的示例，请尝试:

(declare-const x Real)
(assert (= (* x x) 2.0))
(check-sat)
(get-model)

话虽如此，对于许多具体问题，Z3 确实会以实数的有理表示形式做出回应。我认为当您的问题有可能重新归一化并以整数形式解决时，这种情况经常发生。在这些情况下，您可以尝试使用类似于 this question 中的答案的技术强制您的问题在有理数中得到解决。 .然后，您可以断言您的号码有一个分子 p < p_max对于一些常量 p_max .