cprover
equation_symbol_mappingt Class Reference

Maps equation to expressions contained in them and conversely expressions to equations that contain them. More...

#include <string_refinement_util.h>

Collaboration diagram for equation_symbol_mappingt:
[legend]

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< exprtfind_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 142 of file string_refinement_util.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 188 of file string_refinement_util.cpp.

References equations_containing, and strings_in_equation.

Referenced by string_identifiers_resolution_from_equations().

◆ find_equations()

std::vector< std::size_t > equation_symbol_mappingt::find_equations ( const exprt expr)
Parameters
expran expression
Returns
vector of equations containing the given expression expr

Definition at line 201 of file string_refinement_util.cpp.

References equations_containing.

Referenced by string_identifiers_resolution_from_equations().

◆ find_expressions()

std::vector< exprt > equation_symbol_mappingt::find_expressions ( const std::size_t  i)
Parameters
iindex corresponding to an equation
Returns
vector of expressions contained in the equation with the given index i

Definition at line 195 of file string_refinement_util.cpp.

References strings_in_equation.

Referenced by string_identifiers_resolution_from_equations().

Member Data Documentation

◆ equations_containing

std::map<exprt, std::vector<std::size_t> > equation_symbol_mappingt::equations_containing
private

Record index of the equations that contain a given expression.

Definition at line 159 of file string_refinement_util.h.

Referenced by add(), and find_equations().

◆ strings_in_equation

std::unordered_map<std::size_t, std::vector<exprt> > equation_symbol_mappingt::strings_in_equation
private

Record expressions that are contained in the equation with the given index.

Definition at line 161 of file string_refinement_util.h.

Referenced by add(), and find_expressions().


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