From 8b57b18201304a47c4839659e25229ca4ee24b5b Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 17 Mar 2020 09:31:00 +0100
Subject: [PATCH] Fixed compilation with mathsat.
---
src/storm/adapters/MathsatExpressionAdapter.h | 4 +++
src/storm/solver/MathsatSmtSolver.cpp | 35 +++++++++++++++++++
src/storm/solver/MathsatSmtSolver.h | 6 ++--
3 files changed, 43 insertions(+), 2 deletions(-)
diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h
index 88ed84dcd..ca6de5d8c 100644
--- a/src/storm/adapters/MathsatExpressionAdapter.h
+++ b/src/storm/adapters/MathsatExpressionAdapter.h
@@ -106,6 +106,10 @@ namespace storm {
STORM_LOG_ASSERT(declarationVariablePair != declarationToVariableMapping.end(), "Unknown variable declaration.");
return declarationVariablePair->second;
}
+
+ std::unordered_map<storm::expressions::Variable, msat_decl> const& getAllDeclaredVariables() const {
+ return variableToDeclarationMapping;
+ }
virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override {
msat_term leftResult = boost::any_cast<msat_term>(expression.getFirstOperand()->accept(*this, data));
diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp
index 219efe530..f8c1d6f86 100644
--- a/src/storm/solver/MathsatSmtSolver.cpp
+++ b/src/storm/solver/MathsatSmtSolver.cpp
@@ -32,6 +32,22 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve double value from model that only contains boolean values.");
}
+ std::string MathsatSmtSolver::MathsatAllsatModelReference::toString() const {
+ std::stringstream str;
+ bool first = true;
+ str << "[";
+ for (auto const& varSlot : variableToSlotMapping) {
+ if (first) {
+ first = false;
+ } else {
+ str << ", ";
+ }
+ str << varSlot.first.getName() << "=" << std::boolalpha << getBooleanValue(varSlot.first);
+ }
+ str << "]";
+ return str.str();
+ }
+
MathsatSmtSolver::MathsatModelReference::MathsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter) : ModelReference(manager), env(env), expressionAdapter(expressionAdapter) {
// Intentionally left empty.
}
@@ -62,6 +78,25 @@ namespace storm {
storm::expressions::Expression value = expressionAdapter.translateExpression(msatValue);
return value.evaluateAsDouble();
}
+
+ std::string MathsatSmtSolver::MathsatModelReference::toString() const {
+ std::stringstream str;
+ bool first = true;
+ str << "[";
+ for (auto const& varDecl : expressionAdapter.getAllDeclaredVariables()) {
+ if (first) {
+ first = false;
+ } else {
+ str << ", ";
+ }
+ msat_term msatValue = msat_get_model_value(env, expressionAdapter.translateExpression(varDecl.first));
+ STORM_LOG_ASSERT(!MSAT_ERROR_TERM(msatValue), "Unable to retrieve value of variable in model. This could be caused by calls to the solver between checking for satisfiability and model retrieval.");
+ str << varDecl.first.getName() << "=" << expressionAdapter.translateExpression(msatValue);
+ }
+ str << "]";
+ return str.str();
+ }
+
#endif
MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options) : SmtSolver(manager)
diff --git a/src/storm/solver/MathsatSmtSolver.h b/src/storm/solver/MathsatSmtSolver.h
index 0d27c71af..851c00d82 100644
--- a/src/storm/solver/MathsatSmtSolver.h
+++ b/src/storm/solver/MathsatSmtSolver.h
@@ -38,7 +38,8 @@ namespace storm {
virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
-
+ virtual std::string toString() const override;
+
private:
msat_env const& env;
msat_term* model;
@@ -54,7 +55,8 @@ namespace storm {
virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override;
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override;
virtual double getRationalValue(storm::expressions::Variable const& variable) const override;
-
+ virtual std::string toString() const override;
+
private:
msat_env const& env;
storm::adapters::MathsatExpressionAdapter& expressionAdapter;