Invertibility Conditions for Floating-Point Formulas

被引：4

作者：

Brain, Martin ^{[3
,4
]}

Niemetz, Aina ^{[1
]}

Preiner, Mathias ^{[1
]}

Reynolds, Andrew ^{[2
]}

Barrett, Clark ^{[1
]}

Tinelli, Cesare ^{[2
]}

机构：

[1] Stanford Univ, Stanford, CA 94305 USA

[2] Univ Iowa, Iowa City, IA USA

[3] Univ Oxford, Oxford, England

[4] City Univ London, London, England

来源：

COMPUTER AIDED VERIFICATION, CAV 2019, PT II | 2019年 / 11562卷

基金：

美国国家科学基金会;

关键词：

D O I：

10.1007/978-3-030-25543-5_8

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Automated reasoning procedures are essential for a number of applications that involve bit-exact floating-point computations. This paper presents conditions that characterize when a variable in a floating-point constraint has a solution, which we call invertibility conditions. We describe a novel workflow that combines human interaction and a syntax-guided synthesis (SyGuS) solver that was used for discovering these conditions. We verify our conditions for several floating-point formats. One implication of this result is that a fragment of floating-point arithmetic admits compact quantifier elimination. We implement our invertibility conditions in a prototype extension of our solver CVC4, showing their usefulness for solving quantified constraints over floating-points.

引用

页码：116 / 136

页数：21