fixed some guards for smtsolver

Former-commit-id: 2205f1af57

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

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;