cprover
union_find_replacet Class Reference

Similar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find. More...

#include <union_find_replace.h>

+ Collaboration diagram for union_find_replacet:

Public Member Functions

bool replace_expr (exprt &expr) const
 Replace subexpressions of expr by the representative element of the set they belong to. More...
 
exprt find (exprt expr) const
 
exprt make_union (const exprt &a, const exprt &b)
 Merge the set containing a and the set containing b. More...
 
std::vector< std::pair< exprt, exprt > > to_vector () const
 

Private Attributes

replace_mapt map
 

Detailed Description

Similar interface to union-find for expressions, with a function for replacing sub-expressions by their result for find.

Definition at line 16 of file union_find_replace.h.

Member Function Documentation

◆ find()

exprt union_find_replacet::find ( exprt  expr) const
Parameters
expran expression
Returns
representative element of the set expr belongs to

Definition at line 38 of file union_find_replace.cpp.

◆ make_union()

exprt union_find_replacet::make_union ( const exprt a,
const exprt b 
)

Merge the set containing a and the set containing b.

Parameters
aan expression
ban expression
Returns
current representative element of the set containing a and b

Definition at line 15 of file union_find_replace.cpp.

◆ replace_expr()

bool union_find_replacet::replace_expr ( exprt expr) const

Replace subexpressions of expr by the representative element of the set they belong to.

Parameters
expran expression, modified in place
Returns
true if expr is left unchanged

Definition at line 28 of file union_find_replace.cpp.

◆ to_vector()

std::vector< std::pair< exprt, exprt > > union_find_replacet::to_vector ( ) const
Returns
pairs of expression composed of expressions and a representative expression for the set they below to.

Definition at line 46 of file union_find_replace.cpp.

Member Data Documentation

◆ map

replace_mapt union_find_replacet::map
private

Definition at line 28 of file union_find_replace.h.


The documentation for this class was generated from the following files: