From: Tim King Date: Wed, 8 Aug 2018 23:50:16 +0000 (-0700) Subject: Proposal for adding map utility functions to CVC4. (#2232) X-Git-Tag: cvc5-1.0.0~4796 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=987df3df987768e2ce0c36d17469929f8e92fdec;p=cvc5.git Proposal for adding map utility functions to CVC4. (#2232) * Proposal for adding map utility functions to CVC4. --- 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 +bool ContainsKey(const M& map, const Key& key) +{ + return map.find(key) != map.end(); +} + +template +using MapKeyTypeT = typename M::value_type::first_type; +template +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 +const MapMappedTypeT* FindOrNull(const M& map, const MapKeyTypeT& 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 +MapMappedTypeT* FindOrNull(M& map, const MapKeyTypeT& 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 +const MapMappedTypeT& FindOrDie(const M& map, const MapKeyTypeT& 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; public: - // The type of the value mapped to by this class. - using value_type = std::pair; + // The type of the 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::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 and break the const encapsulation + // when necessary. + using value_type = std::pair; 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(d_value.first); } + // See documentation of value_type for why this is needed. + Data& mutable_data() { return const_cast(d_value.second); } CDHashMap* 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 ); } } diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index d58ee411f..b3e0a3808 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -6,6 +6,7 @@ UNIT_TESTS = \ util/cardinality_public if WHITE_AND_BLACK_TESTS UNIT_TESTS += \ + base/map_util_black \ theory/evaluator_white \ theory/logic_info_white \ theory/theory_arith_white \ diff --git a/test/unit/base/map_util_black.h b/test/unit/base/map_util_black.h new file mode 100644 index 000000000..6d2d2bbc7 --- /dev/null +++ b/test/unit/base/map_util_black.h @@ -0,0 +1,216 @@ +/********************* */ +/*! \file map_util_black.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 Black box testing of map utility functions. + ** + ** Black box testing of map utility functions. + **/ + +#include +#include +#include +#include +#include +#include + +#include "base/map_util.h" +#include "context/cdhashmap.h" +#include "context/cdhashset.h" +#include "context/cdinsert_hashmap.h" +#include "context/context.h" + +using CVC4::ContainsKey; +using CVC4::FindOrDie; +using CVC4::FindOrNull; +using CVC4::context::CDHashMap; +using CVC4::context::CDInsertHashMap; +using CVC4::context::Context; +using std::string; + +class MapUtilBlack : public CxxTest::TestSuite +{ + public: + void setUp() {} + void tearDown() {} + + // Returns a map containing {"key"->"value", "other"->"entry"}. + static const std::map& DefaultMap() + { + static const std::map static_stored_map{{"key", "value"}, + {"other", "entry"}}; + return static_stored_map; + } + + void testMap() + { + std::map map = DefaultMap(); + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + if (string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + *found_value = "new value"; + } + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "new value"); + } + + void testConstantMap() + { + const std::map map = DefaultMap(); + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + + if (const string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + } + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry"); + // Cannot do death tests for FindOrDie. + } + + void testUnorderedMap() + { + std::unordered_map map(DefaultMap().begin(), + DefaultMap().end()); + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + if (string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + *found_value = "new value"; + } + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "new value"); + } + + void testConstUnorderedMap() + { + const std::unordered_map map(DefaultMap().begin(), + DefaultMap().end()); + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + + if (const string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + } + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry"); + // Cannot do death tests for FindOrDie. + } + + void testSet() + { + std::set set{"entry", "other"}; + TS_ASSERT(ContainsKey(set, "entry")); + TS_ASSERT(!ContainsKey(set, "non member")); + + const std::set const_set{"entry", "other"}; + TS_ASSERT(ContainsKey(const_set, "entry")); + TS_ASSERT(!ContainsKey(const_set, "non member")); + } + + void testUnorderedSet() + { + std::unordered_set set{"entry", "other"}; + TS_ASSERT(ContainsKey(set, "entry")); + TS_ASSERT(!ContainsKey(set, "non member")); + + const std::unordered_set const_set{"entry", "other"}; + TS_ASSERT(ContainsKey(const_set, "entry")); + TS_ASSERT(!ContainsKey(const_set, "non member")); + } + + // For each pair in source, inserts mapping from key to value + // using insert into dest. + template + void InsertAll(const std::map& source, M* dest) + { + for (const auto& key_value : source) + { + dest->insert(key_value.first, key_value.second); + } + } + + void testCDHashMap() + { + Context context; + CDHashMap map(&context); + InsertAll(DefaultMap(), &map); + + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + + if (const string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + } + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry"); + } + + void testConstCDHashMap() + { + Context context; + CDHashMap store(&context); + InsertAll(DefaultMap(), &store); + const auto& map = store; + + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + + if (const string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + } + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry"); + } + + void testCDInsertHashMap() + { + Context context; + CDInsertHashMap map(&context); + InsertAll(DefaultMap(), &map); + + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + + if (const string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + } + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry"); + } + + void testConstCDInsertHashMap() + { + Context context; + CDInsertHashMap store(&context); + InsertAll(DefaultMap(), &store); + const auto& map = store; + + TS_ASSERT(ContainsKey(map, "key")); + TS_ASSERT(!ContainsKey(map, "non key")); + if (const string* found_value = FindOrNull(map, "other")) + { + TS_ASSERT_EQUALS(*found_value, "entry"); + } + TS_ASSERT(FindOrNull(map, "non key") == nullptr); + TS_ASSERT_EQUALS(FindOrDie(map, "other"), "entry"); + } + +}; /* class MapUtilBlack */