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.