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

Stack Overflow用户

提问于 2014-07-16 04:02:14

回答 1查看 169关注 0票数 3

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

29176049827299110215982818410792217459/804618286561124267999713087296957062500 -556895298158182412321541102649719164259083/4272120792496289300944476637003193523343750

在具有较小分子和分母的替代解决方案(对于同一问题)的情况下，通常会对这些真实变量进行其他赋值。我只是想知道我是否可以限制分子和分母(例如，关于数字的数量)。实际上，我正在寻找一个用于此目的的z3功能。提前感谢您的答复。

回答 1

Stack Overflow用户

发布于 2016-05-28 08:45:20

一般来说，Z3中的实数表示为分子和分母的比率是不正确的。这会将Z3限制为有理数。对于Z3返回无理数的示例，请尝试：

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

也就是说，对于许多特定的问题，Z3确实会用一个实数的有理表示来响应。我认为当你的问题有可能被重新标准化并以整数形式解决时，这种情况经常会发生。在这些情况下，您可以尝试使用与this question中的答案类似的技术，以合理的方式解决您的问题。然后，您可以断言您的数字具有某个常量p_max的分子p < p_max。

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/24767136

复制

相似问题

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

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

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

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

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