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

  1. 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 ]
  2. 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 ]