在 Z3 求解器中，有没有一种方法可以用算术运算支持以定点符号表示数字答案

【问题标题】：In Z3 solver , is there a way to represent numbers in fixed point notation with arithmetic operations support在 Z3 求解器中，有没有一种方法可以用算术运算支持以定点符号表示数字
【发布时间】：2020-06-24 15:35:38
【问题描述】：

在 Z3 求解器中，我想使用定点表示法表示数字并使用舍入执行算术运算。

示例：假设 X、Y 和 Z 代表定点数类型，

X[4,3]  Total 4 digits number with 3 digits after the decimal.
Y[4,2]   
Z[4,1]
Assign fixed point numbers to X, Y
X = 1.234  ( here there are total 4 digits & decimal digits are 3 )
Y = 45.67
Perform the Fixed point numbers Arithmetic operation

Z = X * Y（结果 56.35678 需要四舍五入并赋值给 Z 即 56.36）

我了解，Z3 支持数字的浮点理论，但不支持具有算术运算的数字的定点理论！有没有计划支持数字的不动点理论？如果没有，是否有任何方法可以使用 Z3 求解器中的任何现有理论和示例来实现这一点？

提前感谢您的帮助！

我从 Z3 论坛获得了有关数字定点理论的信息。请在下面的链接中找到信息

An SMT Theory of Fixed-Point Arithmetic

它通过 PySMT 提供一个 API 来处理定点数：

SOAR Lab - PySMT - Fixed Points

【问题讨论】：

这听起来像是对特定技术的支持请求。您可能希望将此支持问题直接发布到他们的支持团队/github 页面/等...
是的，谢谢，我已经在Z3论坛github.com/Z3Prover/z3/issues/4540发帖提问了。

标签： math z3 solver fixed-point

【解决方案1】：

您可以随时在https://github.com/Z3Prover/z3/issues“请求”此类功能

但 SMT 求解器通常遵循 SMTLib 倡议；因此，除非 SMTLib 为定点数提出“逻辑”，否则不太可能实现。见这里：http://smtlib.cs.uiowa.edu/

有一个 SMTLib 论坛，您可以在其中发布您的请求并寻求指导：https://groups.google.com/forum/#!forum/smt-lib

但是，在当前的功能范围内，这些数字不支持开箱即用。鉴于此，我会尝试在 SMT 求解器“外部”建模并使用常规整数库，但其细节取决于您想要投资多少以及您想要处理什么样的问题。（例如，您可以用两个整数表示定点数，一个用于“整数”部分，一个用于“分数”部分，然后自己完成所有算术和舍入等。这可能需要很多工作，但可能是您最好的选择，因为目前没有直接支持这些数字。）

【讨论】：

感谢您提供信息，这很有帮助。我在 Z3 论坛 github.com/Z3Prover/z3/issues/4540 上发布了问题。
我看到了那个帖子，里面提到的论文看起来很有趣。请用您的发现更新您的问题，并参考该论文。这将有助于本论坛的更多读者更轻松地找到该信息。