From 58de346bd58f944fddc436dbd4f0d133335a9fae Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 18 Mar 2020 06:44:23 +0100
Subject: [PATCH] Revert "Fixed compilation with mathsat."

This reverts commit 8b57b18201304a47c4839659e25229ca4ee24b5b.
---
 src/storm/adapters/MathsatExpressionAdapter.h |  4 ---
 src/storm/solver/MathsatSmtSolver.cpp         | 35 -------------------
 src/storm/solver/MathsatSmtSolver.h           |  6 ++--
 3 files changed, 2 insertions(+), 43 deletions(-)

diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h
index ca6de5d8c..88ed84dcd 100644
--- a/src/storm/adapters/MathsatExpressionAdapter.h
+++ b/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));
diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp
index f8c1d6f86..219efe530 100644
--- a/src/storm/solver/MathsatSmtSolver.cpp
+++ b/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)
diff --git a/src/storm/solver/MathsatSmtSolver.h b/src/storm/solver/MathsatSmtSolver.h
index 851c00d82..0d27c71af 100644
--- a/src/storm/solver/MathsatSmtSolver.h
+++ b/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;