9#ifndef CPROVER_UTIL_UNION_FIND_REPLACE_H
10#define CPROVER_UTIL_UNION_FIND_REPLACE_H
25 std::vector<std::pair<exprt, exprt>>
to_vector()
const;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Base class for all expressions.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
exprt find(exprt expr) const
std::vector< std::pair< exprt, exprt > > to_vector() const
exprt make_union(const exprt &a, const exprt &b)
Merge the set containing a and the set containing b.
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
std::unordered_map< exprt, exprt, irep_hash > replace_mapt