diff --git a/src/storm/settings/modules/MultiplierSettings.cpp b/src/storm/settings/modules/MultiplierSettings.cpp index 7e8058c45..befa91086 100644 --- a/src/storm/settings/modules/MultiplierSettings.cpp +++ b/src/storm/settings/modules/MultiplierSettings.cpp @@ -25,8 +25,6 @@ namespace storm { std::string type = this->getOption(multiplierTypeOptionName).getArgumentByName("name").getValueAsString(); if (type == "native") { return storm::solver::MultiplierType::Native; - } else if (type == "inplace") { - return storm::solver::MultiplierType::InPlace; } else if (type == "gmmxx") { return storm::solver::MultiplierType::Gmmxx; } diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index a57633db6..0da52a06a 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -64,8 +64,6 @@ namespace storm { return std::make_unique>(matrix); case MultiplierType::Native: return std::make_unique>(matrix); - case MultiplierType::InPlace: - return std::make_unique>(matrix); } } diff --git a/src/storm/solver/NativeMultiplier.cpp b/src/storm/solver/NativeMultiplier.cpp index f2e74bb71..13b27c617 100644 --- a/src/storm/solver/NativeMultiplier.cpp +++ b/src/storm/solver/NativeMultiplier.cpp @@ -1,4 +1,3 @@ -#include #include "storm/solver/NativeMultiplier.h" #include "storm-config.h" @@ -13,40 +12,17 @@ #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" -#include "storm/utility/vector.h" namespace storm { namespace solver { - template - NativeMultiplier::NativeMultiplier(storm::storage::SparseMatrix const& matrix) : Multiplier(matrix), numRows(0) { + template + NativeMultiplier::NativeMultiplier(storm::storage::SparseMatrix const& matrix) : Multiplier(matrix) { // Intentionally left empty. } - template - void NativeMultiplier::initialize() const { - if (numRows == 0) { - numRows = this->matrix.getRowCount(); - entries.clear(); - columns.clear(); - rowIndications.clear(); - entries.reserve(this->matrix.getNonzeroEntryCount()); - columns.reserve(this->matrix.getColumnCount()); - rowIndications.reserve(numRows + 1); - - rowIndications.push_back(0); - for (IndexType r = 0; r < numRows; ++r) { - for (auto const& entry : this->matrix.getRow(r)) { - entries.push_back(entry.getValue()); - columns.push_back(entry.getColumn()); - } - rowIndications.push_back(entries.size()); - } - } - } - - template - bool NativeMultiplier::parallelize(Environment const& env) const { + template + bool NativeMultiplier::parallelize(Environment const& env) const { #ifdef STORM_HAVE_INTELTBB return storm::settings::getModule().isUseIntelTbbSet(); #else @@ -54,9 +30,8 @@ namespace storm { #endif } - template - void NativeMultiplier::multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const { - initialize(); + template + void NativeMultiplier::multiply(Environment const& env, std::vector const& x, std::vector const* b, std::vector& result) const { std::vector* target = &result; if (&x == &result) { if (this->cachedVector) { @@ -76,32 +51,13 @@ namespace storm { } } - template - void NativeMultiplier::multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b) const { - initialize(); - // multiply the rows in backwards order - IndexType r = numRows; - if (b) { - std::vector const& bRef = *b; - while (r > 0) { - --r; - ValueType xr = bRef[r]; - this->multiplyRow(r, x, xr); - x[r] = std::move(xr); - } - } else { - while (r > 0) { - --r; - ValueType xr = storm::utility::zero(); - this->multiplyRow(r, x, xr); - x[r] = std::move(xr); - } - } + template + void NativeMultiplier::multiplyGaussSeidel(Environment const& env, std::vector& x, std::vector const* b) const { + this->matrix.multiplyWithVectorBackward(x, x, b); } - template - void NativeMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - initialize(); + template + void NativeMultiplier::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { std::vector* target = &result; if (&x == &result) { if (this->cachedVector) { @@ -121,132 +77,39 @@ namespace storm { } } - template - void NativeMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices) const { - initialize(); - assert(rowGroupIndices.size() - 1 == x.size()); - // multiply the rowgroups in backwards order - IndexType g = x.size(); - if (choices) { - while (g > 0) { - --g; - x[g] = multiplyAndReduceRowGroup(dir, rowGroupIndices[g], rowGroupIndices[g + 1], x, b, &((*choices)[g])); - } - } else { - while (g > 0) { - --g; - x[g] = multiplyAndReduceRowGroup(dir, rowGroupIndices[g], rowGroupIndices[g + 1], x, b); - } - } - } - - template - void NativeMultiplier::multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const { - initialize(); - assert(rowIndex < numRows); - IndexType const& rowStart = rowIndications[rowIndex]; - IndexType const& rowEnd = rowIndications[rowIndex + 1]; - for (IndexType e = rowStart; e < rowEnd; ++e) { - value += entries[e] * x[columns[e]]; - } + template + void NativeMultiplier::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector& x, std::vector const* b, std::vector* choices) const { + this->matrix.multiplyAndReduceBackward(dir, rowGroupIndices, x, b, x, choices); } - template - void NativeMultiplier::multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const { - initialize(); - assert(rowIndex < numRows); - IndexType const& rowStart = rowIndications[rowIndex]; - IndexType const& rowEnd = rowIndications[rowIndex + 1]; - for (IndexType e = rowStart; e < rowEnd; ++e) { - val1 += entries[e] * x1[columns[e]]; - val2 += entries[e] * x2[columns[e]]; + template + void NativeMultiplier::multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const { + for (auto const& entry : this->matrix.getRow(rowIndex)) { + value += entry.getValue() * x[entry.getColumn()]; } } - template - ValueType NativeMultiplier::multiplyAndReduceRowGroup(OptimizationDirection const& dir, IndexType const& groupStart, IndexType const& groupEnd, std::vector const& x, std::vector const* b, uint_fast64_t* choice) const { - // Compute value for first row - ValueType result = b ? (*b)[groupStart] : storm::utility::zero(); - multiplyRow(groupStart, x, result); - if (choice) { - *choice = 0; - // Compute the value for the remaining rows. Keep track of the optimal choice - for (IndexType r = groupStart + 1; r < groupEnd; ++r) { - ValueType rowVal = b ? (*b)[r] : storm::utility::zero(); - multiplyRow(r, x, rowVal); - if (dir == OptimizationDirection::Minimize) { - if (rowVal < result) { - result = std::move(rowVal); - *choice = r - groupStart; - } - } else { - if (rowVal > result) { - result = std::move(rowVal); - *choice = r - groupStart; - } - } - } - } else { - // Compute the value for the remaining rows - for (IndexType r = groupStart + 1; r < groupEnd; ++r) { - ValueType rowVal = b ? (*b)[r] : storm::utility::zero(); - multiplyRow(r, x, rowVal); - if (dir == OptimizationDirection::Minimize) { - if (rowVal < result) { - result = std::move(rowVal); - } - } else { - if (rowVal > result) { - result = std::move(rowVal); - } - } - } + template + void NativeMultiplier::multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const { + for (auto const& entry : this->matrix.getRow(rowIndex)) { + val1 += entry.getValue() * x1[entry.getColumn()]; + val2 += entry.getValue() * x2[entry.getColumn()]; } - return result; - } - - template<> - storm::RationalFunction NativeMultiplier::multiplyAndReduceRowGroup(OptimizationDirection const&, uint32_t const&, uint32_t const&, std::vector const&, std::vector const*, uint_fast64_t*) const { - STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "This operation is not supported with the given value type."); - return storm::utility::zero(); } - template - void NativeMultiplier::multAdd(std::vector const& x, std::vector const* b, std::vector& result) const { - // multiply the rows sequentially (in forward order) - if (b) { - std::vector const& bRef = *b; - for (IndexType r = 0; r < numRows; ++r) { - ValueType xr = bRef[r]; - this->multiplyRow(r, x, xr); - result[r] = std::move(xr); - } - } else { - for (IndexType r = 0; r < numRows; ++r) { - ValueType xr = storm::utility::zero(); - this->multiplyRow(r, x, xr); - result[r] = std::move(xr); - } - } + + template + void NativeMultiplier::multAdd(std::vector const& x, std::vector const* b, std::vector& result) const { + this->matrix.multiplyWithVector(x, result, b); } - template - void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { - assert(rowGroupIndices.size() - 1 == x.size()); - // multiply the rowgroups in forward order - if (choices) { - for (IndexType g = 0, groupsEnd = x.size(); g < groupsEnd; ++g) { - result[g] = multiplyAndReduceRowGroup(dir, rowGroupIndices[g], rowGroupIndices[g + 1], x, b, &((*choices)[g])); - } - } else { - for (IndexType g = 0, groupsEnd = x.size(); g < groupsEnd; ++g) { - result[g] = multiplyAndReduceRowGroup(dir, rowGroupIndices[g], rowGroupIndices[g + 1], x, b); - } - } + template + void NativeMultiplier::multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + this->matrix.multiplyAndReduce(dir, rowGroupIndices, x, b, result, choices); } - template - void NativeMultiplier::multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const { + template + void NativeMultiplier::multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const { #ifdef STORM_HAVE_INTELTBB this->matrix.multiplyWithVectorParallel(x, result, b); #else @@ -255,8 +118,8 @@ namespace storm { #endif } - template - void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { + template + void NativeMultiplier::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices) const { #ifdef STORM_HAVE_INTELTBB this->matrix.multiplyAndReduceParallel(dir, rowGroupIndices, x, b, result, choices); #else @@ -265,10 +128,10 @@ namespace storm { #endif } - template class NativeMultiplier; + template class NativeMultiplier; #ifdef STORM_HAVE_CARL - template class NativeMultiplier; - template class NativeMultiplier; + template class NativeMultiplier; + template class NativeMultiplier; #endif } diff --git a/src/storm/solver/NativeMultiplier.h b/src/storm/solver/NativeMultiplier.h index d915b8fc7..90b0f1454 100644 --- a/src/storm/solver/NativeMultiplier.h +++ b/src/storm/solver/NativeMultiplier.h @@ -12,7 +12,7 @@ namespace storm { namespace solver { - template + template class NativeMultiplier : public Multiplier { public: NativeMultiplier(storm::storage::SparseMatrix const& matrix); @@ -24,14 +24,9 @@ namespace storm { virtual void multiplyRow(uint64_t const& rowIndex, std::vector const& x, ValueType& value) const override; virtual void multiplyRow2(uint64_t const& rowIndex, std::vector const& x1, ValueType& val1, std::vector const& x2, ValueType& val2) const override; - private: bool parallelize(Environment const& env) const; - void initialize() const; - - ValueType multiplyAndReduceRowGroup(OptimizationDirection const& dir, IndexType const& groupStart, IndexType const& groupEnd, std::vector const& x, std::vector const* b, uint_fast64_t* choice = nullptr) const; - void multAdd(std::vector const& x, std::vector const* b, std::vector& result) const; void multAddReduce(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; @@ -39,11 +34,6 @@ namespace storm { void multAddParallel(std::vector const& x, std::vector const* b, std::vector& result) const; void multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector const& rowGroupIndices, std::vector const& x, std::vector const* b, std::vector& result, std::vector* choices = nullptr) const; - mutable std::vector entries; - mutable std::vector columns; - mutable std::vector rowIndications; - mutable IndexType numRows; - }; } diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp index bcbe9cc47..d2148e9bc 100644 --- a/src/storm/solver/SolverSelectionOptions.cpp +++ b/src/storm/solver/SolverSelectionOptions.cpp @@ -28,8 +28,6 @@ namespace storm { switch(t) { case MultiplierType::Native: return "Native"; - case MultiplierType::InPlace: - return "InPlace"; case MultiplierType::Gmmxx: return "Gmmxx"; } diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h index 74d1dbc3c..678bc1565 100644 --- a/src/storm/solver/SolverSelectionOptions.h +++ b/src/storm/solver/SolverSelectionOptions.h @@ -7,7 +7,7 @@ namespace storm { namespace solver { ExtendEnumsWithSelectionField(MinMaxMethod, PolicyIteration, ValueIteration, LinearProgramming, Topological, RationalSearch, IntervalIteration, SoundValueIteration, TopologicalCuda) - ExtendEnumsWithSelectionField(MultiplierType, Native, InPlace, Gmmxx) + ExtendEnumsWithSelectionField(MultiplierType, Native, Gmmxx) ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration) ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration)