Needs more profiling: Do not sort operands as part of simplification

Author: tautschnig

src/util/simplify_expr.cpp

@@ -2233,7 +2233,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
 
   bool result=true;
 
-  result=sort_and_join(expr) && result;
+  result = sort_and_join(expr, false) && result;
 
   if(expr.id()==ID_typecast)
     result=simplify_typecast(expr) && result;

src/util/simplify_utils.cpp

@@ -119,7 +119,7 @@ static const struct saj_tablet &sort_and_join(
   return saj_table[i];
 }
 
-bool sort_and_join(exprt &expr)
+bool sort_and_join(exprt &expr, bool do_sort)
 {
   bool result=true;
 
@@ -158,8 +158,9 @@ bool sort_and_join(exprt &expr)
   }
 
   // sort it
+  if(do_sort)
+    result = sort_operands(new_ops) && result;
 
-  result=sort_operands(new_ops) && result;
   expr.operands().swap(new_ops);
 
   return result;

src/util/simplify_utils.h

@@ -14,6 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 bool sort_operands(exprt::operandst &operands);
 
-bool sort_and_join(exprt &expr);
+bool sort_and_join(exprt &expr, bool do_sort=true);
 
 #endif // CPROVER_UTIL_SIMPLIFY_UTILS_H