Storm 1.13.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
14
15namespace storm {
16namespace utility {
17namespace vector {
18
19template<typename ValueType>
20struct VectorHash {
21 size_t operator()(std::vector<ValueType> const& vec) const {
22 std::hash<ValueType> hasher;
23 std::size_t seed = 0;
24 for (ValueType const& element : vec) {
25 seed ^= hasher(element) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
26 }
27 return seed;
28 }
29};
30
43template<class T>
44std::size_t findOrInsert(std::vector<T>& vector, T&& element) {
45 std::size_t position = std::find(vector.begin(), vector.end(), element) - vector.begin();
46 if (position == vector.size()) {
47 vector.emplace_back(std::move(element));
48 }
49 return position;
50}
51
52template<typename T>
53void setAllValues(std::vector<T>& vec, storm::storage::BitVector const& positions, T const& positiveValue = storm::utility::one<T>(),
54 T const& negativeValue = storm::utility::zero<T>()) {
55 if (positions.getNumberOfSetBits() * 2 > positions.size()) {
56 vec.resize(positions.size(), positiveValue);
57 uint64_t index = positions.getNextUnsetIndex(0);
58 while (index < positions.size()) {
59 vec[index] = negativeValue;
60 index = positions.getNextUnsetIndex(index + 1);
61 }
62 } else {
63 vec.resize(positions.size(), negativeValue);
64 for (uint64_t index : positions) {
65 vec[index] = positiveValue;
66 }
67 }
68}
69
77template<class T>
78void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
79 STORM_LOG_ASSERT(positions.size() <= vector.size(), "We cannot set positions that have not been initialized");
80 STORM_LOG_ASSERT(positions.getNumberOfSetBits() <= values.size(), "The number of selected positions (" << positions.getNumberOfSetBits()
81 << ") exceeds the size of the input vector ("
82 << values.size() << ").");
83 uint_fast64_t oldPosition = 0;
84 for (auto position : positions) {
85 vector[position] = values[oldPosition++];
86 }
87}
88
97template<class T>
98void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, T value) {
99 STORM_LOG_ASSERT(positions.size() <= vector.size(), "We cannot set positions that have not been initialized");
100 for (auto position : positions) {
101 vector[position] = value;
102 }
103}
104
105template<typename T>
106void setNonzeroIndices(std::vector<T> const& vec, storm::storage::BitVector& bv) {
107 STORM_LOG_ASSERT(bv.size() == vec.size(), "Bitvector size should match vector size");
108 for (uint64_t i = 0; i < vec.size(); ++i) {
109 if (!storm::utility::isZero(vec[i])) {
110 bv.set(i, true);
111 }
112 }
113}
114
120template<class OutputIterator, class Size, class Assignable>
121void iota_n(OutputIterator first, Size n, Assignable value) {
122 std::generate_n(first, n, [&value]() { return value++; });
123}
124
128template<typename T>
129inline std::vector<T> buildVectorForRange(T min, T max) {
130 STORM_LOG_ASSERT(min <= max, "Invalid range.");
131 T diff = max - min;
132 std::vector<T> v;
133 v.reserve(diff);
134 iota_n(std::back_inserter(v), diff, min);
135 return v;
136}
137
143template<typename T>
144std::vector<uint_fast64_t> getSortedIndices(std::vector<T> const& v) {
145 std::vector<uint_fast64_t> res = buildVectorForRange<uint_fast64_t>(0, v.size());
146 std::sort(res.begin(), res.end(), [&v](uint_fast64_t index1, uint_fast64_t index2) { return v[index1] > v[index2]; });
147 return res;
148}
149
153template<typename T>
154bool isUnique(std::vector<T> const& v) {
155 if (v.size() < 2) {
156 return true;
157 }
158 auto sortedIndices = getSortedIndices(v);
159 auto indexIt = sortedIndices.begin();
160 T const* previous = &v[*indexIt];
161 for (++indexIt; indexIt != sortedIndices.end(); ++indexIt) {
162 T const& current = v[*indexIt];
163 if (current == *previous) {
164 return false;
165 }
166 previous = &current;
167 }
168 return true;
169}
170
171template<typename T, typename Comparator>
172bool compareElementWise(std::vector<T> const& left, std::vector<T> const& right, Comparator comp = std::less<T>()) {
173 STORM_LOG_ASSERT(left.size() == right.size(), "Expected that vectors for comparison have equal size");
174 return std::equal(left.begin(), left.end(), right.begin(), comp);
175}
176
183template<class T>
184void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
185 STORM_LOG_ASSERT(positions.getNumberOfSetBits() <= vector.size(), "The number of selected positions (" << positions.getNumberOfSetBits()
186 << ") exceeds the size of the target vector ("
187 << vector.size() << ").");
188 STORM_LOG_ASSERT(positions.size() == values.size(),
189 "Size mismatch of the positions vector (" << positions.size() << ") and the values vector (" << values.size() << ").");
190 auto targetIt = vector.begin();
191 for (auto position : positions) {
192 *targetIt = values[position];
193 ++targetIt;
194 }
195}
196
205template<class T>
206void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping,
207 std::vector<T> const& values) {
208 auto targetIt = vector.begin();
209 for (auto position : positions) {
210 for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
211 *targetIt = values[i];
212 }
213 }
214}
215
225template<class T>
226void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGrouping,
227 std::vector<T> const& values) {
228 auto targetIt = vector.begin();
229 for (uint_fast64_t i = 0; i < vector.size(); ++i, ++targetIt) {
230 *targetIt = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]];
231 }
232}
233
241template<class T>
242void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& indexSequence, std::vector<T> const& values) {
243 STORM_LOG_ASSERT(indexSequence.size() <= vector.size(),
244 "The number of selected positions (" << indexSequence.size() << ") exceeds the size of the target vector (" << vector.size() << ").");
245
246 for (uint_fast64_t vectorIndex = 0; vectorIndex < vector.size(); ++vectorIndex) {
247 vector[vectorIndex] = values[indexSequence[vectorIndex]];
248 }
249}
250
260template<class T>
261void selectVectorValuesRepeatedly(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping,
262 std::vector<T> const& values) {
263 auto targetIt = vector.begin();
264 for (auto position : positions) {
265 for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i, ++targetIt) {
266 *targetIt = values[position];
267 }
268 }
269}
270
276template<class T>
278 for (auto& element : vector) {
279 element = storm::utility::one<T>() - element;
280 }
281}
282
283template<class T>
284void addFilteredVectorGroupsToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter,
285 std::vector<uint_fast64_t> const& rowGroupIndices) {
286 auto targetIt = target.begin();
287 for (auto group : filter) {
288 auto it = source.cbegin() + rowGroupIndices[group];
289 auto ite = source.cbegin() + rowGroupIndices[group + 1];
290 for (; it != ite; ++targetIt, ++it) {
291 *targetIt += *it;
292 }
293 }
294}
295
304template<class T>
305void addVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, std::vector<uint_fast64_t> const& rowGroupIndices) {
306 auto targetIt = target.begin();
307 auto sourceIt = source.cbegin();
308 auto sourceIte = source.cend();
309 auto rowGroupIt = rowGroupIndices.cbegin();
310
311 for (; sourceIt != sourceIte; ++sourceIt) {
312 uint_fast64_t current = *rowGroupIt;
313 ++rowGroupIt;
314 uint_fast64_t next = *rowGroupIt;
315 for (; current < next; ++targetIt, ++current) {
316 *targetIt += *sourceIt;
317 }
318 }
319}
320
329template<class T>
330void addFilteredVectorToGroupedVector(std::vector<T>& target, std::vector<T> const& source, storm::storage::BitVector const& filter,
331 std::vector<uint_fast64_t> const& rowGroupIndices) {
332 auto targetIt = target.begin();
333 for (auto group : filter) {
334 uint_fast64_t current = rowGroupIndices[group];
335 uint_fast64_t next = rowGroupIndices[group + 1];
336 for (; current < next; ++current, ++targetIt) {
337 *targetIt += source[group];
338 }
339 }
340}
341
350template<class InValueType1, class InValueType2, class OutValueType, class Operation>
351void applyPointwiseTernary(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target,
352 Operation f = Operation()) {
353 auto firstIt = firstOperand.begin();
354 auto firstIte = firstOperand.end();
355 auto secondIt = secondOperand.begin();
356 auto targetIt = target.begin();
357 while (firstIt != firstIte) {
358 *targetIt = f(*firstIt, *secondIt, *targetIt);
359 ++targetIt;
360 ++firstIt;
361 ++secondIt;
362 }
363}
364
373template<class InValueType1, class InValueType2, class OutValueType, class Operation>
374void applyPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target,
375 Operation f = Operation()) {
376 std::transform(firstOperand.begin(), firstOperand.end(), secondOperand.begin(), target.begin(), f);
377}
378
386template<class InValueType, class OutValueType, class Operation>
387void applyPointwise(std::vector<InValueType> const& operand, std::vector<OutValueType>& target, Operation f = Operation()) {
388 std::transform(operand.begin(), operand.end(), target.begin(), f);
389}
390
398template<class InValueType1, class InValueType2, class OutValueType>
399void addVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
401}
402
410template<class InValueType1, class InValueType2, class OutValueType>
411void subtractVectors(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
413}
414
422template<class InValueType1, class InValueType2, class OutValueType>
423void multiplyVectorsPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand,
424 std::vector<OutValueType>& target) {
426}
427
435template<class InValueType1, class InValueType2, class OutValueType>
436void divideVectorsPointwise(std::vector<InValueType1> const& firstOperand, std::vector<InValueType2> const& secondOperand, std::vector<OutValueType>& target) {
438}
439
446template<class ValueType1, class ValueType2>
447void scaleVectorInPlace(std::vector<ValueType1>& target, ValueType2 const& factor) {
448 applyPointwise<ValueType1, ValueType1>(target, target, [&](ValueType1 const& argument) -> ValueType1 { return argument * factor; });
449}
450
459template<class InValueType1, class InValueType2, class InValueType3>
460void addScaledVector(std::vector<InValueType1>& firstOperand, std::vector<InValueType2> const& secondOperand, InValueType3 const& factor) {
462 firstOperand, secondOperand, firstOperand, [&](InValueType1 const& val1, InValueType2 const& val2) -> InValueType1 { return val1 + (factor * val2); });
463}
464
472template<class T>
473T dotProduct(std::vector<T> const& firstOperand, std::vector<T> const& secondOperand) {
474 return std::inner_product(firstOperand.begin(), firstOperand.end(), secondOperand.begin(), storm::utility::zero<T>());
475}
476
485template<class T>
486storm::storage::BitVector filter(std::vector<T> const& values, std::function<bool(T const& value)> const& function) {
487 storm::storage::BitVector result(values.size(), false);
488
489 uint_fast64_t currentIndex = 0;
490 for (auto const& value : values) {
491 if (function(value)) {
492 result.set(currentIndex, true);
493 }
494 ++currentIndex;
495 }
496
497 return result;
498}
499
507template<class T>
508storm::storage::BitVector filterGreaterZero(std::vector<T> const& values) {
509 return filter<T>(values, [](T const& value) -> bool { return value > storm::utility::zero<T>(); });
510}
511
518template<class T>
519storm::storage::BitVector filterZero(std::vector<T> const& values) {
520 return filter<T>(values, storm::utility::isZero<T>);
521}
522
529template<class T>
530storm::storage::BitVector filterOne(std::vector<T> const& values) {
531 return filter<T>(values, storm::utility::isOne<T>);
532}
533
540template<class T>
541storm::storage::BitVector filterInfinity(std::vector<T> const& values) {
543}
544
551template<typename VT>
552VT sum_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
553 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
554 VT sum = storm::utility::zero<VT>();
555 for (auto pos : filter) {
556 sum += values[pos];
557 }
558 return sum;
559}
560
567template<typename VT>
568VT max_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
569 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
570 STORM_LOG_ASSERT(!filter.empty(), "Empty selection.");
571
572 auto it = filter.begin();
573 auto ite = filter.end();
574
575 VT current = values[*it];
576 ++it;
577
578 for (; it != ite; ++it) {
579 current = std::max(values[*it], current);
580 }
581 return current;
582}
583
590template<typename VT>
591VT min_if(std::vector<VT> const& values, storm::storage::BitVector const& filter) {
592 STORM_LOG_ASSERT(values.size() == filter.size(), "Vector sizes mismatch.");
593 STORM_LOG_ASSERT(!filter.empty(), "Empty selection.");
594
595 auto it = filter.begin();
596 auto ite = filter.end();
597
598 VT current = values[*it];
599 ++it;
600
601 for (; it != ite; ++it) {
602 current = std::min(values[*it], current);
603 }
604 return current;
605}
606
617template<class T, class Filter>
618void reduceVector(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices) {
619 Filter f;
620 typename std::vector<T>::iterator targetIt = target.begin();
621 typename std::vector<T>::iterator targetIte = target.end();
622 typename std::vector<uint_fast64_t>::const_iterator rowGroupingIt = rowGrouping.begin();
623 typename std::vector<T>::const_iterator sourceIt = source.begin();
624 typename std::vector<T>::const_iterator sourceIte;
625 typename std::vector<uint_fast64_t>::iterator choiceIt;
626 if (choices) {
627 choiceIt = choices->begin();
628 }
629
630 // Variables for correctly tracking choices (only update if new choice is strictly better).
631 T oldSelectedChoiceValue;
632 uint64_t selectedChoice;
633
634 uint64_t currentRow = 0;
635 for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt, ++choiceIt) {
636 // Only traverse elements if the row group is non-empty.
637 if (*rowGroupingIt != *(rowGroupingIt + 1)) {
638 *targetIt = *sourceIt;
639
640 if (choices) {
641 selectedChoice = 0;
642 if (*choiceIt == 0) {
643 oldSelectedChoiceValue = *targetIt;
644 }
645 }
646
647 ++sourceIt;
648 ++currentRow;
649
650 for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++currentRow) {
651 if (choices && *rowGroupingIt + *choiceIt == currentRow) {
652 oldSelectedChoiceValue = *sourceIt;
653 }
654
655 if (f(*sourceIt, *targetIt)) {
656 *targetIt = *sourceIt;
657 if (choices) {
658 selectedChoice = std::distance(source.begin(), sourceIt) - *rowGroupingIt;
659 }
660 }
661 }
662
663 if (choices && f(*targetIt, oldSelectedChoiceValue)) {
664 *choiceIt = selectedChoice;
665 }
666 } else {
667 *choiceIt = 0;
668 *targetIt = storm::utility::zero<T>();
669 }
670 }
671}
672
681template<class T>
682void reduceVectorMin(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping,
683 std::vector<uint_fast64_t>* choices = nullptr) {
684 reduceVector<T, storm::utility::ElementLess<T>>(source, target, rowGrouping, choices);
685}
686
695template<class T>
696void reduceVectorMax(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping,
697 std::vector<uint_fast64_t>* choices = nullptr) {
698 reduceVector<T, storm::utility::ElementGreater<T>>(source, target, rowGrouping, choices);
699}
700
710template<class T>
711void reduceVectorMinOrMax(storm::solver::OptimizationDirection dir, std::vector<T> const& source, std::vector<T>& target,
712 std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
713 if (dir == storm::solver::OptimizationDirection::Minimize) {
714 reduceVectorMin(source, target, rowGrouping, choices);
715 } else {
716 reduceVectorMax(source, target, rowGrouping, choices);
717 }
718}
719
730template<class T>
731bool equalModuloPrecision(T const& val1, T const& val2, T const& precision, bool relativeError = true) {
732 if (relativeError) {
733 if (storm::utility::isZero<T>(val1)) {
734 return storm::utility::isZero(val2);
735 }
736 T relDiff = (val1 - val2) / val1;
737 if (storm::utility::abs(relDiff) > precision) {
738 return false;
739 }
740 } else {
741 T diff = val1 - val2;
742 if (storm::utility::abs(diff) > precision) {
743 return false;
744 }
745 }
746 return true;
747}
748
749// Specializiation for double as the relative check for doubles very close to zero is not meaningful.
750template<>
751inline bool equalModuloPrecision(double const& val1, double const& val2, double const& precision, bool relativeError) {
752 if (relativeError) {
754 return storm::utility::isAlmostZero(val1);
755 }
756 double relDiff = (val1 - val2) / val1;
757 if (storm::utility::abs(relDiff) > precision) {
758 return false;
759 }
760 } else {
761 double diff = val1 - val2;
762 if (storm::utility::abs(diff) > precision) {
763 return false;
764 }
765 }
766 return true;
767}
768
778template<class T>
779bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T const& precision, bool relativeError) {
780 STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
781
782 auto leftIt = vectorLeft.begin();
783 auto leftIte = vectorLeft.end();
784 auto rightIt = vectorRight.begin();
785 for (; leftIt != leftIte; ++leftIt, ++rightIt) {
786 if (!equalModuloPrecision(*leftIt, *rightIt, precision, relativeError)) {
787 return false;
788 }
789 }
790
791 return true;
792}
793
805template<class T>
806bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, storm::storage::BitVector const& positions, T const& precision,
807 bool relativeError) {
808 STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
809
810 for (auto position : positions) {
811 if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {
812 return false;
813 }
814 }
815
816 return true;
817}
818
830template<class T>
831bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T const& precision,
832 bool relativeError) {
833 STORM_LOG_ASSERT(vectorLeft.size() == vectorRight.size(), "Lengths of vectors does not match.");
834
835 for (uint_fast64_t position : positions) {
836 if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {
837 return false;
838 }
839 }
840
841 return true;
842}
843
844template<class T>
845T maximumElementAbs(std::vector<T> const& vector) {
846 T res = storm::utility::zero<T>();
847 for (auto const& element : vector) {
848 res = std::max(res, storm::utility::abs(element));
849 }
850 return res;
851}
852
853template<class T>
854T maximumElementDiff(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight) {
855 T maxDiff = storm::utility::zero<T>();
856 auto leftIt = vectorLeft.begin();
857 auto leftIte = vectorLeft.end();
858 auto rightIt = vectorRight.begin();
859 for (; leftIt != leftIte; ++leftIt, ++rightIt) {
860 T diff = *leftIt - *rightIt;
861 T possDiff = storm::utility::abs(diff);
862 maxDiff = maxDiff < possDiff ? possDiff : maxDiff;
863 }
864 return maxDiff;
865}
866
867template<class T>
868T computeSquaredNorm2Difference(std::vector<T> const& b1, std::vector<T> const& b2) {
869 STORM_LOG_ASSERT(b1.size() == b2.size(), "Vector sizes mismatch.");
870
871 T result = storm::utility::zero<T>();
872
873 auto b1It = b1.begin();
874 auto b1Ite = b1.end();
875 auto b2It = b2.begin();
876
877 for (; b1It != b1Ite; ++b1It, ++b2It) {
878 result += storm::utility::pow<T>(*b1It - *b2It, 2);
879 }
880
881 return result;
882}
883
887template<typename ValueType>
888void clip(std::vector<ValueType>& x, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound) {
889 for (auto& entry : x) {
890 if (lowerBound && entry < lowerBound.get()) {
891 entry = lowerBound.get();
892 } else if (upperBound && entry > upperBound.get()) {
893 entry = upperBound.get();
894 }
895 }
896}
897
901template<typename ValueType>
902void clip(std::vector<ValueType>& x, ValueType const& bound, bool boundFromBelow) {
903 for (auto& entry : x) {
904 if (boundFromBelow && entry < bound) {
905 entry = bound;
906 } else if (!boundFromBelow && entry > bound) {
907 entry = bound;
908 }
909 }
910}
911
915template<typename ValueType>
916void clip(std::vector<ValueType>& x, std::vector<ValueType> const& bounds, bool boundFromBelow) {
917 auto boundsIt = bounds.begin();
918 for (auto& entry : x) {
919 if (boundFromBelow && entry < *boundsIt) {
920 entry = *boundsIt;
921 } else if (!boundFromBelow && entry > *boundsIt) {
922 entry = *boundsIt;
923 }
924 ++boundsIt;
925 }
926}
927
936template<class T>
937std::vector<T> getConstrainedOffsetVector(std::vector<T> const& offsetVector, storm::storage::BitVector const& constraint) {
938 // Reserve the known amount of slots for the resulting vector.
939 std::vector<uint_fast64_t> subVector(constraint.getNumberOfSetBits() + 1);
940 uint_fast64_t currentRowCount = 0;
941 uint_fast64_t currentIndexCount = 1;
942
943 // Set the first element as this will clearly begin at offset 0.
944 subVector[0] = 0;
945
946 // Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over
947 // to the resulting vector.
948 for (auto index : constraint) {
949 subVector[currentIndexCount] = currentRowCount + offsetVector[index + 1] - offsetVector[index];
950 currentRowCount += offsetVector[index + 1] - offsetVector[index];
951 ++currentIndexCount;
952 }
953
954 // Put a sentinel element at the end.
955 subVector[constraint.getNumberOfSetBits()] = currentRowCount;
956
957 return subVector;
958}
959
965template<typename TargetType, typename SourceType>
966std::vector<TargetType> convertNumericVector(std::vector<SourceType> const& oldVector) {
967 std::vector<TargetType> resultVector;
968 resultVector.reserve(oldVector.size());
969 for (auto const& oldValue : oldVector) {
970 resultVector.push_back(storm::utility::convertNumber<TargetType>(oldValue));
971 }
972 return resultVector;
973}
974
984template<typename TargetType, typename SourceType>
985void convertNumericVector(std::vector<SourceType> const& inputVector, std::vector<TargetType>& targetVector) {
986 assert(inputVector.size() == targetVector.size());
987 applyPointwise(inputVector, targetVector, [](SourceType const& v) { return storm::utility::convertNumber<TargetType>(v); });
988}
989
993template<typename NewValueType, typename ValueType>
994std::vector<NewValueType> toValueType(std::vector<ValueType> const& oldVector) {
995 std::vector<NewValueType> resultVector;
996 resultVector.reserve(oldVector.size());
997 for (auto const& oldValue : oldVector) {
998 resultVector.push_back(static_cast<NewValueType>(oldValue));
999 }
1000 return resultVector;
1001}
1002
1003template<typename ValueType, typename TargetValueType>
1004typename std::enable_if<std::is_same<ValueType, storm::RationalNumber>::value, std::pair<std::vector<TargetValueType>, ValueType>>::type toIntegralVector(
1005 std::vector<ValueType> const& vec) {
1006 // Collect the numbers occurring in the input vector
1007 std::set<ValueType> occurringNonZeroNumbers;
1008 for (auto const& v : vec) {
1009 if (!storm::utility::isZero(v)) {
1010 occurringNonZeroNumbers.insert(v);
1011 }
1012 }
1013
1014 // Compute the scaling factor
1015 ValueType factor;
1016 if (occurringNonZeroNumbers.empty()) {
1018 } else if (occurringNonZeroNumbers.size() == 1) {
1019 factor = *occurringNonZeroNumbers.begin();
1020 } else {
1021 // Obtain the least common multiple of the denominators of the occurring numbers.
1022 // We can then multiply the numbers with the lcm to obtain integers.
1023 auto numberIt = occurringNonZeroNumbers.begin();
1024 ValueType lcm = storm::utility::asFraction(*numberIt).second;
1025 for (++numberIt; numberIt != occurringNonZeroNumbers.end(); ++numberIt) {
1026 lcm = carl::lcm(lcm, storm::utility::asFraction(*numberIt).second);
1027 }
1028 // Multiply all values with the lcm. To reduce the range of considered integers, we also obtain the gcd of the results.
1029 numberIt = occurringNonZeroNumbers.begin();
1030 ValueType gcd = *numberIt * lcm;
1031 for (++numberIt; numberIt != occurringNonZeroNumbers.end(); ++numberIt) {
1032 gcd = carl::gcd(gcd, static_cast<ValueType>(*numberIt * lcm));
1033 }
1034
1035 factor = gcd / lcm;
1036 }
1037
1038 // Build the result
1039 std::vector<TargetValueType> result;
1040 result.reserve(vec.size());
1041 for (auto const& v : vec) {
1042 ValueType vScaled = v / factor;
1043 STORM_LOG_ASSERT(storm::utility::isInteger(vScaled), "Resulting number '(" << v << ")/(" << factor << ") = " << vScaled << "' is not integral.");
1045 }
1046 return std::make_pair(std::move(result), std::move(factor));
1047}
1048
1049template<typename ValueType, typename TargetValueType>
1050typename std::enable_if<!std::is_same<ValueType, storm::RationalNumber>::value, std::pair<std::vector<TargetValueType>, ValueType>>::type toIntegralVector(
1051 std::vector<ValueType> const& vec) {
1052 // TODO: avoid converting back and forth
1053 auto rationalNumberVec = convertNumericVector<storm::RationalNumber>(vec);
1054 auto rationalNumberResult = toIntegralVector<storm::RationalNumber, TargetValueType>(rationalNumberVec);
1055
1056 return std::make_pair(std::move(rationalNumberResult.first), storm::utility::convertNumber<ValueType>(rationalNumberResult.second));
1057}
1058
1059template<typename Type>
1060std::vector<Type> filterVector(std::vector<Type> const& in, storm::storage::BitVector const& filter) {
1061 std::vector<Type> result;
1062 result.reserve(filter.getNumberOfSetBits());
1063 for (auto index : filter) {
1064 result.push_back(in[index]);
1065 }
1066 STORM_LOG_ASSERT(result.size() == filter.getNumberOfSetBits(), "Result does not match.");
1067 return result;
1068}
1069
1070template<typename Type>
1071void filterVectorInPlace(std::vector<Type>& v, storm::storage::BitVector const& filter) {
1072 STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector");
1073 uint_fast64_t size = v.size();
1074 // we can start our work at the first index where the filter has value zero
1075 uint_fast64_t firstUnsetIndex = filter.getNextUnsetIndex(0);
1076 if (firstUnsetIndex < size) {
1077 auto vIt = v.begin() + firstUnsetIndex;
1078 for (uint_fast64_t index = filter.getNextSetIndex(firstUnsetIndex + 1); index != size; index = filter.getNextSetIndex(index + 1)) {
1079 *vIt = std::move(v[index]);
1080 ++vIt;
1081 }
1082 v.resize(vIt - v.begin());
1083 v.shrink_to_fit();
1084 }
1085 STORM_LOG_ASSERT(v.size() == filter.getNumberOfSetBits(), "Result does not match.");
1086}
1087
1100template<class T>
1101void blowUpVectorInPlace(std::vector<T>& vector, storm::storage::BitVector const& positions, T const& defaultValue = storm::utility::zero<T>()) {
1102 STORM_LOG_ASSERT(vector.size() == positions.getNumberOfSetBits(), "The number of selected positions (" << positions.getNumberOfSetBits()
1103 << ") must match the size of the input vector ("
1104 << vector.size() << ").");
1105 auto readPos = vector.size();
1106 vector.resize(positions.size(), defaultValue);
1107 auto writePos = positions.getStartOfZeroSequenceBefore(positions.size());
1108 while (writePos > 0) {
1109 --writePos;
1110 if (positions.get(writePos)) {
1111 --readPos;
1112 if (readPos != writePos) {
1113 STORM_LOG_ASSERT(readPos < writePos, "We shall not write to positions that we later still have to read from.");
1114 vector[writePos] = vector[readPos];
1115 }
1116 } else {
1117 vector[writePos] = defaultValue;
1118 }
1119 }
1120}
1121
1122template<typename T>
1123bool hasNegativeEntry(std::vector<T> const& v) {
1124 return std::any_of(v.begin(), v.end(), [](T value) { return value < storm::utility::zero<T>(); });
1125}
1126
1127template<typename T>
1128bool hasPositiveEntry(std::vector<T> const& v) {
1129 return std::any_of(v.begin(), v.end(), [](T value) { return value > storm::utility::zero<T>(); });
1130}
1131
1132template<typename T>
1133bool hasNonZeroEntry(std::vector<T> const& v) {
1134 return std::any_of(v.begin(), v.end(), [](T value) { return !storm::utility::isZero(value); });
1135}
1136
1137template<typename T>
1138bool hasZeroEntry(std::vector<T> const& v) {
1139 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isZero(value); });
1140}
1141
1142template<typename T>
1143bool hasInfinityEntry(std::vector<T> const& v) {
1144 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isInfinity(value); });
1145}
1146
1147template<typename T>
1148std::vector<T> applyInversePermutation(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source) {
1149 std::vector<T> result;
1150 result.reserve(source.size());
1151 for (uint64_t sourceIndex : inversePermutation) {
1152 result.push_back(source[sourceIndex]);
1153 }
1154 return result;
1155}
1156
1157template<typename T>
1158std::vector<T> applyInversePermutationToGroupedVector(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source,
1159 std::vector<uint64_t> const& rowGroupIndices) {
1160 STORM_LOG_ASSERT(inversePermutation.size() == rowGroupIndices.size() - 1, "Inverse permutation and row group indices do not match.");
1161 std::vector<T> result;
1162 result.reserve(source.size());
1163 for (auto sourceGroupIndex : inversePermutation) {
1164 for (uint64_t sourceIndex = rowGroupIndices[sourceGroupIndex]; sourceIndex < rowGroupIndices[sourceGroupIndex + 1]; ++sourceIndex) {
1165 result.push_back(source[sourceIndex]);
1166 }
1167 }
1168 STORM_LOG_ASSERT(result.size() == source.size(), "result has unexpected length.");
1169 return result;
1170}
1171
1178template<typename ValueType>
1179std::string toString(std::vector<ValueType> const& vector) {
1180 std::stringstream stream;
1181 stream << "vector (" << vector.size() << ") [ ";
1182 if (!vector.empty()) {
1183 for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
1184 stream << vector[i] << ", ";
1185 }
1186 stream << vector.back();
1187 }
1188 stream << " ]";
1189 return stream.str();
1190}
1191
1192} // namespace vector
1193} // namespace utility
1194} // 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:11
std::size_t findOrInsert(std::vector< T > &vector, T &&element)
Finds the given element in the given vector.
Definition vector.h:44
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:966
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:486
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:351
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:591
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:399
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:436
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:473
std::vector< NewValueType > toValueType(std::vector< ValueType > const &oldVector)
Converts the given vector to the given ValueType.
Definition vector.h:994
bool hasInfinityEntry(std::vector< T > const &v)
Definition vector.h:1143
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:305
void setNonzeroIndices(std::vector< T > const &vec, storm::storage::BitVector &bv)
Definition vector.h:106
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:568
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:78
bool compareElementWise(std::vector< T > const &left, std::vector< T > const &right, Comparator comp=std::less< T >())
Definition vector.h:172
std::vector< T > buildVectorForRange(T min, T max)
Constructs a vector [min, min+1, ...., max-1].
Definition vector.h:129
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:53
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:284
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:731
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:184
T computeSquaredNorm2Difference(std::vector< T > const &b1, std::vector< T > const &b2)
Definition vector.h:868
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:154
T maximumElementDiff(std::vector< T > const &vectorLeft, std::vector< T > const &vectorRight)
Definition vector.h:854
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:711
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:508
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:618
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:460
std::string toString(std::vector< ValueType > const &vector)
Output vector as string.
Definition vector.h:1179
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:423
bool hasPositiveEntry(std::vector< T > const &v)
Definition vector.h:1128
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:530
bool hasNegativeEntry(std::vector< T > const &v)
Definition vector.h:1123
T maximumElementAbs(std::vector< T > const &vector)
Definition vector.h:845
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:888
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:330
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:261
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:374
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:682
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:552
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:541
std::vector< T > applyInversePermutation(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source)
Definition vector.h:1148
void filterVectorInPlace(std::vector< Type > &v, storm::storage::BitVector const &filter)
Definition vector.h:1071
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:121
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:411
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:144
bool hasZeroEntry(std::vector< T > const &v)
Definition vector.h:1138
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:519
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:1101
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:447
std::vector< T > applyInversePermutationToGroupedVector(std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source, std::vector< uint64_t > const &rowGroupIndices)
Definition vector.h:1158
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:937
bool hasNonZeroEntry(std::vector< T > const &v)
Definition vector.h:1133
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:277
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:696
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:1004
std::vector< Type > filterVector(std::vector< Type > const &in, storm::storage::BitVector const &filter)
Definition vector.h:1060
ValueType max(ValueType const &first, ValueType const &second)
bool isOne(ValueType const &a)
Definition constants.cpp:34
ValueType min(ValueType const &first, ValueType const &second)
bool isAlmostZero(ValueType const &a)
Definition constants.cpp:93
std::pair< ValueType, ValueType > asFraction(ValueType const &number)
bool isZero(ValueType const &a)
Definition constants.cpp:39
bool isInteger(ValueType const &number)
ValueType abs(ValueType const &number)
ValueType zero()
Definition constants.cpp:24
ValueType pow(ValueType const &value, int_fast64_t exponent)
ValueType one()
Definition constants.cpp:19
bool isInfinity(ValueType const &a)
TargetType convertNumber(SourceType const &number)
size_t operator()(std::vector< ValueType > const &vec) const
Definition vector.h:21