Merge branch 'master' into prism-pomdp

src/storm/adapters/MathsatExpressionAdapter.h

@@ -106,10 +106,6 @@ namespace storm {
                 STORM_LOG_ASSERT(declarationVariablePair != declarationToVariableMapping.end(), "Unknown variable declaration.");
                 return declarationVariablePair->second;
             }
-            
-            std::unordered_map<storm::expressions::Variable, msat_decl> const& getAllDeclaredVariables() const {
-				return variableToDeclarationMapping;
-			}
 
             virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override {
                 msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));

src/storm/solver/MathsatSmtSolver.cpp

@@ -32,22 +32,6 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve double value from model that only contains boolean values.");
         }
         
-        std::string MathsatSmtSolver::MathsatAllsatModelReference::toString() const {
-            std::stringstream str;
-            bool first = true;
-            str << "[";
-            for (auto const& varSlot : variableToSlotMapping) {
-                if (first) {
-                    first = false;
-                } else {
-                    str << ", ";
-                }
-                str << varSlot.first.getName() << "=" << std::boolalpha << getBooleanValue(varSlot.first);
-            }
-            str << "]";
-            return str.str();
-        }
-        
         MathsatSmtSolver::MathsatModelReference::MathsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter) : ModelReference(manager), env(env), expressionAdapter(expressionAdapter) {
             // Intentionally left empty.
         }
@@ -78,25 +62,6 @@ namespace storm {
             storm::expressions::Expression value = expressionAdapter.translateExpression(msatValue);
             return value.evaluateAsDouble();
         }
-        
-        std::string MathsatSmtSolver::MathsatModelReference::toString() const {
-            std::stringstream str;
-            bool first = true;
-            str << "[";
-            for (auto const& varDecl : expressionAdapter.getAllDeclaredVariables()) {
-                if (first) {
-                    first = false;
-                } else {
-                    str << ", ";
-                }
-                msat_term msatValue = msat_get_model_value(env, expressionAdapter.translateExpression(varDecl.first));
-                STORM_LOG_ASSERT(!MSAT_ERROR_TERM(msatValue), "Unable to retrieve value of variable in model. This could be caused by calls to the solver between checking for satisfiability and model retrieval.");
-                str << varDecl.first.getName() << "=" << expressionAdapter.translateExpression(msatValue);
-            }
-            str << "]";
-            return str.str();
-        }
-        
 #endif
 
 		MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options) : SmtSolver(manager)

src/storm/solver/MathsatSmtSolver.h

@@ -38,8 +38,7 @@ namespace storm {
                 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
                 virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
                 virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
-                virtual std::string toString() const override;
-
+                
 			private:
 				msat_env const& env;
                 msat_term* model;
@@ -55,8 +54,7 @@ namespace storm {
                 virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
                 virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
                 virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
-                virtual std::string toString() const override;
-
+                
 			private:
 				msat_env const& env;
                 storm::adapters::MathsatExpressionAdapter& expressionAdapter;