7 #include <unordered_map>    11 #include "dreal/util/exception.h"    16 template <
class Key, 
class T, 
class Hash = std::hash<Key>,
    17           class KeyEqual = std::equal_to<Key>,
    18           class Allocator = std::allocator<std::pair<const Key, T>>>
    22   using UnorderedMapType =
    23       std::unordered_map<Key, T, Hash, KeyEqual, Allocator>;
    24   using value_type = 
typename UnorderedMapType::value_type;
    25   using size_type = 
typename UnorderedMapType::size_type;
    26   using const_iterator = 
typename UnorderedMapType::const_iterator;
    34   using Action = std::tuple<ActionKind, Key, T>;
    48   const_iterator begin()
 const { 
return map_.begin(); }
    49   const_iterator cbegin()
 const { 
return map_.cbegin(); }
    50   const_iterator end()
 const { 
return map_.end(); }
    51   const_iterator cend()
 const { 
return map_.cend(); }
    54   bool empty()
 const { 
return map_.empty(); }
    55   size_type size()
 const { 
return map_.size(); }
    63   void insert(
const Key& k, 
const T& v) {
    64     auto it = map_.find(k);
    65     if (it == map_.end()) {
    78   const T& operator[](
const Key& key)
 const {
    79     const auto it = map_.find(key);
    80     if (it == map_.end()) {
    81       throw DREAL_RUNTIME_ERROR(
    82           "ScopedUnorderedMap has no entry for the key {}.", key);
    87   size_type count(
const Key& key)
 const { 
return map_.count(key); }
    89   const_iterator find(
const Key& key)
 const { 
return map_.find(key); }
    92   void push() { stack_.push_back(actions_.size()); }
    95       throw DREAL_RUNTIME_ERROR(
    96           "ScopedUnorderedMap cannot be popped because it's scope is empty.");
    98     size_type idx = stack_.back();
    99     while (idx < actions_.size()) {
   100       const Action& item{actions_.back()};
   102       const Key& k{std::get<1>(item)};
   103       const T& v{std::get<2>(item)};
   104       auto it = map_.find(k);
   121   std::vector<Action> actions_;
   122   std::vector<size_type> stack_;
   123   UnorderedMapType map_;
 Insert(k, v) means that (k, v) is inserted. 
 
Sum type of symbolic::Expression and symbolic::Formula. 
Definition: api.cc:9
 
Backtrackable map. 
Definition: scoped_unordered_map.h:19
 
ActionKind
Definition: scoped_unordered_map.h:30
 
Update(k, v) means that (k, v) was replaced by a new value.