diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 19:50:48 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-20 19:50:48 +0000 |
commit | 73b8b6c6ea8004225e99225f1e1f7666a5a49593 (patch) | |
tree | 84a5ad9c206ef7c8b42d919b0f1def06a1468c24 /src/theory/bv/cd_set_collection.h | |
parent | 8dd7462696b1d354f2dbdf840e9f50226f4c489a (diff) |
more bugfixes for bitvectors
Diffstat (limited to 'src/theory/bv/cd_set_collection.h')
-rw-r--r-- | src/theory/bv/cd_set_collection.h | 94 |
1 files changed, 89 insertions, 5 deletions
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index aeb28ab7b..d020ef362 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -40,10 +40,19 @@ class BacktrackableSetCollection { /** Backtrackable number of nodes that have been inserted */ context::CDO<unsigned> d_nodesInserted; + /** Check if the reference is valid in the current context */ + inline bool isValid(reference_type set) const { + return d_nodesInserted == d_memory.size() && (set == null || set < d_memory.size()); + } + /** Backtrack */ void backtrack() { while (d_nodesInserted < d_memory.size()) { const tree_entry_type& node = d_memory.back(); + + Debug("cd_set_collection") << "BacktrackableSetCollection::backtrack(): removing " << node.getValue() + << " from " << internalToString(getRoot(d_memory.size()-1)) << std::endl; + if (node.hasParent()) { if (node.isLeft()) { d_memory[node.getParent()].removeLeft(); @@ -64,7 +73,7 @@ class BacktrackableSetCollection { */ reference_type newElement(const value_type& value, reference_type left, reference_type right, reference_type parent, bool isLeft) { reference_type index = d_memory.size(); - d_memory.push_back(tree_entry_type(value, left, right, value, isLeft)); + d_memory.push_back(tree_entry_type(value, left, right, parent, isLeft)); d_nodesInserted = d_nodesInserted + 1; return index; } @@ -91,6 +100,7 @@ class BacktrackableSetCollection { */ reference_type max(reference_type set) const { Assert(set != null); + Assert(isValid(set)); while (d_memory[set].hasRight()) { set = d_memory[set].getRight(); } @@ -102,12 +112,54 @@ class BacktrackableSetCollection { */ reference_type min(reference_type set) const { Assert(set != null); + Assert(isValid(set)); while (d_memory[set].hasLeft()) { set = d_memory[set].getLeft(); } return set; } + /** + * REturns the root of the tree + */ + reference_type getRoot(reference_type set) const { + // We don't check validity as this is used in backtracking + while (set != null && d_memory[set].hasParent()) { + Assert(set > d_memory[set].getParent()); + set = d_memory[set].getParent(); + } + return set; + } + + /** + * Print the list of elements to the output. + */ + void internalPrint(std::ostream& out, reference_type set) const { + if (set == null) { + return; + } + const tree_entry_type& current = d_memory[set]; + if (current.hasLeft()) { + internalPrint(out, current.getLeft()); + out << ","; + } + out << current.getValue(); + if (current.hasRight()) { + out << ","; + internalPrint(out, current.getRight()); + } + } + + /** + * String representation of a set. + */ + std::string internalToString(reference_type set) const { + std::stringstream out; + internalPrint(out, set); + return out.str(); + } + + public: BacktrackableSetCollection(context::Context* context) @@ -118,6 +170,20 @@ public: return d_memory.size(); } + size_t size(reference_type set) const { + backtrack(); + Assert(isValid(set)); + if (set == null) return 0; + size_t n = 1; + if (d_memory[set].hasLeft()) { + n += size(d_memory[set].getLeft()); + } + if (d_memory[set].hasRight()) { + n += size(d_memory[set].getRight()); + } + return n; + } + reference_type newSet(const value_type& value) { backtrack(); return newElement(value, null, null, null, false); @@ -125,6 +191,7 @@ public: void insert(reference_type& root, const value_type& value) { backtrack(); + Assert(isValid(root)); if (root == null) { root = newSet(value); return; @@ -133,20 +200,24 @@ public: reference_type parent = null; reference_type current = root; while (true) { - parent = current; + Assert(isValid(current)); if (value < d_memory[current].getValue()) { if (d_memory[current].hasLeft()) { + parent = current; current = d_memory[current].getLeft(); } else { - d_memory[current].setLeft(newElement(value, null, null, parent, true)); + d_memory[current].setLeft(newElement(value, null, null, current, true)); + Assert(d_memory[current].hasLeft()); return; } } else { - Assert(value != d_memory[root].getValue()); + Assert(value != d_memory[current].getValue()); if (d_memory[current].hasRight()) { + parent = current; current = d_memory[current].getRight(); } else { - d_memory[parent].setRight(newElement(value, null, null, parent, false)); + d_memory[current].setRight(newElement(value, null, null, current, false)); + Assert(d_memory[current].hasRight()); return; } } @@ -158,6 +229,7 @@ public: */ const_value_reference maxElement(reference_type set) const { Assert(set != null); + Assert(isValid(set)); backtrack(); return d_memory[max(set)].getValue(); } @@ -167,6 +239,7 @@ public: */ const_value_reference minElement(reference_type set) const { Assert(set != null); + Assert(isValid(set)); backtrack(); return d_memory[min(set)].getValue(); } @@ -176,6 +249,7 @@ public: */ const_value_reference prev(reference_type set, const_value_reference value) { backtrack(); + Assert(isValid(set)); const_value_reference candidate_value; bool candidate_found = false; @@ -202,6 +276,7 @@ public: const_value_reference next(reference_type set, const_value_reference value) { backtrack(); + Assert(isValid(set)); const_value_reference candidate_value; bool candidate_found = false; @@ -232,6 +307,8 @@ public: unsigned count(reference_type set, const_value_reference lowerBound, const_value_reference upperBound) const { Assert(lowerBound <= upperBound); backtrack(); + Assert(isValid(set)); + // Empty set no elements if (set == null) { return 0; @@ -260,6 +337,7 @@ public: */ bool contains(reference_type set, const_value_reference value) const { backtrack(); + Assert(isValid(set)); return count(set, value, value) > 0; } @@ -270,6 +348,7 @@ public: void getElements(reference_type set, const_value_reference lowerBound, const_value_reference upperBound, std::vector<value_type>& output) const { Assert(lowerBound <= upperBound); backtrack(); + Assert(isValid(set)); Debug("set_collection") << "BacktrackableSetCollection::getElements(" << toString(set) << "," << lowerBound << "," << upperBound << ")" << std::endl; @@ -298,6 +377,8 @@ public: */ void print(std::ostream& out, reference_type set) const { backtrack(); + Assert(isValid(set)); + if (set == null) { return; } @@ -317,6 +398,9 @@ public: * String representation of a set. */ std::string toString(reference_type set) const { + backtrack(); + Assert(isValid(set)); + std::stringstream out; print(out, set); return out.str(); |