Move has_byte_operator to util

There is nothing solvers-specific to this function. Cleanup in
preparation of moving all byte-operator lowering to util.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -2483,21 +2483,6 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
   return result;
 }
 
-bool has_byte_operator(const exprt &src)
-{
-  if(src.id()==ID_byte_update_little_endian ||
-     src.id()==ID_byte_update_big_endian ||
-     src.id()==ID_byte_extract_little_endian ||
-     src.id()==ID_byte_extract_big_endian)
-    return true;
-
-  forall_operands(it, src)
-    if(has_byte_operator(*it))
-      return true;
-
-  return false;
-}
-
 exprt lower_byte_operators(const exprt &src, const namespacet &ns)
 {
   exprt tmp=src;

src/solvers/lowering/expr_lowering.h

@@ -41,6 +41,4 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
 ///   byte_extract_exprt or \ref byte_update_exprt.
 exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
-bool has_byte_operator(const exprt &src);
-
 #endif /* CPROVER_SOLVERS_LOWERING_EXPR_LOWERING_H */

src/util/byte_operators.cpp

@@ -57,3 +57,18 @@ make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value)
   return byte_update_exprt{
     byte_update_id(), _op, _offset, _value, config.ansi_c.char_width};
 }
+
+bool has_byte_operator(const exprt &src)
+{
+  if(src.id()==ID_byte_update_little_endian ||
+     src.id()==ID_byte_update_big_endian ||
+     src.id()==ID_byte_extract_little_endian ||
+     src.id()==ID_byte_extract_big_endian)
+    return true;
+
+  forall_operands(it, src)
+    if(has_byte_operator(*it))
+      return true;
+
+  return false;
+}

src/util/byte_operators.h

@@ -162,4 +162,8 @@ make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type);
 byte_update_exprt
 make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
 
+/// Return true iff \p src or one of its operands contain a byte extract or byte
+/// update expression.
+bool has_byte_operator(const exprt &src);
+
 #endif // CPROVER_UTIL_BYTE_OPERATORS_H