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

expr	an 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

a	an expression
b	an 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

expr	an 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:

• /home/runner/work/cbmc/cbmc/src/util/union_find_replace.h
• /home/runner/work/cbmc/cbmc/src/util/union_find_replace.cpp