ibex-team / ibex-lib

IBEX is a C++ library for constraint processing over real numbers.
http://ibex-team.github.io/ibex-lib/
GNU Lesser General Public License v3.0
67 stars 51 forks source link

Missing solution with -frounding-math #522

Closed kunchtler closed 1 year ago

kunchtler commented 2 years ago

Hello, I've encountered a bug regarding a certain compilation flag that doesn't return all solutions when solving a certain system.

I am using g++ 10.3.0 on Ubuntu 20.04.4 LTS, with the latest version of ibex (2.8.9).

The issue arises when compiling the following piece of code with the "-frounding-math" flag.

#include <iostream>
#include <ibex.h>

int main()
{
    ibex::Variable x("x"), t("t");
    ibex::Function f(x, t, -2 + 19./29 * 4 - ibex::pow(t, 2));
    ibex::Function g(x, t, -2 + 13./29 * 4 - x * t);
    ibex::SystemFactory factory;
    factory.add_var(x);
    factory.add_var(t);
    factory.add_ctr(f(x, t) = 0);
    factory.add_ctr(g(x, t) = 0);

    ibex::System system(factory);
    system.box = {{-2, 2}, {-10, 10}};

    ibex::DefaultSolver solver(system, 1e-9, 1e-6);
    std::cout << system;
    solver.solve(system.box);
    const ibex::CovSolverData& cov = solver.get_data();
    std::cout << cov << "\n";
}

First the expected behaviour. When compiling it with the makefile as explained in the documentation ( http://www.ibex-lib.org/doc/install-cmake.html#install-compiling-running ), the following compilation command gets executed (without "-frounding-math").

g++  -I/usr/local/include -I/usr/local/include/ibex -I/usr/local/include/ibex/3rd  -O3 -DNDEBUG  -std=c++11 -DIBEX_BENCHS_DIR=\"../benchs/solver\" -U__STRICT_ANSI__ -o ibex_bug ibex_bug.cpp -L/usr/local/lib -L/usr/local/lib/ibex/3rd -libex -lgaol -lgdtoa -lultim -lsoplex -lz

When executing the executable, I get the output :

variables: 
  x, t
box: 
  ([-2, 2] ; [-10, 10])
goal: 
  (none)
constraints:
  ((-t^2)+0.62069)=0
  ((-(x*t))+-0.206896)=0
 solution n°1 = ([0.262612865719445, 0.2626128657194452] ; [-0.7878385971583354, -0.7878385971583352])
 solution n°2 = ([-0.2626128657194452, -0.262612865719445] ; [0.7878385971583352, 0.7878385971583354])

2 solution boxes are printed, which is the expected behaviour.

However, when adding at the end of the compilation command the flag "-frounding-math", I get the output :

variables: 
  x, t
box: 
  ([-2, 2] ; [-10, 10])
goal: 
  (none)
constraints:
  ((-t^2)+0.62069)=0
  ((-(x*t))+-0.206896)=0
 solution n°1 = ([-0.2626128657194451, -0.2626128657194449] ; [0.7878385971583354, 0.7878385971583358])

The second solution box is nowhere to be seen (even as a boundary or unknown kind of box).

This behaviour doesn't happen for all constants appearing in the expression of f and g, and it doesn't happen either when replacing "ibex::pow(t, 2)" with "t*t". My guess is that it is a problem within the function pow or sqr itself.

Thank you in advance !

gchabert commented 1 year ago

Hi, The problem does not come from ibex. The problem comes from the way g++ optimizes constant evaluation in your constraint declaration, depending on whether you use "-frounding-math" or not. If you replace the expression 19./29 4 by 2.62068965517241 and 13./29 4 by 1.79310344827586, you get the same result with or without "-frounding-math". So the behavior of the solver is the same regardless of this compiler option. Gilles