Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
vector.h
Go to the documentation of this file.
1#ifndef STORM_UTILITY_VECTOR_H_
2#define STORM_UTILITY_VECTOR_H_
3
4#include <algorithm>
5#include <functional>
6#include <iosfwd>
7#include <numeric>
9
10#include <boost/optional.hpp>
11
16
18
19namespace storm {
20namespace utility {
21namespace vector {
22
23template<typename ValueType>
24struct VectorHash {
25 size_t operator()(std::vector<ValueType> const& vec) const {
26 std::hash<ValueType> hasher;
27 std::size_t seed = 0;
28 for (ValueType const& element : vec) {
29 seed ^= hasher(element) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
30 }
31 return seed;
32 }
33};
34
47template<class T>
48std::size_t findOrInsert(std::vector<T>& vector, T&& element) {
49 std::size_t position = std::find(vector.begin(), vector.end(), element) - vector.begin();
50 if (position == vector.size()) {
51 vector.emplace_back(std::move(element));
52 }
53 return position;
54}
55
56template<typename T>
57void setAllValues(std::vector<T>& vec, storm::storage::BitVector const& positions, T const& positiveValue = storm::utility::one<T>(),
58 T const& negativeValue = storm::utility::zero<T>()) {
59 if (positions.getNumberOfSetBits() * 2 > positions.size()) {
60 vec.resize(positions.size(), positiveValue);
61 uint64_t index = positions.getNextUnsetIndex(0);
62 while (index < positions.size()) {
63 vec[index] = negativeValue;
64 index = positions.getNextUnsetIndex(index + 1);
65 }
66 } else {
67 vec.resize(positions.size(), negativeValue);
68 for (uint64_t index : positions) {
69 vec[index] = positiveValue;
70 }
71 }
72}
73
81template<class T>
82void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
83 STORM_LOG_ASSERT(positions.size() <= vector.size(), "We cannot set positions that have not been initialized");
84 STORM_LOG_ASSERT(positions.getNumberOfSetBits() <= values.size(), "The number of selected positions (" << positions.getNumberOfSetBits()
85 << ") exceeds the size of the input vector ("
86 << values.size() << ").");
87 uint_fast64_t oldPosition = 0;
88 for (auto position : positions) {
89 vector[position] = values[oldPosition++];
90 }
91}
92
101template<class T>
102void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, T value) {
103 STORM_LOG_ASSERT(positions.size() <= vector.size(), "We cannot set positions that have not been initialized");
104 for (auto position : positions) {
105 vector[position] = value;
106 }
107}
108
109template<typename T>
110void setNonzeroIndices(std::vector<T> const& vec, storm::storage::BitVector& bv) {
111 STORM_LOG_ASSERT(bv.size() == vec.size(), "Bitvector size should match vector size");
112 for (uint64_t i = 0; i < vec.size(); ++i) {
113 if (!storm::utility::isZero(vec[i])) {
114 bv.set(i, true);
115 }
116 }
117}
118
124template<class OutputIterator, class Size, class Assignable>
125void iota_n(OutputIterator first, Size n, Assignable value) {
126 std::generate_n(first, n, [&value]() { return value++; });
127}
128
132template<typename T>
133inline std::vector<T> buildVectorForRange(T min, T max) {
134 STORM_LOG_ASSERT(min <= max, "Invalid range.");
135 T diff = max - min;
136 std::vector<T> v;
137 v.reserve(diff);
138 iota_n(std::back_inserter(v), diff, min);
139 return v;
140}
141
147template<typename T>
148std::vector<uint_fast64_t> getSortedIndices(std::vector<T> const& v) {
149 std::vector<uint_fast64_t> res = buildVectorForRange<uint_fast64_t>(0, v.size());
150 std::sort(res.begin(), res.end(), [&v](uint_fast64_t index1, uint_fast64_t index2) { return v[index1] > v[index2]; });
151 return res;
152}
153
157template<typename T>
158bool isUnique(std::vector<T> const& v) {
159 if (v.size() < 2) {
160 return true;
161 }
162 auto sortedIndices = getSortedIndices(v);
163 auto indexIt = sortedIndices.begin();
164 T const* previous = &v[*indexIt];
165 for (++indexIt; indexIt != sortedIndices.end(); ++indexIt) {
166 T const& current = v[*indexIt];
167 if (current == *previous) {
168 return false;
169 }
170 previous = &current;
171 }
172 return true;
173}
174
175template<typename T, typename Comparator>
176bool compareElementWise(std::vector<T> const& left, std::vector<T> const& right, Comparator comp = std::less<T>()) {
177 STORM_LOG_ASSERT(left.size() == right.size(), "Expected that vectors for comparison have equal size");
178 return std::equal(left.begin(), left.end(), right.begin(), comp);
179}
180
187template<class T>
188void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
189 STORM_LOG_ASSERT(positions.getNumberOfSetBits() <= vector.size(), "The number of selected positions (" << positions.getNumberOfSetBits()
190 << ") exceeds the size of the target vector ("
191 << vector.size() << ").");
192 STORM_LOG_ASSERT(positions.size() == values.size(),
193 "Size mismatch of the positions vector (" << positions.size() << ") and the values vector (" << values.size() << ").");
194 auto targetIt = vector.begin();
195 for (auto position : positions) {
196 *targetIt = values[position];
197 ++targetIt;
198 }
199}
200
209template<class T>
210void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping,
211 std::vector<T> const& values) {
212 auto targetIt = vector.begin();
213 for (auto position : positions) {
214 for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
215 *targetIt = values[i];
216 }
217 }
218}
219
229template<class T>
230void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGrouping,
231 std::vector<T> const& values) {
232 auto targetIt = vector.begin();
233 for (uint_fast64_t i = 0; i < vector.size(); ++i, ++targetIt) {
234 *targetIt = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]];
235 }
236}
237
245template<class T>
246void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& indexSequence, std::vector<T> const& values) {
247 STORM_LOG_ASSERT(indexSequence.size() <= vector.size(),
248 "The number of selected positions (" << indexSequence.size() << ") exceeds the size of the target vector (" << vector.size() << ").");
249
250 for (uint_fast64_t vectorIndex = 0; vectorIndex < vector.size(); ++vectorIndex) {
251 vector[vectorIndex] = values[indexSequence[vectorIndex]];
252 }
253}
254
264template<class T>
265void selectVectorValuesRepeatedly(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping,
266 std::vector<T> const& values) {
267 auto targetIt = vector.begin();
268 for (auto position : positions) {
269 for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
270 *targetIt = values[position];
271 }
272 }
273}
274
280template<class T>
281void subtractFromConstantOneVector(std::vector<T>& vector) {
282 for (auto& element : vector) {
283 element = storm::utility::one<T>() - element;
284 }
285}
286
287template<class T>
288void addFilteredVectorGroupsToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter,
289 std::vector<uint_fast64_t> const& rowGroupIndices) {
290 auto targetIt = target.begin();
291 for (auto group : filter) {
292 auto it = source.cbegin() + rowGroupIndices[group];
293 auto ite = source.cbegin() + rowGroupIndices[group + 1];
294 for (; it != ite; ++targetIt, ++it) {
295 *targetIt += *it;
296 }
297 }
298}
299
308template<class T>
309void addVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, std::vector<uint_fast64_t> const& rowGroupIndices) {
310 auto targetIt = target.begin();
311 auto sourceIt = source.cbegin();
312 auto sourceIte = source.cend();
313 auto rowGroupIt = rowGroupIndices.cbegin();
314
315 for (; sourceIt != sourceIte; ++sourceIt) {
316 uint_fast64_t current = *rowGroupIt;
317 ++rowGroupIt;
318 uint_fast64_t next = *rowGroupIt;
319 for (; current < next; ++targetIt, ++current) {
320 *targetIt += *sourceIt;
321 }
322 }
323}
324
333template<class T>
334void addFilteredVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter,
335 std::vector<uint_fast64_t> const& rowGroupIndices) {
336 auto targetIt = target.begin();
337 for (auto group : filter) {
338 uint_fast64_t current = rowGroupIndices[group];
339 uint_fast64_t next = rowGroupIndices[group + 1];
340 for (; current < next; ++current, ++targetIt) {
341 *targetIt += source[group];
342 }
343 }
344}
345
354template<class InValueType1, class InValueType2, class OutValueType, class Operation>
355void applyPointwiseTernary(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target,
356 Operation f = Operation()) {
357 auto firstIt = firstOperand.begin();
358 auto firstIte = firstOperand.end();
359 auto secondIt = secondOperand.begin();
360 auto targetIt = target.begin();
361 while (firstIt != firstIte) {
362 *targetIt = f(*firstIt, *secondIt, *targetIt);
363 ++targetIt;
364 ++firstIt;
365 ++secondIt;
366 }
367}
368
377template<class InValueType1, class InValueType2, class OutValueType, class Operation>
378void applyPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target,
379 Operation f = Operation()) {
380 std::transform(firstOperand.begin(), firstOperand.end(), secondOperand.begin(), target.begin(), f);
381}
382
390template<class InValueType, class OutValueType, class Operation>
391void applyPointwise(std::vector<InValueType> const& operand, std::vector<OutValueType>& target, Operation f = Operation()) {
392 std::transform(operand.begin(), operand.end(), target.begin(), f);
393}
394
402template<class InValueType1, class InValueType2, class OutValueType>
403void addVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
404 applyPointwise<InValueType1, InValueType2, OutValueType, std::plus<>>(firstOperand, secondOperand, target);
405}
406
414template<class InValueType1, class InValueType2, class OutValueType>
415void subtractVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
416 applyPointwise<InValueType1, InValueType2, OutValueType, std::minus<>>(firstOperand, secondOperand, target);
417}
418
426template<class InValueType1, class InValueType2, class OutValueType>
427void multiplyVectorsPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand,
428 std::vector<OutValueType>& target) {
429 applyPointwise<InValueType1, InValueType2, OutValueType, std::multiplies<>>(firstOperand, secondOperand, target);
430}
431
439template<class InValueType1, class InValueType2, class OutValueType>
440void divideVectorsPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
441 applyPointwise<InValueType1, InValueType2, OutValueType, std::divides<>>(firstOperand, secondOperand, target);
442}
443
450template<class ValueType1, class ValueType2>
451void scaleVectorInPlace(std::vector<ValueType1>& target, ValueType2 const& factor) {
452 applyPointwise<ValueType1, ValueType1>(target, target, [&](ValueType1 const& argument) -> ValueType1 { return argument * factor; });
453}
454
463template<class InValueType1, class InValueType2, class InValueType3>
464void addScaledVector(std::vector<InValueType1>& firstOperand, std::vector<InValueType2> const& secondOperand, InValueType3 const& factor) {
465 applyPointwise<InValueType1, InValueType2, InValueType1>(
466 firstOperand, secondOperand, firstOperand, [&](InValueType1 const& val1, InValueType2 const& val2) -> InValueType1 { return val1 + (factor * val2); });
467}
468
476template<class T>
477T dotProduct(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand) {
478 return std::inner_product(firstOperand.begin(), firstOperand.end(), secondOperand.begin(), storm::utility::zero<T>());
479}
480
489template<class T>
490storm::storage::BitVector filter(std::vector<T> const& values, std::function<bool(T const& value)> const& function) {
491 storm::storage::BitVector result(values.size(), false);
492
493 uint_fast64_t currentIndex = 0;
494 for (auto const& value : values) {
495 if (function(value)) {
496 result.set(currentIndex, true);
497 }
498 ++currentIndex;
499 }
500
501 return result;
502}
503
511template<class T>
512storm::storage::BitVector filterGreaterZero(std::vector<T> const& values) {
513 return filter<T>(values, [](T const& value) -> bool { return value > storm::utility::zero<T>(); });
514}
515
522template<class T>
523storm::storage::BitVector filterZero(std::vector<T> const& values) {
524 return filter<T>(values, storm::utility::isZero<T>);
525}
526
533template<class T>
534storm::storage::BitVector filterOne(std::vector<T> const& values) {
535 return filter<T>(values, storm::utility::isOne<T>);
536}
537
544template<class T>
545storm::storage::BitVector filterInfinity(std::vector<T> const& values) {
546 return filter<T>(values, storm::utility::isInfinity<T>);
547}
548
555template<typename VT>
556VT sum_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
557 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
558 VT sum = storm::utility::zero<VT>();
559 for (auto pos : filter) {
560 sum += values[pos];
561 }
562 return sum;
563}
564
571template<typename VT>
572VT max_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
573 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
574 STORM_LOG_ASSERT(!filter.empty(), "Empty selection.");
575
576 auto it = filter.begin();
577 auto ite = filter.end();
578
579 VT current = values[*it];
580 ++it;
581
582 for (; it != ite; ++it) {
583 current = std::max(values[*it], current);
584 }
585 return current;
586}
587
594template<typename VT>
595VT min_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
596 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
597 STORM_LOG_ASSERT(!filter.empty(), "Empty selection.");
598
599 auto it = filter.begin();
600 auto ite = filter.end();
601
602 VT current = values[*it];
603 ++it;
604
605 for (; it != ite; ++it) {
606 current = std::min(values[*it], current);
607 }
608 return current;
609}
610
621template<class T, class Filter>
622void reduceVector(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices) {
623 Filter f;
624 typename std::vector<T>::iterator targetIt = target.begin();
625 typename std::vector<T>::iterator targetIte = target.end();
626 typename std::vector<uint_fast64_t>::const_iterator rowGroupingIt = rowGrouping.begin();
627 typename std::vector<T>::const_iterator sourceIt = source.begin();
628 typename std::vector<T>::const_iterator sourceIte;
629 typename std::vector<uint_fast64_t>::iterator choiceIt;
630 if (choices) {
631 choiceIt = choices->begin();
632 }
633
634 // Variables for correctly tracking choices (only update if new choice is strictly better).
635 T oldSelectedChoiceValue;
636 uint64_t selectedChoice;
637
638 uint64_t currentRow = 0;
639 for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt, ++choiceIt) {
640 // Only traverse elements if the row group is non-empty.
641 if (*rowGroupingIt != *(rowGroupingIt + 1)) {
642 *targetIt = *sourceIt;
643
644 if (choices) {
645 selectedChoice = 0;
646 if (*choiceIt == 0) {
647 oldSelectedChoiceValue = *targetIt;
648 }
649 }
650
651 ++sourceIt;
652 ++currentRow;
653
654 for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++currentRow) {
655 if (choices && *rowGroupingIt + *choiceIt == currentRow) {
656 oldSelectedChoiceValue = *sourceIt;
657 }
658
659 if (f(*sourceIt, *targetIt)) {
660 *targetIt = *sourceIt;
661 if (choices) {
662 selectedChoice = std::distance(source.begin(), sourceIt) - *rowGroupingIt;
663 }
664 }
665 }
666
667 if (choices && f(*targetIt, oldSelectedChoiceValue)) {
668 *choiceIt = selectedChoice;
669 }
670 } else {
671 *choiceIt = 0;
672 *targetIt = storm::utility::zero<T>();
673 }
674 }
675}
676
685template<class T>
686void reduceVectorMin(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping,
687 std::vector<uint_fast64_t>* choices = nullptr) {
688 reduceVector<T, storm::utility::ElementLess<T>>(source, target, rowGrouping, choices);
689}
690
699template<class T>
700void reduceVectorMax(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping,
701 std::vector<uint_fast64_t>* choices = nullptr) {
702 reduceVector<T, storm::utility::ElementGreater<T>>(source, target, rowGrouping, choices);
703}
704
714template<class T>
715void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector<T> const& source, std::vector<T>& target,
716 std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
717 if (dir == storm::solver::OptimizationDirection::Minimize) {
718 reduceVectorMin(source, target, rowGrouping, choices);
719 } else {
720 reduceVectorMax(source, target, rowGrouping, choices);
721 }
722}
723
734template<class T>
735bool equalModuloPrecision(T const& val1, T const& val2, T const& precision, bool relativeError = true) {
736 if (relativeError) {
737 if (storm::utility::isZero<T>(val1)) {
738 return storm::utility::isZero(val2);
739 }
740 T relDiff = (val1 - val2) / val1;
741 if (storm::utility::abs(relDiff) > precision) {
742 return false;
743 }
744 } else {
745 T diff = val1 - val2;
746 if (storm::utility::abs(diff) > precision) {
747 return false;
748 }
749 }
750 return true;
751}
752
753// Specializiation for double as the relative check for doubles very close to zero is not meaningful.
754template<>
755inline bool equalModuloPrecision(double const& val1, double const& val2, double const& precision, bool relativeError) {
756 if (relativeError) {
758 return storm::utility::isAlmostZero(val1);
759 }
760 double relDiff = (val1 - val2) / val1;
761 if (storm::utility::abs(relDiff) > precision) {
762 return false;
763 }
764 } else {
765 double diff = val1 - val2;
766 if (storm::utility::abs(diff) > precision) {
767 return false;
768 }
769 }
770 return true;
771}
772
782template<class T>
783bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T const& precision, bool relativeError) {
784 STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
785
786 auto leftIt = vectorLeft.begin();
787 auto leftIte = vectorLeft.end();
788 auto rightIt = vectorRight.begin();
789 for (; leftIt != leftIte; ++leftIt, ++rightIt) {
790 if (!equalModuloPrecision(*leftIt, *rightIt, precision, relativeError)) {
791 return false;
792 }
793 }
794
795 return true;
796}
797
809template<class T>
810bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, storm::storage::BitVector const& positions, T const& precision,
811 bool relativeError) {
812 STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
813
814 for (auto position : positions) {
815 if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {
816 return false;
817 }
818 }
819
820 return true;
821}
822
834template<class T>
835bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T const& precision,
836 bool relativeError) {
837 STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
838
839 for (uint_fast64_t position : positions) {
840 if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {
841 return false;
842 }
843 }
844
845 return true;
846}
847
848template<class T>
849T maximumElementAbs(std::vector<T> const& vector) {
850 T res = storm::utility::zero<T>();
851 for (auto const& element : vector) {
852 res = std::max(res, storm::utility::abs(element));
853 }
854 return res;
855}
856
857template<class T>
858T maximumElementDiff(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight) {
859 T maxDiff = storm::utility::zero<T>();
860 auto leftIt = vectorLeft.begin();
861 auto leftIte = vectorLeft.end();
862 auto rightIt = vectorRight.begin();
863 for (; leftIt != leftIte; ++leftIt, ++rightIt) {
864 T diff = *leftIt - *rightIt;
865 T possDiff = storm::utility::abs(diff);
866 maxDiff = maxDiff < possDiff ? possDiff : maxDiff;
867 }
868 return maxDiff;
869}
870
871template<class T>
872T computeSquaredNorm2Difference(std::vector<T> const& b1, std::vector<T> const& b2) {
873 STORM_LOG_ASSERT(b1.size() == b2.size(), "Vector sizes mismatch.");
874
875 T result = storm::utility::zero<T>();
876
877 auto b1It = b1.begin();
878 auto b1Ite = b1.end();
879 auto b2It = b2.begin();
880
881 for (; b1It != b1Ite; ++b1It, ++b2It) {
882 result += storm::utility::pow<T>(*b1It - *b2It, 2);
883 }
884
885 return result;
886}
887
891template<typename ValueType>
892void clip(std::vector<ValueType>& x, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound) {
893 for (auto& entry : x) {
894 if (lowerBound && entry < lowerBound.get()) {
895 entry = lowerBound.get();
896 } else if (upperBound && entry > upperBound.get()) {
897 entry = upperBound.get();
898 }
899 }
900}
901
905template<typename ValueType>
906void clip(std::vector<ValueType>& x, ValueType const& bound, bool boundFromBelow) {
907 for (auto& entry : x) {
908 if (boundFromBelow && entry < bound) {
909 entry = bound;
910 } else if (!boundFromBelow && entry > bound) {
911 entry = bound;
912 }
913 }
914}
915
919template<typename ValueType>
920void clip(std::vector<ValueType>& x, std::vector<ValueType> const& bounds, bool boundFromBelow) {
921 auto boundsIt = bounds.begin();
922 for (auto& entry : x) {
923 if (boundFromBelow && entry < *boundsIt) {
924 entry = *boundsIt;
925 } else if (!boundFromBelow && entry > *boundsIt) {
926 entry = *boundsIt;
927 }
928 ++boundsIt;
929 }
930}
931
940template<class T>
941std::vector<T> getConstrainedOffsetVector(std::vector<T> const& offsetVector, storm::storage::BitVector const& constraint) {
942 // Reserve the known amount of slots for the resulting vector.
943 std::vector<uint_fast64_t> subVector(constraint.getNumberOfSetBits() + 1);
944 uint_fast64_t currentRowCount = 0;
945 uint_fast64_t currentIndexCount = 1;
946
947 // Set the first element as this will clearly begin at offset 0.
948 subVector[0] = 0;
949
950 // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over
951 // to the resulting vector.
952 for (auto index : constraint) {
953 subVector[currentIndexCount] = currentRowCount + offsetVector[index + 1] - offsetVector[index];
954 currentRowCount += offsetVector[index + 1] - offsetVector[index];
955 ++currentIndexCount;
956 }
957
958 // Put a sentinel element at the end.
959 subVector[constraint.getNumberOfSetBits()] = currentRowCount;
960
961 return subVector;
962}
963
969template<typename TargetType, typename SourceType>
970std::vector<TargetType> convertNumericVector(std::vector<SourceType> const& oldVector) {
971 std::vector<TargetType> resultVector;
972 resultVector.reserve(oldVector.size());
973 for (auto const& oldValue : oldVector) {
974 resultVector.push_back(storm::utility::convertNumber<TargetType>(oldValue));
975 }
976 return resultVector;
977}
978
988template<typename TargetType, typename SourceType>
989void convertNumericVector(std::vector<SourceType> const& inputVector, std::vector<TargetType>& targetVector) {
990 assert(inputVector.size() == targetVector.size());
991 applyPointwise(inputVector, targetVector, [](SourceType const& v) { return storm::utility::convertNumber<TargetType>(v); });
992}
993
997template<typename NewValueType, typename ValueType>
998std::vector<NewValueType> toValueType(std::vector<ValueType> const& oldVector) {
999 std::vector<NewValueType> resultVector;
1000 resultVector.reserve(oldVector.size());
1001 for (auto const& oldValue : oldVector) {
1002 resultVector.push_back(static_cast<NewValueType>(oldValue));
1003 }
1004 return resultVector;
1005}
1006
1007template<typename ValueType, typename TargetValueType>
1008typename std::enable_if<std::is_same<ValueType, storm::RationalNumber>::value, std::pair<std::vector<TargetValueType>, ValueType>>::type toIntegralVector(
1009 std::vector<ValueType> const& vec) {
1010 // Collect the numbers occurring in the input vector
1011 std::set<ValueType> occurringNonZeroNumbers;
1012 for (auto const& v : vec) {
1013 if (!storm::utility::isZero(v)) {
1014 occurringNonZeroNumbers.insert(v);
1015 }
1016 }
1017
1018 // Compute the scaling factor
1019 ValueType factor;
1020 if (occurringNonZeroNumbers.empty()) {
1021 factor = storm::utility::one<ValueType>();
1022 } else if (occurringNonZeroNumbers.size() == 1) {
1023 factor = *occurringNonZeroNumbers.begin();
1024 } else {
1025 // Obtain the least common multiple of the denominators of the occurring numbers.
1026 // We can then multiply the numbers with the lcm to obtain integers.
1027 auto numberIt = occurringNonZeroNumbers.begin();
1028 ValueType lcm = storm::utility::asFraction(*numberIt).second;
1029 for (++numberIt; numberIt != occurringNonZeroNumbers.end(); ++numberIt) {
1030 lcm = carl::lcm(lcm, storm::utility::asFraction(*numberIt).second);
1031 }
1032 // Multiply all values with the lcm. To reduce the range of considered integers, we also obtain the gcd of the results.
1033 numberIt = occurringNonZeroNumbers.begin();
1034 ValueType gcd = *numberIt * lcm;
1035 for (++numberIt; numberIt != occurringNonZeroNumbers.end(); ++numberIt) {
1036 gcd = carl::gcd(gcd, static_cast<ValueType>(*numberIt * lcm));
1037 }
1038
1039 factor = gcd / lcm;
1040 }
1041
1042 // Build the result
1043 std::vector<TargetValueType> result;
1044 result.reserve(vec.size());
1045 for (auto const& v : vec) {
1046 ValueType vScaled = v / factor;
1047 STORM_LOG_ASSERT(storm::utility::isInteger(vScaled), "Resulting number '(" << v << ")/(" << factor << ") = " << vScaled << "' is not integral.");
1048 result.push_back(storm::utility::convertNumber<TargetValueType, ValueType>(vScaled));
1049 }
1050 return std::make_pair(std::move(result), std::move(factor));
1051}
1052
1053template<typename ValueType, typename TargetValueType>
1054typename std::enable_if<!std::is_same<ValueType, storm::RationalNumber>::value, std::pair<std::vector<TargetValueType>, ValueType>>::type toIntegralVector(
1055 std::vector<ValueType> const& vec) {
1056 // TODO: avoid converting back and forth
1057 auto rationalNumberVec = convertNumericVector<storm::RationalNumber>(vec);
1058 auto rationalNumberResult = toIntegralVector<storm::RationalNumber, TargetValueType>(rationalNumberVec);
1059
1060 return std::make_pair(std::move(rationalNumberResult.first), storm::utility::convertNumber<ValueType>(rationalNumberResult.second));
1061}
1062
1063template<typename Type>
1064std::vector<Type> filterVector(std::vector<Type> const& in, storm::storage::BitVector const& filter) {
1065 std::vector<Type> result;
1066 result.reserve(filter.getNumberOfSetBits());
1067 for (auto index : filter) {
1068 result.push_back(in[index]);
1069 }
1070 STORM_LOG_ASSERT(result.size() == filter.getNumberOfSetBits(), "Result does not match.");
1071 return result;
1072}
1073
1074template<typename Type>
1075void filterVectorInPlace(std::vector<Type>& v, storm::storage::BitVector const& filter) {
1076 STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector");
1077 uint_fast64_t size = v.size();
1078 // we can start our work at the first index where the filter has value zero
1079 uint_fast64_t firstUnsetIndex = filter.getNextUnsetIndex(0);
1080 if (firstUnsetIndex < size) {
1081 auto vIt = v.begin() + firstUnsetIndex;
1082 for (uint_fast64_t index = filter.getNextSetIndex(firstUnsetIndex + 1); index != size; index = filter.getNextSetIndex(index + 1)) {
1083 *vIt = std::move(v[index]);
1084 ++vIt;
1085 }
1086 v.resize(vIt - v.begin());
1087 v.shrink_to_fit();
1088 }
1089 STORM_LOG_ASSERT(v.size() == filter.getNumberOfSetBits(), "Result does not match.");
1090}
1091
1092template<typename T>
1093bool hasNegativeEntry(std::vector<T> const& v) {
1094 return std::any_of(v.begin(), v.end(), [](T value) { return value < storm::utility::zero<T>(); });
1095}
1096
1097template<typename T>
1098bool hasPositiveEntry(std::vector<T> const& v) {
1099 return std::any_of(v.begin(), v.end(), [](T value) { return value > storm::utility::zero<T>(); });
1100}
1101
1102template<typename T>
1103bool hasNonZeroEntry(std::vector<T> const& v) {
1104 return std::any_of(v.begin(), v.end(), [](T value) { return !storm::utility::isZero(value); });
1105}
1106
1107template<typename T>
1108bool hasZeroEntry(std::vector<T> const& v) {
1109 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isZero(value); });
1110}
1111
1112template<typename T>
1113bool hasInfinityEntry(std::vector<T> const& v) {
1114 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isInfinity(value); });
1115}
1116
1117template<typename T>
1118std::vector<T> applyInversePermutation(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source) {
1119 std::vector<T> result;
1120 result.reserve(source.size());
1121 for (uint64_t sourceIndex : inversePermutation) {
1122 result.push_back(source[sourceIndex]);
1123 }
1124 return result;
1125}
1126
1127template<typename T>
1128std::vector<T> applyInversePermutationToGroupedVector(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source,
1129 std::vector<uint64_t> const& rowGroupIndices) {
1130 STORM_LOG_ASSERT(inversePermutation.size() == rowGroupIndices.size() - 1, "Inverse permutation and row group indices do not match.");
1131 std::vector<T> result;
1132 result.reserve(source.size());
1133 for (auto sourceGroupIndex : inversePermutation) {
1134 for (uint64_t sourceIndex = rowGroupIndices[sourceGroupIndex]; sourceIndex < rowGroupIndices[sourceGroupIndex + 1]; ++sourceIndex) {
1135 result.push_back(source[sourceIndex]);
1136 }
1137 }
1138 STORM_LOG_ASSERT(result.size() == source.size(), "result has unexpected length.");
1139 return result;
1140}
1141
1148template<typename ValueType>
1149std::string toString(std::vector<ValueType> const& vector) {
1150 std::stringstream stream;
1151 stream << "vector (" << vector.size() << ") [ ";
1152 if (!vector.empty()) {
1153 for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
1154 stream << vector[i] << ", ";
1155 }
1156 stream << vector.back();
1157 }
1158 stream << " ]";
1159 return stream.str();
1160}
1161
1162template<typename PT1, typename PT2>
1163std::string toString(std::vector<std::pair<PT1, PT2>> const& vector) {
1164 std::stringstream stream;
1165 stream << "vector (" << vector.size() << ") [ ";
1166 if (!vector.empty()) {
1167 for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
1168 stream << "{" << vector[i].first << "," << vector[i].second << "}, ";
1169 }
1170 stream << "{" << vector.back().first << "," << vector.back().second << "}";
1171 }
1172 stream << " ]";
1173 return stream.str();
1174}
1175
1176} // namespace vector
1177} // namespace utility
1178} // namespace storm
1179
1180#endif /* STORM_UTILITY_VECTOR_H_ */
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
void set(uint_fast64_t index, bool value=true)
Sets the given truth value at the given index.
size_t size() const
Retrieves the number of bits this bit vector can store.
uint_fast64_t getNextUnsetIndex(uint_fast64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to false in the bit vector.
uint_fast64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:11
std::size_t findOrInsert(std::vector< T > &vector, T &&element)
Finds the given element in the given vector.
Definition vector.h:48
std::vector< TargetType > convertNumericVector(std::vector< SourceType > const &oldVector)
Converts the given vector to the given ValueType Assumes that both, TargetType and SourceType are num...
Definition vector.h:970
storm::storage::BitVector filter(std::vector< T > const &values, std::function< bool(T const &value)> const &function)
Retrieves a bit vector containing all the indices for which the value at this position makes the give...
Definition vector.h:490
void applyPointwiseTernary(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target, Operation f=Operation())
Applies the given operation pointwise on the two given vectors and writes the result to the third vec...
Definition vector.h:355
VT min_if(std::vector< VT > const &values, storm::storage::BitVector const &filter)
Computes the minimum of the entries from the values that are selected by the (non-empty) filter.
Definition vector.h:595
void addVectors(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Adds the two given vectors and writes the result to the target vector.
Definition vector.h:403
void divideVectorsPointwise(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Divides the two given vectors (pointwise) and writes the result to the target vector.
Definition vector.h:440
T dotProduct(std::vector< T > const &firstOperand, std::vector< T > const &secondOperand)
Computes the dot product (aka scalar product) and returns the result.
Definition vector.h:477
std::vector< NewValueType > toValueType(std::vector< ValueType > const &oldVector)
Converts the given vector to the given ValueType.
Definition vector.h:998
bool hasInfinityEntry(std::vector< T > const &v)
Definition vector.h:1113
void addVectorToGroupedVector(std::vector< T > &target, std::vector< T > const &source, std::vector< uint_fast64_t > const &rowGroupIndices)
Adds the source vector to the target vector in a way such that the i-th entry is added to all element...
Definition vector.h:309
void setNonzeroIndices(std::vector< T > const &vec, storm::storage::BitVector &bv)
Definition vector.h:110
VT max_if(std::vector< VT > const &values, storm::storage::BitVector const &filter)
Computes the maximum of the entries from the values that are selected by the (non-empty) filter.
Definition vector.h:572
void setVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Sets the provided values at the provided positions in the given vector.
Definition vector.h:82
bool compareElementWise(std::vector< T > const &left, std::vector< T > const &right, Comparator comp=std::less< T >())
Definition vector.h:176
std::vector< T > buildVectorForRange(T min, T max)
Constructs a vector [min, min+1, ...., max-1].
Definition vector.h:133
void setAllValues(std::vector< T > &vec, storm::storage::BitVector const &positions, T const &positiveValue=storm::utility::one< T >(), T const &negativeValue=storm::utility::zero< T >())
Definition vector.h:57
void addFilteredVectorGroupsToGroupedVector(std::vector< T > &target, std::vector< T > const &source, storm::storage::BitVector const &filter, std::vector< uint_fast64_t > const &rowGroupIndices)
Definition vector.h:288
bool equalModuloPrecision(T const &val1, T const &val2, T const &precision, bool relativeError=true)
Compares the given elements and determines whether they are equal modulo the given precision.
Definition vector.h:735
void selectVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< T > const &values)
Selects the elements from a vector at the specified positions and writes them consecutively into anot...
Definition vector.h:188
T computeSquaredNorm2Difference(std::vector< T > const &b1, std::vector< T > const &b2)
Definition vector.h:872
bool isUnique(std::vector< T > const &v)
Returns true iff every element in the given vector is unique, i.e., there are no i,...
Definition vector.h:158
T maximumElementDiff(std::vector< T > const &vectorLeft, std::vector< T > const &vectorRight)
Definition vector.h:858
void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector< T > const &source, std::vector< T > &target, std::vector< uint_fast64_t > const &rowGrouping, std::vector< uint_fast64_t > *choices=nullptr)
Reduces the given source vector by selecting either the smallest or the largest out of each row group...
Definition vector.h:715
storm::storage::BitVector filterGreaterZero(std::vector< T > const &values)
Retrieves a bit vector containing all the indices for which the value at this position is greater tha...
Definition vector.h:512
void reduceVector(std::vector< T > const &source, std::vector< T > &target, std::vector< uint_fast64_t > const &rowGrouping, std::vector< uint_fast64_t > *choices)
Reduces the given source vector by selecting an element according to the given filter out of each row...
Definition vector.h:622
void addScaledVector(std::vector< InValueType1 > &firstOperand, std::vector< InValueType2 > const &secondOperand, InValueType3 const &factor)
Computes x:= x + a*y, i.e., adds each element of the first vector and (the corresponding element of t...
Definition vector.h:464
std::string toString(std::vector< ValueType > const &vector)
Output vector as string.
Definition vector.h:1149
void multiplyVectorsPointwise(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Multiplies the two given vectors (pointwise) and writes the result to the target vector.
Definition vector.h:427
bool hasPositiveEntry(std::vector< T > const &v)
Definition vector.h:1098
storm::storage::BitVector filterOne(std::vector< T > const &values)
Retrieves a bit vector containing all the indices for which the value at this position is equal to on...
Definition vector.h:534
bool hasNegativeEntry(std::vector< T > const &v)
Definition vector.h:1093
T maximumElementAbs(std::vector< T > const &vector)
Definition vector.h:849
void clip(std::vector< ValueType > &x, boost::optional< ValueType > const &lowerBound, boost::optional< ValueType > const &upperBound)
Takes the input vector and ensures that all entries conform to the bounds.
Definition vector.h:892
void addFilteredVectorToGroupedVector(std::vector< T > &target, std::vector< T > const &source, storm::storage::BitVector const &filter, std::vector< uint_fast64_t > const &rowGroupIndices)
Adds the source vector to the target vector in a way such that the i-th selected entry is added to al...
Definition vector.h:334
void selectVectorValuesRepeatedly(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< uint_fast64_t > const &rowGrouping, std::vector< T > const &values)
Selects values from a vector at the specified positions and writes them into another vector as often ...
Definition vector.h:265
void applyPointwise(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target, Operation f=Operation())
Applies the given operation pointwise on the two given vectors and writes the result to the third vec...
Definition vector.h:378
void reduceVectorMin(std::vector< T > const &source, std::vector< T > &target, std::vector< uint_fast64_t > const &rowGrouping, std::vector< uint_fast64_t > *choices=nullptr)
Reduces the given source vector by selecting the smallest element out of each row group.
Definition vector.h:686
VT sum_if(std::vector< VT > const &values, storm::storage::BitVector const &filter)
Sum the entries from values that are set to one in the filter vector.
Definition vector.h:556
storm::storage::BitVector filterInfinity(std::vector< T > const &values)
Retrieves a bit vector containing all the indices for which the value at this position is equal to on...
Definition vector.h:545
std::vector< T > applyInversePermutation(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source)
Definition vector.h:1118
void filterVectorInPlace(std::vector< Type > &v, storm::storage::BitVector const &filter)
Definition vector.h:1075
void iota_n(OutputIterator first, Size n, Assignable value)
Iota function as a helper for efficient creating a range in a vector.
Definition vector.h:125
void subtractVectors(std::vector< InValueType1 > const &firstOperand, std::vector< InValueType2 > const &secondOperand, std::vector< OutValueType > &target)
Subtracts the two given vectors and writes the result to the target vector.
Definition vector.h:415
std::vector< uint_fast64_t > getSortedIndices(std::vector< T > const &v)
Returns a list of indices such that the first index refers to the highest entry of the given vector,...
Definition vector.h:148
bool hasZeroEntry(std::vector< T > const &v)
Definition vector.h:1108
storm::storage::BitVector filterZero(std::vector< T > const &values)
Retrieves a bit vector containing all the indices for which the value at this position is equal to ze...
Definition vector.h:523
void scaleVectorInPlace(std::vector< ValueType1 > &target, ValueType2 const &factor)
Multiplies each element of the given vector with the given factor and writes the result into the vect...
Definition vector.h:451
std::vector< T > applyInversePermutationToGroupedVector(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source, std::vector< uint64_t > const &rowGroupIndices)
Definition vector.h:1128
std::vector< T > getConstrainedOffsetVector(std::vector< T > const &offsetVector, storm::storage::BitVector const &constraint)
Takes the given offset vector and applies the given contraint.
Definition vector.h:941
bool hasNonZeroEntry(std::vector< T > const &v)
Definition vector.h:1103
void subtractFromConstantOneVector(std::vector< T > &vector)
Subtracts the given vector from the constant one-vector and writes the result to the input vector.
Definition vector.h:281
void reduceVectorMax(std::vector< T > const &source, std::vector< T > &target, std::vector< uint_fast64_t > const &rowGrouping, std::vector< uint_fast64_t > *choices=nullptr)
Reduces the given source vector by selecting the largest element out of each row group.
Definition vector.h:700
std::enable_if< std::is_same< ValueType, storm::RationalNumber >::value, std::pair< std::vector< TargetValueType >, ValueType > >::type toIntegralVector(std::vector< ValueType > const &vec)
Definition vector.h:1008
std::vector< Type > filterVector(std::vector< Type > const &in, storm::storage::BitVector const &filter)
Definition vector.h:1064
ValueType max(ValueType const &first, ValueType const &second)
ValueType min(ValueType const &first, ValueType const &second)
bool isAlmostZero(ValueType const &a)
Definition constants.cpp:56
std::pair< ValueType, ValueType > asFraction(ValueType const &number)
bool isZero(ValueType const &a)
Definition constants.cpp:41
bool isInteger(ValueType const &number)
Definition constants.cpp:76
ValueType abs(ValueType const &number)
LabParser.cpp.
Definition cli.cpp:18
size_t operator()(std::vector< ValueType > const &vec) const
Definition vector.h:25