Storm 1.11.1.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>
277void subtractFromConstantOneVector(std::vector<T>& vector) {
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) {
400 applyPointwise<InValueType1, InValueType2, OutValueType, std::plus<>>(firstOperand, secondOperand, 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) {
412 applyPointwise<InValueType1, InValueType2, OutValueType, std::minus<>>(firstOperand, secondOperand, 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) {
425 applyPointwise<InValueType1, InValueType2, OutValueType, std::multiplies<>>(firstOperand, secondOperand, 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) {
437 applyPointwise<InValueType1, InValueType2, OutValueType, std::divides<>>(firstOperand, secondOperand, 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) {
461 applyPointwise<InValueType1, InValueType2, InValueType1>(
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) {
542 return filter<T>(values, storm::utility::isInfinity<T>);
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()) {
1017 factor = storm::utility::one<ValueType>();
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.");
1044 result.push_back(storm::utility::convertNumber<TargetValueType, ValueType>(vScaled));
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
1088template<typename T>
1089bool hasNegativeEntry(std::vector<T> const& v) {
1090 return std::any_of(v.begin(), v.end(), [](T value) { return value < storm::utility::zero<T>(); });
1091}
1092
1093template<typename T>
1094bool hasPositiveEntry(std::vector<T> const& v) {
1095 return std::any_of(v.begin(), v.end(), [](T value) { return value > storm::utility::zero<T>(); });
1096}
1097
1098template<typename T>
1099bool hasNonZeroEntry(std::vector<T> const& v) {
1100 return std::any_of(v.begin(), v.end(), [](T value) { return !storm::utility::isZero(value); });
1101}
1102
1103template<typename T>
1104bool hasZeroEntry(std::vector<T> const& v) {
1105 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isZero(value); });
1106}
1107
1108template<typename T>
1109bool hasInfinityEntry(std::vector<T> const& v) {
1110 return std::any_of(v.begin(), v.end(), [](T value) { return storm::utility::isInfinity(value); });
1111}
1112
1113template<typename T>
1114std::vector<T> applyInversePermutation(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source) {
1115 std::vector<T> result;
1116 result.reserve(source.size());
1117 for (uint64_t sourceIndex : inversePermutation) {
1118 result.push_back(source[sourceIndex]);
1119 }
1120 return result;
1121}
1122
1123template<typename T>
1124std::vector<T> applyInversePermutationToGroupedVector(std::vector<uint64_t> const& inversePermutation, std::vector<T> const& source,
1125 std::vector<uint64_t> const& rowGroupIndices) {
1126 STORM_LOG_ASSERT(inversePermutation.size() == rowGroupIndices.size() - 1, "Inverse permutation and row group indices do not match.");
1127 std::vector<T> result;
1128 result.reserve(source.size());
1129 for (auto sourceGroupIndex : inversePermutation) {
1130 for (uint64_t sourceIndex = rowGroupIndices[sourceGroupIndex]; sourceIndex < rowGroupIndices[sourceGroupIndex + 1]; ++sourceIndex) {
1131 result.push_back(source[sourceIndex]);
1132 }
1133 }
1134 STORM_LOG_ASSERT(result.size() == source.size(), "result has unexpected length.");
1135 return result;
1136}
1137
1144template<typename ValueType>
1145std::string toString(std::vector<ValueType> const& vector) {
1146 std::stringstream stream;
1147 stream << "vector (" << vector.size() << ") [ ";
1148 if (!vector.empty()) {
1149 for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
1150 stream << vector[i] << ", ";
1151 }
1152 stream << vector.back();
1153 }
1154 stream << " ]";
1155 return stream.str();
1156}
1157
1158} // namespace vector
1159} // namespace utility
1160} // namespace storm
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
uint64_t getNextSetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to true in the bit vector.
const_iterator end() const
Returns an iterator pointing at the element past the back of the bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
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.
const_iterator begin() const
Returns an iterator to the indices of the set bits in the bit vector.
size_t size() const
Retrieves the number of bits this bit vector can store.
#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:1109
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:1145
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:1094
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:1089
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:1114
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:1104
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 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:1124
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:1099
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)
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)
size_t operator()(std::vector< ValueType > const &vec) const
Definition vector.h:21