From f35ac73547c2b9180de86f8622cfda8af07ee6b3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 19 Nov 2013 16:54:24 +0100 Subject: [PATCH] Splitted VectorSet in header/source file which caused certain minor changes in its interface. Fixed some issues in the Markov automaton parser and made it substantially faster by dropping sscanf. This however introduces other limitations that need to be addressed in the future. Former-commit-id: 44eb4aabc93df23ea7392355cca4332fef61a746 --- .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 6 +- .../MarkovAutomatonSparseTransitionParser.cpp | 97 ++---- .../MaximalEndComponentDecomposition.cpp | 2 +- src/storage/VectorSet.cpp | 282 ++++++++++++++++ src/storage/VectorSet.h | 317 ++++-------------- 6 files changed, 380 insertions(+), 326 deletions(-) create mode 100644 src/storage/VectorSet.cpp diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 8e9e23503..ccc5f06cf 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1312,7 +1312,7 @@ namespace storm { // (4.5) Read off result from variables. storm::storage::VectorSet usedLabelSet = getUsedLabelsInSolution(environmentModelPair.first, environmentModelPair.second, variableInformation); - usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end()); + usedLabelSet.insert(choiceInformation.knownLabels); // Display achieved probability. std::pair initialStateProbabilityPair = getReachabilityProbability(environmentModelPair.first, environmentModelPair.second, labeledMdp, variableInformation); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index e3fa9e394..2391b772b 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -228,7 +228,7 @@ namespace storm { // If the state is initial, we need to add all the choice labels to the initial label set. if (initialStates.get(currentState)) { - initialLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); + initialLabels.insert(choiceLabeling[currentChoice]); initialCombinations.insert(choiceLabeling[currentChoice]); } @@ -246,7 +246,7 @@ namespace storm { // If the choice can reach a target state directly, we add all the labels to the target label set. if (canReachTargetState) { - targetLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); + targetLabels.insert(choiceLabeling[currentChoice]); targetCombinations.insert(choiceLabeling[currentChoice]); } } @@ -1513,7 +1513,7 @@ namespace storm { // Restrict the given MDP to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); - commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); + commandSet.insert(relevancyInformation.knownLabels); storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index ac909d69f..52af4c6f2 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -43,29 +43,14 @@ namespace storm { // Record that the current source was the last source. lastsource = source; - char actionNameBuffer[20]; -#ifdef WINDOWS - int length = sscanf_s(buf, "%20s\n", actionNameBuffer, 20); -#else - int length = sscanf(buf, "%20s\n", actionNameBuffer); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else { - // If the action name was parsed successfully, we need to move by the corresponding number of characters. - buf += strlen(actionNameBuffer); - } - // Depending on the action name, the choice is either a probabilitic one or a markovian one. bool isMarkovianChoice = false; - if (strcmp(actionNameBuffer, "!") == 0) { + if (buf[0] == '!') { isMarkovianChoice = true; } else { isMarkovianChoice = false; } + ++buf; if (isMarkovianChoice) { if (stateHasMarkovianChoice) { @@ -89,33 +74,21 @@ namespace storm { // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state. do { - // Now parse the next symbol to see whether there is another target state for the current choice - // or not. - char star[1]; -#ifdef WINDOWS - length = sscanf_s(buf, "%1s\n", star, 1); -#else - length = sscanf(buf, "%1s\n", star); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length == EOF) { + // If the end of the file was reached, we need to abort and check whether we are in a legal state. + if (buf[0] == '\0') { if (!hasSuccessorState) { - LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."); - throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."; + LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << "."); + throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << "."; } else { // If there was at least one successor for the current choice, this is legal and we need to move on. encounteredEOF = true; } - } else if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else if (strcmp(star, "*") == 0) { + } else if (buf[0] == '*') { // We need to record that we found at least one successor state for the current choice. hasSuccessorState = true; // As we have encountered a "*", we know that there is an additional successor state for the current choice. - buf += strlen(star); + ++buf; // Now we need to read the successor state and check if we already saw a higher state index. target = checked_strtol(buf, &buf); @@ -161,11 +134,11 @@ namespace storm { while (buf[0] != '\0' && !encounteredEOF) { // At the current point, the next thing to read is the source state of the next choice to come. source = checked_strtol(buf, &buf); - + // If we have skipped some states, we need to insert self-loops if requested. if (source > lastsource + 1) { if (fixDeadlocks) { - for (uint_fast64_t index = lastsource + 1; index < source; ++source) { + for (uint_fast64_t index = lastsource + 1; index < source; ++index) { result.nondeterministicChoiceIndices[index] = currentChoice; result.transitionMatrix.addNextValue(currentChoice, index, 1); ++currentChoice; @@ -184,25 +157,9 @@ namespace storm { // Record that the current source was the last source. lastsource = source; - char actionNameBuffer[20]; -#ifdef WINDOWS - int length = sscanf_s(buf, "%20s\n", actionNameBuffer, 20); -#else - int length = sscanf(buf, "%20s\n", actionNameBuffer); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else { - // If the action name was parsed successfully, we need to move by the corresponding number of characters. - buf += strlen(actionNameBuffer); - } - // Depending on the action name, the choice is either a probabilitic one or a markovian one. bool isMarkovianChoice = false; - if (strcmp(actionNameBuffer, "!") == 0) { + if (buf[0] == '!') { isMarkovianChoice = true; // Mark the current state as a Markovian one. @@ -219,40 +176,24 @@ namespace storm { // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state. do { - // Now parse the next symbol to see whether there is another target state for the current choice - // or not. - char star[1]; -#ifdef WINDOWS - length = sscanf_s(buf, "%1s\n", star, 1); -#else - length = sscanf(buf, "%1s\n", star); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length == EOF) { - if (!hasSuccessorState) { - LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."); - throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."; - } else { - // If there was at least one successor for the current choice, this is legal and we need to move on. - encounteredEOF = true; - } - } else if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else if (strcmp(star, "*") == 0) { + // If the end of the file was reached, we need to abort and check whether we are in a legal state. + if (buf[0] == '\0') { + // Under the assumption that the currently open choice has at least one successor (which is given after the first run) + // we may legally stop reading here. + encounteredEOF = true; + } else if (buf[0] == '*') { // We need to record that we found at least one successor state for the current choice. hasSuccessorState = true; // As we have encountered a "*", we know that there is an additional successor state for the current choice. - buf += strlen(star); + ++buf; // Now we need to read the successor state and check if we already saw a higher state index. target = checked_strtol(buf, &buf); // And the corresponding probability/rate. double val = checked_strtod(buf, &buf); - + // Record the value as well as the exit rate in case of a Markovian choice. result.transitionMatrix.addNextValue(currentChoice, target, val); if (isMarkovianChoice) { diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 0a4fe4441..26035baf7 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -94,7 +94,7 @@ namespace storm { // Now erase the states that have no option to stay inside the MEC with all successors. mecChanged |= !statesToRemove.empty(); std::vector statesToRemoveList = statesToRemove.getSetIndicesList(); - scc.erase(storm::storage::VectorSet(statesToRemoveList.begin(), statesToRemoveList.end())); + scc.erase(storm::storage::VectorSet(statesToRemoveList)); // Now check which states should be reconsidered, because successors of them were removed. statesToCheck.clear(); diff --git a/src/storage/VectorSet.cpp b/src/storage/VectorSet.cpp new file mode 100644 index 000000000..5fcffae4a --- /dev/null +++ b/src/storage/VectorSet.cpp @@ -0,0 +1,282 @@ +#include "src/storage/VectorSet.h" + +namespace storm { + namespace storage { + template + VectorSet::VectorSet() : data(), dirty(false) { + // Intentionally left empty. + } + + template + VectorSet::VectorSet(uint_fast64_t size) : data(), dirty(false) { + data.reserve(size); + } + + template + VectorSet::VectorSet(std::vector const& data) : data(data), dirty(true) { + ensureSet(); + } + + template + VectorSet::VectorSet(std::set const& data) : dirty(false) { + this->data.reserve(data.size()); + for (auto const& element : data) { + this->data.push_back(element); + } + } + + template + VectorSet::VectorSet(uint_fast64_t from, uint_fast64_t to) : dirty(false) { + data.reserve(to - from); + + for (uint_fast64_t element = from; element < to; ++element) { + data.push_back(element); + } + } + + template + VectorSet::VectorSet(VectorSet const& other) : dirty(false) { + other.ensureSet(); + data = other.data; + } + + template + VectorSet& VectorSet::operator=(VectorSet const& other) { + data = other.data; + dirty = other.dirty; + return *this; + } + + template + VectorSet::VectorSet(VectorSet&& other) : data(std::move(other.data)), dirty(std::move(other.dirty)) { + // Intentionally left empty. + } + + template + VectorSet& VectorSet::operator=(VectorSet&& other) { + data = std::move(other.data); + dirty = std::move(other.dirty); + return *this; + } + + template + bool VectorSet::operator==(VectorSet const& other) const { + ensureSet(); + if (this->size() != other.size()) return false; + return std::equal(data.begin(), data.end(), other.begin()); + } + + template + bool VectorSet::operator<(VectorSet const& other) const { + ensureSet(); + if (this->size() < other.size()) return true; + if (this->size() > other.size()) return false; + for (auto it1 = this->begin(), it2 = other.begin(); it1 != this->end(); ++it1, ++it2) { + if (*it1 < *it2) return true; + if (*it1 > *it2) return false; + } + return false; + } + + template + bool VectorSet::operator>(VectorSet const& other) const { + ensureSet(); + if (this->size() > other.size()) return true; + if (this->size() < other.size()) return false; + for (auto it1 = this->begin(), it2 = other.begin(); it1 != this->end(); ++it1, ++it2) { + if (*it1 > *it2) return true; + if (*it1 < *it2) return false; + } + return false; + } + + template + void VectorSet::ensureSet() const { + if (dirty) { + std::sort(data.begin(), data.end()); + data.erase(std::unique(data.begin(), data.end()), data.end()); + dirty = false; + } + } + + template + bool VectorSet::contains(ValueType const& element) const { + ensureSet(); + return std::binary_search(data.begin(), data.end(), element); + } + + template + bool VectorSet::subsetOf(VectorSet const& other) const { + ensureSet(); + other.ensureSet(); + return std::includes(other.begin(), other.end(), data.begin(), data.end()); + } + + template + bool VectorSet::supersetOf(VectorSet const& other) const { + ensureSet(); + return other.subsetOf(*this); + } + + template + VectorSet VectorSet::intersect(VectorSet const& other) { + ensureSet(); + other.ensureSet(); + VectorSet result; + std::set_intersection(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); + return result; + } + + template + VectorSet VectorSet::join(VectorSet const& other) { + ensureSet(); + other.ensureSet(); + VectorSet result; + std::set_union(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); + return result; + } + + template + typename VectorSet::iterator VectorSet::begin() { + ensureSet(); + return data.begin(); + } + + template + typename VectorSet::iterator VectorSet::end() { + ensureSet(); + return data.end(); + } + + template + typename VectorSet::const_iterator VectorSet::begin() const { + ensureSet(); + return data.begin(); + } + + template + typename VectorSet::const_iterator VectorSet::end() const { + ensureSet(); + return data.end(); + } + + template + ValueType const& VectorSet::min() const { + if (this->size() == 0) { + throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; + } + + ensureSet(); + return data.front(); + } + + template + ValueType const& VectorSet::max() const { + if (this->size() == 0) { + throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; + } + + ensureSet(); + return data.back(); + } + + template + void VectorSet::insert(ValueType const& element) { + data.push_back(element); + dirty = true; + } + + template + typename VectorSet::iterator VectorSet::insert(typename VectorSet::const_iterator pos, ValueType const& element) { + dirty = true; + return data.insert(pos, element); + } + + template + void VectorSet::insert(VectorSet const& other) { + data.insert(data.end(), other.data.begin(), other.data.end()); + } + + template + bool VectorSet::empty() const { + ensureSet(); + return data.empty(); + } + + template + size_t VectorSet::size() const { + ensureSet(); + return data.size(); + } + + template + void VectorSet::clear() { + data.clear(); + dirty = false; + } + + template + bool VectorSet::erase(ValueType const& element) { + ensureSet(); + uint_fast64_t lowerBound = 0; + uint_fast64_t upperBound = data.size(); + while (lowerBound != upperBound) { + uint_fast64_t currentPosition = lowerBound + (upperBound - lowerBound) / 2; + bool searchInLowerHalf = element < data[currentPosition]; + if (searchInLowerHalf) { + upperBound = currentPosition; + } else { + bool searchInRightHalf = element > data[currentPosition]; + if (searchInRightHalf) { + lowerBound = currentPosition + 1; + } else { + // At this point we have found the element. + data.erase(data.begin() + currentPosition); + return true; + } + } + } + return false; + } + + template + void VectorSet::erase(VectorSet const& eraseSet) { + if (eraseSet.size() > 0) { + ensureSet(); + eraseSet.ensureSet(); + + for (typename std::vector::reverse_iterator delIt = eraseSet.data.rbegin(), setIt = data.rbegin(); delIt != eraseSet.data.rend() && setIt != eraseSet.data.rend(); ++delIt) { + while (setIt != eraseSet.data.rend() && *setIt > *delIt) { + ++setIt; + } + if (setIt != data.rend()) break; + + if (*setIt == *delIt) { + data.erase((setIt + 1).base()); + ++setIt; + } + } + } + } + + template + std::ostream& operator<<(std::ostream& stream, VectorSet const& set) { + set.ensureSet(); + stream << "VectorSet(" << set.size() << ") { "; + if (set.size() > 0) { + for (uint_fast64_t index = 0; index < set.size() - 1; ++index) { + stream << set.data[index] << ", "; + } + stream << set.data[set.size() - 1] << " }"; + } else { + stream << "}"; + } + return stream; + } + + template class VectorSet; + template class VectorSet>; + template std::ostream& operator<<(std::ostream& stream, VectorSet const& set); + template std::ostream& operator<<(std::ostream& stream, VectorSet> const& set); + } +} \ No newline at end of file diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h index 78057d684..e366611bd 100644 --- a/src/storage/VectorSet.h +++ b/src/storage/VectorSet.h @@ -19,254 +19,85 @@ namespace storm { namespace storage { - template + template class VectorSet { public: - typedef T* difference_type; - typedef T value_type; - typedef T* pointer; - typedef T& reference; - typedef typename std::vector::iterator iterator; - typedef typename std::vector::const_iterator const_iterator; - - VectorSet() : data(), dirty(false) { - // Intentionally left empty. - } - - VectorSet(uint_fast64_t size) : data(), dirty(false) { - data.reserve(size); - } - - VectorSet(std::vector const& data) : data(data), dirty(true) { - ensureSet(); - } - - VectorSet(std::set const& data) : dirty(false) { - this->data.reserve(data.size()); - for (auto const& element : data) { - this->data.push_back(element); - } - } - - VectorSet(uint_fast64_t from, uint_fast64_t to) : dirty(false) { - data.reserve(to - from); - - for (uint_fast64_t element = from; element < to; ++element) { - data.push_back(element); - } - } - - template - VectorSet(InputIterator first, InputIterator last) : data(first, last), dirty(true) { - ensureSet(); - } - - VectorSet(VectorSet const& other) : dirty(false) { - other.ensureSet(); - data = other.data; - } - - VectorSet& operator=(VectorSet const& other) { - data = other.data; - dirty = other.dirty; - return *this; - } - - VectorSet(VectorSet&& other) : data(std::move(other.data)), dirty(std::move(other.dirty)) { - // Intentionally left empty. - } - - VectorSet& operator=(VectorSet&& other) { - data = std::move(other.data); - dirty = std::move(other.dirty); - return *this; - } - - bool operator==(VectorSet const& other) const { - ensureSet(); - if (this->size() != other.size()) return false; - return std::equal(data.begin(), data.end(), other.begin()); - } - - bool operator<(VectorSet const& other) const { - ensureSet(); - if (this->size() < other.size()) return true; - if (this->size() > other.size()) return false; - for (auto it1 = this->begin(), it2 = other.begin(); it1 != this->end(); ++it1, ++it2) { - if (*it1 < *it2) return true; - if (*it1 > *it2) return false; - } - return false; - } - - void ensureSet() const { - if (dirty) { - std::sort(data.begin(), data.end()); - data.erase(std::unique(data.begin(), data.end()), data.end()); - dirty = false; - } - } - - bool contains(T const& element) const { - ensureSet(); - return std::binary_search(data.begin(), data.end(), element); - } - - bool subsetOf(VectorSet const& other) const { - ensureSet(); - other.ensureSet(); - return std::includes(other.begin(), other.end(), data.begin(), data.end()); - } - - bool supersetOf(VectorSet const& other) const { - ensureSet(); - return other.subsetOf(*this); - } - - VectorSet intersect(VectorSet const& other) { - ensureSet(); - other.ensureSet(); - VectorSet result; - std::set_intersection(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); - return result; - } - - VectorSet join(VectorSet const& other) { - ensureSet(); - other.ensureSet(); - VectorSet result; - std::set_union(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); - return result; - } - - iterator begin() { - ensureSet(); - return data.begin(); - } - - iterator end() { - ensureSet(); - return data.end(); - } - - const_iterator begin() const { - ensureSet(); - return data.begin(); - } - - const_iterator end() const { - ensureSet(); - return data.end(); - } - - T const& min() const { - if (this->size() == 0) { - throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; - } - - ensureSet(); - return data.first; - } - - T const& max() const { - if (this->size() == 0) { - throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; - } - - ensureSet(); - return data.back; - } - - void insert(T const& element) { - data.push_back(element); - dirty = true; - } - - template - iterator insert(InputIterator first, InputIterator last) { - dirty = true; - return data.insert(data.end(), first, last); - } - - template - iterator insert(InputIterator pos, T element) { - dirty = true; - return data.insert(pos, element); - } - - bool empty() const { - ensureSet(); - return data.empty(); - } - - size_t size() const { - ensureSet(); - return data.size(); - } - - void clear() { - data.clear(); - dirty = false; - } - - bool erase(T const& element) { - ensureSet(); - uint_fast64_t lowerBound = 0; - uint_fast64_t upperBound = data.size(); - while (lowerBound != upperBound) { - uint_fast64_t currentPosition = lowerBound + (upperBound - lowerBound) / 2; - bool searchInLowerHalf = element < data[currentPosition]; - if (searchInLowerHalf) { - upperBound = currentPosition; - } else { - bool searchInRightHalf = element > data[currentPosition]; - if (searchInRightHalf) { - lowerBound = currentPosition + 1; - } else { - // At this point we have found the element. - data.erase(data.begin() + currentPosition); - return true; - } - } - } - return false; - } - - void erase(VectorSet const& eraseSet) { - if (eraseSet.size() > 0) { - ensureSet(); - eraseSet.ensureSet(); - - for (typename std::vector::reverse_iterator delIt = eraseSet.data.rbegin(), setIt = data.rbegin(); delIt != eraseSet.data.rend() && setIt != eraseSet.data.rend(); ++delIt) { - while (setIt != eraseSet.data.rend() && *setIt > *delIt) { - ++setIt; - } - if (setIt != data.rend()) break; + typedef ValueType* difference_type; + typedef ValueType value_type; + typedef ValueType* pointer; + typedef ValueType& reference; + typedef typename std::vector::iterator iterator; + typedef typename std::vector::const_iterator const_iterator; + + VectorSet(); + + VectorSet(uint_fast64_t size); + + VectorSet(std::vector const& data); + + VectorSet(std::set const& data); + + VectorSet(uint_fast64_t from, uint_fast64_t to); - if (*setIt == *delIt) { - data.erase((setIt + 1).base()); - ++setIt; - } - } - } - } - - friend std::ostream& operator<< (std::ostream& stream, VectorSet const& set) { - set.ensureSet(); - stream << "VectorSet(" << set.size() << ") { "; - if (set.size() > 0) { - for (uint_fast64_t index = 0; index < set.size() - 1; ++index) { - stream << set.data[index] << ", "; - } - stream << set.data[set.size() - 1] << " }"; - } else { - stream << "}"; - } - return stream; - } + VectorSet(VectorSet const& other); + + VectorSet& operator=(VectorSet const& other); + + VectorSet(VectorSet&& other); + + VectorSet& operator=(VectorSet&& other); + + bool operator==(VectorSet const& other) const; + + bool operator<(VectorSet const& other) const; + + bool operator>(VectorSet const& other) const; + + void ensureSet() const; + + bool contains(ValueType const& element) const; + + bool subsetOf(VectorSet const& other) const; + + bool supersetOf(VectorSet const& other) const; + + VectorSet intersect(VectorSet const& other); + + VectorSet join(VectorSet const& other); + + iterator begin(); + + iterator end(); + + const_iterator begin() const; + + const_iterator end() const; + + ValueType const& min() const; + + ValueType const& max() const; + + void insert(ValueType const& element); + + iterator insert(const_iterator pos, ValueType const& element); + + void insert(VectorSet const& other); + + bool empty() const; + + size_t size() const; + + void clear(); + + bool erase(ValueType const& element); + + void erase(VectorSet const& eraseSet); + + template + friend std::ostream& operator<< (std::ostream& stream, VectorSet const& set); private: - mutable std::vector data; + mutable std::vector data; mutable bool dirty; }; }