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:
[legend]

Public Member Functions

bool replace_expr (exprt &expr) const
 Replace subexpressions of expr by a canonical element of the set they belong to. More...
 
exprt find (exprt expr) const
 
exprt make_union (const exprt &a, const exprt &b)
 Keeps a map of symbols to expressions, such as none of the mapped values exist as a key. 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
canonical representation for expressions which belong to the same set

Definition at line 42 of file union_find_replace.cpp.

References replace_expr().

Referenced by make_union(), and to_vector().

◆ make_union()

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

Keeps a map of symbols to expressions, such as none of the mapped values exist as a key.

Parameters
aan expression of type char array
ban expression to map it to, which should be either a symbol a string_exprt, an array_exprt, an array_of_exprt or an if_exprt with branches of the previous kind
Returns
the new mapped value

Definition at line 18 of file union_find_replace.cpp.

References find(), and map.

Referenced by add_string_equation_to_symbol_resolution().

◆ replace_expr()

bool union_find_replacet::replace_expr ( exprt expr) const

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

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

Definition at line 31 of file union_find_replace.cpp.

References map.

Referenced by string_refinementt::add_lemma(), string_refinementt::dec_solve(), find(), string_refinementt::get(), string_constraintt::replace_expr(), and replace_symbols_in_equations().

◆ to_vector()

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

Definition at line 50 of file union_find_replace.cpp.

References find(), and map.

Referenced by check_axioms(), and string_refinementt::dec_solve().

Member Data Documentation

◆ map

replace_mapt union_find_replacet::map
private

Definition at line 28 of file union_find_replace.h.

Referenced by make_union(), replace_expr(), and to_vector().


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