union_find_replace.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: util
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
#include "union_find_replace.h"
 
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;
}
 
bool union_find_replacet::replace_expr(exprt &expr) const
{
  bool unchanged = ::replace_expr(map, expr);
  while(!unchanged && !::replace_expr(map, expr))
    continue;
  return unchanged;
}
 
exprt union_find_replacet::find(exprt expr) const
{
  replace_expr(expr);
  return expr;
}
 
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;
}