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

Question

在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提供了一个处理定点数的接口：

SOAR Lab - PySMT - Fixed Points

Answer 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求解器之外对此进行建模，并使用常规整型库，但具体细节取决于您想要投资多少以及您想要处理哪种类型的问题。(例如，您可以用两个整数表示定点数字，一个表示“整型”部分，另一个表示“小数”部分，并执行所有的算术和舍入等操作。你自己。这可能需要大量的工作，但考虑到目前没有对这些数字的直接支持，这可能是您最好的选择。)