symbol_table.h

Go to the documentation of this file.

 
 
 
#ifndef CPROVER_UTIL_SYMBOL_TABLE_H
#define CPROVER_UTIL_SYMBOL_TABLE_H
 
#include "symbol_table_base.h"
 
class symbol_tablet : public symbol_table_baset
{
private:
  symbolst internal_symbols;
  symbol_base_mapt internal_symbol_base_map;
  symbol_module_mapt internal_symbol_module_map;
 
public:
  symbol_tablet()
    : symbol_table_baset(
        internal_symbols,
        internal_symbol_base_map,
        internal_symbol_module_map)
  {
  }
 
  symbol_tablet(const symbol_tablet &other)
    : symbol_table_baset(
        internal_symbols,
        internal_symbol_base_map,
        internal_symbol_module_map),
      internal_symbols(other.internal_symbols),
      internal_symbol_base_map(other.internal_symbol_base_map),
      internal_symbol_module_map(other.internal_symbol_module_map)
  {
  }
 
  symbol_tablet &operator=(const symbol_tablet &other)
  {
    // Copy to temp and then call move assignment
    return *this=symbol_tablet(other);
  }
 
  symbol_tablet(symbol_tablet &&other)
    : symbol_table_baset(
        internal_symbols,
        internal_symbol_base_map,
        internal_symbol_module_map),
      internal_symbols(std::move(other.internal_symbols)),
      internal_symbol_base_map(std::move(other.internal_symbol_base_map)),
      internal_symbol_module_map(std::move(other.internal_symbol_module_map))
  {
  }
 
  symbol_tablet &operator=(symbol_tablet &&other)
  {
    internal_symbols = std::move(other.internal_symbols);
    internal_symbol_base_map = std::move(other.internal_symbol_base_map);
    internal_symbol_module_map = std::move(other.internal_symbol_module_map);
    return *this;
  }
 
  void swap(symbol_tablet &other)
  {
    internal_symbols.swap(other.internal_symbols);
    internal_symbol_base_map.swap(other.internal_symbol_base_map);
    internal_symbol_module_map.swap(other.internal_symbol_module_map);
  }
 
public:
  virtual const symbol_tablet &get_symbol_table() const override
  {
    return *this;
  }
 
  virtual symbolt *get_writeable(const irep_idt &name) override
  {
    symbolst::iterator it = internal_symbols.find(name);
    return it != internal_symbols.end() ? &it->second : nullptr;
  }
 
  virtual std::pair<symbolt &, bool> insert(symbolt symbol) override;
  virtual bool move(symbolt &symbol, symbolt *&new_symbol) override;
 
  virtual void erase(const symbolst::const_iterator &entry) override;
  virtual void clear() override
  {
    internal_symbols.clear();
    internal_symbol_base_map.clear();
    internal_symbol_module_map.clear();
  }
 
  virtual iteratort begin() override
  {
    return iteratort(internal_symbols.begin());
  }
  virtual iteratort end() override
  {
    return iteratort(internal_symbols.end());
  }
 
  using symbol_table_baset::begin;
  using symbol_table_baset::end;
 
  void validate(
    const validation_modet vm = validation_modet::INVARIANT) const override;
 
  bool operator==(const symbol_tablet &other) const;
};
 
#endif // CPROVER_UTIL_SYMBOL_TABLE_H