Approximate Translation from Floating-Point to Real-Interval Arithmetic
Approximate Translation from Floating-Point to Real-Interval Arithmetic
复制标题
从浮点运算到实数区间运算的近似转换
DOI：
10.1007/978-3-031-06773-0_39
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Toshiaki Aoki
中科院分区：
文献类型：
--
作者：
Daisuke Ishii;Takashi Tomita;Toshiaki Aoki
浮点运算（FPA）是真实的运算（RA）的机械表示，其中每个运算都用舍入的对应运算代替。通过使用支持FPA逻辑的SMT解算器可以验证各种数值属性。然而，与RA相比，求解过程的可扩展性仍然有限。在本文中，我们提出了一个决定程序FPA，利用RA解决的效率。该方法将FP数抽象为有理区间，将FPA表达式抽象为区间算术（IA）表达式，然后使用现成的RA求解器（使用CVC 4和Z3）求解IA公式，以检查FPA公式的可满足性。为了换取抽象所获得的效率，求解过程变得准完整;当可满足性受到可能的数值错误的影响时，我们允许输出。此外，我们的IA是精心形式化处理的特殊值。我们实现了所提出的方法，并在实验中将其与四个现有的SMT求解器进行了比较。因此，我们确认，我们的求解器是有效的舍入模式参数化的情况下。
Floating-point arithmetic (FPA) is a mechanical representation of real arithmetic (RA), where each operation is replaced with a rounded counterpart. Various numerical properties can be verified by using SMT solvers that support the logic of FPA. However, the scalability of the solving process remains limited when compared to RA. In this paper, we present a decision procedure for FPA that takes advantage of the efficiency of RA solving. The proposed method abstracts FP numbers as rational intervals and FPA expressions as interval arithmetic (IA) expressions; then, we solve IA formulas to check the satisfiability of an FPA formula using an off-the-shelf RA solver (we useCVC4andZ3). In exchange for the efficiency gained by abstraction, the solving process becomes quasi-complete; we allow to outputwhen the satisfiability is affected by possible numerical errors. Furthermore, our IA is meticulously formalized to handle the special value. We implemented the proposed method and compared it to four existing SMT solvers in the experiments. As a result, we confirmed that our solver was efficient for instances where rounding modes were parameterized.