change optimization direction if overridden

src/storm/solver/GmmxxMultiplier.cpp

@@ -1,5 +1,7 @@
 #include "storm/solver/GmmxxMultiplier.h"
 
+#include <boost/optional.hpp>
+
 #include "storm/adapters/RationalNumberAdapter.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/adapters/IntelTbbAdapter.h"
@@ -166,11 +168,17 @@ namespace storm {
                 choice_it = backwards ? choices->end() - 1 : choices->begin();
             }
 
+            boost::optional<storm::storage::BitVector> optimizationDirectionOverride;
+            if(this->getOptimizationDirectionOverride().is_initialized()) {
+                optimizationDirectionOverride = this->getOptimizationDirectionOverride();
+            }
+
             // Variables for correctly tracking choices (only update if new choice is strictly better).
             ValueType oldSelectedChoiceValue;
             uint64_t selectedChoice;
 
             uint64_t currentRow = backwards ? gmmMatrix.nrows() - 1 : 0;
+            uint64_t currentRowGroup = backwards ? rowGroupIndices.size() - 1 : 0;
             auto row_group_it = backwards ? rowGroupIndices.end() - 2 : rowGroupIndices.begin();
             auto row_group_ite = backwards ? rowGroupIndices.begin() - 1 : rowGroupIndices.end() - 1;
             while (row_group_it != row_group_ite) {
@@ -213,7 +221,7 @@ namespace storm {
                             oldSelectedChoiceValue = newValue;
                         }
 
-                        if (compare(newValue, currentValue)) {
+                        if(isOverridden(currentRowGroup) ? !compare(newValue, currentValue) : compare(newValue, currentValue)) {
                             currentValue = newValue;
                             if (choices) {
                                 selectedChoice = currentRow - *row_group_it;
@@ -233,7 +241,7 @@ namespace storm {
 
                     // Finally write value to target vector.
                     *target_it = currentValue;
-                    if (choices && compare(currentValue, oldSelectedChoiceValue)) {
+                    if(choices && isOverridden(currentRowGroup) ? !compare(currentValue, oldSelectedChoiceValue) : compare(currentValue, oldSelectedChoiceValue) ) {
                         *choice_it = selectedChoice;
                     }
                 }
@@ -243,10 +251,12 @@ namespace storm {
                     --row_group_it;
                     --choice_it;
                     --target_it;
+                    --currentRowGroup;
                 } else {
                     ++row_group_it;
                     ++choice_it;
                     ++target_it;
+                    ++currentRowGroup;
                 }
             }
         }

src/storm/solver/Multiplier.cpp

@@ -84,6 +84,12 @@ namespace storm {
             return optimizationDirectionOverride;
         }
 
+        template<typename ValueType>
+        bool Multiplier<ValueType>::isOverridden(uint_fast64_t const index) const {
+            if(!optimizationDirectionOverride.is_initialized()) return false;
+            return optimizationDirectionOverride.get().get(index);
+        }
+
         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();

src/storm/solver/Multiplier.h

@@ -147,6 +147,11 @@ namespace storm {
              */
             boost::optional<storm::storage::BitVector> getOptimizationDirectionOverride() const;
 
+            /*
+             *  TODO
+             */
+            bool isOverridden(uint_fast64_t const index) const;
+
         protected:
             mutable std::unique_ptr<std::vector<ValueType>> cachedVector;
             storm::storage::SparseMatrix<ValueType> const& matrix;