我们可以通过分子/分母表示来限制 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。