From ab36c5fb0d61eb51821db8412c032233de746178 Mon Sep 17 00:00:00 2001 From: David_Korzeniewski Date: Thu, 29 Jan 2015 15:04:02 +0100 Subject: [PATCH] Workarounds for more Windows quirks. Compiles but tests crash. Former-commit-id: 0c47ae886d0fcd4577cf9752392993ff331ff812 --- src/solver/MathsatSmtSolver.cpp | 2 ++ src/solver/MathsatSmtSolver.h | 2 ++ src/solver/SmtSolver.h | 4 +++- src/storage/expressions/Expression.h | 10 ++++++++++ 4 files changed, 17 insertions(+), 1 deletion(-) diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index 9627c8dea..16610f4ad 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -191,6 +191,7 @@ namespace storm { #endif } +#ifndef WINDOWS SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_MSAT @@ -218,6 +219,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support."); #endif } +#endif storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() { diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h index badca77a8..a1ec0810b 100644 --- a/src/solver/MathsatSmtSolver.h +++ b/src/solver/MathsatSmtSolver.h @@ -79,7 +79,9 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; +#endif virtual storm::expressions::SimpleValuation getModelAsValuation() override; diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index d97481b09..475c3ee95 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -152,8 +152,10 @@ namespace storm { * @param assumptions The assumptions to add to the call. * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability. - */ + */ +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) = 0; +#endif /*! * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 2c7360b08..777bde9f9 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -324,4 +324,14 @@ namespace storm { } } +//specialize +namespace std { + template<> + struct less < storm::expressions::Expression > { + bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const { + return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer(); + } + }; +} + #endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */ \ No newline at end of file