template instantiation of game solver with rationals

src/storm/solver/AbstractGameSolver.cpp

@@ -2,6 +2,7 @@
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/NativeEquationSolverSettings.h"
+#include "storm/adapters/CarlAdapter.h"
 
 #include "storm/exceptions/InvalidSettingsException.h"
 
@@ -14,12 +15,12 @@ namespace storm {
 
             // Get appropriate settings.
             maximalNumberOfIterations = settings.getMaximalIterationCount();
-            precision = settings.getPrecision();
+            precision = storm::utility::convertNumber<ValueType>(settings.getPrecision());
             relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative;
         }
 
         template <typename ValueType>
-        AbstractGameSolver<ValueType>::AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
+        AbstractGameSolver<ValueType>::AbstractGameSolver(ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : precision(precision), maximalNumberOfIterations(maximalNumberOfIterations), relative(relative) {
             // Intentionally left empty.
         }
         
@@ -52,7 +53,7 @@ namespace storm {
 
         
         template <typename ValueType>
-        double AbstractGameSolver<ValueType>::getPrecision() const {
+        ValueType AbstractGameSolver<ValueType>::getPrecision() const {
             return precision;
         }
         
@@ -83,6 +84,7 @@ namespace storm {
         }
     
         template class AbstractGameSolver<double>;
+        template class AbstractGameSolver<storm::RationalNumber>;
         
     }
 }

src/storm/solver/AbstractGameSolver.h

@@ -31,7 +31,7 @@ namespace storm {
              * @param maximalNumberOfIterations The maximal number of iterations to perform.
              * @param relative A flag indicating whether a relative or an absolute stopping criterion is to be used.
              */
-            AbstractGameSolver(double precision, uint_fast64_t maximalNumberOfIterations, bool relative);
+            AbstractGameSolver(ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative);
             
             /*!
              * Sets schedulers that might be considered by the solver as an initial guess
@@ -49,12 +49,12 @@ namespace storm {
             storm::storage::TotalScheduler const& getPlayer1Scheduler() const;
             storm::storage::TotalScheduler const& getPlayer2Scheduler() const;
             
-            double getPrecision() const;
+            ValueType getPrecision() const;
             bool getRelative() const;
 
         protected:
             // The precision to achieve.
-            double precision;
+            ValueType precision;
 
             // The maximal number of iterations to perform.
             uint_fast64_t maximalNumberOfIterations;

src/storm/solver/GameSolver.cpp

@@ -20,7 +20,7 @@ namespace storm {
         }
 
         template <typename ValueType>
-        GameSolver<ValueType>::GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) {
+        GameSolver<ValueType>::GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), player1Matrix(player1Matrix), player2Matrix(player2Matrix) {
             // Intentionally left empty.
         }
 
@@ -202,5 +202,6 @@ namespace storm {
         }
     
         template class GameSolver<double>;
+        template class GameSolver<storm::RationalNumber>;
     }
 }

src/storm/solver/GameSolver.h

@@ -36,7 +36,7 @@ namespace storm {
              * @param maximalNumberOfIterations The maximal number of iterations.
              * @param relative Sets whether or not to detect convergence with a relative or absolute criterion.
              */
-            GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, double precision, uint_fast64_t maximalNumberOfIterations, bool relative);
+            GameSolver(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix, storm::storage::SparseMatrix<ValueType> const& player2Matrix, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative);
 
             /*!
              * Solves the equation system defined by the game matrices. Note that the game matrices have to be given upon

src/storm/solver/SymbolicGameSolver.cpp

@@ -20,7 +20,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) {
+        SymbolicGameSolver<Type, ValueType>::SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative) : AbstractGameSolver<ValueType>(precision, maximalNumberOfIterations, relative), A(A), allRows(allRows), illegalPlayer1Mask(illegalPlayer1Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), illegalPlayer2Mask(illegalPlayer2Mask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), player1Variables(player1Variables), player2Variables(player2Variables), generatePlayer1Strategy(false), generatePlayer2Strategy(false) {
             // Intentionally left empty.
         }
         

src/storm/solver/SymbolicGameSolver.h

@@ -54,7 +54,7 @@ namespace storm {
              * equation system iteratively.
              * @param relative Sets whether or not to use a relativ stopping criterion rather than an absolute one.
              */
-            SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, double precision, uint_fast64_t maximalNumberOfIterations, bool relative);
+            SymbolicGameSolver(storm::dd::Add<Type, ValueType> const& A, storm::dd::Bdd<Type> const& allRows, storm::dd::Bdd<Type> const& illegalPlayer1Mask, storm::dd::Bdd<Type> const& illegalPlayer2Mask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables, ValueType precision, uint_fast64_t maximalNumberOfIterations, bool relative);
             
             /*!
              * Solves the equation system defined by the game matrix. Note that the game matrix has to be given upon

src/storm/utility/solver.cpp

@@ -110,6 +110,7 @@ namespace storm {
             template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;
             template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>;
             template class GameSolverFactory<double>;
+            template class GameSolverFactory<storm::RationalNumber>;
         }
     }
 }