CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
union_find_replace.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: util
4
5Author: Romain Brenguier, romain.brenguier@diffblue.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_UTIL_UNION_FIND_REPLACE_H
10#define CPROVER_UTIL_UNION_FIND_REPLACE_H
11
12#include "replace_expr.h"
13
17{
18public:
19 bool replace_expr(exprt &expr) const;
20
21 exprt find(exprt expr) const;
22
23 exprt make_union(const exprt &a, const exprt &b);
24
25 std::vector<std::pair<exprt, exprt>> to_vector() const;
26
27private:
29};
30
31#endif // CPROVER_UTIL_UNION_FIND_REPLACE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
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