Z3 中是否有测试数字是否有理数的函数？

Question

在 Z3 中处理实数时，有理数会自动显示为分数。这意味着Z3有一个机制来测试一个数字是否有理（以决定如何描述它），对吧？

是否可以通过 Z3 中的具体函数访问此机制？我知道自己可以编写这样的函数，但如果 Z3 本身已经可以做到这一点，那就没有必要了。谢谢！

Answer 1

API 中有两个函数可以帮助您：

以上在Python API中，但你可以在API的其他API中找到类似的功能来自C/C++/Java等。如果您仅使用 SMTLib 接口，我认为这些是不可用的。

请注意，如果基于静态检查并且只有当您具有完全确定的值时，这些才会正常工作。例如：

>>> is_rational_value(Real('x'))
False

当然 x 稍后可以绑定到一个合理的值，具体取决于您添加的所有其他约束。即：

>>> x = Real('x')
>>> is_rational_value(x)
False
>>> s = Solver()
>>> s.add(x == 1)
>>> s.check()
sat
>>> m = s.model()
>>> m[x]
1
>>> is_rational_value(m[x])
True
>>> is_algebraic_value(m[x])
False

将此与以下内容进行比较：

>>> y = Real('y')
>>> s = Solver()
>>> s.add(y * y == 2)
>>> s.check()
sat
>>> m = s.model()
>>> m[y]
-1.4142135623?
>>> is_rational_value(m[y])
False
>>> is_algebraic_value(m[y])
True

Z3 中是否有测试数字是否有理数的函数？

Is there a function to test if a number is rational in Z3?

z3