【发布时间】:2019-02-05 08:07:02
【问题描述】:
我想构建 Z3 的复制品,我需要接受有关二进制到十进制和十进制到二进制转换算法的培训。
Z3中使用的算法据说是这样的。让我们举个例子,比如 5 * 10 ^ 4。所以首先我们将 5 转换为二进制,所以我们有 0101,我们将它设置在尾数单元的 -13 位。然后我们将 13 添加到指数以补偿我们输入它的位置 t。然后我们规范化尾数。所以现在在指数中我们有 1101 和尾数 1.01。然后它说我们需要将尾数乘以指数指定的 10 倍。所以这将是 1.01 * 10 的四倍?
但这对我来说毫无意义。我们把它归一化,然后相乘?而且算法从来没有说指数是如何实际设置的?
【问题讨论】:
-
在我看来,描述算法的语言的解释存在问题。您应该向我们展示您所指的文件。
-
@EricPostpischil pdfs.semanticscholar.org/be8b/…
-
@EricPostpischil 输入的十进制指数是什么意思?
-
我认为从第 13 页开始的“读取和显示说明”部分中解释十进制输入的描述省略了一些步骤。我看不到它在哪里讨论了此操作的浮点寄存器的初始化。我怀疑指数 Ab 和有效数字 Bb 设置为表示值为零(因此 Ab 设置为 -64),而指数 Aa 设置为表示 2^0 的比例(因此 Aa 设置为 0)。然后将输入的十进制数字写入 Ba,并执行加法。然后执行乘以 10,然后将下一个输入数字写入 Ba,以此类推。
-
归一化内置于加法和乘法中。处理完四位数字后,有效数字就完成了,并且 (Ab, Bb) 包含一个表示有效数字的浮点数。如果 e 为非负数或 0.1 | 则乘以 10 e 倍处理十进制指数 e e |如果 e 为负数。 (指数 e 是通过按下机器上的输入按钮来设置的。)
标签: floating-point