Browse Source

Some compile errors on Windows fixed, some still persist.

Former-commit-id: 1a9331371b
main
David_Korzeniewski 11 years ago
parent
commit
7da35af0bb
  1. 8
      src/modelchecker/ExplicitQualitativeCheckResult.cpp
  2. 1
      src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
  3. 6
      src/solver/SmtSolver.h
  4. 5
      src/solver/Z3SmtSolver.cpp
  5. 2
      src/solver/Z3SmtSolver.h
  6. 2
      src/storage/expressions/LinearCoefficientVisitor.h

8
src/modelchecker/ExplicitQualitativeCheckResult.cpp

@ -111,10 +111,18 @@ namespace storm {
out << std::boolalpha; out << std::boolalpha;
map_type const& map = boost::get<map_type>(truthValues); map_type const& map = boost::get<map_type>(truthValues);
#ifndef WINDOWS
typename map_type::const_iterator it = map.begin(); typename map_type::const_iterator it = map.begin();
typename map_type::const_iterator itPlusOne = map.begin(); typename map_type::const_iterator itPlusOne = map.begin();
++itPlusOne; ++itPlusOne;
typename map_type::const_iterator ite = map.end(); typename map_type::const_iterator ite = map.end();
#else
map_type::const_iterator it = map.begin();
map_type::const_iterator itPlusOne = map.begin();
++itPlusOne;
map_type::const_iterator ite = map.end();
#endif
for (; it != ite; ++itPlusOne, ++it) { for (; it != ite; ++itPlusOne, ++it) {
out << it->second; out << it->second;

1
src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp

@ -1,6 +1,7 @@
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include <algorithm> #include <algorithm>
#include <chrono>
#ifdef PARAMETRIC_SYSTEMS #ifdef PARAMETRIC_SYSTEMS
#include "src/storage/parameters.h" #include "src/storage/parameters.h"

6
src/solver/SmtSolver.h

@ -70,9 +70,15 @@ namespace storm {
virtual ~SmtSolver(); virtual ~SmtSolver();
SmtSolver(SmtSolver const& other) = default; SmtSolver(SmtSolver const& other) = default;
#ifndef WINDOWS
SmtSolver(SmtSolver&& other) = default; SmtSolver(SmtSolver&& other) = default;
#endif
SmtSolver& operator=(SmtSolver const& other) = default; SmtSolver& operator=(SmtSolver const& other) = default;
#ifndef WINDOWS
SmtSolver& operator=(SmtSolver&& other) = default; SmtSolver& operator=(SmtSolver&& other) = default;
#endif
/*! /*!
* Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those

5
src/solver/Z3SmtSolver.cpp

@ -155,6 +155,7 @@ namespace storm {
#endif #endif
} }
#ifndef WINDOWS
SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions)
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
@ -181,7 +182,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif #endif
} }
#endif
storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation() storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation()
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
@ -229,7 +230,7 @@ namespace storm {
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
std::vector<storm::expressions::SimpleValuation> valuations; std::vector<storm::expressions::SimpleValuation> valuations;
this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
this->allSat(important, static_cast<std::function<bool(storm::expressions::SimpleValuation&)>>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }));
return valuations; return valuations;
#else #else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");

2
src/solver/Z3SmtSolver.h

@ -51,7 +51,9 @@ namespace storm {
virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override; virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
#ifndef WINDOWS
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override; virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
#endif
virtual storm::expressions::SimpleValuation getModelAsValuation() override; virtual storm::expressions::SimpleValuation getModelAsValuation() override;

2
src/storage/expressions/LinearCoefficientVisitor.h

@ -18,8 +18,10 @@ namespace storm {
VariableCoefficients(VariableCoefficients const& other) = default; VariableCoefficients(VariableCoefficients const& other) = default;
VariableCoefficients& operator=(VariableCoefficients const& other) = default; VariableCoefficients& operator=(VariableCoefficients const& other) = default;
#ifndef WINDOWS
VariableCoefficients(VariableCoefficients&& other) = default; VariableCoefficients(VariableCoefficients&& other) = default;
VariableCoefficients& operator=(VariableCoefficients&& other) = default; VariableCoefficients& operator=(VariableCoefficients&& other) = default;
#endif
VariableCoefficients& operator+=(VariableCoefficients&& other); VariableCoefficients& operator+=(VariableCoefficients&& other);
VariableCoefficients& operator-=(VariableCoefficients&& other); VariableCoefficients& operator-=(VariableCoefficients&& other);

Loading…
Cancel
Save