SAT solver performance problem with floating point equalities

[peterschrammel]

Tests in #4338.

void main() {
  double a, b, c;
  __CPROVER_assume(a + b > c);
  assert(!(c > a + b) );
}

has equation

file Float-equality1/main.c line 10 function main
assertion !(c > a + b)
...
{-12} floatbv_plus(main::1::a!0@1#1, main::1::b!0@1#1, 0) > main::1::c!0@1#1
├──────────────────────────
{1} ¬(main::1::c!0@1#1 > floatbv_plus(main::1::a!0@1#1, main::1::b!0@1#1, 0))

and solves quickly,

whereas

void main() {
  double a, b, c;
  __CPROVER_assume(a + b > c);
  double x = a, y = b, z = c;
  assert(!(z > x + y) );
}

with the equation

file Float-equality1/main.c line 10 function main
assertion !(c > a + b)
...
{-12} floatbv_plus(main::1::a!0@1#1, main::1::b!0@1#1, 0) > main::1::c!0@1#1
{-13} main::1::x!0@1#2 = main::1::a!0@1#1
{-14} main::1::y!0@1#2 = main::1::b!0@1#1
{-15} main::1::z!0@1#2 = main::1::c!0@1#1
├──────────────────────────
{1} ¬(main::1::c!0@1#1 > floatbv_plus(main::1::a!0@1#1, main::1::b!0@1#1, 0))

takes forever to solve.

[tautschnig]

Adding another ASSUME fixes this, even when the expressions strictly can't be cached (the problem is as bad with float instead of double):

void main() {
  float a, b, c;
  __CPROVER_assume(a + b > c);
  float x = a, y = b, z = c;
  __CPROVER_assume(x + y + 0 > z + 0);
  assert(!(z > x + y) );
}

[tautschnig]

Attaching a zip file of a CNF for future reference.
float.cnf.zip

[tautschnig]

Here's a variation on the "easy" case that's also hard:

void main() {
  float a, b, c;
  __CPROVER_assume(a + b > c);
  assert(!(c > 0 + a + b) );
}

A key difference is that 0 + a + b enforces that a + b cannot be reused while encoding. Corresponding CNF is attached.
float.cnf.zip

[martin-cs]

@peterschrammel : this one is interesting because the expression substitution on equality is definitely happening. I should probably check that it also re-orders 'b + a' although it is not the problem here.

@tautschnig : the cases you give have a number of more subtle things going on. '0' is an integer which promotes to double IIRC, so like '0.0' it forces type promotion of the whole expression. As it's not cast back, the double rounding trick doesn't let us optimise. Then there is the issue that 'x + 0' is not always bit identical to 'x' so it can't be optimised away. Then there is associativity issues. I think at least some of these were expected / intended. My guess is that you will see the same effects for '0.0f' as well.

[tautschnig]

@martin-cs Yes, using 0.0f produces exactly the same formula (the C front-end type-casts the 0 to a float, and the simplifier turns this into 0.0f).