From 810f423849b46a2cad7f5650478c1c0398a015c0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 16 Jan 2017 22:26:18 +0100
Subject: [PATCH] pumped cudd to -O3, fixed reference of linear equation
 solver, removed superfluous multiplications in symbolic dtmc helper

---
 resources/3rdparty/include_cudd.cmake                         | 4 ++--
 .../modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp     | 4 ++--
 src/storm/solver/SymbolicLinearEquationSolver.h               | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake
index 731758830..a23bb46f6 100644
--- a/resources/3rdparty/include_cudd.cmake
+++ b/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}.")
\ No newline at end of file
+message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.")
diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
index 84d7bcd15..c8dd1f1f3 100644
--- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp
+++ b/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 {
diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h
index 1b64c1d55..13686d3f4 100644
--- a/src/storm/solver/SymbolicLinearEquationSolver.h
+++ b/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;