Skip to content

Document union_find_replacet #3229

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 30, 2018
Merged

Document union_find_replacet #3229

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
20 changes: 8 additions & 12 deletions src/util/union_find_replace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,10 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com

#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
/// Merge the set containing `a` and the set containing `b`.
/// \param a: an expression
/// \param b: an expression
/// \return current representative element of the set containing `a` and `b`
exprt union_find_replacet::make_union(const exprt &a, const exprt &b)
{
const exprt &lhs_root = find(a);
Expand All @@ -24,8 +21,8 @@ exprt union_find_replacet::make_union(const exprt &a, const exprt &b)
return rhs_root;
}

/// Replace subexpressions of `expr` by a canonical element of the set they
/// belong to.
/// Replace subexpressions of `expr` by the representative 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
Expand All @@ -37,15 +34,14 @@ bool union_find_replacet::replace_expr(exprt &expr) const
}

/// \param expr: an expression
/// \return canonical representation for expressions which belong to the same
/// set
/// \return representative element of the set `expr` belongs to
exprt union_find_replacet::find(exprt expr) const
{
replace_expr(expr);
return expr;
}

/// \return pairs of expression composed of expressions and a canonical
/// \return pairs of expression composed of expressions and a representative
/// expression for the set they below to.
std::vector<std::pair<exprt, exprt>> union_find_replacet::to_vector() const
{
Expand Down