Browse Source

Revert "Fixed compilation with mathsat."

This reverts commit 8b57b18201.
tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
58de346bd5
  1. 4
      src/storm/adapters/MathsatExpressionAdapter.h
  2. 35
      src/storm/solver/MathsatSmtSolver.cpp
  3. 6
      src/storm/solver/MathsatSmtSolver.h

4
src/storm/adapters/MathsatExpressionAdapter.h

@ -106,10 +106,6 @@ 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));

35
src/storm/solver/MathsatSmtSolver.cpp

@ -32,22 +32,6 @@ 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.
}
@ -78,25 +62,6 @@ 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)

6
src/storm/solver/MathsatSmtSolver.h

@ -38,8 +38,7 @@ 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;
@ -55,8 +54,7 @@ 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;

Loading…
Cancel
Save