## FPCS: a Floating point Constraint Solver

FPCS is a floating point constraint solver.
Floating point constraints have been introduced in [1] to allow to reason correctly on floating point computations.
Therefore, floating point constraint are dedicated to the test and verification of programs that contain floating point computation.
Such a tool is required to correctly handle floating point constraints: for instance, a constraint like
x*x == 2.0 with x < 0 has not solution over the floats with a rounding mode set to near while it has a solution over the reals.

FPCS mainly relies on [2] (see Publications for other related papers)
to filter constraints over the floats with respect to the IEEE 754 standard.

FPCS is a C++ library (~50k lines, ~30k being generated with macros).
It supports 4 different rounding modes, basic arithmetic operations, comparisons, float/integer conversions
and some usual functions like the square root.
2B consistency filtering is complemented with stronger kB consistency filtering.

FPCS targets C programs running under linux (32 or 64 bits) and compiled with gcc without any optimization.

#### Papers

* Solving constraints over floating-point numbers.*

Claude Michel, Michel Rueher, Yahia Lebbah.

In *Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming (CP'01)*,
LNCS 2239, pages 524-538, Paphos, Chypre, 26-1st November 2001.

[ .ps | .pdf ]
* Exact projection functions for floating point number constraints.*

Claude Michel.

In *Seventh international symposium on Artificial Intelligence and Mathematics (7th AIMA)*,
Fort Lauderdale, Floride (US), 2-4th January 2002.

[ .ps | .pdf ]