diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/Makefile.am | 6 | ||||
-rw-r--r-- | src/expr/kind_map.h | 275 |
2 files changed, 279 insertions, 2 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 4ed5a3ac7..ced34b8be 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -11,7 +11,7 @@ libexpr_la_SOURCES = \ type_node.h \ type_node.cpp \ node_builder.h \ - convenience_node_builders.h \ + convenience_node_builders.h \ type.h \ type.cpp \ node_value.h \ @@ -27,7 +27,9 @@ libexpr_la_SOURCES = \ declaration_scope.cpp \ expr_manager_scope.h \ node_self_iterator.h \ - expr_stream.h + expr_stream.h \ + kind_map.h + nodist_libexpr_la_SOURCES = \ kind.h \ metakind.h \ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h new file mode 100644 index 000000000..a02339e5e --- /dev/null +++ b/src/expr/kind_map.h @@ -0,0 +1,275 @@ +/********************* */ +/*! \file kind_map.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A bitmap of Kinds + ** + ** This is a class representation for a bitmap of Kinds that is + ** iterable, manipulable, and packed. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__KIND_MAP_H +#define __CVC4__KIND_MAP_H + +#include <stdint.h> +#include <iterator> + +#include "expr/kind.h" + +namespace CVC4 { + +/** A bitmap of Kinds. */ +class KindMap { + static const size_t SIZE = (kind::LAST_KIND + 63) / 64; + + uint64_t d_bitmap[SIZE]; + + /** + * Accessor proxy class used so that things like "map[k] = true" + * will work as expected (we have to return a proxy from + * KindMap::operator[]() in that case, since we can't construct an + * address to the individual *bit* in the packed representation). + */ + class Accessor { + KindMap& d_map; + Kind d_kind; + + Accessor(KindMap& m, Kind k) : + d_map(m), + d_kind(k) { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + } + + friend class KindMap; + + public: + + operator bool() const { + return d_map.tst(d_kind); + } + + Accessor operator=(bool b) const { + if(b) { + d_map.set(d_kind); + } else { + d_map.clr(d_kind); + } + return *this; + } + + };/* class KindMap::Accessor */ + +public: + + /** An iterator over a KindMap. */ + class iterator { + const KindMap* d_map; + Kind d_kind; + + public: + typedef std::input_iterator_tag iterator_category; + typedef Kind value_type; + + iterator() : + d_map(NULL), + d_kind(Kind(0)) { + } + iterator(const KindMap& m, Kind k) : + d_map(&m), + d_kind(k) { + AssertArgument(k >= Kind(0) && k <= kind::LAST_KIND, k, "invalid kind"); + while(d_kind < kind::LAST_KIND && + ! d_map->tst(d_kind)) { + d_kind = Kind(uint64_t(d_kind) + 1); + } + } + iterator& operator++() { + if(d_kind < kind::LAST_KIND) { + d_kind = Kind(uint64_t(d_kind) + 1); + while(d_kind < kind::LAST_KIND && + ! d_map->tst(d_kind)) { + d_kind = Kind(uint64_t(d_kind) + 1); + } + } + return *this; + } + iterator operator++(int) const { + const_iterator i = *this; + ++i; + return i; + } + Kind operator*() const { + return d_kind; + } + bool operator==(iterator i) const { + return d_map == i.d_map && d_kind == i.d_kind; + } + bool operator!=(iterator i) const { + return !(*this == i); + } + };/* class KindMap::iterator */ + typedef iterator const_iterator; + + KindMap() { + clear(); + } + KindMap(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] = m.d_bitmap[i]; + } + } + KindMap(Kind k) { + clear(); + set(k); + } + + /** Empty the map. */ + void clear() { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] = uint64_t(0); + } + } + /** Tests whether the map is empty. */ + bool isEmpty() const { + for(unsigned i = 0; i < SIZE; ++i) { + if(d_bitmap[i] != uint64_t(0)) { + return false; + } + } + return true; + } + /** Test whether k is in the map. */ + bool tst(Kind k) const { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + return (d_bitmap[k / 64] >> (k % 64)) & uint64_t(1); + } + /** Set k in the map. */ + void set(Kind k) { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + d_bitmap[k / 64] |= (uint64_t(1) << (k % 64)); + } + /** Clear k from the map. */ + void clr(Kind k) { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + d_bitmap[k / 64] &= ~(uint64_t(1) << (k % 64)); + } + + /** Iterate over the map. */ + const_iterator begin() const { + return const_iterator(*this, Kind(0)); + } + const_iterator end() const { + return const_iterator(*this, kind::LAST_KIND); + } + + /** Invert the map. */ + KindMap operator~() const { + KindMap r; + for(unsigned i = 0; i < SIZE; ++i) { + r.d_bitmap[i] = ~d_bitmap[i]; + } + return r; + } + /** Bitwise-AND the map (with assignment). */ + KindMap& operator&=(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] &= m.d_bitmap[i]; + } + return *this; + } + /** Bitwise-AND the map. */ + KindMap operator&(const KindMap& m) const { + KindMap r(*this); + r &= m; + return r; + } + /** Bitwise-OR the map (with assignment). */ + KindMap& operator|=(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] |= m.d_bitmap[i]; + } + return *this; + } + /** Bitwise-OR the map. */ + KindMap operator|(const KindMap& m) const { + KindMap r(*this); + r |= m; + return r; + } + /** Bitwise-XOR the map (with assignment). */ + KindMap& operator^=(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] ^= m.d_bitmap[i]; + } + return *this; + } + /** Bitwise-XOR the map. */ + KindMap operator^(const KindMap& m) const { + KindMap r(*this); + r ^= m; + return r; + } + + /** Test whether k is in the map. */ + bool operator[](Kind k) const { + return tst(k); + } + /** Test whether k is in the map (allowing assignment). */ + Accessor operator[](Kind k) { + return Accessor(*this, k); + } + + /** Test equality between two maps. */ + bool operator==(KindMap m) { + for(unsigned i = 0; i < SIZE; ++i) { + if(d_bitmap[i] != m.d_bitmap[i]) { + return false; + } + } + return true; + } + bool operator!=(KindMap m) { + return !(*this == m); + } +};/* class KindMap */ + +inline KindMap operator~(Kind k) { + KindMap m(k); + return ~m; +} +inline KindMap operator&(Kind k1, Kind k2) { + KindMap m(k1); + return m &= k2; +} +inline KindMap operator&(Kind k1, KindMap m2) { + return m2 & k1; +} +inline KindMap operator|(Kind k1, Kind k2) { + KindMap m(k1); + return m |= k2; +} +inline KindMap operator|(Kind k1, KindMap m2) { + return m2 | k1; +} +inline KindMap operator^(Kind k1, Kind k2) { + KindMap m(k1); + return m ^= k2; +} +inline KindMap operator^(Kind k1, KindMap m2) { + return m2 ^ k1; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__KIND_MAP_H */ |