[SMT-LIB] new SMT-LIB theory: FloatingPoints

[Tinelli, Cesare]

Hi all,

Please find attached an SMT-LIB theory declaration for a general theory of floating point numbers.

The version below was written by Martin Brain and myself with the input of an ad hoc work group, and starting from a proposal by Philipp Ruemmer and Thomas Wahl [RW10].

We are now submitting it to the SMT-LIB community for additional comments, questions and feedback in general before we incorporate it officially in the SMT-LIB standard.

Please send your feedback to this list by **July 7, 2013**.

Note that we have only the theory for now. We will propose a couple of logics for it in the near future. Two likely candidates are
- a quantifier-free logic combining floating points with EUF, arrays
  and bitvectors and
- a quantifier-free logic combining floating point arithmetic with
  non-linear real (or mixed integer and real) arithmetic.
As usual, the details of these logics will depend on the availability of benchmarks and the state of the art in SMT solving for the theories involved.

Thanks,


Cesare

---------------------------
Some notes about the theory
---------------------------

The bulk of the work group discussion was through a Google group. For those who are interested, it can be found here: https://groups.google.com/forum/#!forum/smt-fp

The theory is largely based on the IEEE standard 754-2008 for floating-point arithmetic (http://grouper.ieee.org/groups/754/) but restricted to the binary case only.

A major extension over 754-2008 is that the theory has a sort for every
possible exponent and significand length. The theory also includes conversion functions from and to bit vectors and real numbers.

The theory follows closely the Ruemmer and Wahl's proposal. Main differences are
- it replaces a sort for rational numbers with one for real one;
- it allows a bit-precise representation of concrete FP values;
- it adds conversion to the IEEE binary interchange format (via
  a bitvector encoding) as wellas C/Java-style casting to machine
  integers (also expressed with bitvectors).

[RW10] Philipp Ruemmer and Thomas Wahl.
       An SMT-LIB Theory of Binary Floating-Point Arithmetic.
       Proceedings of the 8th International Workshop on
       Satisfiability Modulo Theories (SMT'10), Edinburgh, UK, July 2010.
       (http://www.philipp.ruemmer.org/publications/smt-fpa.pdf)



-------------- next part --------------
A non-text attachment was scrubbed...
Name: FloatingPoints.smt2
Type: application/octet-stream
Size: 16981 bytes
Desc: FloatingPoints.smt2
URL: </pipermail/smt-lib/attachments/20130627/0f7841c7/attachment.obj>