Real Behavior of Floating Point Numbers - Archive ouverte HAL Access content directly
Conference Papers Year :

Real Behavior of Floating Point Numbers

(1, 2) , (2, 1) , (2, 1)
1
2

Abstract

We present an efficient constraint programming (CP) approach to the SMTLIB theory of quantifier-free floating-point arithmetic (QF FP). We rely on dense interreduction between many domain representations to greatly reduce the search space. We compare our tool to current state-of-the-art SMT solvers and show that it is consistently better on large problems involving non-linear arithmetic operations (for which bit-blasting techniques tend to scale badly). Our results emphasize the importance of the conservation of the high-level structure of the original problems.
Fichier principal
Vignette du fichier
main.pdf (337.25 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

cea-01795760 , version 1 (18-05-2018)

Identifiers

  • HAL Id : cea-01795760 , version 1

Cite

Bruno Marre, François Bobot, Zakaria Chihani. Real Behavior of Floating Point Numbers. The SMT Workshop, SMT 2017, 15th International Workshop on Satisfiability Modulo Theories, Jul 2017, Heidelberg, Germany. ⟨cea-01795760⟩
143 View
144 Download

Share

Gmail Facebook Twitter LinkedIn More