diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-02-25 02:11:14 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-02-25 02:11:14 +0000 |
commit | 48101a9e2416a16b645f31936776694a25cf9efd (patch) | |
tree | 0d7211a61c89299b6a7cef34cf83b74e73b473ec /src/theory/bv/cd_set_collection.h | |
parent | b71b7d0aa648f39ea1243632b5b9867ada53109a (diff) |
slicing manager is not breaking the old regressions, time to sync
Diffstat (limited to 'src/theory/bv/cd_set_collection.h')
-rw-r--r-- | src/theory/bv/cd_set_collection.h | 316 |
1 files changed, 316 insertions, 0 deletions
diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h new file mode 100644 index 000000000..bd26a3595 --- /dev/null +++ b/src/theory/bv/cd_set_collection.h @@ -0,0 +1,316 @@ +/* + * set_collection.h + * + * Created on: Feb 24, 2011 + * Author: dejan + */ + +#pragma once + +#include <iostream> +#include "context/cdo.h" + +namespace CVC4 { +namespace context { + +/** + * A class representing a backtrackable set of slice points. The memory should allow indexing with the TreeEntry.left and + * TreeEntry.right. TreeEntry should also provide null for the non-existing reference and a constructor with (value, + * left, right). + */ +template <typename memory_type, typename tree_entry_type, typename value_type, bool pass_value_by_reference = false> +class BacktrackableSetCollection { + + /** + * This is an interesting C++ question: how to make class applicable to non-by-value elements. If we turn + * below into const value_type& it doesn't work for the bit-slicing as size_t it is passed by value, and moreover + * we are using only a part of the word for the value. Hmmm. + */ + typedef value_type const_value_reference; + + /** Type of the reference */ + typedef typename tree_entry_type::reference_type reference_type; + + /** The null reference */ + static const reference_type null = tree_entry_type::null; + + /** The memory this set collection will use */ + memory_type d_memory; + + /** Backtrackable number of nodes that have been inserted */ + context::CDO<unsigned> d_nodesInserted; + + /** Backtrack */ + void backtrack() { + while (d_nodesInserted < d_memory.size()) { + const tree_entry_type& node = d_memory.back(); + if (node.hasParent()) { + if (node.isLeft()) { + d_memory[node.getParent()].removeLeft(); + } else { + d_memory[node.getParent()].removeRight(); + } + } + d_memory.pop_back(); + } + } + + inline void backtrack() const { + const_cast<BacktrackableSetCollection*>(this)->backtrack(); + } + + /** + * Create a new set. The set must have at least one element. + */ + 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_nodesInserted = d_nodesInserted + 1; + return index; + } + + /** + * Return the reference to the value if it's in the set or null otherwise + */ + reference_type find(reference_type set, const value_type& value) const { + while (set != null) { + const tree_entry_type& node = d_memory[set]; + if (node.getValue() == value) { + return set; + } else if (value < node.getValue()) { + set = node.getLeft(); + } else { + set = node.getRight(); + } + } + return null; + } + + /** + * Returns the maximal value in the set + */ + reference_type max(reference_type set) const { + Assert(set != null); + while (d_memory[set].hasRight()) { + set = d_memory[set].getRight(); + } + return set; + } + + /** + * Returns the minimal value in the set + */ + reference_type min(reference_type set) const { + Assert(set != null); + while (d_memory[set].hasLeft()) { + set = d_memory[set].getLeft(); + } + return set; + } + +public: + + BacktrackableSetCollection(context::Context* context) + : d_nodesInserted(context, 0) {} + + size_t size() const { + backtrack(); + return d_memory.size(); + } + + reference_type newSet(const value_type& value) { + backtrack(); + return newElement(value, null, null, null, false); + } + + void insert(memory_type& memory, reference_type root, const value_type& value) { + backtrack(); + if (root == null) { + return newSet(value); + } + // We already have a set, find the spot + reference_type parent = null; + while (true) { + parent = root; + if (value < d_memory[root].value) { + root = d_memory[root].left; + if (root == null) { + root = newElement(value, null, null, parent, true); + d_memory[parent].left = root; + return; + } + } else { + Assert(value != d_memory[root].value); + root = d_memory[root].right; + if (root == null) { + root = newElement(value, null, null, parent, false); + d_memory[parent].right = root; + return; + } + } + } + } + + /** + * Returns the maximal value in the set + */ + const_value_reference maxElement(reference_type set) const { + Assert(set != null); + backtrack(); + return d_memory[max(set)].getValue(); + } + + /** + * Returns the minimal value in the set + */ + const_value_reference minElement(reference_type set) const { + Assert(set != null); + backtrack(); + return d_memory[min(set)].getValue(); + } + + /** + * Return the previous (smaller) element. + */ + const_value_reference prev(reference_type set, const_value_reference value) { + backtrack(); + // Get the node of this value + reference_type node_ref = find(set, value); + Assert(node_ref != null); + const tree_entry_type& node = d_memory[node_ref]; + // For a left node, we know that it is smaller than all the parents and the parents other children + // The smaller node must then be the max of the left subtree + if (!node.hasParent() || node.isLeft()) { + return maxElement(node.getLeft()); + } + // For a right node, we know that it is bigger than the parent. But, we also know that the left subtree + // is also bigger than the parent + else { + if (node.hasLeft()) { + return maxElement(node.getLeft()); + } else { + Assert(node.hasParent()); + return d_memory[node.getParent()].getValue(); + } + } + } + + const_value_reference next(reference_type set, const_value_reference value) { + backtrack(); + // Get the node of this value + reference_type node_ref = find(set, value); + Assert(node_ref != null); + const tree_entry_type& node = d_memory[node_ref]; + // For a right node, we know that it is bigger than all the parents and the parents other children + // The bigger node must then be the min of the right subtree + if (!node.hasParent() || node.isRight()) { + return minElement(node.getRight()); + } + // For a left node, we know that it is smaller than the parent. But, we also know that the right subtree + // is also smaller than the parent + else { + if (node.hasRight()) { + return minElement(node.getRight()); + } else { + Assert(node.hasParent()); + return d_memory[node.getParent()].getValue(); + } + } + } + + /** + * Count the number of elements in the given bounds. + */ + unsigned count(reference_type set, const_value_reference lowerBound, const_value_reference upperBound) const { + Assert(lowerBound <= upperBound); + backtrack(); + // Empty set no elements + if (set == null) { + return 0; + } + // The counter + unsigned c = 0; + // Current set + const tree_entry_type& current = d_memory[set]; + // Left child (smaller elements) + if (lowerBound < current.getValue()) { + c += count(current.getLeft(), lowerBound, upperBound); + } + // Current element + if (lowerBound <= current.getValue() && current.getValue() <= upperBound) { + ++ c; + } + // Right child (bigger elements) + if (current.getValue() <= upperBound) { + c += count(current.getRight(), lowerBound, upperBound); + } + return c; + } + + /** + * Check for membership. + */ + bool contains(reference_type set, const_value_reference value) const { + backtrack(); + return count(set, value, value) > 0; + } + + /** + * Returns the elements (sorted) in the set between the given lower and upper bound. If include borders is on, + * and the + */ + void getElements(reference_type set, const_value_reference lowerBound, const_value_reference upperBound, std::vector<value_type>& output) const { + Assert(lowerBound <= upperBound); + backtrack(); + // Empty set no elements + if (set == null) { + return; + } + // Current set + const tree_entry_type& current = d_memory[set]; + // Left child (smaller elements) + if (lowerBound < current.getValue()) { + getElements(current.getLeft(), lowerBound, upperBound, output); + } + // Current element + if (lowerBound <= current.getValue() && current.getValue() <= upperBound) { + output.push_back(current.getValue()); + } + // Right child (bigger elements) + if (current.getValue() <= upperBound) { + getElements(current.getRight(), lowerBound, upperBound, output); + } + } + + /** + * Print the list of elements to the output. + */ + void print(std::ostream& out, reference_type set) { + backtrack(); + if (set == null) { + return; + } + const tree_entry_type& current = d_memory[set]; + if (current.hasLeft()) { + print(out, current.getLeft()); + out << ","; + } + out << current.getValue(); + if (current.hasRight()) { + out << ","; + print(out, current.getRight()); + } + } + + /** + * String representation of a set. + */ + std::string toString(reference_type set) { + stringstream out; + print(out, set); + return out.str(); + } +}; + +} // Namespace context +} // Namespace CVC4s |