New class for union find replace

This has a similar interface to union_find but also allows to replace
expressions.
It will be used in the string solver instead of a simple replace_mapt.

Author: romainbrenguier

src/util/Makefile

@@ -92,6 +92,7 @@ SRC = arith_tools.cpp \
       ui_message.cpp \
       unicode.cpp \
       union_find.cpp \
+      union_find_replace.cpp \
       xml.cpp \
       xml_expr.cpp \
       xml_irep.cpp \

src/util/union_find_replace.cpp

@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+Module: util
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#include "union_find_replace.h"
+
+/// Keeps a map of symbols to expressions, such as none of the mapped values
+/// exist as a key
+/// \param a: an expression of type char array
+/// \param b: an expression to map it to, which should be either a symbol
+///             a string_exprt, an array_exprt, an array_of_exprt or an
+///             if_exprt with branches of the previous kind
+/// \return the new mapped value
+exprt union_find_replacet::make_union(const exprt &a, const exprt &b)
+{
+  const exprt &lhs_root = find(a);
+  const exprt &rhs_root = find(b);
+  if(lhs_root != rhs_root)
+    map[lhs_root] = rhs_root;
+  return rhs_root;
+}
+
+/// Replace subexpressions of `expr` by a canonical element of the set they
+/// belong to.
+/// \param expr: an expression, modified in place
+/// \return true if expr is left unchanged
+bool union_find_replacet::replace_expr(exprt &expr) const
+{
+  bool unchanged = ::replace_expr(map, expr);
+  while(!unchanged && !::replace_expr(map, expr))
+    continue;
+  return unchanged;
+}
+
+/// \param expr: an expression
+/// \return canonical representation for expressions which belong to the same
+///         set
+exprt union_find_replacet::find(exprt expr) const
+{
+  replace_expr(expr);
+  return expr;
+}
+
+/// \return pairs of expression composed of expressions and a canonical
+///         expression for the set they below to.
+std::vector<std::pair<exprt, exprt>> union_find_replacet::to_vector() const
+{
+  std::vector<std::pair<exprt, exprt>> equations;
+  for(const auto &pair : map)
+    equations.emplace_back(pair.first, find(pair.second));
+  return equations;
+}

src/util/union_find_replace.h

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: util
+
+Author: Romain Brenguier, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_UNION_FIND_REPLACE_H
+#define CPROVER_UTIL_UNION_FIND_REPLACE_H
+
+#include <util/replace_expr.h>
+
+/// Similar interface to union-find for expressions, with a function for
+/// replacing sub-expressions by their result for find.
+class union_find_replacet
+{
+public:
+  bool replace_expr(exprt &expr) const;
+
+  exprt find(exprt expr) const;
+
+  exprt make_union(const exprt &a, const exprt &b);
+
+  std::vector<std::pair<exprt, exprt>> to_vector() const;
+
+private:
+  replace_mapt map;
+};
+
+#endif // CPROVER_UTIL_UNION_FIND_REPLACE_H