diff --git a/src/adapters/MathSatExpressionAdapter.h b/src/adapters/MathSatExpressionAdapter.h index 949ae46c5..4436959e1 100644 --- a/src/adapters/MathSatExpressionAdapter.h +++ b/src/adapters/MathSatExpressionAdapter.h @@ -15,9 +15,10 @@ #include "storage/expressions/Expressions.h" #include "storage/expressions/ExpressionVisitor.h" -#include "src/exceptions/ExceptionMacros.h" +#include "src/utility/macros.h" #include "src/exceptions/ExpressionEvaluationException.h" #include "src/exceptions/InvalidTypeException.h" +#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/NotImplementedException.h" namespace storm { @@ -225,15 +226,13 @@ namespace storm { } virtual void visit(expressions::VariableExpression const* expression) override { - if (variableToDeclMap.count(expression->getVariableName()) == 0) { - LOG4CPLUS_ERROR(logger, "Variable " << expression->getVariableName() << " is unknown!"); - } + STORM_LOG_THROW(variableToDeclMap.count(expression->getVariableName()) != 0, storm::exceptions::InvalidArgumentException, "Variable '" << expression->getVariableName() << "' is unknown."); //LOG4CPLUS_TRACE(logger, "Variable "<getVariableName()); //char* repr = msat_decl_repr(variableToDeclMap.at(expression->getVariableName())); //LOG4CPLUS_TRACE(logger, "Decl: "<getVariableName()))) { - LOG4CPLUS_WARN(logger, "Encountered an invalid MathSAT declaration"); + STORM_LOG_WARN("Encountered an invalid MathSAT declaration."); } stack.push(msat_make_constant(env, variableToDeclMap.at(expression->getVariableName()))); } diff --git a/src/solver/MathSatSmtSolver.cpp b/src/solver/MathSatSmtSolver.cpp index f03ee3d6e..285f8d422 100644 --- a/src/solver/MathSatSmtSolver.cpp +++ b/src/solver/MathSatSmtSolver.cpp @@ -32,7 +32,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_push_backtrack_point(m_env); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -41,7 +41,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_pop_backtrack_point(m_env); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -52,7 +52,7 @@ namespace storm { this->pop(); } #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -61,7 +61,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_reset_env(m_env); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -70,7 +70,7 @@ namespace storm { #ifdef STORM_HAVE_MSAT msat_assert_formula(m_env, m_adapter->translateExpression(e, true)); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -91,7 +91,7 @@ namespace storm { } return this->lastResult; #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -119,7 +119,7 @@ namespace storm { } return this->lastResult; #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -147,7 +147,7 @@ namespace storm { } return this->lastResult; #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -155,11 +155,11 @@ namespace storm { { #ifdef STORM_HAVE_MSAT - LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT."); + STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::SAT, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT."); return this->MathSatModelToStorm(); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -188,7 +188,7 @@ namespace storm { stormModel.addDoubleIdentifier(std::string(name), var_i_interp.evaluateAsDouble()); break; default: - LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") + STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") break; } @@ -211,7 +211,7 @@ namespace storm { return valuations; #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -281,9 +281,9 @@ namespace storm { uint_fast64_t MathSatSmtSolver::allSat(std::function callback, std::vector const& important) { #ifdef STORM_HAVE_MSAT - LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented."); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -308,7 +308,7 @@ namespace storm { return unsatAssumptions; #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -325,7 +325,7 @@ namespace storm { } msat_set_itp_group(m_env, groupIter->second); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } @@ -351,7 +351,7 @@ namespace storm { return this->m_adapter->translateTerm(interpolant); #else - LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support."); #endif } }