diff options
author | Tim King <taking@cs.nyu.edu> | 2018-08-08 16:50:16 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-08 16:50:16 -0700 |
commit | 987df3df987768e2ce0c36d17469929f8e92fdec (patch) | |
tree | 6d85a85966084879e55b8ab04c330662a4cfe7f0 /src | |
parent | ece17ee2c38fa5769ae3ab7fa3607c0e88c0021f (diff) |
Proposal for adding map utility functions to CVC4. (#2232)
* Proposal for adding map utility functions to CVC4.
Diffstat (limited to 'src')
-rw-r--r-- | src/base/Makefile.am | 1 | ||||
-rw-r--r-- | src/base/map_util.h | 97 | ||||
-rw-r--r-- | src/context/cdhashmap.h | 21 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 18 |
4 files changed, 129 insertions, 8 deletions
diff --git a/src/base/Makefile.am b/src/base/Makefile.am index 3619b226e..3706f57a3 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -26,6 +26,7 @@ libbase_la_SOURCES = \ exception.h \ listener.cpp \ listener.h \ + map_util.h \ modal_exception.h \ output.cpp \ output.h diff --git a/src/base/map_util.h b/src/base/map_util.h new file mode 100644 index 000000000..2e17c9290 --- /dev/null +++ b/src/base/map_util.h @@ -0,0 +1,97 @@ +/********************* */ +/*! \file map_util.h + ** \verbatim + ** Top contributors (to current version): + ** Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility functions for dealing with maps in a mostly uniform fashion. + ** + ** Utility functions for dealing with maps and related classed in a mostly + ** uniform fashion. These are stylistically encouraged (but not required) in + ** new code. Supports: + ** - std::map + ** - std::unordered_map + ** - CVC4::context::CDHashmap + ** - CVC4::context::CDInsertHashmap + ** The ContainsKey function is also compatible with std::[unordered_]set. + ** + ** Currently implemented classes of functions: + ** - ContainsKey + ** Returns true if a map contains a key. (Also Supports std::set and + ** std::unordered_set.) + ** - FindOr* + ** Finds an data element mapped to by the map. Variants include FindOrNull + ** and FindOrDie. + ** + ** Potential future classes of functions: + ** - InsertOrUpdate + ** - InsertIfNotPresent + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BASE__MAP_UTIL_H +#define __CVC4__BASE__MAP_UTIL_H + +#include "base/cvc4_check.h" + +namespace CVC4 { + +// Returns true if the `map` contains the `key`. +// +// Supports sets as well. +template <class M, class Key> +bool ContainsKey(const M& map, const Key& key) +{ + return map.find(key) != map.end(); +} + +template <typename M> +using MapKeyTypeT = typename M::value_type::first_type; +template <typename M> +using MapMappedTypeT = typename M::value_type::second_type; + +// Returns a pointer to the const value mapped by `key` if it exists, or nullptr +// otherwise. +template <class M> +const MapMappedTypeT<M>* FindOrNull(const M& map, const MapKeyTypeT<M>& key) +{ + auto it = map.find(key); + if (it == map.end()) + { + return nullptr; + } + return &((*it).second); +} + +// Returns a pointer to the non-const value mapped by `key` if it exists, or +// nullptr otherwise. +template <class M> +MapMappedTypeT<M>* FindOrNull(M& map, const MapKeyTypeT<M>& key) +{ + auto it = map.find(key); + if (it == map.end()) + { + return nullptr; + } + return &((*it).second); +} + +// Returns a const reference to the value mapped by `key` if it exists. Dies +// if the element is not there. +template <class M> +const MapMappedTypeT<M>& FindOrDie(const M& map, const MapKeyTypeT<M>& key) +{ + auto it = map.find(key); + CVC4_CHECK(it != map.end()) << "The map does not contain the key."; + return (*it).second; +} + +} // namespace CVC4 + +#endif /* __CVC4__BASE__MAP_UTIL_H */ diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h index 958c48e22..ae530f106 100644 --- a/src/context/cdhashmap.h +++ b/src/context/cdhashmap.h @@ -101,13 +101,26 @@ class CDOhash_map : public ContextObj { friend class CDHashMap<Key, Data, HashFcn>; public: - // The type of the <Key, Data> value mapped to by this class. - using value_type = std::pair<Key, Data>; + // The type of the <Key, Data> pair mapped by this class. + // + // Implementation: + // The data and key visible to users of CDHashMap are only visible through + // const references. Thus the type of dereferencing a + // CDHashMap<Key, Data>::iterator.second is intended to always be a + // `const Data&`. (Otherwise, to get a Data& safely, access operations + // would need to makeCurrent() to get the Data&, which is an unacceptable + // performance hit.) To allow for the desired updating in other scenarios, we + // store a std::pair<const Key, const Data> and break the const encapsulation + // when necessary. + using value_type = std::pair<const Key, const Data>; private: value_type d_value; - Key& mutable_key() { return d_value.first; } - Data& mutable_data() { return d_value.second; } + + // See documentation of value_type for why this is needed. + Key& mutable_key() { return const_cast<Key&>(d_value.first); } + // See documentation of value_type for why this is needed. + Data& mutable_data() { return const_cast<Data&>(d_value.second); } CDHashMap<Key, Data, HashFcn>* d_map; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 7094ad541..cfa50bef8 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -15,6 +15,7 @@ **/ #include "theory/quantifiers/fmf/bounded_integers.h" + #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/first_order_model.h" @@ -451,11 +452,20 @@ void BoundedIntegers::checkOwnership(Node f) success = true; //set Attributes on literals for( unsigned b=0; b<2; b++ ){ - if( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ){ - Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() ); + if (bound_lit_map[b].find(v) != bound_lit_map[b].end()) + { + // WARNING_CANDIDATE: + // This assertion may fail. We intentionally do not enable this in + // production as it is considered safe for this to fail. We fail + // in debug mode to have this instances raised to our attention. + Assert(bound_lit_pol_map[b].find(v) + != bound_lit_pol_map[b].end()); BoundIntLitAttribute bila; - bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 ); - }else{ + bound_lit_map[b][v].setAttribute(bila, + bound_lit_pol_map[b][v] ? 1 : 0); + } + else + { Assert( it->second!=BOUND_INT_RANGE ); } } |