CBMC
union_find_replace.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: util
4 
5 Author: 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 {
18 public:
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 
27 private:
29 };
30 
31 #endif // CPROVER_UTIL_UNION_FIND_REPLACE_H
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
Definition: replace_expr.h:22