Classes
struct	VectorHash

Functions
std::set< storm::RationalFunctionVariable >	getVariables (std::vector< storm::RationalFunction > const &vector)

template<class T >
std::size_t	findOrInsert (std::vector< T > &vector, T &&element)
	Finds the given element in the given vector.

template<typename T >
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 >())

template<class T >
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.

template<class T >
void	setVectorValues (std::vector< T > &vector, storm::storage::BitVector const &positions, T value)
	Sets the provided value at the provided positions in the given vector.

template<typename T >
void	setNonzeroIndices (std::vector< T > const &vec, storm::storage::BitVector &bv)

template<class OutputIterator , class Size , class Assignable >
void	iota_n (OutputIterator first, Size n, Assignable value)
	Iota function as a helper for efficient creating a range in a vector.

template<typename T >
std::vector< T >	buildVectorForRange (T min, T max)
	Constructs a vector [min, min+1, ...., max-1].

template<typename T >
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, the second index refers to the entry with the second highest value, ... Example: v={3,8,4,5} yields res={1,3,2,0}.

template<typename T >
bool	isUnique (std::vector< T > const &v)
	Returns true iff every element in the given vector is unique, i.e., there are no i,j with i!=j and v[i]==v[j].

template<typename T , typename Comparator >
bool	compareElementWise (std::vector< T > const &left, std::vector< T > const &right, Comparator comp=std::less< T >())

template<class T >
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 another vector.

template<class T >
void	selectVectorValues (std::vector< T > &vector, storm::storage::BitVector const &positions, std::vector< uint_fast64_t > const &rowGrouping, std::vector< T > const &values)
	Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector.

template<class T >
void	selectVectorValues (std::vector< T > &vector, std::vector< uint_fast64_t > const &rowGroupToRowIndexMapping, std::vector< uint_fast64_t > const &rowGrouping, std::vector< T > const &values)
	Selects one element out of each row group and writes it to the target vector.

template<class T >
void	selectVectorValues (std::vector< T > &vector, std::vector< uint_fast64_t > const &indexSequence, std::vector< T > const &values)
	Selects values from a vector at the specified sequence of indices and writes them into another vector.

template<class T >
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 as given by the size of the corresponding group of elements.

template<class T >
void	subtractFromConstantOneVector (std::vector< T > &vector)
	Subtracts the given vector from the constant one-vector and writes the result to the input vector.

template<class T >
void	addFilteredVectorGroupsToGroupedVector (std::vector< T > &target, std::vector< T > const &source, storm::storage::BitVector const &filter, std::vector< uint_fast64_t > const &rowGroupIndices)

template<class T >
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 elements of the i-th row group in the target vector.

template<class T >
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 all elements of the i-th row group in the target vector.

template<class InValueType1 , class InValueType2 , class OutValueType , class Operation >
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 vector.

template<class InValueType1 , class InValueType2 , class OutValueType , class Operation >
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 vector.

template<class InValueType , class OutValueType , class Operation >
void	applyPointwise (std::vector< InValueType > const &operand, std::vector< OutValueType > &target, Operation f=Operation())
	Applies the given function pointwise on the given vector.

template<class InValueType1 , class InValueType2 , class OutValueType >
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.

template<class InValueType1 , class InValueType2 , class OutValueType >
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.

template<class InValueType1 , class InValueType2 , class OutValueType >
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.

template<class InValueType1 , class InValueType2 , class OutValueType >
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.

template<class ValueType1 , class ValueType2 >
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 vector.

template<class InValueType1 , class InValueType2 , class InValueType3 >
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 the second vector times the given factor) and writes the result into the first vector.

template<class T >
T	dotProduct (std::vector< T > const &firstOperand, std::vector< T > const &secondOperand)
	Computes the dot product (aka scalar product) and returns the result.

template<class T >
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 given function evaluate to true.

template<class T >
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 than zero.

template<class T >
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 zero.

template<class T >
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 one.

template<class T >
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 one.

template<typename VT >
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.

template<typename VT >
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.

template<typename VT >
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.

template<class T , class Filter >
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 group.

template<class T >
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.

template<class T >
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.

template<class T >
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.

template<class T >
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.

template<>
bool	equalModuloPrecision (double const &val1, double const &val2, double const &precision, bool relativeError)

template<class T >
bool	equalModuloPrecision (std::vector< T > const &vectorLeft, std::vector< T > const &vectorRight, T const &precision, bool relativeError)
	Compares the two vectors and determines whether they are equal modulo the provided precision.

template<class T >
bool	equalModuloPrecision (std::vector< T > const &vectorLeft, std::vector< T > const &vectorRight, storm::storage::BitVector const &positions, T const &precision, bool relativeError)
	Compares the two vectors at the specified positions and determines whether they are equal modulo the provided precision.

template<class T >
bool	equalModuloPrecision (std::vector< T > const &vectorLeft, std::vector< T > const &vectorRight, std::vector< uint_fast64_t > const &positions, T const &precision, bool relativeError)
	Compares the two vectors at the specified positions and determines whether they are equal modulo the provided precision.

template<class T >
T	maximumElementAbs (std::vector< T > const &vector)

template<class T >
T	maximumElementDiff (std::vector< T > const &vectorLeft, std::vector< T > const &vectorRight)

template<class T >
T	computeSquaredNorm2Difference (std::vector< T > const &b1, std::vector< T > const &b2)

template<typename ValueType >
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.

template<typename ValueType >
void	clip (std::vector< ValueType > &x, ValueType const &bound, bool boundFromBelow)
	Takes the input vector and ensures that all entries conform to the bounds.

template<typename ValueType >
void	clip (std::vector< ValueType > &x, std::vector< ValueType > const &bounds, bool boundFromBelow)
	Takes the input vector and ensures that all entries conform to the bounds.

template<class T >
std::vector< T >	getConstrainedOffsetVector (std::vector< T > const &offsetVector, storm::storage::BitVector const &constraint)
	Takes the given offset vector and applies the given contraint.

template<typename TargetType , typename SourceType >
std::vector< TargetType >	convertNumericVector (std::vector< SourceType > const &oldVector)
	Converts the given vector to the given ValueType Assumes that both, TargetType and SourceType are numeric.

template<typename TargetType , typename SourceType >
void	convertNumericVector (std::vector< SourceType > const &inputVector, std::vector< TargetType > &targetVector)
	Converts the given vector to the given ValueType Assumes that both, TargetType and SourceType are numeric.

template<typename NewValueType , typename ValueType >
std::vector< NewValueType >	toValueType (std::vector< ValueType > const &oldVector)
	Converts the given vector to the given ValueType.

template<typename ValueType , typename TargetValueType >
std::enable_if< std::is_same< ValueType, storm::RationalNumber >::value, std::pair< std::vector< TargetValueType >, ValueType > >::type	toIntegralVector (std::vector< ValueType > const &vec)

template<typename ValueType , typename TargetValueType >
std::enable_if<!std::is_same< ValueType, storm::RationalNumber >::value, std::pair< std::vector< TargetValueType >, ValueType > >::type	toIntegralVector (std::vector< ValueType > const &vec)

template<typename Type >
std::vector< Type >	filterVector (std::vector< Type > const &in, storm::storage::BitVector const &filter)

template<typename Type >
void	filterVectorInPlace (std::vector< Type > &v, storm::storage::BitVector const &filter)

template<typename T >
bool	hasNegativeEntry (std::vector< T > const &v)

template<typename T >
bool	hasPositiveEntry (std::vector< T > const &v)

template<typename T >
bool	hasNonZeroEntry (std::vector< T > const &v)

template<typename T >
bool	hasZeroEntry (std::vector< T > const &v)

template<typename T >
bool	hasInfinityEntry (std::vector< T > const &v)

template<typename T >
std::vector< T >	applyInversePermutation (std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source)

template<typename T >
std::vector< T >	applyInversePermutationToGroupedVector (std::vector< uint64_t > const &inversePermutation, std::vector< T > const &source, std::vector< uint64_t > const &rowGroupIndices)

template<typename ValueType >
std::string	toString (std::vector< ValueType > const &vector)
	Output vector as string.

template<typename PT1 , typename PT2 >
std::string	toString (std::vector< std::pair< PT1, PT2 > > const &vector)

Function Documentation

◆ addFilteredVectorGroupsToGroupedVector()

template<class T >

void storm::utility::vector::addFilteredVectorGroupsToGroupedVector	(	std::vector< T > &	target,
		std::vector< T > const &	source,
		storm::storage::BitVector const &	filter,
		std::vector< uint_fast64_t > const &	rowGroupIndices
	)

Definition at line 289 of file vector.h.

◆ addFilteredVectorToGroupedVector()

template<class T >

void storm::utility::vector::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 all elements of the i-th row group in the target vector.

Parameters

target	The target ("row grouped") vector.
source	The source vector.
rowGroupIndices	A vector representing the row groups in the target vector.

Definition at line 335 of file vector.h.

◆ addScaledVector()

template<class InValueType1 , class InValueType2 , class InValueType3 >

void storm::utility::vector::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 the second vector times the given factor) and writes the result into the first vector.

Parameters

firstOperand	The first operand.
secondOperand	The second operand
factor	The factor for the elements of the second operand

Definition at line 504 of file vector.h.

◆ addVectors()

template<class InValueType1 , class InValueType2 , class OutValueType >

void storm::utility::vector::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.

Parameters

firstOperand	The first operand.
secondOperand	The second operand
target	The target vector.

Definition at line 443 of file vector.h.

◆ addVectorToGroupedVector()

template<class T >

void storm::utility::vector::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 elements of the i-th row group in the target vector.

Parameters

target	The target ("row grouped") vector.
source	The source vector.
rowGroupIndices	A vector representing the row groups in the target vector.

Definition at line 310 of file vector.h.

◆ applyInversePermutation()

template<typename T >

std::vector< T > storm::utility::vector::applyInversePermutation	(	std::vector< uint64_t > const &	inversePermutation,
		std::vector< T > const &	source
	)

Definition at line 1267 of file vector.h.

◆ applyInversePermutationToGroupedVector()

template<typename T >

std::vector< T > storm::utility::vector::applyInversePermutationToGroupedVector	(	std::vector< uint64_t > const &	inversePermutation,
		std::vector< T > const &	source,
		std::vector< uint64_t > const &	rowGroupIndices
	)

Definition at line 1277 of file vector.h.

◆ applyPointwise() [1/2]

template<class InValueType , class OutValueType , class Operation >

void storm::utility::vector::applyPointwise	(	std::vector< InValueType > const &	operand,
		std::vector< OutValueType > &	target,
		Operation	f = `Operation()`
	)

Applies the given function pointwise on the given vector.

Parameters

operand	The vector to which to apply the function.
target	The target vector.
function	The function to apply.

Definition at line 422 of file vector.h.

◆ applyPointwise() [2/2]

template<class InValueType1 , class InValueType2 , class OutValueType , class Operation >

void storm::utility::vector::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 vector.

To obtain an in-place operation, the third vector may be equal to any of the other two vectors.

Parameters

firstOperand	The first operand.
secondOperand	The second operand.
target	The target vector.

Definition at line 398 of file vector.h.

◆ applyPointwiseTernary()

template<class InValueType1 , class InValueType2 , class OutValueType , class Operation >

void storm::utility::vector::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 vector.

To obtain an in-place operation, the third vector may be equal to any of the other two vectors.

Parameters

firstOperand	The first operand.
secondOperand	The second operand.
target	The target vector.

Definition at line 356 of file vector.h.

◆ buildVectorForRange()

template<typename T >

std::vector< T > storm::utility::vector::buildVectorForRange	(	T	min,
		T	max
	)

inline

Constructs a vector [min, min+1, ...., max-1].

Definition at line 134 of file vector.h.

◆ clip() [1/3]

template<typename ValueType >

void storm::utility::vector::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 at line 1041 of file vector.h.

◆ clip() [2/3]

template<typename ValueType >

void storm::utility::vector::clip	(	std::vector< ValueType > &	x,
		std::vector< ValueType > const &	bounds,
		bool	boundFromBelow
	)

Takes the input vector and ensures that all entries conform to the bounds.

Definition at line 1069 of file vector.h.

◆ clip() [3/3]

template<typename ValueType >

void storm::utility::vector::clip	(	std::vector< ValueType > &	x,
		ValueType const &	bound,
		bool	boundFromBelow
	)

Takes the input vector and ensures that all entries conform to the bounds.

Definition at line 1055 of file vector.h.

◆ compareElementWise()

template<typename T , typename Comparator >

bool storm::utility::vector::compareElementWise	(	std::vector< T > const &	left,
		std::vector< T > const &	right,
		Comparator	comp = `std::less<T>()`
	)

Definition at line 177 of file vector.h.

◆ computeSquaredNorm2Difference()

template<class T >

T storm::utility::vector::computeSquaredNorm2Difference	(	std::vector< T > const &	b1,
		std::vector< T > const &	b2
	)

Definition at line 1021 of file vector.h.

◆ convertNumericVector() [1/2]

template<typename TargetType , typename SourceType >

void storm::utility::vector::convertNumericVector	(	std::vector< SourceType > const &	inputVector,
		std::vector< TargetType > &	targetVector
	)

Converts the given vector to the given ValueType Assumes that both, TargetType and SourceType are numeric.

Parameters

inputVector	the vector that needs to be converted
targetVector	the vector where the result is written to. Should have the same size as inputVector

Note: this does not allocate new memory

Definition at line 1138 of file vector.h.

◆ convertNumericVector() [2/2]

template<typename TargetType , typename SourceType >

std::vector< TargetType > storm::utility::vector::convertNumericVector ( std::vector< SourceType > const & oldVector )

Converts the given vector to the given ValueType Assumes that both, TargetType and SourceType are numeric.

Returns: the resulting vector

Definition at line 1119 of file vector.h.

◆ divideVectorsPointwise()

template<class InValueType1 , class InValueType2 , class OutValueType >

void storm::utility::vector::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.

Parameters

firstOperand	The first operand.
secondOperand	The second operand
target	The target vector.

Definition at line 480 of file vector.h.

◆ dotProduct()

template<class T >

T storm::utility::vector::dotProduct	(	std::vector< T > const &	firstOperand,
		std::vector< T > const &	secondOperand
	)

Computes the dot product (aka scalar product) and returns the result.

Parameters

firstOperand	The first operand.
secondOperand	The second operand

Returns: firstOperand*secondOperand

Definition at line 517 of file vector.h.

◆ equalModuloPrecision() [1/5]

template<>

bool storm::utility::vector::equalModuloPrecision	(	double const &	val1,
		double const &	val2,
		double const &	precision,
		bool	relativeError
	)

inline

Definition at line 904 of file vector.h.

◆ equalModuloPrecision() [2/5]

template<class T >

bool storm::utility::vector::equalModuloPrecision	(	std::vector< T > const &	vectorLeft,
		std::vector< T > const &	vectorRight,
		std::vector< uint_fast64_t > const &	positions,
		T const &	precision,
		bool	relativeError
	)

Compares the two vectors at the specified positions and determines whether they are equal modulo the provided precision.

Depending on whether the flag is set, the difference between the vectors is computed relative to the value or in absolute terms.

Parameters

vectorLeft	The first vector of the comparison.
vectorRight	The second vector of the comparison.
precision	The precision up to which the vectors are to be checked for equality.
positions	A vector representing a set of positions at which the vectors are compared.
relativeError	If set, the difference between the vectors is computed relative to the value or in absolute terms.

Definition at line 984 of file vector.h.

◆ equalModuloPrecision() [3/5]

template<class T >

bool storm::utility::vector::equalModuloPrecision	(	std::vector< T > const &	vectorLeft,
		std::vector< T > const &	vectorRight,
		storm::storage::BitVector const &	positions,
		T const &	precision,
		bool	relativeError
	)

Compares the two vectors at the specified positions and determines whether they are equal modulo the provided precision.

Depending on whether the flag is set, the difference between the vectors is computed relative to the value or in absolute terms.

Parameters

vectorLeft	The first vector of the comparison.
vectorRight	The second vector of the comparison.
precision	The precision up to which the vectors are to be checked for equality.
positions	A vector representing a set of positions at which the vectors are compared.
relativeError	If set, the difference between the vectors is computed relative to the value or in absolute terms.

Definition at line 959 of file vector.h.

◆ equalModuloPrecision() [4/5]

template<class T >

bool storm::utility::vector::equalModuloPrecision	(	std::vector< T > const &	vectorLeft,
		std::vector< T > const &	vectorRight,
		T const &	precision,
		bool	relativeError
	)

Compares the two vectors and determines whether they are equal modulo the provided precision.

Depending on whether the flag is set, the difference between the vectors is computed relative to the value or in absolute terms.

Parameters

vectorLeft	The first vector of the comparison.
vectorRight	The second vector of the comparison.
precision	The precision up to which the vectors are to be checked for equality.
relativeError	If set, the difference between the vectors is computed relative to the value or in absolute terms.

Definition at line 932 of file vector.h.

◆ equalModuloPrecision() [5/5]

template<class T >

bool storm::utility::vector::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.

The provided flag additionaly specifies whether the error is computed in relative or absolute terms.

Parameters

val1	The first value to compare.
val2	The second value to compare.
precision	The precision up to which the elements are compared.
relativeError	If set, the error is computed relative to the second value.

Returns: True iff the elements are considered equal.

Definition at line 884 of file vector.h.

◆ filter()

template<class T >

storm::storage::BitVector storm::utility::vector::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 given function evaluate to true.

Parameters

values	The vector of values.
function	The function that selects some elements.

Returns: The resulting bit vector.

Definition at line 530 of file vector.h.

◆ filterGreaterZero()

template<class T >

storm::storage::BitVector storm::utility::vector::filterGreaterZero ( std::vector< T > const & values )

Retrieves a bit vector containing all the indices for which the value at this position is greater than zero.

Parameters

values The vector of values.

Returns: The resulting bit vector.

Definition at line 552 of file vector.h.

◆ filterInfinity()

template<class T >

storm::storage::BitVector storm::utility::vector::filterInfinity ( std::vector< T > const & values )

Retrieves a bit vector containing all the indices for which the value at this position is equal to one.

Parameters

values The vector of values.

Returns: The resulting bit vector.

Definition at line 585 of file vector.h.

◆ filterOne()

template<class T >

storm::storage::BitVector storm::utility::vector::filterOne ( std::vector< T > const & values )

Retrieves a bit vector containing all the indices for which the value at this position is equal to one.

Parameters

values The vector of values.

Returns: The resulting bit vector.

Definition at line 574 of file vector.h.

◆ filterVector()

template<typename Type >

std::vector< Type > storm::utility::vector::filterVector	(	std::vector< Type > const &	in,
		storm::storage::BitVector const &	filter
	)

Definition at line 1213 of file vector.h.

◆ filterVectorInPlace()

template<typename Type >

void storm::utility::vector::filterVectorInPlace	(	std::vector< Type > &	v,
		storm::storage::BitVector const &	filter
	)

Definition at line 1224 of file vector.h.

◆ filterZero()

template<class T >

storm::storage::BitVector storm::utility::vector::filterZero ( std::vector< T > const & values )

Retrieves a bit vector containing all the indices for which the value at this position is equal to zero.

Parameters

values The vector of values.

Returns: The resulting bit vector.

Definition at line 563 of file vector.h.

◆ findOrInsert()

template<class T >

std::size_t storm::utility::vector::findOrInsert	(	std::vector< T > &	vector,
		T &&	element
	)

Finds the given element in the given vector.

If the vector does not contain the element, it is inserted (at the end of vector). Either way, the returned value will be the position of the element inside the vector,

Note: old indices to other elements remain valid, as the vector will not be sorted.

Parameters

vector	The vector in which the element is searched and possibly insert
element	The element that will be searched for (or inserted)

Returns: The position at which the element is located

Definition at line 49 of file vector.h.

◆ getConstrainedOffsetVector()

template<class T >

std::vector< T > storm::utility::vector::getConstrainedOffsetVector	(	std::vector< T > const &	offsetVector,
		storm::storage::BitVector const &	constraint
	)

Takes the given offset vector and applies the given contraint.

That is, it produces another offset vector that contains the relative offsets of the entries given by the constraint.

Parameters

offsetVector	The offset vector to constrain.
constraint	The constraint to apply to the offset vector.

Returns: An offset vector that contains all selected relative offsets.

Definition at line 1090 of file vector.h.

◆ getSortedIndices()

template<typename T >

std::vector< uint_fast64_t > storm::utility::vector::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, the second index refers to the entry with the second highest value, ... Example: v={3,8,4,5} yields res={1,3,2,0}.

Definition at line 149 of file vector.h.

◆ getVariables()

std::set< storm::RationalFunctionVariable > storm::utility::vector::getVariables ( std::vector< storm::RationalFunction > const & vector )

inline

Definition at line 5 of file rationalfunction.h.

◆ hasInfinityEntry()

template<typename T >

bool storm::utility::vector::hasInfinityEntry ( std::vector< T > const & v )

Definition at line 1262 of file vector.h.

◆ hasNegativeEntry()

template<typename T >

bool storm::utility::vector::hasNegativeEntry ( std::vector< T > const & v )

Definition at line 1242 of file vector.h.

◆ hasNonZeroEntry()

template<typename T >

bool storm::utility::vector::hasNonZeroEntry ( std::vector< T > const & v )

Definition at line 1252 of file vector.h.

◆ hasPositiveEntry()

template<typename T >

bool storm::utility::vector::hasPositiveEntry ( std::vector< T > const & v )

Definition at line 1247 of file vector.h.

◆ hasZeroEntry()

template<typename T >

bool storm::utility::vector::hasZeroEntry ( std::vector< T > const & v )

Definition at line 1257 of file vector.h.

◆ iota_n()

template<class OutputIterator , class Size , class Assignable >

void storm::utility::vector::iota_n	(	OutputIterator	first,
		Size	n,
		Assignable	value
	)

Iota function as a helper for efficient creating a range in a vector.

See also: buildVectorForRange

Definition at line 126 of file vector.h.

◆ isUnique()

template<typename T >

bool storm::utility::vector::isUnique ( std::vector< T > const & v )

Returns true iff every element in the given vector is unique, i.e., there are no i,j with i!=j and v[i]==v[j].

Definition at line 159 of file vector.h.

◆ max_if()

template<typename VT >

VT storm::utility::vector::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.

Parameters

values	The values in which to search.
filter	The filter to use.

Returns: The maximum over the selected values.

Definition at line 612 of file vector.h.

◆ maximumElementAbs()

template<class T >

T storm::utility::vector::maximumElementAbs ( std::vector< T > const & vector )

Definition at line 998 of file vector.h.

◆ maximumElementDiff()

template<class T >

T storm::utility::vector::maximumElementDiff	(	std::vector< T > const &	vectorLeft,
		std::vector< T > const &	vectorRight
	)

Definition at line 1007 of file vector.h.

◆ min_if()

template<typename VT >

VT storm::utility::vector::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.

Parameters

values	The values in which to search.
filter	The filter to use.

Returns: The minimum over the selected values.

Definition at line 635 of file vector.h.

◆ multiplyVectorsPointwise()

template<class InValueType1 , class InValueType2 , class OutValueType >

void storm::utility::vector::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.

Parameters

firstOperand	The first operand.
secondOperand	The second operand
target	The target vector.

Definition at line 467 of file vector.h.

◆ reduceVector()

template<class T , class Filter >

void storm::utility::vector::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 group.

Parameters

source	The source vector which is to be reduced.
target	The target vector into which a single element from each row group is written.
rowGrouping	A vector that specifies the begin and end of each group of elements in the values vector.
filter	A function that compares two elements v1 and v2 according to some filter criterion. This function must return true iff v1 is supposed to be taken instead of v2.
choices	If non-null, this vector is used to store the choices made during the selection.

Definition at line 735 of file vector.h.

◆ reduceVectorMax()

template<class T >

void storm::utility::vector::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.

Parameters

source	The source vector which is to be reduced.
target	The target vector into which a single element from each row group is written.
rowGrouping	A vector that specifies the begin and end of each group of elements in the source vector.
choices	If non-null, this vector is used to store the choices made during the selection.

Definition at line 829 of file vector.h.

◆ reduceVectorMin()

template<class T >

void storm::utility::vector::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.

Parameters

source	The source vector which is to be reduced.
target	The target vector into which a single element from each row group is written.
rowGrouping	A vector that specifies the begin and end of each group of elements in the source vector.
choices	If non-null, this vector is used to store the choices made during the selection.

Definition at line 807 of file vector.h.

◆ reduceVectorMinOrMax()

template<class T >

void storm::utility::vector::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.

Parameters

dir	If true, select the smallest, else select the largest.
source	The source vector which is to be reduced.
target	The target vector into which a single element from each row group is written.
rowGrouping	A vector that specifies the begin and end of each group of elements in the source vector.
choices	If non-null, this vector is used to store the choices made during the selection.

Definition at line 852 of file vector.h.

◆ scaleVectorInPlace()

template<class ValueType1 , class ValueType2 >

void storm::utility::vector::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 vector.

Parameters

target	The operand and target vector.
factor	The scaling factor

Definition at line 491 of file vector.h.

◆ selectVectorValues() [1/4]

template<class T >

void storm::utility::vector::selectVectorValues	(	std::vector< T > &	vector,
		std::vector< uint_fast64_t > const &	indexSequence,
		std::vector< T > const &	values
	)

Selects values from a vector at the specified sequence of indices and writes them into another vector.

Parameters

vector	The vector into which the selected elements are written.
indexSequence	a sequence of indices at which the desired values can be found
values	the values from which to select

Definition at line 247 of file vector.h.

◆ selectVectorValues() [2/4]

template<class T >

void storm::utility::vector::selectVectorValues	(	std::vector< T > &	vector,
		std::vector< uint_fast64_t > const &	rowGroupToRowIndexMapping,
		std::vector< uint_fast64_t > const &	rowGrouping,
		std::vector< T > const &	values
	)

Selects one element out of each row group and writes it to the target vector.

Parameters

vector	The target vector to which the values are written.
rowGroupToRowIndexMapping	A mapping from row group indices to an offset that specifies which of the values to take from the row group.
rowGrouping	A vector that specifies the begin and end of each group of elements in the values vector.
values	The vector from which to select the values.

Definition at line 231 of file vector.h.

◆ selectVectorValues() [3/4]

template<class T >

void storm::utility::vector::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 another vector.

Parameters

vector	The vector into which the selected elements are to be written.
positions	The positions at which to select the elements from the values vector.
values	The vector from which to select the elements.

Definition at line 189 of file vector.h.

◆ selectVectorValues() [4/4]

template<class T >

void storm::utility::vector::selectVectorValues	(	std::vector< T > &	vector,
		storm::storage::BitVector const &	positions,
		std::vector< uint_fast64_t > const &	rowGrouping,
		std::vector< T > const &	values
	)

Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector.

Parameters

vector	The vector into which the selected elements are to be written.
positions	The positions of the groups of elements that are to be selected.
rowGrouping	A vector that specifies the begin and end of each group of elements in the values vector.
values	The vector from which to select groups of elements.

Definition at line 211 of file vector.h.

◆ selectVectorValuesRepeatedly()

template<class T >

void storm::utility::vector::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 as given by the size of the corresponding group of elements.

Parameters

vector	The vector into which the selected elements are written.
positions	The positions at which to select the values.
rowGrouping	A vector that specifies the begin and end of each group of elements in the values vector. This implicitly defines the number of times any element is written to the output vector.

Definition at line 266 of file vector.h.

◆ setAllValues()

template<typename T >

void storm::utility::vector::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 at line 58 of file vector.h.

◆ setNonzeroIndices()

template<typename T >

void storm::utility::vector::setNonzeroIndices	(	std::vector< T > const &	vec,
		storm::storage::BitVector &	bv
	)

Definition at line 111 of file vector.h.

◆ setVectorValues() [1/2]

template<class T >

void storm::utility::vector::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.

Parameters

vector	The vector in which the values are to be set.
positions	The positions at which the values are to be set.
values	The values that are to be set.

Definition at line 83 of file vector.h.

◆ setVectorValues() [2/2]

template<class T >

void storm::utility::vector::setVectorValues	(	std::vector< T > &	vector,
		storm::storage::BitVector const &	positions,
		T	value
	)

Sets the provided value at the provided positions in the given vector.

Note that the vector must be at least as long.

Parameters

vector	The vector in which the value is to be set.
positions	The positions at which the value is to be set.
value	The value that is to be set.

Definition at line 103 of file vector.h.

◆ subtractFromConstantOneVector()

template<class T >

void storm::utility::vector::subtractFromConstantOneVector ( std::vector< T > & vector )

Subtracts the given vector from the constant one-vector and writes the result to the input vector.

Parameters

vector The vector that is to be subtracted from the constant one-vector.

Definition at line 282 of file vector.h.

◆ subtractVectors()

template<class InValueType1 , class InValueType2 , class OutValueType >

void storm::utility::vector::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.

Parameters

firstOperand	The first operand.
secondOperand	The second operand
target	The target vector.

Definition at line 455 of file vector.h.

◆ sum_if()

template<typename VT >

VT storm::utility::vector::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.

Parameters

values
filter

Returns: The sum of the values with a corresponding one in the filter.

Definition at line 596 of file vector.h.

◆ toIntegralVector() [1/2]

template<typename ValueType , typename TargetValueType >

std::enable_if< std::is_same< ValueType, storm::RationalNumber >::value, std::pair< std::vector< TargetValueType >, ValueType > >::type storm::utility::vector::toIntegralVector ( std::vector< ValueType > const & vec )

Definition at line 1157 of file vector.h.

◆ toIntegralVector() [2/2]

template<typename ValueType , typename TargetValueType >

std::enable_if<!std::is_same< ValueType, storm::RationalNumber >::value, std::pair< std::vector< TargetValueType >, ValueType > >::type storm::utility::vector::toIntegralVector ( std::vector< ValueType > const & vec )

Definition at line 1203 of file vector.h.

◆ toString() [1/2]

template<typename PT1 , typename PT2 >

std::string storm::utility::vector::toString ( std::vector< std::pair< PT1, PT2 > > const & vector )

Definition at line 1312 of file vector.h.

◆ toString() [2/2]

template<typename ValueType >

std::string storm::utility::vector::toString ( std::vector< ValueType > const & vector )

Output vector as string.

Parameters

vector Vector to output.

Returns: String containing the representation of the vector.

Definition at line 1298 of file vector.h.

◆ toValueType()

template<typename NewValueType , typename ValueType >

std::vector< NewValueType > storm::utility::vector::toValueType ( std::vector< ValueType > const & oldVector )

Converts the given vector to the given ValueType.

Definition at line 1147 of file vector.h.

Classes

Functions

Function Documentation

◆ addFilteredVectorGroupsToGroupedVector()

◆ addFilteredVectorToGroupedVector()

◆ addScaledVector()

◆ addVectors()

◆ addVectorToGroupedVector()

◆ applyInversePermutation()

◆ applyInversePermutationToGroupedVector()

◆ applyPointwise() [1/2]

◆ applyPointwise() [2/2]

◆ applyPointwiseTernary()

◆ buildVectorForRange()

◆ clip() [1/3]

◆ clip() [2/3]

◆ clip() [3/3]

◆ compareElementWise()

◆ computeSquaredNorm2Difference()

◆ convertNumericVector() [1/2]

◆ convertNumericVector() [2/2]

◆ divideVectorsPointwise()

◆ dotProduct()

◆ equalModuloPrecision() [1/5]

◆ equalModuloPrecision() [2/5]

◆ equalModuloPrecision() [3/5]

◆ equalModuloPrecision() [4/5]

◆ equalModuloPrecision() [5/5]

◆ filter()

◆ filterGreaterZero()

◆ filterInfinity()

◆ filterOne()

◆ filterVector()

◆ filterVectorInPlace()

◆ filterZero()

◆ findOrInsert()

◆ getConstrainedOffsetVector()

◆ getSortedIndices()

◆ getVariables()

◆ hasInfinityEntry()

◆ hasNegativeEntry()

◆ hasNonZeroEntry()

◆ hasPositiveEntry()

◆ hasZeroEntry()

◆ iota_n()

◆ isUnique()

◆ max_if()

◆ maximumElementAbs()

◆ maximumElementDiff()

◆ min_if()

◆ multiplyVectorsPointwise()

◆ reduceVector()

◆ reduceVectorMax()

◆ reduceVectorMin()

◆ reduceVectorMinOrMax()

◆ scaleVectorInPlace()

◆ selectVectorValues() [1/4]

◆ selectVectorValues() [2/4]

◆ selectVectorValues() [3/4]

◆ selectVectorValues() [4/4]

◆ selectVectorValuesRepeatedly()

◆ setAllValues()

◆ setNonzeroIndices()

◆ setVectorValues() [1/2]

◆ setVectorValues() [2/2]

◆ subtractFromConstantOneVector()

◆ subtractVectors()

◆ sum_if()

◆ toIntegralVector() [1/2]

◆ toIntegralVector() [2/2]

◆ toString() [1/2]

◆ toString() [2/2]

◆ toValueType()