pumped cudd to -O3, fixed reference of linear equation solver, removed superfluous multiplications in symbolic dtmc helper

resources/3rdparty/include_cudd.cmake

@@ -23,7 +23,7 @@ ExternalProject_Add(
         PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0
         PATCH_COMMAND ${AUTORECONF}
         CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
-        BUILD_COMMAND make "CFLAGS=-O2 -w"
+        BUILD_COMMAND make "CFLAGS=-O3 -w"
         INSTALL_COMMAND make install
         BUILD_IN_SOURCE 0
         LOG_CONFIGURE ON
@@ -49,4 +49,4 @@ else()
     list(APPEND STORM_DEP_TARGETS cudd_STATIC)
 endif()
 
-message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.")
+message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.")

src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@@ -58,7 +58,7 @@ namespace storm {
                         
                         // Solve the equation system.
                         std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
-                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector);
+                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0), subvector);
                         
                         return statesWithProbability01.second.template toAdd<ValueType>() + result;
                     } else {
@@ -175,7 +175,7 @@ namespace storm {
 
                         // Solve the equation system.
                         std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
-                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector);
+                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0), subvector);
                         
                         return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result);
                     } else {

src/storm/solver/SymbolicLinearEquationSolver.h

@@ -83,7 +83,7 @@ namespace storm {
             
         protected:
             // The matrix defining the coefficients of the linear equation system.
-            storm::dd::Add<DdType, ValueType> const& A;
+            storm::dd::Add<DdType, ValueType> A;
             
             // A BDD characterizing all rows of the equation system.
             storm::dd::Bdd<DdType> const& allRows;