Simplify: sort operands for commutative, but not associative operations

Testing floating-point equality is expensive, and thus warrants handling
special cases (even if they might be rare) in the simplifier. This
(simplistic) test would take 5 seconds with CaDiCaL as SAT back-end when
not performing simplification.

Author: tautschnig

regression/cbmc/Float-equality2/main.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float a;
+  float b;
+  // We could do "if (isnormal(a) && isnormal(b))", but __CPROVER_isnanf(a+b)
+  // will permit solving this entirely via the simplifier, if, and only if, the
+  // equality is successfully simplified (despite the different order of
+  // operands).
+  assert(__CPROVER_isnanf(a + b) || a + b == b + a);
+}

regression/cbmc/Float-equality2/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This requires simplification of commutative, but not associative operations.

src/util/simplify_expr_floatbv.cpp

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include "invariant.h"
 #include "namespace.h"
 #include "simplify_expr.h"
+#include "simplify_utils.h"
 #include "std_expr.h"
 
 simplify_exprt::resultt<>
@@ -361,7 +362,15 @@ simplify_exprt::simplify_ieee_float_relation(const binary_relation_exprt &expr)
       UNREACHABLE;
   }
 
-  if(expr.lhs() == expr.rhs())
+  // addition and multiplication are commutative, but not associative
+  exprt lhs_sorted = expr.lhs();
+  if(lhs_sorted.id() == ID_floatbv_plus || lhs_sorted.id() == ID_floatbv_mult)
+    sort_operands(lhs_sorted.operands());
+  exprt rhs_sorted = expr.rhs();
+  if(rhs_sorted.id() == ID_floatbv_plus || rhs_sorted.id() == ID_floatbv_mult)
+    sort_operands(rhs_sorted.operands());
+
+  if(lhs_sorted == rhs_sorted)
   {
     // x!=x is the same as saying isnan(op)
     exprt isnan = isnan_exprt(expr.lhs());