From 0bd4b9b8ad31b6a73b67c4e6a2e5cc0a7f958238 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Thu, 6 Aug 2015 10:01:42 +0200
Subject: [PATCH] fixed some guards for smtsolver

Former-commit-id: 2205f1af5709f810e155be7aa576a62b9c7f7cc6
---
 src/solver/SmtratSmtSolver.cpp | 25 +++----------------------
 src/solver/SmtratSmtSolver.h   |  3 +--
 2 files changed, 4 insertions(+), 24 deletions(-)

diff --git a/src/solver/SmtratSmtSolver.cpp b/src/solver/SmtratSmtSolver.cpp
index ca6e8942d..cacc47836 100644
--- a/src/solver/SmtratSmtSolver.cpp
+++ b/src/solver/SmtratSmtSolver.cpp
@@ -5,7 +5,6 @@
 
 #ifdef STORM_HAVE_SMTRAT
 #include "lib/smtrat.h"
-#endif 
 
 namespace storm {
 	namespace solver {
@@ -13,9 +12,6 @@ namespace storm {
         
 		SmtratSmtSolver::SmtratSmtSolver(storm::expressions::ExpressionManager& manager) : SmtSolver(manager)
 		{
-#ifndef STORM_HAVE_SMTRAT
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
-#else 
                      // Construct the settingsManager.
                     //smtrat::RuntimeSettingsManager settingsManager;
                     
@@ -28,7 +24,6 @@ namespace storm {
                     // Introduce the settingsObjects from the modules to the manager.
                     //settingsManager.addSettingsObject( settingsObjects );
                     //settingsObjects.clear();
-#endif 
                 }  
         
 		SmtratSmtSolver::~SmtratSmtSolver() {
@@ -37,35 +32,23 @@ namespace storm {
 
 		void SmtratSmtSolver::push()
 		{
-#ifndef STORM_HAVE_SMTRAT
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
-#else
                     this->solver->push();
-#endif
 		}
 
 		void SmtratSmtSolver::pop()
 		{
-#ifndef STORM_HAVE_SMTRAT
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
-#else
                     this->solver->pop();
-#endif		
                 }
 
 		void SmtratSmtSolver::pop(uint_fast64_t n)
 		{
-#ifndef STORM_HAVE_SMTRAT
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without SMT-RAT support.");
-#else
                     this->solver->pop(static_cast<unsigned int>(n));
-#endif
 		}
 
 		
 		SmtSolver::CheckResult SmtratSmtSolver::check()
 		{
-#ifdef STORM_HAVE_SMTRAT
+
                     switch (this->solver->check()) {
                         case smtrat::Answer::True:
                             this->lastResult = SmtSolver::CheckResult::Sat;
@@ -82,11 +65,8 @@ namespace storm {
                             break;
                     }
                     return this->lastResult;
-#else
-			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
-#endif
+
 		}
-                
                 void SmtratSmtSolver::add(const storm::RawPolynomial& pol, storm::CompareRelation cr) {
                     this->solver->add(smtrat::FormulaT(pol, cr));
                 }
@@ -105,3 +85,4 @@ namespace storm {
 
         }
 }
+#endif
\ No newline at end of file
diff --git a/src/solver/SmtratSmtSolver.h b/src/solver/SmtratSmtSolver.h
index 22bfa08e7..4f9126771 100644
--- a/src/solver/SmtratSmtSolver.h
+++ b/src/solver/SmtratSmtSolver.h
@@ -26,7 +26,7 @@ namespace storm {
 			virtual void pop(uint_fast64_t n) override;
 
 			virtual CheckResult check() override;
-#ifdef STORM_HAVE_CARL 
+
                         void add(storm::RawPolynomial const&, storm::CompareRelation);
                         
                         template<typename ReturnType>
@@ -38,7 +38,6 @@ namespace storm {
                         
                         
                         
-#endif
             
             // The last result that was returned by any of the check methods.
 			CheckResult lastResult;