fixed use of gmp numbers

resources/3rdparty/CMakeLists.txt

@@ -276,9 +276,8 @@ if(USE_HYPRO)
 	find_package(hypro QUIET REQUIRED)
 	if(hypro_FOUND)
 		set(STORM_HAVE_HYPRO ON)
-		message(STATUS "Storm - Linking with hypro ${hypro_VERSION_STRING}.")
+		message(STATUS "Storm - Linking with hypro.")
 		include_directories("${hypro_INCLUDE_DIR}")
-		link_directories( /Users/tim/hypro/build )
 		list(APPEND STORM_LINK_LIBRARIES ${hypro_LIBRARIES})
 	else()
 		message(FATAL_ERROR "StoRM - HyPro was requested but not found")

src/storm/adapters/NumberAdapter.h

@@ -6,7 +6,7 @@
 
 #include <carl/numbers/numbers.h>
 namespace storm {
-#if defined STORM_HAVE_CLN && defined USE_CLN_NUMBERS
+#if defined STORM_HAVE_CLN && defined STORM_USE_CLN_NUMBERS
     typedef cln::cl_RA RationalNumber;
 #else
     typedef mpq_class RationalNumber;

src/storm/solver/stateelimination/ConditionalStateEliminator.cpp

@@ -13,12 +13,12 @@ namespace storm {
             
             template<typename ValueType>
             void ConditionalStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                oneStepProbabilities[state] = storm::utility::simplify(loopProbability * oneStepProbabilities[state]);
+                oneStepProbabilities[state] = storm::utility::simplify((ValueType) (loopProbability * oneStepProbabilities[state]));
             }
             
             template<typename ValueType>
             void ConditionalStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                oneStepProbabilities[predecessor] = storm::utility::simplify(oneStepProbabilities[predecessor] * storm::utility::simplify(probability * oneStepProbabilities[state]));
+                oneStepProbabilities[predecessor] = storm::utility::simplify((ValueType) (oneStepProbabilities[predecessor] * storm::utility::simplify((ValueType) (probability * oneStepProbabilities[state]))));
             }
                         
             template<typename ValueType>

src/storm/solver/stateelimination/EliminatorBase.cpp

@@ -58,8 +58,7 @@ namespace storm {
                     for (auto entryIt = entriesInRow.begin(), entryIte = entriesInRow.end(); entryIt != entryIte; ++entryIt) {
                         // Only scale the entries in a different column.
                         if (entryIt->getColumn() != column) {
-                            auto tmpVal = entryIt->getValue() * columnValue;
-                            entryIt->setValue(storm::utility::simplify(tmpVal));
+                            entryIt->setValue(storm::utility::simplify((ValueType) (entryIt->getValue() * columnValue)));
                         }
                     }
                     updateValue(column, columnValue);

src/storm/solver/stateelimination/MultiValueStateEliminator.cpp

@@ -18,17 +18,17 @@ namespace storm {
 
             template<typename ValueType>
             void MultiValueStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                this->stateValues[state] = storm::utility::simplify(loopProbability * this->stateValues[state]);
+                this->stateValues[state] = storm::utility::simplify((ValueType) (loopProbability * this->stateValues[state]));
                 for(auto additionalStateValueVectorRef : additionalStateValues) {
-                    additionalStateValueVectorRef.get()[state] = storm::utility::simplify(loopProbability * additionalStateValueVectorRef.get()[state]);
+                    additionalStateValueVectorRef.get()[state] = storm::utility::simplify((ValueType) (loopProbability * additionalStateValueVectorRef.get()[state]));
                 }
             }
-       
+
             template<typename ValueType>
             void MultiValueStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                this->stateValues[predecessor] = storm::utility::simplify(this->stateValues[predecessor] + storm::utility::simplify(probability * this->stateValues[state]));
+                this->stateValues[predecessor] = storm::utility::simplify((ValueType) (this->stateValues[predecessor] + storm::utility::simplify((ValueType) (probability * this->stateValues[state]))));
                 for(auto additionalStateValueVectorRef : additionalStateValues) {
-                    additionalStateValueVectorRef.get()[predecessor] = storm::utility::simplify(additionalStateValueVectorRef.get()[predecessor] + storm::utility::simplify(probability * additionalStateValueVectorRef.get()[state]));
+                    additionalStateValueVectorRef.get()[predecessor] = storm::utility::simplify((ValueType) (additionalStateValueVectorRef.get()[predecessor] + storm::utility::simplify((ValueType) (probability * additionalStateValueVectorRef.get()[state]))));
                 }
             }
 
@@ -39,7 +39,7 @@ namespace storm {
                     additionStateValueVectorRef.get()[state] = storm::utility::zero<ValueType>();
                 }
             }
-            
+
             template class MultiValueStateEliminator<double>;
 
 #ifdef STORM_HAVE_CARL

src/storm/solver/stateelimination/PrioritizedStateEliminator.cpp

@@ -22,12 +22,12 @@ namespace storm {
             
             template<typename ValueType>
             void PrioritizedStateEliminator<ValueType>::updateValue(storm::storage::sparse::state_type const& state, ValueType const& loopProbability) {
-                stateValues[state] = storm::utility::simplify(loopProbability * stateValues[state]);
+                stateValues[state] = storm::utility::simplify((ValueType) (loopProbability * stateValues[state]));
             }
        
             template<typename ValueType>
             void PrioritizedStateEliminator<ValueType>::updatePredecessor(storm::storage::sparse::state_type const& predecessor, ValueType const& probability, storm::storage::sparse::state_type const& state) {
-                stateValues[predecessor] = storm::utility::simplify(stateValues[predecessor] + storm::utility::simplify(probability * stateValues[state]));
+                stateValues[predecessor] = storm::utility::simplify((ValueType) (stateValues[predecessor] + storm::utility::simplify((ValueType) (probability * stateValues[state]))));
             }
             
             template<typename ValueType>

src/storm/storage/geometry/Halfspace.h

@@ -41,7 +41,7 @@ namespace storm {
                  * In contrast to the euclideanDistance method, there are no inaccuracies introduced (providing ValueType is exact for +, -, and *)
                  */
                 ValueType distance(std::vector<ValueType> const& point) const {
-                    return std::max(storm::utility::zero<ValueType>(), storm::utility::vector::dotProduct(point, normalVector()) - offset());
+                    return std::max(storm::utility::zero<ValueType>(), (ValueType) (storm::utility::vector::dotProduct(point, normalVector()) - offset()));
                 }
                 
                 /*

src/storm/utility/constants.cpp

@@ -312,10 +312,10 @@ namespace storm {
         RationalNumber convertNumber(double const& number){
             return carl::rationalize<RationalNumber>(number);
         }
-        
+
         template<>
         RationalNumber convertNumber(uint_fast64_t const& number){
-            return RationalNumber(number);
+            return carl::rationalize<RationalNumber>(number);
         }
 
         template<>

src/storm/utility/vector.h

@@ -396,7 +396,7 @@ namespace storm {
              */
             template<class ValueType1, class ValueType2>
             void scaleVectorInPlace(std::vector<ValueType1>& target, ValueType2 const& factor) {
-                applyPointwise<ValueType1, ValueType2>(target, target, [&] (ValueType1 const& argument) -> ValueType1 { return argument * factor; });
+                applyPointwise<ValueType1, ValueType1>(target, target, [&] (ValueType1 const& argument) -> ValueType1 { return argument * factor; });
             }
             
             /*!

src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp

@@ -114,7 +114,7 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) {
     
     std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());
     ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
-    EXPECT_NEAR(121.61288420945114, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
+    EXPECT_NEAR(121.61288, result->asExplicitQuantitativeCheckResult<double>()[initState], storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision());
 }