CBMC
equation_symbol_mapping.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: String solver
4 
5 Author: Diffblue Ltd.
6 
7 \*******************************************************************/
8 
10 
11 void equation_symbol_mappingt::add(const std::size_t i, const exprt &expr)
12 {
13  equations_containing[expr].push_back(i);
14  strings_in_equation[i].push_back(expr);
15 }
16 
17 std::vector<exprt>
19 {
20  return strings_in_equation[i];
21 }
22 
23 std::vector<std::size_t>
25 {
26  return equations_containing[expr];
27 }
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
std::vector< std::size_t > find_equations(const exprt &expr)
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.
std::vector< exprt > find_expressions(const std::size_t i)
Base class for all expressions.
Definition: expr.h:56