cprover
|
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>
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 |
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.
expr | an expression |
Definition at line 42 of file union_find_replace.cpp.
References replace_expr().
Referenced by make_union(), and to_vector().
Keeps a map of symbols to expressions, such as none of the mapped values exist as a key.
a | an expression of type char array |
b | an 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 |
Definition at line 18 of file union_find_replace.cpp.
Referenced by add_string_equation_to_symbol_resolution().
bool union_find_replacet::replace_expr | ( | exprt & | expr | ) | const |
Replace subexpressions of expr
by a canonical element of the set they belong to.
expr | an expression, modified in place |
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().
Definition at line 50 of file union_find_replace.cpp.
Referenced by check_axioms(), and string_refinementt::dec_solve().
|
private |
Definition at line 28 of file union_find_replace.h.
Referenced by make_union(), replace_expr(), and to_vector().