array_pool.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: String solver
 
Author: Romain Brenguier, romain.brenguier@diffblue.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_SOLVERS_STRINGS_ARRAY_POOL_H
#define CPROVER_SOLVERS_STRINGS_ARRAY_POOL_H
 
#include <util/std_expr.h>
#include <util/string_expr.h>
 
class symbol_generatort final
{
public:
  symbol_exprt
  operator()(const irep_idt &prefix, const typet &type = bool_typet());
 
private:
  unsigned symbol_count = 0;
 
#ifdef DEBUG
public:
  std::vector<symbol_exprt> created_symbols;
#endif
};
class symbol_generatort final {…};
 
class array_poolt final
{
public:
  explicit array_poolt(symbol_generatort &symbol_generator)
    : fresh_symbol(symbol_generator)
  {
  }
  explicit array_poolt(symbol_generatort &symbol_generator) {…}
 
  const std::unordered_map<exprt, array_string_exprt, irep_hash> &
  get_arrays_of_pointers() const
  {
    return arrays_of_pointers;
  }
  get_arrays_of_pointers() const {…}
 
  exprt get_or_create_length(const array_string_exprt &s);
 
  std::optional<exprt> get_length_if_exists(const array_string_exprt &s) const;
 
  void insert(const exprt &pointer_expr, const array_string_exprt &array);
 
  array_string_exprt find(const exprt &pointer, const exprt &length);
 
  const std::unordered_map<array_string_exprt, exprt, irep_hash> &
  created_strings() const;
 
  array_string_exprt
  fresh_string(const typet &index_type, const typet &char_type);
 
private:
  std::unordered_map<exprt, array_string_exprt, irep_hash> arrays_of_pointers;
 
  std::unordered_map<array_string_exprt, exprt, irep_hash> length_of_array;
 
  symbol_generatort &fresh_symbol;
 
  array_string_exprt make_char_array_for_char_pointer(
    const exprt &char_pointer,
    const typet &char_array_type);
};
class array_poolt final {…};
 
array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg);
 
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr);
 
#endif // CPROVER_SOLVERS_STRINGS_ARRAY_POOL_H