sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Moved to new macros. 

Former-commit-id: d97c947c22
tempestpy_adaptions
dehnert 10 years ago
parent
2912ec23fe
commit
3231ea6c06
2 changed files with 21 additions and 22 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      src/adapters/MathSatExpressionAdapter.h
  2. 34
      src/solver/MathSatSmtSolver.cpp

9
src/adapters/MathSatExpressionAdapter.h
View File

@ -15,9 +15,10 @@
#include "storage/expressions/Expressions.h" #include "storage/expressions/Expressions.h"
#include "storage/expressions/ExpressionVisitor.h" #include "storage/expressions/ExpressionVisitor.h"
#include "src/exceptions/ExceptionMacros.h"
#include "src/utility/macros.h"
#include "src/exceptions/ExpressionEvaluationException.h" #include "src/exceptions/ExpressionEvaluationException.h"
#include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/NotImplementedException.h" #include "src/exceptions/NotImplementedException.h"
namespace storm { namespace storm {
@ -225,15 +226,13 @@ namespace storm {
} }
virtual void visit(expressions::VariableExpression const* expression) override { 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 "<<expression->getVariableName()); //LOG4CPLUS_TRACE(logger, "Variable "<<expression->getVariableName());
//char* repr = msat_decl_repr(variableToDeclMap.at(expression->getVariableName())); //char* repr = msat_decl_repr(variableToDeclMap.at(expression->getVariableName()));
//LOG4CPLUS_TRACE(logger, "Decl: "<<repr); //LOG4CPLUS_TRACE(logger, "Decl: "<<repr);
//msat_free(repr); //msat_free(repr);
if (MSAT_ERROR_DECL(variableToDeclMap.at(expression->getVariableName()))) { if (MSAT_ERROR_DECL(variableToDeclMap.at(expression->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()))); stack.push(msat_make_constant(env, variableToDeclMap.at(expression->getVariableName())));
} }

34
src/solver/MathSatSmtSolver.cpp
View File

@ -32,7 +32,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_push_backtrack_point(m_env); msat_push_backtrack_point(m_env);
#else #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 #endif
} }
@ -41,7 +41,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_pop_backtrack_point(m_env); msat_pop_backtrack_point(m_env);
#else #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 #endif
} }
@ -52,7 +52,7 @@ namespace storm {
this->pop(); this->pop();
} }
#else #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 #endif
} }
@ -61,7 +61,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_reset_env(m_env); msat_reset_env(m_env);
#else #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 #endif
} }
@ -70,7 +70,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_assert_formula(m_env, m_adapter->translateExpression(e, true)); msat_assert_formula(m_env, m_adapter->translateExpression(e, true));
#else #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 #endif
} }
@ -91,7 +91,7 @@ namespace storm {
} }
return this->lastResult; return this->lastResult;
#else #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 #endif
} }
@ -119,7 +119,7 @@ namespace storm {
} }
return this->lastResult; return this->lastResult;
#else #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 #endif
} }
@ -147,7 +147,7 @@ namespace storm {
} }
return this->lastResult; return this->lastResult;
#else #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 #endif
} }
@ -155,11 +155,11 @@ namespace storm {
{ {
#ifdef STORM_HAVE_MSAT #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(); return this->MathSatModelToStorm();
#else #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 #endif
} }
@ -188,7 +188,7 @@ namespace storm {
stormModel.addDoubleIdentifier(std::string(name), var_i_interp.evaluateAsDouble()); stormModel.addDoubleIdentifier(std::string(name), var_i_interp.evaluateAsDouble());
break; break;
default: 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; break;
} }
@ -211,7 +211,7 @@ namespace storm {
return valuations; return valuations;
#else #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 #endif
} }
@ -281,9 +281,9 @@ namespace storm {
uint_fast64_t MathSatSmtSolver::allSat(std::function<bool(SmtSolver::ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important) uint_fast64_t MathSatSmtSolver::allSat(std::function<bool(SmtSolver::ModelReference&)> callback, std::vector<storm::expressions::Expression> const& important)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented.");
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented.");
#else #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 #endif
} }
@ -308,7 +308,7 @@ namespace storm {
return unsatAssumptions; return unsatAssumptions;
#else #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 #endif
} }
@ -325,7 +325,7 @@ namespace storm {
} }
msat_set_itp_group(m_env, groupIter->second); msat_set_itp_group(m_env, groupIter->second);
#else #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 #endif
} }
@ -351,7 +351,7 @@ namespace storm {
return this->m_adapter->translateTerm(interpolant); return this->m_adapter->translateTerm(interpolant);
#else #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 #endif
} }
} }
Write Preview
Loading…
Cancel
Save