work towards symbolic rational search

resources/3rdparty/CMakeLists.txt

@@ -436,6 +436,9 @@ ExternalProject_Add(
         LOG_BUILD ON
         DEPENDS ${sylvan_dep}
         BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT}
+        
+        // FIXME: remove
+        BUILD_ALWAYS 1
 )
 
 ExternalProject_Get_Property(sylvan source_dir)

resources/3rdparty/sylvan/src/storm_wrapper.cpp

@@ -149,6 +149,15 @@ double storm_rational_number_get_value_double(storm_rational_number_ptr a) {
     return storm::utility::convertNumber<double>(srn_a);
 }
 
+storm_rational_number_ptr storm_rational_number_from_double(double value) {
+#ifndef RATIONAL_NUMBER_THREAD_SAFE
+    std::lock_guard<std::mutex> lock(rationalNumberMutex);
+#endif
+    
+    storm::RationalNumber* number = new storm::RationalNumber(storm::utility::convertNumber<storm::RationalNumber>(value));
+    return number;
+}
+
 storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a, storm_rational_number_ptr b) {
 #ifndef RATIONAL_NUMBER_THREAD_SAFE
     std::lock_guard<std::mutex> lock(rationalNumberMutex);

resources/3rdparty/sylvan/src/storm_wrapper.h

@@ -29,7 +29,8 @@ extern "C" {
     int storm_rational_number_is_zero(storm_rational_number_ptr a);
     uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed);
     double storm_rational_number_get_value_double(storm_rational_number_ptr a);
-    
+    storm_rational_number_ptr storm_rational_number_from_double(double value);
+
     // Binary operations.
     storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a, storm_rational_number_ptr b);
     storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b);

resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.c

@@ -621,6 +621,35 @@ TASK_IMPL_2(MTBDD, mtbdd_sharpen, MTBDD, dd, size_t, p)
     return mtbdd_uapply(dd, TASK(mtbdd_op_sharpen), p);
 }
 
+TASK_IMPL_2(MTBDD, mtbdd_op_to_rational_number, MTBDD, a, size_t, p)
+{
+    /* We only expect double or rational number terminals, or false */
+    if (a == mtbdd_false) return mtbdd_false;
+    if (a == mtbdd_true) return mtbdd_true;
+    
+    // a != constant
+    mtbddnode_t na = MTBDD_GETNODE(a);
+    
+    if (mtbddnode_isleaf(na)) {
+        if (mtbddnode_gettype(na) == 1) {
+            MTBDD result = mtbdd_storm_rational_number(storm_rational_number_from_double(mtbdd_getdouble(a)));
+            return result;
+        } else {
+            printf("ERROR: Unsupported value type in conversion to rational number.\n");
+            assert(0);
+        }
+    }
+    
+    return mtbdd_invalid;
+    (void)p; // unused variable
+}
+
+TASK_IMPL_2(MTBDD, mtbdd_to_rational_number, MTBDD, dd, size_t, p)
+{
+    return mtbdd_uapply(dd, TASK(mtbdd_to_rational_number), 0);
+}
+
+
 TASK_IMPL_3(BDD, mtbdd_min_abstract_representative, MTBDD, a, BDD, v, BDDVAR, prev_level) {
 	/* Maybe perform garbage collection */
     sylvan_gc_test();

resources/3rdparty/sylvan/src/sylvan_mtbdd_storm.h

@@ -133,6 +133,13 @@ MTBDD mtbdd_ithvar(uint32_t var);
 TASK_DECL_2(MTBDD, mtbdd_op_sharpen, MTBDD, size_t)
 TASK_DECL_2(MTBDD, mtbdd_sharpen, MTBDD, size_t)
 #define mtbdd_sharpen(dd, p) CALL(mtbdd_sharpen, dd, p)
+
+/**
+ * Monad that converts the double MTBDD to an MTBDD over rational numbers.
+ */
+TASK_DECL_2(MTBDD, mtbdd_op_to_rational_number, MTBDD, size_t)
+TASK_DECL_2(MTBDD, mtbdd_to_rational_number, MTBDD, size_t)
+#define mtbdd_to_rational_number(dd) CALL(mtbdd_to_rational_number, dd, 0)
     
 /**
  * Unary operation Complement.

resources/3rdparty/sylvan/src/sylvan_obj_mtbdd_storm.hpp

@@ -32,6 +32,8 @@ bool EqualNormRel(const Mtbdd& other, double epsilon) const;
 
 Mtbdd SharpenKwekMehlhorn(size_t precision) const;
 
+Mtbdd ToRationalNumber() const;
+
 // Functions that operate on Mtbdds over rational numbers.
 static Mtbdd stormRationalNumberTerminal(storm::RationalNumber const& value);
 

resources/3rdparty/sylvan/src/sylvan_obj_storm.cpp

@@ -203,6 +203,12 @@ Mtbdd::SharpenKwekMehlhorn(size_t precision) const {
     return mtbdd_sharpen(mtbdd, precision);
 }
 
+Mtbdd
+Mtbdd::ToRationalNumber() const {
+    LACE_ME;
+    return mtbdd_to_rational_number(mtbdd);
+}
+
 // Functions for Mtbdds over rational numbers.
 Mtbdd
 Mtbdd::stormRationalNumberTerminal(storm::RationalNumber const& value)

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -172,7 +172,7 @@ namespace storm {
             }
             solver->setCachingEnabled(true);
             
-            Status status = Status::InProgress;
+            SolverStatus status = SolverStatus::InProgress;
             uint64_t iterations = 0;
             this->startMeasureProgress();
             do {
@@ -209,7 +209,7 @@ namespace storm {
                 
                 // If the scheduler did not improve, we are done.
                 if (!schedulerImproved) {
-                    status = Status::Converged;
+                    status = SolverStatus::Converged;
                 } else {
                     // Update the scheduler and the solver.
                     submatrix = this->A->selectRowsFromRowGroups(scheduler, true);
@@ -224,7 +224,7 @@ namespace storm {
 
                 // Potentially show progress.
                 this->showProgressIterative(iterations);
-            } while (status == Status::InProgress);
+            } while (status == SolverStatus::InProgress);
             
             reportStatus(status, iterations);
             
@@ -237,7 +237,7 @@ namespace storm {
                 clearCache();
             }
             
-            return status == Status::Converged || status == Status::TerminatedEarly;
+            return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
         }
         
         template<typename ValueType>
@@ -336,8 +336,8 @@ namespace storm {
             
             std::vector<ValueType>* originalX = currentX;
             
-            Status status = Status::InProgress;
-            while (status == Status::InProgress) {
+            SolverStatus status = SolverStatus::InProgress;
+            while (status == SolverStatus::InProgress) {
                 // Compute x' = min/max(A*x + b).
                 if (useGaussSeidelMultiplication) {
                     // Copy over the current vector so we can modify it in-place.
@@ -349,7 +349,7 @@ namespace storm {
                 
                 // Determine whether the method converged.
                 if (storm::utility::vector::equalModuloPrecision<ValueType>(*currentX, *newX, precision, relative)) {
-                    status = Status::Converged;
+                    status = SolverStatus::Converged;
                 }
                 
                 // Update environment variables.
@@ -437,7 +437,7 @@ namespace storm {
                 clearCache();
             }
             
-            return result.status == Status::Converged || result.status == Status::TerminatedEarly;
+            return result.status == SolverStatus::Converged || result.status == SolverStatus::TerminatedEarly;
         }
         
         template<typename ValueType>
@@ -500,7 +500,7 @@ namespace storm {
             // Proceed with the iterations as long as the method did not converge or reach the maximum number of iterations.
             uint64_t iterations = 0;
             
-            Status status = Status::InProgress;
+            SolverStatus status = SolverStatus::InProgress;
             bool doConvergenceCheck = true;
             bool useDiffs = this->hasRelevantValues();
             std::vector<ValueType> oldValues;
@@ -514,7 +514,7 @@ namespace storm {
                 precision *= storm::utility::convertNumber<ValueType>(2.0);
             }
             this->startMeasureProgress();
-            while (status == Status::InProgress && iterations < this->getSettings().getMaximalNumberOfIterations()) {
+            while (status == SolverStatus::InProgress && iterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Remember in which directions we took steps in this iteration.
                 bool lowerStep = false;
                 bool upperStep = false;
@@ -597,9 +597,9 @@ namespace storm {
                 if (doConvergenceCheck) {
                     // Determine whether the method converged.
                     if (this->hasRelevantValues()) {
-                        status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
+                        status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, this->getRelevantValues(), precision, this->getSettings().getRelativeTerminationCriterion()) ? SolverStatus::Converged : status;
                     } else {
-                        status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? Status::Converged : status;
+                        status = storm::utility::vector::equalModuloPrecision<ValueType>(*lowerX, *upperX, precision, this->getSettings().getRelativeTerminationCriterion()) ? SolverStatus::Converged : status;
                     }
                 }
                 
@@ -640,7 +640,7 @@ namespace storm {
                 clearCache();
             }
             
-            return status == Status::Converged;
+            return status == SolverStatus::Converged;
         }
         
         template<typename ValueType>
@@ -868,12 +868,12 @@ namespace storm {
             std::vector<ImpreciseType>* currentX = &x;
             std::vector<ImpreciseType>* newX = &tmpX;
 
-            Status status = Status::InProgress;
+            SolverStatus status = SolverStatus::InProgress;
             uint64_t overallIterations = 0;
             uint64_t valueIterationInvocations = 0;
             ValueType precision = this->getSettings().getPrecision();
             impreciseSolver.startMeasureProgress();
-            while (status == Status::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) {
+            while (status == SolverStatus::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Perform value iteration with the current precision.
                 typename IterativeMinMaxLinearEquationSolver<ImpreciseType>::ValueIterationResult result = impreciseSolver.performValueIteration(dir, currentX, newX, b, storm::utility::convertNumber<ImpreciseType, ValueType>(precision), this->getSettings().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, overallIterations);
                 
@@ -897,7 +897,7 @@ namespace storm {
                 // After sharpen, if a solution was found, it is contained in the free rational.
                 
                 if (foundSolution) {
-                    status = Status::Converged;
+                    status = SolverStatus::Converged;
                     
                     TemporaryHelper<RationalType, ImpreciseType>::swapSolutions(rationalX, temporaryRational, x, currentX, newX);
                 } else {
@@ -906,13 +906,13 @@ namespace storm {
                 }
             }
             
-            if (status == Status::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) {
-                status = Status::MaximalIterationsExceeded;
+            if (status == SolverStatus::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) {
+                status = SolverStatus::MaximalIterationsExceeded;
             }
             
             reportStatus(status, overallIterations);
             
-            return status == Status::Converged || status == Status::TerminatedEarly;
+            return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
         }
 
         template<typename ValueType>
@@ -1028,23 +1028,23 @@ namespace storm {
         }
 
         template<typename ValueType>
-        typename IterativeMinMaxLinearEquationSolver<ValueType>::Status IterativeMinMaxLinearEquationSolver<ValueType>::updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations, SolverGuarantee const& guarantee) const {
-            if (status != Status::Converged) {
+        SolverStatus IterativeMinMaxLinearEquationSolver<ValueType>::updateStatusIfNotConverged(SolverStatus status, std::vector<ValueType> const& x, uint64_t iterations, SolverGuarantee const& guarantee) const {
+            if (status != SolverStatus::Converged) {
                 if (this->hasCustomTerminationCondition() && this->getTerminationCondition().terminateNow(x, guarantee)) {
-                    status = Status::TerminatedEarly;
+                    status = SolverStatus::TerminatedEarly;
                 } else if (iterations >= this->getSettings().getMaximalNumberOfIterations()) {
-                    status = Status::MaximalIterationsExceeded;
+                    status = SolverStatus::MaximalIterationsExceeded;
                 }
             }
             return status;
         }
         
         template<typename ValueType>
-        void IterativeMinMaxLinearEquationSolver<ValueType>::reportStatus(Status status, uint64_t iterations) {
+        void IterativeMinMaxLinearEquationSolver<ValueType>::reportStatus(SolverStatus status, uint64_t iterations) {
             switch (status) {
-                case Status::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break;
-                case Status::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break;
-                case Status::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break;
+                case SolverStatus::Converged: STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations."); break;
+                case SolverStatus::TerminatedEarly: STORM_LOG_INFO("Iterative solver terminated early after " << iterations << " iterations."); break;
+                case SolverStatus::MaximalIterationsExceeded: STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Iterative solver terminated unexpectedly.");
             }

src/storm/solver/IterativeMinMaxLinearEquationSolver.h

@@ -7,6 +7,8 @@
 #include "storm/solver/LinearEquationSolver.h"
 #include "storm/solver/StandardMinMaxLinearEquationSolver.h"
 
+#include "storm/solver/SolverStatus.h"
+
 namespace storm {
     namespace solver {
         
@@ -84,18 +86,14 @@ namespace storm {
             static bool isSolution(storm::OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& matrix, std::vector<ValueType> const& values, std::vector<ValueType> const& b);
 
             void computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, uint_fast64_t* choice = nullptr) const;
-            
-            enum class Status {
-                Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
-            };
-            
+                        
             struct ValueIterationResult {
-                ValueIterationResult(uint64_t iterations, Status status) : iterations(iterations), status(status) {
+                ValueIterationResult(uint64_t iterations, SolverStatus status) : iterations(iterations), status(status) {
                     // Intentionally left empty.
                 }
                 
                 uint64_t iterations;
-                Status status;
+                SolverStatus status;
             };
             
             template <typename ValueTypePrime>
@@ -110,8 +108,8 @@ namespace storm {
             mutable std::unique_ptr<std::vector<ValueType>> auxiliaryRowGroupVector2; // A.rowGroupCount() entries
             mutable std::unique_ptr<std::vector<uint64_t>> rowGroupOrdering; // A.rowGroupCount() entries
             
-            Status updateStatusIfNotConverged(Status status, std::vector<ValueType> const& x, uint64_t iterations, SolverGuarantee const& guarantee) const;
-            static void reportStatus(Status status, uint64_t iterations);
+            SolverStatus updateStatusIfNotConverged(SolverStatus status, std::vector<ValueType> const& x, uint64_t iterations, SolverGuarantee const& guarantee) const;
+            static void reportStatus(SolverStatus status, uint64_t iterations);
             
             /// The settings of this solver.
             IterativeMinMaxLinearEquationSolverSettings<ValueType> settings;

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -428,7 +428,7 @@ namespace storm {
                 std::swap(currentX, newX);
             }
             
-            return PowerIterationResult(iterations - currentIterations, converged ? Status::Converged : (terminate ? Status::TerminatedEarly : Status::MaximalIterationsExceeded));
+            return PowerIterationResult(iterations - currentIterations, converged ? SolverStatus::Converged : (terminate ? SolverStatus::TerminatedEarly : SolverStatus::MaximalIterationsExceeded));
         }
         
         template<typename ValueType>
@@ -457,9 +457,9 @@ namespace storm {
                 clearCache();
             }
             
-            this->logIterations(result.status == Status::Converged, result.status == Status::TerminatedEarly, result.iterations);
+            this->logIterations(result.status == SolverStatus::Converged, result.status == SolverStatus::TerminatedEarly, result.iterations);
 
-            return result.status == Status::Converged || result.status == Status::TerminatedEarly;
+            return result.status == SolverStatus::Converged || result.status == SolverStatus::TerminatedEarly;
         }
         
         template<typename ValueType>
@@ -688,12 +688,12 @@ namespace storm {
             std::vector<ImpreciseType>* currentX = &x;
             std::vector<ImpreciseType>* newX = &tmpX;
             
-            Status status = Status::InProgress;
+            SolverStatus status = SolverStatus::InProgress;
             uint64_t overallIterations = 0;
             uint64_t valueIterationInvocations = 0;
             ValueType precision = this->getSettings().getPrecision();
             impreciseSolver.startMeasureProgress();
-            while (status == Status::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) {
+            while (status == SolverStatus::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) {
                 // Perform value iteration with the current precision.
                 typename NativeLinearEquationSolver<ImpreciseType>::PowerIterationResult result = impreciseSolver.performPowerIteration(currentX, newX, b, storm::utility::convertNumber<ImpreciseType, ValueType>(precision), this->getSettings().getRelativeTerminationCriterion(), SolverGuarantee::LessOrEqual, overallIterations);
                 
@@ -717,7 +717,7 @@ namespace storm {
                 // After sharpen, if a solution was found, it is contained in the free rational.
                 
                 if (foundSolution) {
-                    status = Status::Converged;
+                    status = SolverStatus::Converged;
                     
                     TemporaryHelper<RationalType, ImpreciseType>::swapSolutions(rationalX, temporaryRational, x, currentX, newX);
                 } else {
@@ -726,13 +726,13 @@ namespace storm {
                 }
             }
             
-            if (status == Status::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) {
-                status = Status::MaximalIterationsExceeded;
+            if (status == SolverStatus::InProgress && overallIterations == this->getSettings().getMaximalNumberOfIterations()) {
+                status = SolverStatus::MaximalIterationsExceeded;
             }
             
-            this->logIterations(status == Status::Converged, status == Status::TerminatedEarly, overallIterations);
+            this->logIterations(status == SolverStatus::Converged, status == SolverStatus::TerminatedEarly, overallIterations);
             
-            return status == Status::Converged || status == Status::TerminatedEarly;
+            return status == SolverStatus::Converged || status == SolverStatus::TerminatedEarly;
         }
      
         template<typename ValueType>

src/storm/solver/NativeLinearEquationSolver.h

@@ -6,6 +6,7 @@
 #include "storm/solver/LinearEquationSolver.h"
 
 #include "storm/solver/NativeMultiplier.h"
+#include "storm/solver/SolverStatus.h"
 
 #include "storm/utility/NumberTraits.h"
 
@@ -78,17 +79,13 @@ namespace storm {
             virtual bool internalSolveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const override;
             
         private:
-            enum class Status {
-                Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
-            };
-            
             struct PowerIterationResult {
-                PowerIterationResult(uint64_t iterations, Status status) : iterations(iterations), status(status) {
+                PowerIterationResult(uint64_t iterations, SolverStatus status) : iterations(iterations), status(status) {
                     // Intentionally left empty.
                 }
                 
                 uint64_t iterations;
-                Status status;
+                SolverStatus status;
             };
             
             template <typename ValueTypePrime>

src/storm/solver/SolverStatus.cpp

@@ -1,8 +1,17 @@
-//
-//  SolverStatus.cpp
-//  storm
-//
-//  Created by Christian Dehnert on 10.10.17.
-//
+#include "storm/solver/SolverStatus.h"
 
-#include "SolverStatus.hpp"
+namespace storm {
+    namespace solver {
+        
+        std::ostream& operator<<(std::ostream& out, SolverStatus const& status) {
+            switch (status) {
+                case SolverStatus::Converged: out << "converged"; break;
+                case SolverStatus::TerminatedEarly: out << "terminated"; break;
+                case SolverStatus::MaximalIterationsExceeded: out << "maximal iterations exceeded"; break;
+                case SolverStatus::InProgress: out << "in progress"; break;
+            }
+            return out;
+        }
+        
+    }
+}

src/storm/solver/SolverStatus.h

@@ -1,13 +1,15 @@
-//
-//  SolverStatus.hpp
-//  storm
-//
-//  Created by Christian Dehnert on 10.10.17.
-//
+#pragma once
 
-#ifndef SolverStatus_hpp
-#define SolverStatus_hpp
+#include <ostream>
 
-#include <stdio.h>
-
-#endif /* SolverStatus_hpp */
+namespace storm {
+    namespace solver {
+        
+        enum class SolverStatus {
+            Converged, TerminatedEarly, MaximalIterationsExceeded, InProgress
+        };
+     
+        std::ostream& operator<<(std::ostream& out, SolverStatus const& status);
+        
+    }
+}

src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp

@@ -124,11 +124,13 @@ namespace storm {
         }
         
         template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::CUDD, double>;
+        template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::CUDD, storm::RationalNumber>;
         template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
         template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalNumber>;
         template class SymbolicEliminationLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalFunction>;
 
         template class SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
+        template class SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::CUDD, storm::RationalNumber>;
         template class SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
         template class SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>;
         template class SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>;

src/storm/solver/SymbolicLinearEquationSolver.cpp

@@ -116,17 +116,20 @@ namespace storm {
         }
         
         template class SymbolicLinearEquationSolver<storm::dd::DdType::CUDD, double>;
+        template class SymbolicLinearEquationSolver<storm::dd::DdType::CUDD, storm::RationalNumber>;
+
         template class SymbolicLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
-        
         template class SymbolicLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalNumber>;
         template class SymbolicLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         
         template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
+        template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, storm::RationalNumber>;
         template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
         template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>;
         template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>;
         
         template class GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
+        template class GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, storm::RationalNumber>;
         template class GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
         template class GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>;
         template class GeneralSymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>;

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -1,7 +1,5 @@
 #include "storm/solver/SymbolicMinMaxLinearEquationSolver.h"
 
-
-
 #include "storm/storage/dd/DdManager.h"
 
 #include "storm/storage/dd/Add.h"
@@ -32,6 +30,7 @@ namespace storm {
             switch (method) {
                 case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break;
                 case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break;
+                case MinMaxMethod::RationalSearch: this->solutionMethod = SolutionMethod::RationalSearch; break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique.");
             }
@@ -97,25 +96,25 @@ namespace storm {
                 case SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration:
                     return solveEquationsPolicyIteration(dir, x, b);
                     break;
+                case SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch:
+                    return solveEquationsRationalSearch(dir, x, b);
+                    break;
             }
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        storm::dd::Add<DdType, ValueType>  SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
-            // Set up the environment.
-            storm::dd::Add<DdType, ValueType> xCopy = x;
-            uint_fast64_t iterations = 0;
-            bool converged = false;
-            
-            // If we were given an initial scheduler, we take its solution as the starting point.
-            if (this->hasInitialScheduler()) {
-                xCopy = solveEquationsWithScheduler(this->getInitialScheduler(), xCopy, b);
-            }
+        typename SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::ValueIterationResult SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::performValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b, ValueType const& precision, bool relativeTerminationCriterion) const {
+
+            // Set up local variables.
+            storm::dd::Add<DdType, ValueType> localX = x;
+            uint64_t iterations = 0;
             
-            while (!converged && iterations < this->settings.getMaximalNumberOfIterations()) {
+            // Value iteration loop.
+            SolverStatus status = SolverStatus::InProgress;
+            while (status == SolverStatus::Converged && iterations < this->settings.getMaximalNumberOfIterations()) {
                 // Compute tmp = A * x + b
-                storm::dd::Add<DdType, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
-                storm::dd::Add<DdType, ValueType> tmp = this->A.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables);
+                storm::dd::Add<DdType, ValueType> localXAsColumn = localX.swapVariables(this->rowColumnMetaVariablePairs);
+                storm::dd::Add<DdType, ValueType> tmp = this->A.multiplyMatrix(localXAsColumn, this->columnMetaVariables);
                 tmp += b;
                 
                 if (dir == storm::solver::OptimizationDirection::Minimize) {
@@ -126,20 +125,163 @@ namespace storm {
                 }
                 
                 // Now check if the process already converged within our precision.
-                converged = xCopy.equalModuloPrecision(tmp, this->settings.getPrecision(), this->settings.getRelativeTerminationCriterion());
+                if (localX.equalModuloPrecision(tmp, precision, relativeTerminationCriterion)) {
+                    status = SolverStatus::Converged;
+                }
+
+                // Set up next iteration.
+                localX = tmp;
+                ++iterations;
+            }
+            
+            if (status != SolverStatus::Converged) {
+                status = SolverStatus::MaximalIterationsExceeded;
+            }
+            
+            return SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::ValueIterationResult(status, iterations, localX);
+        }
+
+        template<storm::dd::DdType DdType, typename ValueType>
+        bool SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::isSolution(OptimizationDirection dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            storm::dd::Add<DdType, ValueType> xAsColumn = x.swapVariables(this->rowColumnMetaVariablePairs);
+            storm::dd::Add<DdType, ValueType> tmp = this->A.multiplyMatrix(xAsColumn, this->columnMetaVariables);
+            tmp += b;
+            
+            if (dir == storm::solver::OptimizationDirection::Minimize) {
+                tmp += illegalMaskAdd;
+                tmp = tmp.minAbstract(this->choiceVariables);
+            } else {
+                tmp = tmp.maxAbstract(this->choiceVariables);
+            }
+            
+            return x == tmp;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        template<typename RationalType, typename ImpreciseType>
+        storm::dd::Add<DdType, RationalType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::sharpen(OptimizationDirection dir, uint64_t precision, SymbolicMinMaxLinearEquationSolver<DdType, RationalType> const& rationalSolver, storm::dd::Add<DdType, ImpreciseType> const& x, storm::dd::Add<DdType, RationalType> const& rationalB, bool& isSolution) {
+            
+            storm::dd::Add<DdType, RationalType> sharpenedX;
+            
+            for (uint64_t p = 1; p < precision; ++p) {
+                storm::dd::Add<DdType, RationalType> sharpenedX = x.sharpenKwekMehlhorn(precision);
+                isSolution = rationalSolver.isSolution(dir, sharpenedX, rationalB);
+                
+                if (isSolution) {
+                    break;
+                }
+            }
+            
+            return sharpenedX;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        template<typename RationalType, typename ImpreciseType>
+        storm::dd::Add<DdType, RationalType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(OptimizationDirection dir, SymbolicMinMaxLinearEquationSolver<DdType, RationalType> const& rationalSolver, SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType> const& impreciseSolver, storm::dd::Add<DdType, RationalType> const& rationalX, storm::dd::Add<DdType, RationalType> const& rationalB, storm::dd::Add<DdType, ImpreciseType> const& x, storm::dd::Add<DdType, ImpreciseType> const& b) const {
+            
+            // Storage for the rational sharpened vector.
+            storm::dd::Add<DdType, RationalType> sharpenedX;
+            
+            // The actual rational search.
+            uint64_t overallIterations = 0;
+            uint64_t valueIterationInvocations = 0;
+            ValueType precision = this->getSettings().getPrecision();
+            SolverStatus status = SolverStatus::InProgress;
+            while (status == SolverStatus::InProgress && overallIterations < this->getSettings().getMaximalNumberOfIterations()) {
+                typename SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType>::ValueIterationResult viResult = impreciseSolver.performValueIteration(dir, x, b, storm::utility::convertNumber<ImpreciseType, ValueType>(precision), this->getSettings().getRelativeTerminationCriterion());
                 
-                xCopy = tmp;
+                ++valueIterationInvocations;
+                STORM_LOG_TRACE("Completed " << valueIterationInvocations << " value iteration invocations, the last one with precision " << precision << " completed in " << viResult.iterations << " iterations.");
+
+                // Count the iterations.
+                overallIterations += viResult.iterations;
                 
-                ++iterations;
+                // Compute maximal precision until which to sharpen.
+                uint64_t p = storm::utility::convertNumber<uint64_t>(storm::utility::ceil(storm::utility::log10<ValueType>(storm::utility::one<ValueType>() / precision)));
+
+                bool isSolution = false;
+                storm::dd::Add<DdType, RationalType> sharpenedX = sharpen<RationalType, ImpreciseType>(dir, p, rationalSolver, viResult.values, rationalB, isSolution);
+                
+                if (isSolution) {
+                    status = SolverStatus::Converged;
+                } else {
+                    precision = precision / 100;
+                }
             }
             
-            if (converged) {
-                STORM_LOG_INFO("Iterative solver (value iteration) converged in " << iterations << " iterations.");
+            if (status == SolverStatus::InProgress) {
+                status = SolverStatus::MaximalIterationsExceeded;
+            }
+            
+            if (status == SolverStatus::Converged) {
+                STORM_LOG_INFO("Iterative solver (rational search) converged in " << overallIterations << " iterations.");
             } else {
-                STORM_LOG_WARN("Iterative solver (value iteration) did not converge in " << iterations << " iterations.");
+                STORM_LOG_WARN("Iterative solver (rational search) did not converge in " << overallIterations << " iterations.");
             }
             
-            return xCopy;
+            return sharpenedX;
+        }
+
+        template<storm::dd::DdType DdType, typename ValueType>
+        template<typename ImpreciseType>
+        typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            
+            storm::dd::Add<DdType, storm::RationalNumber> rationalX = x.template toValueType<storm::RationalNumber>();
+            storm::dd::Add<DdType, storm::RationalNumber> rationalB = b.template toValueType<storm::RationalNumber>();
+            SymbolicMinMaxLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver;
+            
+            storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(dir, *this, *this, rationalX, rationalB, x, b);
+            return rationalResult.template toValueType<ValueType>();
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        template<typename ImpreciseType>
+        typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && !storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+
+            storm::dd::Add<DdType, storm::RationalNumber> rationalX = x.template toValueType<storm::RationalNumber>();
+            storm::dd::Add<DdType, storm::RationalNumber> rationalB = b.template toValueType<storm::RationalNumber>();
+            SymbolicMinMaxLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver;
+            
+            storm::dd::Add<DdType, storm::RationalNumber> rationalResult = solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(dir, rationalSolver, *this, rationalX, rationalB, x, b);
+            return rationalResult.template toValueType<ValueType>();
+        }
+
+        template<storm::dd::DdType DdType, typename ValueType>
+        template<typename ImpreciseType>
+        typename std::enable_if<!std::is_same<ValueType, ImpreciseType>::value, storm::dd::Add<DdType, ValueType>>::type SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            
+            storm::dd::Add<DdType, ImpreciseType> impreciseX = x.template toValueType<ImpreciseType>();
+            storm::dd::Add<DdType, ImpreciseType> impreciseB = b.template toValueType<ImpreciseType>();
+            SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType> impreciseSolver;
+
+            storm::dd::Add<DdType, ValueType> rationalResult = solveEquationsRationalSearchHelper<ValueType, ImpreciseType>(dir, *this, impreciseSolver, x, b, impreciseX, impreciseB);
+            return rationalResult.template toValueType<ValueType>();
+        }
+
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::dd::Add<DdType, ValueType> SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearch(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            return solveEquationsRationalSearchHelper<double>(dir, x, b);
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        storm::dd::Add<DdType, ValueType>  SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            // Set up the environment.
+            storm::dd::Add<DdType, ValueType> localX = x;
+            
+            // If we were given an initial scheduler, we take its solution as the starting point.
+            if (this->hasInitialScheduler()) {
+                localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
+            }
+            
+            ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion());
+            
+            if (viResult.status == SolverStatus::Converged) {
+                STORM_LOG_INFO("Iterative solver (value iteration) converged in " << viResult.iterations << " iterations.");
+            } else {
+                STORM_LOG_WARN("Iterative solver (value iteration) did not converge in " << viResult.iterations << " iterations.");
+            }
+            
+            return viResult.values;
         }
         
         template<storm::dd::DdType DdType, typename ValueType>

src/storm/solver/SymbolicMinMaxLinearEquationSolver.h

@@ -7,11 +7,12 @@
 #include <boost/optional.hpp>
 
 #include "storm/solver/OptimizationDirection.h"
-
 #include "storm/solver/SymbolicLinearEquationSolver.h"
-
 #include "storm/solver/EquationSystemType.h"
 #include "storm/solver/MinMaxLinearEquationSolverRequirements.h"
+#include "storm/solver/SolverStatus.h"
+
+#include "storm/utility/NumberTraits.h"
 
 #include "storm/storage/expressions/Variable.h"
 #include "storm/storage/dd/DdType.h"
@@ -32,7 +33,7 @@ namespace storm {
             SymbolicMinMaxLinearEquationSolverSettings();
             
             enum class SolutionMethod {
-                ValueIteration, PolicyIteration
+                ValueIteration, PolicyIteration, RationalSearch
             };
             
             void setSolutionMethod(SolutionMethod const& solutionMethod);
@@ -137,14 +138,47 @@ namespace storm {
              * Retrieves whether the solver is aware that the requirements were checked.
              */
             bool isRequirementsCheckedSet() const;
-            
+
+            /*!
+             * Determines whether the given vector x satisfies x = Ax + b.
+             */
+            bool isSolution(OptimizationDirection dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
+
         private:
             storm::dd::Add<DdType, ValueType> solveEquationsWithScheduler(storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
             storm::dd::Add<DdType, ValueType> solveEquationsWithScheduler(SymbolicLinearEquationSolver<DdType, ValueType>& solver, storm::dd::Bdd<DdType> const& scheduler, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b, storm::dd::Add<DdType, ValueType> const& diagonal) const;
             
             storm::dd::Add<DdType, ValueType> solveEquationsValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
             storm::dd::Add<DdType, ValueType> solveEquationsPolicyIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
-
+            storm::dd::Add<DdType, ValueType> solveEquationsRationalSearch(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
+            
+            template<typename RationalType, typename ImpreciseType>
+            static storm::dd::Add<DdType, RationalType> sharpen(OptimizationDirection dir, uint64_t precision, SymbolicMinMaxLinearEquationSolver<DdType, RationalType> const& rationalSolver, storm::dd::Add<DdType, ImpreciseType> const& x, storm::dd::Add<DdType, RationalType> const& rationalB, bool& isSolution);
+            
+            template<typename RationalType, typename ImpreciseType>
+            storm::dd::Add<DdType, RationalType> solveEquationsRationalSearchHelper(OptimizationDirection dir, SymbolicMinMaxLinearEquationSolver<DdType, RationalType> const& rationalSolver, SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType> const& impreciseSolver, storm::dd::Add<DdType, RationalType> const& rationalX, storm::dd::Add<DdType, RationalType> const& rationalB, storm::dd::Add<DdType, ImpreciseType> const& x, storm::dd::Add<DdType, ImpreciseType> const& b) const;
+            template<typename ImpreciseType>
+            typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
+            template<typename ImpreciseType>
+            typename std::enable_if<std::is_same<ValueType, ImpreciseType>::value && !storm::NumberTraits<ValueType>::IsExact, storm::dd::Add<DdType, ValueType>>::type solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
+            template<typename ImpreciseType>
+            typename std::enable_if<!std::is_same<ValueType, ImpreciseType>::value, storm::dd::Add<DdType, ValueType>>::type solveEquationsRationalSearchHelper(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const;
+            
+            template<storm::dd::DdType DdTypePrime, typename ValueTypePrime>
+            friend class SymbolicMinMaxLinearEquationSolver;
+            
+            struct ValueIterationResult {
+                ValueIterationResult(SolverStatus status, uint64_t iterations, storm::dd::Add<DdType, ValueType> const& values) : status(status), iterations(iterations), values(values) {
+                    // Intentionally left empty.
+                }
+                
+                SolverStatus status;
+                uint64_t iterations;
+                storm::dd::Add<DdType, ValueType> values;
+            };
+            
+            ValueIterationResult performValueIteration(storm::solver::OptimizationDirection const& dir, storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b, ValueType const& precision, bool relativeTerminationCriterion) const;
+            
         protected:
             // The matrix defining the coefficients of the linear equation system.
             storm::dd::Add<DdType, ValueType> A;

src/storm/solver/SymbolicNativeLinearEquationSolver.cpp

@@ -129,10 +129,12 @@ namespace storm {
         template class SymbolicNativeLinearEquationSolverSettings<storm::RationalNumber>;
 
         template class SymbolicNativeLinearEquationSolver<storm::dd::DdType::CUDD, double>;
+        template class SymbolicNativeLinearEquationSolver<storm::dd::DdType::CUDD, storm::RationalNumber>;
         template class SymbolicNativeLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
         template class SymbolicNativeLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalNumber>;
 
         template class SymbolicNativeLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
+        template class SymbolicNativeLinearEquationSolverFactory<storm::dd::DdType::CUDD, storm::RationalNumber>;
         template class SymbolicNativeLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
         template class SymbolicNativeLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>;
     }

src/storm/storage/dd/Add.cpp

@@ -976,30 +976,36 @@ namespace storm {
         
 		template<DdType LibraryType, typename ValueType>
         template<typename TargetValueType>
-		Add<LibraryType, TargetValueType> Add<LibraryType, ValueType>::toValueType() const {
-            if (std::is_same<TargetValueType, ValueType>::value) {
-                return *this;
-            }
-			STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot convert this ADD to the target type.");
-		}
-
-#ifdef STORM_HAVE_CARL
-		template<>
-        template<>
-		Add<storm::dd::DdType::Sylvan, double> Add<storm::dd::DdType::Sylvan, storm::RationalFunction>::toValueType() const {
-			return Add<storm::dd::DdType::Sylvan, double>(this->getDdManager(), internalAdd.toValueType<double>(), this->getContainedMetaVariables());
+        typename std::enable_if<std::is_same<TargetValueType, ValueType>::value, Add<LibraryType, TargetValueType>>::type Add<LibraryType, ValueType>::toValueType() const {
+            return *this;
 		}
-#endif
+    
+        template<DdType LibraryType, typename ValueType>
+        template<typename TargetValueType>
+        typename std::enable_if<!std::is_same<TargetValueType, ValueType>::value, Add<LibraryType, TargetValueType>>::type Add<LibraryType, ValueType>::toValueType() const {
+            return Add<LibraryType, TargetValueType>(this->getDdManager(), internalAdd.template toValueType<TargetValueType>(), this->getContainedMetaVariables());
+        }
 		
         template class Add<storm::dd::DdType::CUDD, double>;
         template class Add<storm::dd::DdType::CUDD, uint_fast64_t>;
 
         template class Add<storm::dd::DdType::Sylvan, double>;
         template class Add<storm::dd::DdType::Sylvan, uint_fast64_t>;
-        
+
 #ifdef STORM_HAVE_CARL
+        template class Add<storm::dd::DdType::CUDD, storm::RationalNumber>;
+
         template class Add<storm::dd::DdType::Sylvan, storm::RationalNumber>;
 		template class Add<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+
+        template Add<storm::dd::DdType::CUDD, storm::RationalNumber> Add<storm::dd::DdType::CUDD, storm::RationalNumber>::toValueType<storm::RationalNumber>() const;
+        template Add<storm::dd::DdType::CUDD, storm::RationalNumber> Add<storm::dd::DdType::CUDD, double>::toValueType<storm::RationalNumber>() const;
+        template Add<storm::dd::DdType::CUDD, double> Add<storm::dd::DdType::CUDD, storm::RationalNumber>::toValueType<double>() const;
+
+        template Add<storm::dd::DdType::Sylvan, storm::RationalNumber> Add<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<storm::RationalNumber>() const;
+        template Add<storm::dd::DdType::Sylvan, storm::RationalNumber> Add<storm::dd::DdType::Sylvan, double>::toValueType<storm::RationalNumber>() const;
+        template Add<storm::dd::DdType::Sylvan, double> Add<storm::dd::DdType::Sylvan, storm::RationalNumber>::toValueType<double>() const;
+        template Add<storm::dd::DdType::Sylvan, double> Add<storm::dd::DdType::Sylvan, storm::RationalFunction>::toValueType<double>() const;
 #endif
     }
 }

src/storm/storage/dd/Add.h

@@ -266,7 +266,9 @@ namespace storm {
              * @return The resulting function represented as an ADD.
              */
             template<typename TargetValueType>
-            Add<LibraryType, TargetValueType> toValueType() const;
+            typename std::enable_if<std::is_same<TargetValueType, ValueType>::value, Add<LibraryType, TargetValueType>>::type toValueType() const;
+            template<typename TargetValueType>
+            typename std::enable_if<!std::is_same<TargetValueType, ValueType>::value, Add<LibraryType, TargetValueType>>::type toValueType() const;
 
             /*!
              * Sum-abstracts from the given meta variables.

src/storm/storage/dd/Bdd.cpp

@@ -424,13 +424,16 @@ namespace storm {
         
         template Add<DdType::CUDD, double> Bdd<DdType::CUDD>::toAdd() const;
         template Add<DdType::CUDD, uint_fast64_t> Bdd<DdType::CUDD>::toAdd() const;
-        
+        template Add<DdType::CUDD, storm::RationalNumber> Bdd<DdType::CUDD>::toAdd() const;
+
         template std::vector<double> Bdd<DdType::CUDD>::filterExplicitVector(Odd const& odd, std::vector<double> const& values) const;
         template std::vector<uint_fast64_t> Bdd<DdType::CUDD>::filterExplicitVector(Odd const& odd, std::vector<uint_fast64_t> const& values) const;
         
         template Add<DdType::CUDD, double> Bdd<DdType::CUDD>::ite(Add<DdType::CUDD, double> const& thenAdd, Add<DdType::CUDD, double> const& elseAdd) const;
         template Add<DdType::CUDD, uint_fast64_t> Bdd<DdType::CUDD>::ite(Add<DdType::CUDD, uint_fast64_t> const& thenAdd, Add<DdType::CUDD, uint_fast64_t> const& elseAdd) const;
-        
+#ifdef STORM_HAVE_CARL
+        template Add<DdType::CUDD, storm::RationalNumber> Bdd<DdType::CUDD>::ite(Add<DdType::CUDD, storm::RationalNumber> const& thenAdd, Add<DdType::CUDD, storm::RationalNumber> const& elseAdd) const;
+#endif
         
         template class Bdd<DdType::Sylvan>;
 

src/storm/storage/dd/DdManager.cpp

@@ -481,14 +481,26 @@ namespace storm {
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getAddZero() const;
         template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getAddZero() const;
 
+#ifdef STORM_HAVE_CARL
+        template Add<DdType::CUDD, storm::RationalNumber> DdManager<DdType::CUDD>::getAddZero() const;
+#endif
+        
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getAddOne() const;
         template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getAddOne() const;
 
+#ifdef STORM_HAVE_CARL
+        template Add<DdType::CUDD, storm::RationalNumber> DdManager<DdType::CUDD>::getAddOne() const;
+#endif
+
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getInfinity<double>() const;
         template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getInfinity<uint_fast64_t>() const;
 
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getConstant(double const& value) const;
         template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const;
+
+#ifdef STORM_HAVE_CARL
+        template Add<DdType::CUDD, storm::RationalNumber> DdManager<DdType::CUDD>::getConstant(storm::RationalNumber const& value) const;
+#endif
         
         template Add<DdType::CUDD, double> DdManager<DdType::CUDD>::getIdentity(storm::expressions::Variable const& variable) const;
         template Add<DdType::CUDD, uint_fast64_t> DdManager<DdType::CUDD>::getIdentity(storm::expressions::Variable const& variable) const;

src/storm/storage/dd/cudd/CuddAddIterator.cpp

@@ -4,6 +4,8 @@
 #include "storm/utility/macros.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 
+#include "storm/utility/constants.h"
+
 #include <cmath>
 
 namespace storm {
@@ -14,7 +16,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        AddIterator<DdType::CUDD, ValueType>::AddIterator(DdManager<DdType::CUDD> const& ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(&ddManager), generator(generator), cube(cube), valueAsDouble(static_cast<double>(value)), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager.getExpressionManager().getSharedPointer()) {
+        AddIterator<DdType::CUDD, ValueType>::AddIterator(DdManager<DdType::CUDD> const& ddManager, DdGen* generator, int* cube, ValueType const& value, bool isAtEnd, std::set<storm::expressions::Variable> const* metaVariables, bool enumerateDontCareMetaVariables) : ddManager(&ddManager), generator(generator), cube(cube), valueAsDouble(storm::utility::convertNumber<double>(value)), isAtEnd(isAtEnd), metaVariables(metaVariables), enumerateDontCareMetaVariables(enumerateDontCareMetaVariables), cubeCounter(), relevantDontCareDdVariables(), currentValuation(ddManager.getExpressionManager().getSharedPointer()) {
             // If the given generator is not yet at its end, we need to create the current valuation from the cube from
             // scratch.
             if (!this->isAtEnd) {
@@ -186,5 +188,9 @@ namespace storm {
         
         template class AddIterator<DdType::CUDD, double>;
         template class AddIterator<DdType::CUDD, uint_fast64_t>;
+
+#ifdef STORM_HAVE_CARL
+        template class AddIterator<DdType::CUDD, storm::RationalNumber>;
+#endif
     }
 }

src/storm/storage/dd/cudd/InternalCuddAdd.cpp

@@ -143,6 +143,18 @@ namespace storm {
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().Maximum(other.getCuddAdd()));
         }
         
+        template<typename ValueType>
+        template<typename TargetValueType>
+        typename std::enable_if<std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
+            return *this;
+        }
+
+        template<typename ValueType>
+        template<typename TargetValueType>
+        typename std::enable_if<!std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type InternalAdd<DdType::CUDD, ValueType>::toValueType() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
+        }
+
         template<typename ValueType>
         InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::sumAbstract(InternalBdd<DdType::CUDD> const& cube) const {
             return InternalAdd<DdType::CUDD, ValueType>(ddManager, this->getCuddAdd().ExistAbstract(cube.toAdd<ValueType>().getCuddAdd()));
@@ -176,6 +188,11 @@ namespace storm {
                 return this->getCuddAdd().EqualSupNorm(other.getCuddAdd(), precision);
             }
         }
+
+        template<>
+        bool InternalAdd<DdType::CUDD, storm::RationalNumber>::equalModuloPrecision(InternalAdd<DdType::CUDD, storm::RationalNumber> const& other, storm::RationalNumber const& precision, bool relative) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
+        }
         
         template<typename ValueType>
         InternalAdd<DdType::CUDD, ValueType> InternalAdd<DdType::CUDD, ValueType>::swapVariables(std::vector<InternalBdd<DdType::CUDD>> const& from, std::vector<InternalBdd<DdType::CUDD>> const& to) const {
@@ -229,22 +246,42 @@ namespace storm {
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(ValueType const& value) const {
             return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddStrictThreshold(value));
         }
-        
+
+        template<>
+        InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::greater(storm::RationalNumber const& value) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
+        }
+
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(ValueType const& value) const {
             return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddThreshold(value));
         }
+
+        template<>
+        InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::greaterOrEqual(storm::RationalNumber const& value) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
+        }
         
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(ValueType const& value) const {
             return InternalBdd<DdType::CUDD>(ddManager, ~this->getCuddAdd().BddThreshold(value));
         }
         
+        template<>
+        InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::less(storm::RationalNumber const& value) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
+        }
+        
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(ValueType const& value) const {
             return InternalBdd<DdType::CUDD>(ddManager, ~this->getCuddAdd().BddStrictThreshold(value));
         }
         
+        template<>
+        InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, storm::RationalNumber>::lessOrEqual(storm::RationalNumber const& value) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
+        }
+        
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notZero() const {
             return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().BddPattern());
@@ -655,7 +692,21 @@ namespace storm {
             }
         }
         
+        template<>
+        DdNode* InternalAdd<DdType::CUDD, storm::RationalNumber>::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector<storm::RationalNumber> const& values, Odd const& odd, std::vector<uint_fast64_t> const& ddVariableIndices) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported");
+        }
+        
         template class InternalAdd<DdType::CUDD, double>;
+        template InternalAdd<DdType::CUDD, double> InternalAdd<DdType::CUDD, double>::toValueType<double>() const;
         template class InternalAdd<DdType::CUDD, uint_fast64_t>;
+        template InternalAdd<DdType::CUDD, uint_fast64_t> InternalAdd<DdType::CUDD, uint_fast64_t>::toValueType<uint_fast64_t>() const;
+
+#ifdef STORM_HAVE_CARL
+        template class InternalAdd<DdType::CUDD, storm::RationalNumber>;
+        template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalAdd<DdType::CUDD, storm::RationalNumber>::toValueType<storm::RationalNumber>() const;
+        template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalAdd<DdType::CUDD, double>::toValueType<storm::RationalNumber>() const;
+        template InternalAdd<DdType::CUDD, double> InternalAdd<DdType::CUDD, storm::RationalNumber>::toValueType<double>() const;
+#endif
     }
 }

src/storm/storage/dd/cudd/InternalCuddAdd.h

@@ -262,6 +262,16 @@ namespace storm {
              */
             InternalAdd<DdType::CUDD, ValueType> maximum(InternalAdd<DdType::CUDD, ValueType> const& other) const;
             
+            /*!
+             * Replaces the leaves in this MTBDD with the converted values in the target value type.
+             *
+             * @return The resulting function represented as an ADD.
+             */
+            template<typename TargetValueType>
+            typename std::enable_if<std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type toValueType() const;
+            template<typename TargetValueType>
+            typename std::enable_if<!std::is_same<ValueType, TargetValueType>::value, InternalAdd<DdType::CUDD, TargetValueType>>::type toValueType() const;
+
             /*!
              * Sum-abstracts from the given cube.
              *

src/storm/storage/dd/cudd/InternalCuddBdd.cpp

@@ -528,6 +528,9 @@ namespace storm {
                 
         template InternalAdd<DdType::CUDD, double> InternalBdd<DdType::CUDD>::toAdd() const;
         template InternalAdd<DdType::CUDD, uint_fast64_t> InternalBdd<DdType::CUDD>::toAdd() const;
+#ifdef STORM_HAVE_CARL
+        template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalBdd<DdType::CUDD>::toAdd() const;
+#endif
         
         template void InternalBdd<DdType::CUDD>::filterExplicitVectorRec<double>(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<double>& result, uint_fast64_t& currentIndex, std::vector<double> const& values);
         template void InternalBdd<DdType::CUDD>::filterExplicitVectorRec<uint_fast64_t>(DdNode const* dd, cudd::Cudd const& manager, uint_fast64_t currentLevel, bool complement, uint_fast64_t maxLevel, std::vector<uint_fast64_t> const& ddVariableIndices, uint_fast64_t currentOffset, storm::dd::Odd const& odd, std::vector<uint_fast64_t>& result, uint_fast64_t& currentIndex, std::vector<uint_fast64_t> const& values);
@@ -537,5 +540,6 @@ namespace storm {
 
         template InternalAdd<DdType::CUDD, double> InternalBdd<DdType::CUDD>::ite(InternalAdd<DdType::CUDD, double> const& thenAdd, InternalAdd<DdType::CUDD, double> const& elseAdd) const;
         template InternalAdd<DdType::CUDD, uint_fast64_t> InternalBdd<DdType::CUDD>::ite(InternalAdd<DdType::CUDD, uint_fast64_t> const& thenAdd, InternalAdd<DdType::CUDD, uint_fast64_t> const& elseAdd) const;
+        template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalBdd<DdType::CUDD>::ite(InternalAdd<DdType::CUDD, storm::RationalNumber> const& thenAdd, InternalAdd<DdType::CUDD, storm::RationalNumber> const& elseAdd) const;
     }
 }

src/storm/storage/dd/cudd/InternalCuddDdManager.cpp

@@ -102,6 +102,11 @@ namespace storm {
             return InternalAdd<DdType::CUDD, ValueType>(this, cuddManager.constant(value));
         }
 
+        template<>
+        InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getConstant(storm::RationalNumber const& value) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Operation not supported.");
+        }
+
         std::vector<InternalBdd<DdType::CUDD>> InternalDdManager<DdType::CUDD>::createDdVariables(uint64_t numberOfLayers, boost::optional<uint_fast64_t> const& position) {
             std::vector<InternalBdd<DdType::CUDD>> result;
             
@@ -166,11 +171,14 @@ namespace storm {
 
         template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getAddOne() const;
         template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getAddOne() const;
-        
+        template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getAddOne() const;
+
         template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getAddZero() const;
         template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getAddZero() const;
-        
+        template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getAddZero() const;
+
         template InternalAdd<DdType::CUDD, double> InternalDdManager<DdType::CUDD>::getConstant(double const& value) const;
         template InternalAdd<DdType::CUDD, uint_fast64_t> InternalDdManager<DdType::CUDD>::getConstant(uint_fast64_t const& value) const;
+        template InternalAdd<DdType::CUDD, storm::RationalNumber> InternalDdManager<DdType::CUDD>::getConstant(storm::RationalNumber const& value) const;
     }
 }

src/storm/storage/dd/sylvan/InternalSylvanAdd.cpp

@@ -457,7 +457,12 @@ namespace storm {
             return InternalAdd<DdType::Sylvan, double>(ddManager, this->sylvanMtbdd.ToDoubleRN());
         }
 
-        
+        template<>
+        template<>
+        InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalAdd<DdType::Sylvan, double>::toValueType() const {
+            return InternalAdd<DdType::Sylvan, storm::RationalNumber>(ddManager, this->sylvanMtbdd.ToRationalNumber());
+        }
+
 #ifdef STORM_HAVE_CARL
 		template<>
         template<>

src/storm/storage/dd/sylvan/InternalSylvanAdd.h

@@ -256,7 +256,7 @@ namespace storm {
             InternalAdd<DdType::Sylvan, ValueType> maximum(InternalAdd<DdType::Sylvan, ValueType> const& other) const;
             
 			/*!
-             * Replaces the leaves in this MTBDD, converting them to double if possible, and -1.0 else.
+             * Replaces the leaves in this MTBDD with the converted values in the target value type.
              *
              * @return The resulting function represented as an ADD.
              */

src/test/storm/storage/SylvanDdTest.cpp

@@ -855,6 +855,23 @@ TEST(SylvanDd, AddSharpenTest) {
     ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("19/10")), sharpened.getValue(metaVariableToValueMap));
 }
 
+TEST(SylvanDd, AddToRationalTest) {
+    std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
+    std::pair<storm::expressions::Variable, storm::expressions::Variable> x = manager->addMetaVariable("x", 1, 9);
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, double> dd = manager->template getAddOne<double>();
+    ASSERT_NO_THROW(dd.setValue(x.first, 4, 0.4));
+    ASSERT_EQ(2ul, dd.getLeafCount());
+    
+    storm::dd::Add<storm::dd::DdType::Sylvan, storm::RationalNumber> rationalDd = dd.template toValueType<storm::RationalNumber>();
+    
+    std::map<storm::expressions::Variable, int_fast64_t> metaVariableToValueMap;
+    metaVariableToValueMap.emplace(x.first, 4);
+    
+    ASSERT_EQ(storm::utility::convertNumber<storm::RationalNumber>(std::string("4/10")), rationalDd.getValue(metaVariableToValueMap));
+}
+
+
 TEST(SylvanDd, BddOddTest) {
     std::shared_ptr<storm::dd::DdManager<storm::dd::DdType::Sylvan>> manager(new storm::dd::DdManager<storm::dd::DdType::Sylvan>());
     std::pair<storm::expressions::Variable, storm::expressions::Variable> a = manager->addMetaVariable("a");