Maps equation to expressions contained in them and conversely expressions to equations that contain them. More...
#include <equation_symbol_mapping.h>
Collaboration diagram for equation_symbol_mappingt: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... | |
Detailed Description
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 21 of file equation_symbol_mapping.h.
Member Function Documentation
◆ add()
| 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 11 of file equation_symbol_mapping.cpp.
◆ find_equations()
| std::vector< std::size_t > equation_symbol_mappingt::find_equations | ( | const exprt & | expr | ) |
- Parameters
-
expr an expression
- Returns
- vector of equations containing the given expression
expr
Definition at line 24 of file equation_symbol_mapping.cpp.
◆ find_expressions()
| std::vector< exprt > equation_symbol_mappingt::find_expressions | ( | const std::size_t | i | ) |
- Parameters
-
i index corresponding to an equation
- Returns
- vector of expressions contained in the equation with the given index
i
Definition at line 18 of file equation_symbol_mapping.cpp.
Member Data Documentation
◆ equations_containing
|
private |
Record index of the equations that contain a given expression.
Definition at line 38 of file equation_symbol_mapping.h.
◆ strings_in_equation
|
private |
Record expressions that are contained in the equation with the given index.
Definition at line 40 of file equation_symbol_mapping.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/equation_symbol_mapping.h
- /home/runner/work/cbmc-documentation/cbmc-documentation/src/solvers/strings/equation_symbol_mapping.cpp
