surprize surprize

1 files changed, 275 insertions, 0 deletions

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 */