From 85a4376e399b2517138291179b422a2fb9f615f1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 23 Dec 2014 22:39:07 +0100 Subject: [PATCH] Now StoRM can be properly compiled without support for MathSAT if needed. Former-commit-id: 28da4f5ed8bac4f7f0e2f6d786c41d5e1159d98f --- src/adapters/MathsatExpressionAdapter.h | 2 ++ .../SMTMinimalCommandSetGenerator.h | 2 +- src/solver/MathsatSmtSolver.cpp | 24 ++++++++++------- src/solver/MathsatSmtSolver.h | 26 +++++++------------ 4 files changed, 28 insertions(+), 26 deletions(-) diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h index 46189935f..1aee8f53f 100644 --- a/src/adapters/MathsatExpressionAdapter.h +++ b/src/adapters/MathsatExpressionAdapter.h @@ -5,7 +5,9 @@ #include +#ifdef STORM_HAVE_MSAT #include "mathsat.h" +#endif #include "storage/expressions/Expressions.h" #include "storage/expressions/ExpressionVisitor.h" diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 2fe722951..3f8748e44 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -620,7 +620,7 @@ namespace storm { } } - storm::adapters::Z3ExpressionAdapter expressionAdapter(localContext, solverVariables); + storm::adapters::Z3ExpressionAdapter expressionAdapter(localContext, false, solverVariables); // Then add the constraints for bounds of the integer variables.. for (auto const& integerVariable : program.getGlobalIntegerVariables()) { diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 3c0778b3d..4c095690b 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -11,7 +11,7 @@ namespace storm { MathsatSmtSolver::MathsatAllsatModelReference::MathsatAllsatModelReference(msat_env const& env, msat_term* model, std::unordered_map const& atomNameToSlotMapping) : env(env), model(model), atomNameToSlotMapping(atomNameToSlotMapping) { // Intentionally left empty. } -#endif + bool MathsatSmtSolver::MathsatAllsatModelReference::getBooleanValue(std::string const& name) const { std::unordered_map::const_iterator nameSlotPair = atomNameToSlotMapping.find(name); STORM_LOG_THROW(nameSlotPair != atomNameToSlotMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve value of unknown variable '" << name << "' from model."); @@ -32,11 +32,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve double value from model that only contains boolean values."); } -#ifdef STORM_HAVE_MSAT MathsatSmtSolver::MathsatModelReference::MathsatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter) : env(env), expressionAdapter(expressionAdapter) { // Intentionally left empty. } -#endif + bool MathsatSmtSolver::MathsatModelReference::getBooleanValue(std::string const& name) const { msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name)); msat_term msatValue = msat_get_model_value(env, msatVariable); @@ -63,7 +62,8 @@ namespace storm { STORM_LOG_THROW(value.hasIntegralReturnType(), storm::exceptions::InvalidArgumentException, "Unable to retrieve double value of non-double variable '" << name << "'."); return value.evaluateAsDouble(); } - +#endif + MathsatSmtSolver::MathsatSmtSolver(Options const& options) #ifdef STORM_HAVE_MSAT : expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) @@ -92,8 +92,12 @@ namespace storm { } MathsatSmtSolver::~MathsatSmtSolver() { +#ifdef STORM_HAVE_MSAT STORM_LOG_THROW(!MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Illegal MathSAT environment."); msat_destroy_env(env); +#else + // Empty. +#endif } void MathsatSmtSolver::push() { @@ -113,7 +117,11 @@ namespace storm { } void MathsatSmtSolver::pop(uint_fast64_t n) { +#ifdef STORM_HAVE_MSAT SmtSolver::pop(n); +#else + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); +#endif } void MathsatSmtSolver::reset() @@ -347,8 +355,7 @@ namespace storm { #endif - uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) - { + uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. this->push(); @@ -368,12 +375,11 @@ namespace storm { this->pop(); return static_cast(numberOfModels); #else - LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } - uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) - { + uint_fast64_t MathsatSmtSolver::allSat(std::vector const& important, std::function const& callback) { #ifdef STORM_HAVE_MSAT // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure. this->push(); diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index 011f0547a..db5015bb9 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -6,10 +6,6 @@ #include "src/adapters/MathsatExpressionAdapter.h" #include -#ifndef STORM_HAVE_MSAT -#define STORM_HAVE_MSAT -#endif - #ifdef STORM_HAVE_MSAT #include "mathsat.h" #endif @@ -34,38 +30,36 @@ namespace storm { bool enableInterpolantGeneration = false; }; +#ifdef STORM_HAVE_MSAT class MathsatAllsatModelReference : public SmtSolver::ModelReference { public: -#ifdef STORM_HAVE_MSAT MathsatAllsatModelReference(msat_env const& env, msat_term* model, std::unordered_map const& atomNameToSlotMapping); -#endif - virtual bool getBooleanValue(std::string const& name) const override; + + virtual bool getBooleanValue(std::string const& name) const override; virtual int_fast64_t getIntegerValue(std::string const& name) const override; virtual double getDoubleValue(std::string const& name) const override; private: -#ifdef STORM_HAVE_MSAT msat_env const& env; msat_term* model; std::unordered_map const& atomNameToSlotMapping; -#endif }; +#endif +#ifdef STORM_HAVE_MSAT class MathsatModelReference : public SmtSolver::ModelReference { public: -#ifdef STORM_HAVE_MSAT MathsatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter); -#endif - virtual bool getBooleanValue(std::string const& name) const override; + + virtual bool getBooleanValue(std::string const& name) const override; virtual int_fast64_t getIntegerValue(std::string const& name) const override; virtual double getDoubleValue(std::string const& name) const override; private: -#ifdef STORM_HAVE_MSAT msat_env const& env; storm::adapters::MathsatExpressionAdapter& expressionAdapter; -#endif }; +#endif MathsatSmtSolver(Options const& options = Options()); @@ -104,15 +98,16 @@ namespace storm { virtual storm::expressions::Expression getInterpolant(std::vector const& groupsA) override; private: -#ifdef STORM_HAVE_MSAT storm::expressions::SimpleValuation convertMathsatModelToValuation(); +#ifdef STORM_HAVE_MSAT // The MathSAT environment. msat_env env; // The expression adapter used to translate expressions to MathSAT's format. This has to be a pointer, since // it must be initialized after creating the environment, but the adapter class has no default constructor. std::unique_ptr expressionAdapter; +#endif // A flag storing whether the last call was a check involving assumptions. bool lastCheckAssumptions; @@ -123,7 +118,6 @@ namespace storm { // A mapping of interpolation group indices to their MathSAT identifier. typedef boost::container::flat_map InterpolationGroupMapType; InterpolationGroupMapType interpolationGroups; -#endif }; } }