cprover
|
Maps equation to expressions contained in them and conversely expressions to equations that contain them. More...
#include <string_refinement_util.h>
Public Member Functions | |
void | add (const std::size_t i, const exprt &expr) |
Record the fact that equation i contains expression expr More... | |
std::vector< exprt > | find_expressions (const std::size_t i) |
std::vector< std::size_t > | find_equations (const exprt &expr) |
Private Attributes | |
std::map< exprt, std::vector< std::size_t > > | equations_containing |
Record index of the equations that contain a given expression. More... | |
std::unordered_map< std::size_t, std::vector< exprt > > | strings_in_equation |
Record expressions that are contained in the equation with the given index. More... | |
Maps equation to expressions contained in them and conversely expressions to equations that contain them.
This can be used on a subset of expressions which interests us, in particular strings. Equations are identified by an index of type std::size_t
for more efficient insertion and lookup.
Definition at line 140 of file string_refinement_util.h.
void equation_symbol_mappingt::add | ( | const std::size_t | i, |
const exprt & | expr | ||
) |
Record the fact that equation i
contains expression expr
Definition at line 186 of file string_refinement_util.cpp.
std::vector< std::size_t > equation_symbol_mappingt::find_equations | ( | const exprt & | expr | ) |
expr | an expression |
expr
Definition at line 199 of file string_refinement_util.cpp.
std::vector< exprt > equation_symbol_mappingt::find_expressions | ( | const std::size_t | i | ) |
i | index corresponding to an equation |
i
Definition at line 193 of file string_refinement_util.cpp.
|
private |
Record index of the equations that contain a given expression.
Definition at line 157 of file string_refinement_util.h.
|
private |
Record expressions that are contained in the equation with the given index.
Definition at line 159 of file string_refinement_util.h.