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`

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.

std::unordered_map< std::size_t, std::vector< exprt > >	strings_in_equation
	Record expressions that are contained in the equation with the given index.

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

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 38 of file equation_symbol_mapping.h.

◆ 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 40 of file equation_symbol_mapping.h.

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

/home/runner/work/cbmc/cbmc/src/solvers/strings/equation_symbol_mapping.h
/home/runner/work/cbmc/cbmc/src/solvers/strings/equation_symbol_mapping.cpp

Public Member Functions

Private Attributes