Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
vector.h
Go to the documentation of this file.
1#pragma once
2
3#include <algorithm>
4#include <boost/optional.hpp>
5#include <functional>
6#include <iosfwd>
7#include <numeric>
8
15
16namespace storm {
17namespace utility {
18namespace vector {
19
20template<typename ValueType>
21struct VectorHash {
22 size_t operator()(std::vector<ValueType> const& vec) const {
23 std::hash<ValueType> hasher;
24 std::size_t seed = 0;
25 for (ValueType const& element : vec) {
26 seed ^= hasher(element) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
27 }
28 return seed;
29 }
30};
31
44template<class T>
45std::size_t findOrInsert(std::vector<T>& vector, T&& element) {
46 std::size_t position = std::find(vector.begin(), vector.end(), element) - vector.begin();
47 if (position == vector.size()) {
48 vector.emplace_back(std::forward<T>(element));
49 }
50 return position;
51}
52
53template<typename T>
54void setAllValues(std::vector<T>& vec, storm::storage::BitVector const& positions, T const& positiveValue = storm::utility::one<T>(),
55 T const& negativeValue = storm::utility::zero<T>()) {
56 if (positions.getNumberOfSetBits() * 2 > positions.size()) {
57 vec.resize(positions.size(), positiveValue);
58 uint64_t index = positions.getNextUnsetIndex(0);
59 while (index < positions.size()) {
60 vec[index] = negativeValue;
61 index = positions.getNextUnsetIndex(index + 1);
62 }
63 } else {
64 vec.resize(positions.size(), negativeValue);
65 for (uint64_t index : positions) {
66 vec[index] = positiveValue;
67 }
68 }
69}
70
78template<class T, class S>
79void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<S> const& values) {
80 STORM_LOG_ASSERT(positions.size() <= vector.size(), "We cannot set positions that have not been initialized.");
81 STORM_LOG_ASSERT(positions.getNumberOfSetBits() <= values.size(), "The number of selected positions (" << positions.getNumberOfSetBits()
82 << ") exceeds the size of the input vector ("
83 << values.size() << ").");
84 uint_fast64_t oldPosition = 0;
85 for (uint64_t position : positions) {
86 vector[position] = values[oldPosition++];
87 }
88}
89
98template<class T, class S>
99void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, S const& value) {
100 STORM_LOG_ASSERT(positions.size() <= vector.size(), "We cannot set positions that have not been initialized.");
101 for (uint64_t position : positions) {
102 vector[position] = value;
103 }
104}
105
106template<typename T>
107void setNonzeroIndices(std::vector<T> const& vec, storm::storage::BitVector& bv) {
108 STORM_LOG_ASSERT(bv.size() == vec.size(), "Bitvector size should match vector size.");
109 for (uint64_t i = 0; i < vec.size(); ++i) {
110 if (!storm::utility::isZero(vec[i])) {
111 bv.set(i, true);
112 }
113 }
114}
115
121template<class OutputIterator, class Size, class Assignable>
122void iota_n(OutputIterator first, Size n, Assignable value) {
123 std::generate_n(first, n, [&value]() { return value++; });
124}
125
129template<typename T>
130inline std::vector<T> buildVectorForRange(T min, T max) {
131 STORM_LOG_ASSERT(min <= max, "Invalid range.");
132 T diff = max - min;
133 std::vector<T> v;
134 v.reserve(diff);
135 iota_n(std::back_inserter(v), diff, min);
136 return v;
137}
138
144template<typename T>
145std::vector<uint_fast64_t> getSortedIndices(std::vector<T> const& v) {
146 std::vector<uint_fast64_t> res = buildVectorForRange<uint_fast64_t>(0, v.size());
147 std::sort(res.begin(), res.end(), [&v](uint_fast64_t index1, uint_fast64_t index2) { return v[index1] > v[index2]; });
148 return res;
149}
150
154template<typename T>
155bool isUnique(std::vector<T> const& v) {
156 if (v.size() < 2) {
157 return true;
158 }
159 auto sortedIndices = getSortedIndices(v);
160 auto indexIt = sortedIndices.begin();
161 T const* previous = &v[*indexIt];
162 for (++indexIt; indexIt != sortedIndices.end(); ++indexIt) {
163 T const& current = v[*indexIt];
164 if (current == *previous) {
165 return false;
166 }
167 previous = &current;
168 }
169 return true;
170}
171
172template<typename T, typename Comparator>
173bool compareElementWise(std::vector<T> const& left, std::vector<T> const& right, Comparator comp = std::less<T>()) {
174 STORM_LOG_ASSERT(left.size() == right.size(), "Expected that vectors for comparison have equal size.");
175 return std::equal(left.begin(), left.end(), right.begin(), comp);
176}
177
184template<class T>
185void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
186 STORM_LOG_ASSERT(positions.getNumberOfSetBits() <= vector.size(), "The number of selected positions (" << positions.getNumberOfSetBits()
187 << ") exceeds the size of the target vector ("
188 << vector.size() << ").");
189 STORM_LOG_ASSERT(positions.size() == values.size(),
190 "Size mismatch of the positions vector (" << positions.size() << ") and the values vector (" << values.size() << ").");
191 auto targetIt = vector.begin();
192 for (uint64_t position : positions) {
193 *targetIt = values[position];
194 ++targetIt;
195 }
196}
197
206template<class T>
207void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping,
208 std::vector<T> const& values) {
209 auto targetIt = vector.begin();
210 for (uint64_t position : positions) {
211 for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
212 *targetIt = values[i];
213 }
214 }
215}
216
226template<class T>
227void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGrouping,
228 std::vector<T> const& values) {
229 auto targetIt = vector.begin();
230 for (uint_fast64_t i = 0; i < vector.size(); ++i, ++targetIt) {
231 *targetIt = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]];
232 }
233}
234
242template<class T>
243void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& indexSequence, std::vector<T> const& values) {
244 STORM_LOG_ASSERT(indexSequence.size() <= vector.size(),
245 "The number of selected positions (" << indexSequence.size() << ") exceeds the size of the target vector (" << vector.size() << ").");
246
247 for (uint_fast64_t vectorIndex = 0; vectorIndex < vector.size(); ++vectorIndex) {
248 vector[vectorIndex] = values[indexSequence[vectorIndex]];
249 }
250}
251
261template<class T>
262void selectVectorValuesRepeatedly(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping,
263 std::vector<T> const& values) {
264 auto targetIt = vector.begin();
265 for (uint64_t position : positions) {
266 for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
267 *targetIt = values[position];
268 }
269 }
270}
271
277template<class T>
279 for (auto& element : vector) {
280 element = storm::utility::one<T>() - element;
281 }
282}
283
284template<class T>
285void addFilteredVectorGroupsToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter,
286 std::vector<uint_fast64_t> const& rowGroupIndices) {
287 auto targetIt = target.begin();
288 for (uint64_t group : filter) {
289 auto it = source.cbegin() + rowGroupIndices[group];
290 auto ite = source.cbegin() + rowGroupIndices[group + 1];
291 for (; it != ite; ++targetIt, ++it) {
292 *targetIt += *it;
293 }
294 }
295}
296
305template<class T>
306void addVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, std::vector<uint_fast64_t> const& rowGroupIndices) {
307 auto targetIt = target.begin();
308 auto sourceIt = source.cbegin();
309 auto sourceIte = source.cend();
310 auto rowGroupIt = rowGroupIndices.cbegin();
311
312 for (; sourceIt != sourceIte; ++sourceIt) {
313 uint_fast64_t current = *rowGroupIt;
314 ++rowGroupIt;
315 uint_fast64_t next = *rowGroupIt;
316 for (; current < next; ++targetIt, ++current) {
317 *targetIt += *sourceIt;
318 }
319 }
320}
321
330template<class T>
331void addFilteredVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter,
332 std::vector<uint_fast64_t> const& rowGroupIndices) {
333 auto targetIt = target.begin();
334 for (uint64_t group : filter) {
335 uint_fast64_t current = rowGroupIndices[group];
336 uint_fast64_t next = rowGroupIndices[group + 1];
337 for (; current < next; ++current, ++targetIt) {
338 *targetIt += source[group];
339 }
340 }
341}
342
351template<class InValueType1, class InValueType2, class OutValueType, class Operation>
352void applyPointwiseTernary(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target,
353 Operation f = Operation()) {
354 auto firstIt = firstOperand.begin();
355 auto firstIte = firstOperand.end();
356 auto secondIt = secondOperand.begin();
357 auto targetIt = target.begin();
358 while (firstIt != firstIte) {
359 *targetIt = f(*firstIt, *secondIt, *targetIt);
360 ++targetIt;
361 ++firstIt;
362 ++secondIt;
363 }
364}
365
374template<class InValueType1, class InValueType2, class OutValueType, class Operation>
375void applyPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target,
376 Operation f = Operation()) {
377 std::transform(firstOperand.begin(), firstOperand.end(), secondOperand.begin(), target.begin(), f);
378}
379
387template<class InValueType, class OutValueType, class Operation>
388void applyPointwise(std::vector<InValueType> const& operand, std::vector<OutValueType>& target, Operation f = Operation()) {
389 std::transform(operand.begin(), operand.end(), target.begin(), f);
390}
391
399template<class InValueType1, class InValueType2, class OutValueType>
400void addVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
402}
403
411template<class InValueType1, class InValueType2, class OutValueType>
412void subtractVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
414}
415
423template<class InValueType1, class InValueType2, class OutValueType>
424void multiplyVectorsPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand,
425 std::vector<OutValueType>& target) {
427}
428
436template<class InValueType1, class InValueType2, class OutValueType>
437void divideVectorsPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
439}
440
447template<class ValueType1, class ValueType2>
448void scaleVectorInPlace(std::vector<ValueType1>& target, ValueType2 const& factor) {
449 applyPointwise<ValueType1, ValueType1>(target, target, [&](ValueType1 const& argument) -> ValueType1 { return argument * factor; });
450}
451
460template<class InValueType1, class InValueType2, class InValueType3>
461void addScaledVector(std::vector<InValueType1>& firstOperand, std::vector<InValueType2> const& secondOperand, InValueType3 const& factor) {
463 firstOperand, secondOperand, firstOperand, [&](InValueType1 const& val1, InValueType2 const& val2) -> InValueType1 { return val1 + (factor * val2); });
464}
465
473template<class T>
474T dotProduct(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand) {
475 return std::inner_product(firstOperand.begin(), firstOperand.end(), secondOperand.begin(), storm::utility::zero<T>());
476}
477
486template<class T>
487storm::storage::BitVector filter(std::vector<T> const& values, std::function<bool(T const& value)> const& function) {
488 storm::storage::BitVector result(values.size(), false);
489
490 uint_fast64_t currentIndex = 0;
491 for (auto const& value : values) {
492 if (function(value)) {
493 result.set(currentIndex, true);
494 }
495 ++currentIndex;
496 }
497
498 return result;
499}
500
508template<class T>
509storm::storage::BitVector filterGreaterZero(std::vector<T> const& values) {
510 return filter<T>(values, [](T const& value) -> bool { return value > storm::utility::zero<T>(); });
511}
512
519template<class T>
520storm::storage::BitVector filterZero(std::vector<T> const& values) {
521 return filter<T>(values, [](T const& value) { return storm::utility::isZero(value); });
522}
523
530template<class T>
531storm::storage::BitVector filterOne(std::vector<T> const& values) {
532 return filter<T>(values, [](T const& value) { return storm::utility::isOne(value); });
533}
534
541template<class T>
542storm::storage::BitVector filterInfinity(std::vector<T> const& values) {
543 return filter<T>(values, [](T const& value) { return storm::utility::isInfinity(value); });
544}
545
552template<typename VT>
553VT sum_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
554 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
555 VT sum = storm::utility::zero<VT>();
556 for (uint64_t pos : filter) {
557 sum += values[pos];
558 }
559 return sum;
560}
561
568template<typename VT>
569VT max_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
570 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
571 STORM_LOG_ASSERT(!filter.empty(), "Empty selection.");
572
573 auto it = filter.begin();
574 auto ite = filter.end();
575
576 VT current = values[*it];
577 ++it;
578
579 for (; it != ite; ++it) {
580 current = std::max(values[*it], current);
581 }
582 return current;
583}
584
591template<typename VT>
592VT min_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
593 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
594 STORM_LOG_ASSERT(!filter.empty(), "Empty selection.");
595
596 auto it = filter.begin();
597 auto ite = filter.end();
598
599 VT current = values[*it];
600 ++it;
601
602 for (; it != ite; ++it) {
603 current = std::min(values[*it], current);
604 }
605 return current;
606}
607
618template<class T, class Filter>
619void reduceVector(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices) {
620 Filter f;
621 typename std::vector<T>::iterator targetIt = target.begin();
622 typename std::vector<T>::iterator targetIte = target.end();
623 typename std::vector<uint_fast64_t>::const_iterator rowGroupingIt = rowGrouping.begin();
624 typename std::vector<T>::const_iterator sourceIt = source.begin();
625 typename std::vector<T>::const_iterator sourceIte;
626 typename std::vector<uint_fast64_t>::iterator choiceIt;
627 if (choices) {
628 choiceIt = choices->begin();
629 }
630
631 // Variables for correctly tracking choices (only update if new choice is strictly better).
632 T oldSelectedChoiceValue;
633 uint64_t selectedChoice;
634
635 uint64_t currentRow = 0;
636 for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt, ++choiceIt) {
637 // Only traverse elements if the row group is non-empty.
638 if (*rowGroupingIt != *(rowGroupingIt + 1)) {
639 *targetIt = *sourceIt;
640
641 if (choices) {
642 selectedChoice = 0;
643 if (*choiceIt == 0) {
644 oldSelectedChoiceValue = *targetIt;
645 }
646 }
647
648 ++sourceIt;
649 ++currentRow;
650
651 for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++currentRow) {
652 if (choices && *rowGroupingIt + *choiceIt == currentRow) {
653 oldSelectedChoiceValue = *sourceIt;
654 }
655
656 if (f(*sourceIt, *targetIt)) {
657 *targetIt = *sourceIt;
658 if (choices) {
659 selectedChoice = std::distance(source.begin(), sourceIt) - *rowGroupingIt;
660 }
661 }
662 }
663
664 if (choices && f(*targetIt, oldSelectedChoiceValue)) {
665 *choiceIt = selectedChoice;
666 }
667 } else {
668 *choiceIt = 0;
669 *targetIt = storm::utility::zero<T>();
670 }
671 }
672}
673
682template<class T>
683void reduceVectorMin(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping,
684 std::vector<uint_fast64_t>* choices = nullptr) {
685 reduceVector<T, storm::utility::ElementLess<T>>(source, target, rowGrouping, choices);
686}
687
696template<class T>
697void reduceVectorMax(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping,
698 std::vector<uint_fast64_t>* choices = nullptr) {
699 reduceVector<T, storm::utility::ElementGreater<T>>(source, target, rowGrouping, choices);
700}
701
711template<class T>
712void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector<T> const& source, std::vector<T>& target,
713 std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
714 if (dir == storm::solver::OptimizationDirection::Minimize) {
715 reduceVectorMin(source, target, rowGrouping, choices);
716 } else {
717 reduceVectorMax(source, target, rowGrouping, choices);
718 }
719}
720
731template<class T>
732bool equalModuloPrecision(T const& val1, T const& val2, T const& precision, bool relativeError = true) {
734 return val1 == val2;
735 }
736 if (relativeError) {
737 if (storm::utility::isZero(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 (uint64_t 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 (uint64_t 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 STORM_LOG_ASSERT(inputVector.size() == targetVector.size(), "Vector size mismatch.");
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()) {
1022 } else if (occurringNonZeroNumbers.size() == 1) {
1023 factor = *occurringNonZeroNumbers.begin();
1024 } else {
1026 // Obtain the least common multiple of the denominators of the occurring numbers.
1027 // We can then multiply the numbers with the lcm to obtain integers.
1028 auto numberIt = occurringNonZeroNumbers.begin();
1030 for (++numberIt; numberIt != occurringNonZeroNumbers.end(); ++numberIt) {
1032 }
1033 // Multiply all values with the lcm. To reduce the range of considered integers, we also obtain the gcd of the results.
1034 numberIt = occurringNonZeroNumbers.begin();
1036 "Number '" << *numberIt << "' is not integral.");
1037 IntegerType gcd = storm::utility::numerator(ValueType(*numberIt * lcm));
1038 for (++numberIt; numberIt != occurringNonZeroNumbers.end(); ++numberIt) {
1040 "Number '" << *numberIt << "' is not integral.");
1041 gcd = storm::utility::gcd(gcd, storm::utility::numerator(ValueType(*numberIt * lcm)));
1042 }
1043
1045 }
1046
1047 // Build the result
1048 std::vector<TargetValueType> result;
1049 result.reserve(vec.size());
1050 for (auto const& v : vec) {
1051 ValueType vScaled = v / factor;
1052 STORM_LOG_ASSERT(storm::utility::isInteger(vScaled), "Resulting number '(" << v << ")/(" << factor << ") = " << vScaled << "' is not integral.");
1054 }
1055 return std::make_pair(std::move(result), std::move(factor));
1056}
1057
1058template<typename ValueType, typename TargetValueType>
1059typename std::enable_if<!std::is_same<ValueType, storm::RationalNumber>::value, std::pair<std::vector<TargetValueType>, ValueType>>::type toIntegralVector(
1060 std::vector<ValueType> const& vec) {
1061 // TODO: avoid converting back and forth
1062 auto rationalNumberVec = convertNumericVector<storm::RationalNumber>(vec);
1063 auto rationalNumberResult = toIntegralVector<storm::RationalNumber, TargetValueType>(rationalNumberVec);
1064
1065 return std::make_pair(std::move(rationalNumberResult.first), storm::utility::convertNumber<ValueType>(rationalNumberResult.second));
1066}
1067
1068template<typename Type>
1069std::vector<Type> filterVector(std::vector<Type> const& in, storm::storage::BitVector const& filter) {
1070 std::vector<Type> result;
1071 result.reserve(filter.getNumberOfSetBits());
1072 for (uint64_t index : filter) {
1073 result.push_back(in[index]);
1074 }
1075 STORM_LOG_ASSERT(result.size() == filter.getNumberOfSetBits(), "Result does not match.");
1076 return result;
1077}
1078
1079template<typename Type>
1080void filterVectorInPlace(std::vector<Type>& v, storm::storage::BitVector const& filter) {
1081 STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector.");
1082 uint_fast64_t size = v.size();
1083 // we can start our work at the first index where the filter has value zero
1084 uint_fast64_t firstUnsetIndex = filter.getNextUnsetIndex(0);
1085 if (firstUnsetIndex < size) {
1086 auto vIt = v.begin() + firstUnsetIndex;
1087 for (uint_fast64_t index = filter.getNextSetIndex(firstUnsetIndex + 1); index != size; index = filter.getNextSetIndex(index + 1)) {
1088 *vIt = std::move(v[index]);
1089 ++vIt;
1090 }
1091 v.resize(vIt - v.begin());
1092 v.shrink_to_fit();
1093 }
1094 STORM_LOG_ASSERT(v.size() == filter.getNumberOfSetBits(), "Result does not match.");
1095}
1096
1109template<class T>
1110void blowUpVectorInPlace(std::vector<T>& vector, storm::storage::BitVector const& positions, T const& defaultValue = storm::utility::zero<T>()) {
1111 STORM_LOG_ASSERT(vector.size() == positions.getNumberOfSetBits(), "The number of selected positions (" << positions.getNumberOfSetBits()
1112 << ") must match the size of the input vector ("
1113 << vector.size() << ").");
1114 auto readPos = vector.size();
1115 vector.resize(positions.size(), defaultValue);
1116 auto writePos = positions.getStartOfZeroSequenceBefore(positions.size());
1117 while (writePos > 0) {
1118 --writePos;
1119 if (positions.get(writePos)) {
1120 --readPos;
1121 if (readPos != writePos) {
1122 STORM_LOG_ASSERT(readPos < writePos, "We shall not write to positions that we later still have to read from.");
1123 vector[writePos] = vector[readPos];
1124 }
1125 } else {
1126 vector[writePos] = defaultValue;
1127 }
1128 }
1129}
1130
1131template<typename T>
1132bool hasNegativeEntry(std::vector<T> const& v) {
1133 return std::any_of(v.begin(), v.end(), [](T value) { return value < storm::utility::zero<T>(); });
1134}
1135
1136template<typename T>
1137bool hasPositiveEntry(std::vector<T> const& v) {
1138 return std::any_of(v.begin(), v.end(), [](T value) { return value > storm::utility::zero<T>(); });
1139}
1140
1141template<typename T>
1142bool hasNonZeroEntry(std::vector<T> const& v) {
1143 return std::any_of(v.begin(), v.end(), [](T value) { return !storm::utility::isZero(value); });
1144}
1145
1146template<typename T>
1147bool hasZeroEntry(std::vector<T> const& v) {
1148 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isZero(value); });
1149}
1150
1151template<typename T>
1152bool hasInfinityEntry(std::vector<T> const& v) {
1153 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isInfinity(value); });
1154}
1155
1156template<typename T>
1157std::vector<T> applyInversePermutation(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source) {
1158 std::vector<T> result;
1159 result.reserve(source.size());
1160 for (uint64_t sourceIndex : inversePermutation) {
1161 result.push_back(source[sourceIndex]);
1162 }
1163 return result;
1164}
1165
1166template<typename T>
1167std::vector<T> applyInversePermutationToGroupedVector(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source,
1168 std::vector<uint64_t> const& rowGroupIndices) {
1169 STORM_LOG_ASSERT(inversePermutation.size() == rowGroupIndices.size() - 1, "Inverse permutation and row group indices do not match.");
1170 std::vector<T> result;
1171 result.reserve(source.size());
1172 for (auto sourceGroupIndex : inversePermutation) {
1173 for (uint64_t sourceIndex = rowGroupIndices[sourceGroupIndex]; sourceIndex < rowGroupIndices[sourceGroupIndex + 1]; ++sourceIndex) {
1174 result.push_back(source[sourceIndex]);
1175 }
1176 }
1177 STORM_LOG_ASSERT(result.size() == source.size(), "Result has unexpected length.");
1178 return result;
1179}
1180
1187template<typename ValueType>
1188std::string toString(std::vector<ValueType> const& vector) {
1189 std::stringstream stream;
1190 stream << "vector (" << vector.size() << ") [ ";
1191 if (!vector.empty()) {
1192 for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
1193 stream << vector[i] << ", ";
1194 }
1195 stream << vector.back();
1196 }
1197 stream << " ]";
1198 return stream.str();
1199}
1200
1201} // namespace vector
1202} // namespace utility
1203} // namespace storm
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
uint64_t getNumberOfSetBits() const
Returns the number of bits that are set to true in this bit vector.
uint64_t getNextUnsetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to false in the bit vector.
void set(uint64_t index, bool value=true)
Sets the given truth value at the given index.
uint64_t getStartOfZeroSequenceBefore(uint64_t endIndex) const
Retrieves the smallest index i such that all bits in the range [i,endIndex) are 0.
size_t size() const
Retrieves the number of bits this bit vector can store.
bool get(uint64_t index) const
Retrieves the truth value of the bit at the given index and performs a bound check.
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:9
std::size_t findOrInsert(std::vector< T > &vector, T &&element)
Finds the given element in the given vector.
Definition vector.h:45
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:487
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:352
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:592
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:400
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:437
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:474
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:1152
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:306
void setNonzeroIndices(std::vector< T > const &vec, storm::storage::BitVector &bv)
Definition vector.h:107
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:569
bool compareElementWise(std::vector< T > const &left, std::vector< T > const &right, Comparator comp=std::less< T >())
Definition vector.h:173
void setVectorValues(std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< S > const &values)
Sets the provided values at the provided positions in the given vector.
Definition vector.h:79
std::vector< T > buildVectorForRange(T min, T max)
Constructs a vector [min, min+1, ...., max-1].
Definition vector.h:130
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:54
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:285
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:732
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:185
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:155
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:712
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:509
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:619
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:461
std::string toString(std::vector< ValueType > const &vector)
Output vector as string.
Definition vector.h:1188
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:424
bool hasPositiveEntry(std::vector< T > const &v)
Definition vector.h:1137
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:531
bool hasNegativeEntry(std::vector< T > const &v)
Definition vector.h:1132
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:331
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:262
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:375
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:683
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:553
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:542
std::vector< T > applyInversePermutation(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source)
Definition vector.h:1157
void filterVectorInPlace(std::vector< Type > &v, storm::storage::BitVector const &filter)
Definition vector.h:1080
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:122
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:412
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:145
bool hasZeroEntry(std::vector< T > const &v)
Definition vector.h:1147
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:520
void blowUpVectorInPlace(std::vector< T > &vector, storm::storage::BitVector const &positions, T const &defaultValue=storm::utility::zero< T >())
Gets as input a vector with size n and a BitVector with size m>=n and exactly n set bits.
Definition vector.h:1110
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:448
std::vector< T > applyInversePermutationToGroupedVector(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source, std::vector< uint64_t > const &rowGroupIndices)
Definition vector.h:1167
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:1142
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:278
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:697
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:1069
ValueType max(ValueType const &first, ValueType const &second)
bool isOne(ValueType const &a)
Definition constants.cpp:39
NumberTraits< RationalType >::IntegerType denominator(RationalType const &number)
bool isFinite(ExtendedNumber< ValueType > const &value)
NumberTraits< RationalType >::IntegerType numerator(RationalType const &number)
ValueType min(ValueType const &first, ValueType const &second)
bool isAlmostZero(ValueType const &a)
Definition constants.cpp:98
IntegerType lcm(IntegerType const &first, IntegerType const &second)
bool isZero(ValueType const &a)
Definition constants.cpp:44
bool isInteger(ValueType const &number)
ValueType abs(ValueType const &number)
ValueType zero()
Definition constants.cpp:26
IntegerType gcd(IntegerType const &first, IntegerType const &second)
ValueType pow(ValueType const &value, int_fast64_t exponent)
ValueType one()
Definition constants.cpp:21
bool isInfinity(ValueType const &a)
TargetType convertNumber(SourceType const &number)
size_t operator()(std::vector< ValueType > const &vec) const
Definition vector.h:22