dReal4
scoped_unordered_map.h
1 #pragma once
2 
3 #include <functional>
4 #include <iostream>
5 #include <memory>
6 #include <tuple>
7 #include <unordered_map>
8 #include <utility>
9 #include <vector>
10 
11 #include "dreal/util/exception.h"
12 
13 namespace dreal {
14 
15 /// Backtrackable map.
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>>>
20  public:
21  // Aliases.
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;
27 
28  // To backtrack, we need to record the actions applied to this
29  // container.
30  enum class ActionKind {
31  INSERT, ///< Insert(k, v) means that (k, v) is inserted.
32  UPDATE, ///< Update(k, v) means that (k, v) was replaced by a new value.
33  };
34  using Action = std::tuple<ActionKind, Key, T>;
35 
36  ScopedUnorderedMap() = default;
37  ScopedUnorderedMap(const ScopedUnorderedMap&) = default;
38  ScopedUnorderedMap(ScopedUnorderedMap&&) noexcept = default;
39  ScopedUnorderedMap& operator=(const ScopedUnorderedMap&) = default;
40  ScopedUnorderedMap& operator=(ScopedUnorderedMap&&) noexcept = default;
41  ~ScopedUnorderedMap() = default;
42 
43  // Iterators.
44  //
45  // @note We only provide 'const' iterators because any modification
46  // should be done explicitly via its APIs so that we can keep track
47  // of changes and undo when pop() is called.
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(); }
52 
53  // Capacity
54  bool empty() const { return map_.empty(); }
55  size_type size() const { return map_.size(); }
56 
57  // Modifiers
58  void clear() {
59  map_.clear();
60  actions_.clear();
61  stack_.clear();
62  }
63  void insert(const Key& k, const T& v) {
64  auto it = map_.find(k);
65  if (it == map_.end()) {
66  // Case 1) k does not exist.
67  actions_.emplace_back(ActionKind::INSERT, k, v);
68  map_.emplace(k, v);
69  } else {
70  // Case 2) k exists. Save the old value so that we can roll
71  // back later.
72  actions_.emplace_back(ActionKind::UPDATE, k, it->second);
73  it->second = v; // Perform Update.
74  }
75  }
76 
77  // Lookup
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);
83  } else {
84  return it->second;
85  }
86  }
87  size_type count(const Key& key) const { return map_.count(key); }
88  // @note It returns 'const' iterator.
89  const_iterator find(const Key& key) const { return map_.find(key); }
90 
91  // Push/Pop
92  void push() { stack_.push_back(actions_.size()); }
93  void pop() {
94  if (stack_.empty()) {
95  throw DREAL_RUNTIME_ERROR(
96  "ScopedUnorderedMap cannot be popped because it's scope is empty.");
97  }
98  size_type idx = stack_.back();
99  while (idx < actions_.size()) {
100  const Action& item{actions_.back()};
101  const ActionKind kind{std::get<0>(item)};
102  const Key& k{std::get<1>(item)};
103  const T& v{std::get<2>(item)};
104  auto it = map_.find(k);
105  switch (kind) {
106  case ActionKind::INSERT:
107  // Remove (k, v).
108  map_.erase(it);
109  break;
110  case ActionKind::UPDATE:
111  // Roll back to map_[k] = v.
112  it->second = v;
113  break;
114  }
115  actions_.pop_back();
116  }
117  stack_.pop_back();
118  }
119 
120  private:
121  std::vector<Action> actions_;
122  std::vector<size_type> stack_;
123  UnorderedMapType map_;
124 };
125 } // namespace dreal
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
Update(k, v) means that (k, v) was replaced by a new value.