equation_symbol_mapping.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: String solver
 
Author: Diffblue Ltd.
 
\*******************************************************************/
 
#ifndef CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H
#define CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H
 
#include <map>
#include <unordered_map>
 
#include <util/expr.h>

class equation_symbol_mappingt
{
public:
  void add(const std::size_t i, const exprt &expr);

  std::vector<exprt> find_expressions(const std::size_t i);

  std::vector<std::size_t> find_equations(const exprt &expr);
 
private:
  std::map<exprt, std::vector<std::size_t>> equations_containing;
  std::unordered_map<std::size_t, std::vector<exprt>> strings_in_equation;
};
 
#endif // CPROVER_SOLVERS_STRINGS_EQUATION_SYMBOL_MAPPING_H