added opt dir override bitvector to multiplier

This is mainly used by the SMG model checker to override row group
optimization directions.

src/storm/environment/solver/MultiplierEnvironment.cpp

@@ -6,28 +6,36 @@
 #include "storm/utility/macros.h"
 
 namespace storm {
-    
+
     MultiplierEnvironment::MultiplierEnvironment() {
         auto const& multiplierSettings = storm::settings::getModule<storm::settings::modules::MultiplierSettings>();
         type = multiplierSettings.getMultiplierType();
         typeSetFromDefault = multiplierSettings.isMultiplierTypeSetFromDefaultValue();
     }
-    
+
     MultiplierEnvironment::~MultiplierEnvironment() {
         // Intentionally left empty
     }
-    
+
     storm::solver::MultiplierType const& MultiplierEnvironment::getType() const {
         return type;
     }
-    
+
     bool const& MultiplierEnvironment::isTypeSetFromDefault() const {
         return typeSetFromDefault;
     }
-    
+
     void MultiplierEnvironment::setType(storm::solver::MultiplierType value, bool isSetFromDefault) {
         type = value;
         typeSetFromDefault = isSetFromDefault;
     }
-    
+
+    void MultiplierEnvironment::setOptimizationDirectionOverride(storm::storage::BitVector optDirOverride) {
+        optimizationDirectionOverride = optDirOverride;
+    }
+
+    boost::optional<storm::storage::BitVector> const& MultiplierEnvironment::getOptimizationDirectionOverride() const {
+        return optimizationDirectionOverride;
+    }
+
 }

src/storm/environment/solver/MultiplierEnvironment.h

@@ -1,23 +1,31 @@
 #pragma once
 
+#include <boost/optional.hpp>
+
 #include "storm/environment/solver/SolverEnvironment.h"
 #include "storm/solver/SolverSelectionOptions.h"
 
+#include "storm/storage/BitVector.h"
+
 namespace storm {
-    
+
     class MultiplierEnvironment {
     public:
-        
+
         MultiplierEnvironment();
         ~MultiplierEnvironment();
-        
+
         storm::solver::MultiplierType const& getType() const;
         bool const& isTypeSetFromDefault() const;
         void setType(storm::solver::MultiplierType value, bool isSetFromDefault = false);
-        
+
+        void setOptimizationDirectionOverride(storm::storage::BitVector optimizationDirectionOverride);
+        boost::optional<storm::storage::BitVector> const& getOptimizationDirectionOverride() const;
+
     private:
         storm::solver::MultiplierType type;
         bool typeSetFromDefault;
+
+        boost::optional<storm::storage::BitVector> optimizationDirectionOverride = boost::none;
     };
 }
-

src/storm/solver/Multiplier.cpp

@@ -18,17 +18,17 @@
 
 namespace storm {
     namespace solver {
-        
+
         template<typename ValueType>
         Multiplier<ValueType>::Multiplier(storm::storage::SparseMatrix<ValueType> const& matrix) : matrix(matrix) {
             // Intentionally left empty.
         }
-    
+
         template<typename ValueType>
         void Multiplier<ValueType>::clearCache() const {
             cachedVector.reset();
         }
-        
+
         template<typename ValueType>
         void Multiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
             multiplyAndReduce(env, dir, this->matrix.getRowGroupIndices(), x, b, result, choices);
@@ -38,7 +38,7 @@ namespace storm {
         void Multiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
             multiplyAndReduceGaussSeidel(env, dir, this->matrix.getRowGroupIndices(), x, b, choices, backwards);
         }
-    
+
         template<typename ValueType>
         void Multiplier<ValueType>::repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
             storm::utility::ProgressMeasurement progress("multiplications");
@@ -53,7 +53,7 @@ namespace storm {
                 }
             }
         }
-    
+
         template<typename ValueType>
         void Multiplier<ValueType>::repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const {
             storm::utility::ProgressMeasurement progress("multiplications");
@@ -67,17 +67,27 @@ namespace storm {
                 }
             }
         }
-    
+
         template<typename ValueType>
         void Multiplier<ValueType>::multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const {
             multiplyRow(rowIndex, x1, val1);
             multiplyRow(rowIndex, x2, val2);
         }
-        
+
+        template<typename ValueType>
+        void Multiplier<ValueType>::setOptimizationDirectionOverride(storm::storage::BitVector const& optDirOverride) {
+            optimizationDirectionOverride = optDirOverride;
+        }
+
+        template<typename ValueType>
+        boost::optional<storm::storage::BitVector> Multiplier<ValueType>::getOptimizationDirectionOverride() const {
+            return optimizationDirectionOverride;
+        }
+
         template<typename ValueType>
         std::unique_ptr<Multiplier<ValueType>> MultiplierFactory<ValueType>::create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix) {
             auto type = env.solver().multiplier().getType();
-            
+
             // Adjust the multiplier type if an eqsolver was specified but not a multiplier
             if (!env.solver().isLinearEquationSolverTypeSetFromDefaultValue() && env.solver().multiplier().isTypeSetFromDefault()) {
                 bool changed = false;
@@ -90,7 +100,7 @@ namespace storm {
                 }
                 STORM_LOG_INFO_COND(!changed, "Selecting '" + toString(type) + "' as the multiplier type to match the selected equation solver. If you want to override this, please explicitly specify a different multiplier type.");
             }
-            
+
             switch (type) {
                 case MultiplierType::Gmmxx:
                     return std::make_unique<GmmxxMultiplier<ValueType>>(matrix);
@@ -99,16 +109,16 @@ namespace storm {
             }
             STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Unknown MultiplierType");
         }
-        
+
         template class Multiplier<double>;
         template class MultiplierFactory<double>;
-        
+
 #ifdef STORM_HAVE_CARL
         template class Multiplier<storm::RationalNumber>;
         template class MultiplierFactory<storm::RationalNumber>;
         template class Multiplier<storm::RationalFunction>;
         template class MultiplierFactory<storm::RationalFunction>;
 #endif
-        
+
     }
 }

src/storm/solver/Multiplier.h

@@ -2,34 +2,37 @@
 
 #include <vector>
 #include <memory>
+#include <boost/optional.hpp>
+
+#include "storm/storage/BitVector.h"
 
 #include "storm/solver/OptimizationDirection.h"
 #include "storm/solver/MultiplicationStyle.h"
 
 namespace storm {
-    
+
     class Environment;
-    
+
     namespace storage {
         template<typename ValueType>
         class SparseMatrix;
     }
-    
+
     namespace solver {
-        
+
         template<typename ValueType>
         class Multiplier {
         public:
-            
+
             Multiplier(storm::storage::SparseMatrix<ValueType> const& matrix);
-            
+
             virtual ~Multiplier() = default;
-            
+
             /*
              * Clears the currently cached data of this multiplier in order to free some memory.
              */
             virtual void clearCache() const;
-            
+
             /*!
              * Performs a matrix-vector multiplication x' = A*x + b.
              *
@@ -41,7 +44,7 @@ namespace storm {
              * to the number of rows of A. Can be the same as the x vector.
              */
             virtual void multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const = 0;
-            
+
             /*!
              * Performs a matrix-vector multiplication in gauss-seidel style.
              *
@@ -52,7 +55,7 @@ namespace storm {
              * @param backwards if true, the iterations will be performed beginning from the last row and ending at the first row.
              */
             virtual void multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards = true) const = 0;
-            
+
             /*!
              * Performs a matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups
              * so that the resulting vector has the size of number of row groups of A.
@@ -69,7 +72,7 @@ namespace storm {
              */
             void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const;
             virtual void multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices = nullptr) const = 0;
-            
+
             /*!
              * Performs a matrix-vector multiplication in gauss-seidel style and then minimizes/maximizes over the row groups
              * so that the resulting vector has the size of number of row groups of A.
@@ -87,7 +90,7 @@ namespace storm {
              */
             void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const;
             virtual void multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices = nullptr, bool backwards = true) const = 0;
-            
+
             /*!
              * Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b. After
              * performing the necessary multiplications, the result is written to the input vector x. Note that the
@@ -100,7 +103,7 @@ namespace storm {
              * @param n The number of times to perform the multiplication.
              */
             void repeatedMultiply(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const;
-            
+
             /*!
              * Performs repeated matrix-vector multiplication x' = A*x + b and then minimizes/maximizes over the row groups
              * so that the resulting vector has the size of number of row groups of A.
@@ -115,7 +118,7 @@ namespace storm {
              * @param n The number of times to perform the multiplication.
              */
             void repeatedMultiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType>& x, std::vector<ValueType> const* b, uint64_t n) const;
-  
+
             /*!
              * Multiplies the row with the given index with x and adds the result to the provided value
              * @param rowIndex The index of the considered row
@@ -123,7 +126,7 @@ namespace storm {
              * @param value The multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix.
              */
             virtual void multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const = 0;
-            
+
             /*!
              * Multiplies the row with the given index with x1 and x2 and adds the given offset o1 and o2, respectively
              * @param rowIndex The index of the considered row
@@ -133,12 +136,24 @@ namespace storm {
              * @param val2 The second multiplication result is added to this value. It shall not reffer to a value in x or in the Matrix.
              */
             virtual void multiplyRow2(uint64_t const& rowIndex, std::vector<ValueType> const& x1, ValueType& val1, std::vector<ValueType> const& x2, ValueType& val2) const;
-            
+
+            /*
+             *  TODO
+             */
+            void setOptimizationDirectionOverride(storm::storage::BitVector const& optimizationDirectionOverride);
+
+            /*
+             *  TODO
+             */
+            boost::optional<storm::storage::BitVector> getOptimizationDirectionOverride() const;
+
         protected:
             mutable std::unique_ptr<std::vector<ValueType>> cachedVector;
             storm::storage::SparseMatrix<ValueType> const& matrix;
+
+            boost::optional<storm::storage::BitVector> optimizationDirectionOverride = boost::none;
         };
-        
+
         template<typename ValueType>
         class MultiplierFactory {
         public:
@@ -147,6 +162,6 @@ namespace storm {
 
             std::unique_ptr<Multiplier<ValueType>> create(Environment const& env, storm::storage::SparseMatrix<ValueType> const& matrix);
         };
-        
+
     }
 }