Merge branch 'exact_equation_solver' into monolithic-dft

Former-commit-id: b32cf17622

src/CMakeLists.txt

@@ -32,7 +32,8 @@ file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOUR
 file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp)
 file(GLOB STORM_SETTINGS_FILES ${PROJECT_SOURCE_DIR}/src/settings/*.h ${PROJECT_SOURCE_DIR}/src/settings/*.cpp)
 file(GLOB STORM_SETTINGS_MODULES_FILES ${PROJECT_SOURCE_DIR}/src/settings/modules/*.h ${PROJECT_SOURCE_DIR}/src/settings/modules/*.cpp)
-file(GLOB_RECURSE STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp)
+file(GLOB STORM_SOLVER_FILES ${PROJECT_SOURCE_DIR}/src/solver/*.h ${PROJECT_SOURCE_DIR}/src/solver/*.cpp)
+file(GLOB STORM_SOLVER_STATEELIMINATION_FILES ${PROJECT_SOURCE_DIR}/src/solver/stateelimination/*.h ${PROJECT_SOURCE_DIR}/src/solver/stateelimination/*.cpp)
 file(GLOB STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp)
 file(GLOB STORM_STORAGE_BISIMULATION_FILES ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.h ${PROJECT_SOURCE_DIR}/src/storage/bisimulation/*.cpp)
 file(GLOB STORM_STORAGE_DD_FILES ${PROJECT_SOURCE_DIR}/src/storage/dd/*.h ${PROJECT_SOURCE_DIR}/src/storage/dd/*.cpp)
@@ -83,6 +84,7 @@ source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES})
 source_group(settings FILES ${STORM_SETTINGS_FILES})
 source_group(settings\\modules FILES ${STORM_SETTINGS_MODULES_FILES})
 source_group(solver FILES ${STORM_SOLVER_FILES})
+source_group(solver\\stateelimination FILES ${STORM_SOLVER_STATEELIMINATION_FILES})
 source_group(storage FILES ${STORM_STORAGE_FILES})
 source_group(storage\\bisimulation FILES ${STORM_STORAGE_BISIMULATION_FILES})
 source_group(storage\\dd FILES ${STORM_STORAGE_DD_FILES})

src/adapters/CarlAdapter.h

@@ -41,6 +41,14 @@ namespace carl {
         std::hash<Interval<Number>> h;
         return h(i);
     }
+
+}
+
+namespace cln {
+    inline size_t hash_value(cl_RA const& n) {
+        std::hash<cln::cl_RA> h;
+        return h(n);
+    }
 }
 
 namespace storm {

src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@@ -739,15 +739,12 @@ namespace storm {
                                                              eliminationOrderNeedsReversedDistances(order));
             }
             
-            std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
             storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(submatrix);
             storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(submatrixTransposed, true);
-            std::chrono::high_resolution_clock::time_point conversionEnd = std::chrono::high_resolution_clock::now();
             
             std::shared_ptr<StatePriorityQueue<ValueType>> statePriorities = createStatePriorityQueue(distanceBasedPriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, statesToEliminate);
 
             STORM_LOG_INFO("Computing conditional probilities." << std::endl);
-            std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
             uint_fast64_t numberOfStatesToEliminate = statePriorities->size();
             STORM_LOG_INFO("Eliminating " << numberOfStatesToEliminate << " states using the state elimination technique." << std::endl);
             performPrioritizedStateElimination(statePriorities, flexibleMatrix, flexibleBackwardTransitions, oneStepProbabilities, this->getModel().getInitialStates(), true);
@@ -969,10 +966,7 @@ namespace storm {
             // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
             storm::storage::FlexibleSparseMatrix<ValueType> flexibleMatrix(transitionMatrix);
             storm::storage::FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions(backwardTransitions);
-            auto conversionEnd = std::chrono::high_resolution_clock::now();
-            
-            std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
-            
+
             storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder order = storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder();
             boost::optional<std::vector<uint_fast64_t>> distanceBasedPriorities;
             if (eliminationOrderNeedsDistances(order)) {

src/solver/EliminationLinearEquationSolver.cpp

@@ -54,7 +54,7 @@ namespace storm {
         template class EliminationLinearEquationSolver<double>;
         
         // TODO: make this work with the proper implementation of solveEquationSystem.
-        template class EliminationLinearEquationSolver<storm::RationalNumber>;
+        template class EliminationLinearEquationSolver<storm::CarlRationalNumber>;
         template class EliminationLinearEquationSolver<storm::RationalFunction>;
         
     }

src/storage/SparseMatrix.cpp

@@ -1257,6 +1257,15 @@ namespace storm {
         template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
 
 #ifdef STORM_HAVE_CARL
+        // Rat Function
+        template class MatrixEntry<typename SparseMatrix<CarlRationalNumber>::index_type, CarlRationalNumber>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, CarlRationalNumber> const& entry);
+        template class SparseMatrixBuilder<CarlRationalNumber>;
+        template class SparseMatrix<CarlRationalNumber>;
+        template std::ostream& operator<<(std::ostream& out, SparseMatrix<CarlRationalNumber> const& matrix);
+        template std::vector<storm::CarlRationalNumber> SparseMatrix<CarlRationalNumber>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<storm::CarlRationalNumber> const& otherMatrix) const;
+        template bool SparseMatrix<storm::CarlRationalNumber>::isSubmatrixOf(SparseMatrix<storm::CarlRationalNumber> const& matrix) const;
+        
         // Rat Function
         template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);

src/utility/ConstantsComparator.cpp

@@ -114,6 +114,7 @@ namespace storm {
         template class ConstantsComparator<RationalFunction>;
         template class ConstantsComparator<Polynomial>;
         template class ConstantsComparator<Interval>;
+        template class ConstantsComparator<CarlRationalNumber>;
 #endif
     }
 }

src/utility/constants.cpp

@@ -76,6 +76,17 @@ namespace storm {
             // FIXME: this should be treated more properly.
             return storm::RationalFunction(-1.0);
         }
+        
+        template<>
+        bool isOne(storm::CarlRationalNumber const& a) {
+            return carl::isOne(a);
+        }
+        
+        template<>
+        bool isZero(storm::CarlRationalNumber const& a) {
+            return carl::isZero(a);
+        }
+        
 #endif
         
         template<typename ValueType>
@@ -214,13 +225,21 @@ namespace storm {
         template storm::RationalFunction infinity();
         
         template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
-        
-        template Polynomial one();
-        template Polynomial zero();
         template RationalFunction simplify(RationalFunction value);
         template RationalFunction& simplify(RationalFunction& value);
         template RationalFunction&& simplify(RationalFunction&& value);
         
+        
+        template Polynomial one();
+        template Polynomial zero();
+        
+        template bool isOne(CarlRationalNumber const& value);
+        template bool isZero(CarlRationalNumber const& value);
+        template bool isConstant(CarlRationalNumber const& value);
+        
+        template CarlRationalNumber one();
+        template CarlRationalNumber zero();
+        
         template bool isOne(Interval const& value);
         template bool isZero(Interval const& value);
         template bool isConstant(Interval const& value);