summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/kind_map.h225
-rw-r--r--src/theory/uf/equality_engine.cpp33
-rw-r--r--src/theory/uf/equality_engine.h14
3 files changed, 52 insertions, 220 deletions
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index e9036838b..ef46c2093 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -20,216 +20,37 @@
#ifndef CVC4__KIND_MAP_H
#define CVC4__KIND_MAP_H
-#include <iterator>
+#include <bitset>
#include "base/check.h"
#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];
-
-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 equality between two maps. */
- bool operator==(const KindMap& m) const
+/** A very simple bitmap for Kinds */
+class KindMap
+{
+ public:
+ /** Set the bit for k */
+ void set(Kind k) { d_bits.set(fromKind(k)); }
+ /** Reset the bit for k */
+ void reset(Kind k) { d_bits.reset(fromKind(k)); }
+ /** Check whether the bit for k is set */
+ bool test(Kind k) const { return d_bits.test(fromKind(k)); }
+ /** Check whether the bit for k is set */
+ bool operator[](Kind k) const { return test(k); }
+
+ private:
+ /** Convert kind to std::size_t and check bounds */
+ static std::size_t fromKind(Kind k)
{
- for (size_t i = 0; i < SIZE; ++i)
- {
- if (d_bitmap[i] != m.d_bitmap[i])
- {
- return false;
- }
- }
- return true;
+ AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind");
+ return static_cast<std::size_t>(k);
}
- bool operator!=(const KindMap& m) const { 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;
-}
+ /** The bitmap */
+ std::bitset<kind::LAST_KIND> d_bits;
+};
-}/* CVC4 namespace */
+} // namespace CVC4
#endif /* CVC4__KIND_MAP_H */
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 2173c6922..7ad243073 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -276,16 +276,26 @@ EqualityNodeId EqualityEngine::newNode(TNode node) {
return newId;
}
-void EqualityEngine::addFunctionKind(Kind fun, bool interpreted, bool extOperator) {
- d_congruenceKinds |= fun;
- if (fun != kind::EQUAL) {
- if (interpreted) {
- Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl;
- d_congruenceKindsInterpreted |= fun;
+void EqualityEngine::addFunctionKind(Kind fun,
+ bool interpreted,
+ bool extOperator)
+{
+ d_congruenceKinds.set(fun);
+ if (fun != kind::EQUAL)
+ {
+ if (interpreted)
+ {
+ Debug("equality::evaluation")
+ << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted "
+ << std::endl;
+ d_congruenceKindsInterpreted.set(fun);
}
- if (extOperator) {
- Debug("equality::extoperator") << d_name << "::eq::addFunctionKind(): " << fun << " is an external operator kind " << std::endl;
- d_congruenceKindsExtOperators |= fun;
+ if (extOperator)
+ {
+ Debug("equality::extoperator")
+ << d_name << "::eq::addFunctionKind(): " << fun
+ << " is an external operator kind " << std::endl;
+ d_congruenceKindsExtOperators.set(fun);
}
}
}
@@ -1744,8 +1754,9 @@ void EqualityEngine::addTriggerPredicate(TNode predicate) {
// equality is handled separately
return addTriggerEquality(predicate);
}
- Assert(d_congruenceKinds.tst(predicate.getKind()))
- << "No point in adding non-congruence predicates, kind is " << predicate.getKind();
+ Assert(d_congruenceKinds.test(predicate.getKind()))
+ << "No point in adding non-congruence predicates, kind is "
+ << predicate.getKind();
if (d_done) {
return;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 70d5389c1..92665b358 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -683,22 +683,22 @@ private:
/**
* Returns true if this kind is used for congruence closure.
*/
- bool isFunctionKind(Kind fun) const {
- return d_congruenceKinds.tst(fun);
- }
+ bool isFunctionKind(Kind fun) const { return d_congruenceKinds.test(fun); }
/**
* Returns true if this kind is used for congruence closure + evaluation of constants.
*/
- bool isInterpretedFunctionKind(Kind fun) const {
- return d_congruenceKindsInterpreted.tst(fun);
+ bool isInterpretedFunctionKind(Kind fun) const
+ {
+ return d_congruenceKindsInterpreted.test(fun);
}
/**
* Returns true if this kind has an operator that is considered external (e.g. not internal).
*/
- bool isExternalOperatorKind(Kind fun) const {
- return d_congruenceKindsExtOperators.tst(fun);
+ bool isExternalOperatorKind(Kind fun) const
+ {
+ return d_congruenceKindsExtOperators.test(fun);
}
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback