diff --git a/src/adapters/MathsatExpressionAdapter.h b/src/adapters/MathsatExpressionAdapter.h
index 854b20542..9fec0cf15 100644
--- a/src/adapters/MathsatExpressionAdapter.h
+++ b/src/adapters/MathsatExpressionAdapter.h
@@ -22,9 +22,9 @@
namespace std {
// Define hashing operator for MathSAT's declarations.
template <>
- struct std::hash<msat_decl> {
- std::size_t operator()(msat_decl const& declaration) const {
- return std::hash<void*>()(declaration.repr);
+ struct hash<msat_decl> {
+ size_t operator()(msat_decl const& declaration) const {
+ return hash<void*>()(declaration.repr);
}
};
}
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 96b6298d0..a3d80d067 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -244,7 +244,7 @@ namespace storm {
// not only appear in the probabilities, we re
if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram->hasUndefinedConstants()) {
#else
- if (preparedProgram.hasUndefinedConstants()) {
+ if (preparedProgram->hasUndefinedConstants()) {
#endif
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram->getUndefinedConstants();
std::stringstream stream;
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index a1e71c0b7..e30965998 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -320,7 +320,7 @@ namespace storm {
return this->rewardModels;
}
- std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalNumber> const& model) {
+ std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
return storm::storage::getVariables(model.getTransitionMatrix());
}
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 1bc2f9af0..253609210 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -1208,6 +1208,19 @@ namespace storm {
return result;
}
+
+#ifdef STORM_HAVE_CARL
+ std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix)
+ {
+ std::set<storm::Variable> result;
+ for(auto const& entry : matrix) {
+ entry.getValue().gatherVariables(result);
+ }
+ return result;
+ }
+
+#endif
+
// Explicitly instantiate the entry, builder and the matrix.
// double
template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 21d675cab..f9d9916c4 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -8,7 +8,7 @@
#include <iterator>
#include "src/utility/OsDetection.h"
-
+#include "src/adapters/CarlAdapter.h"
#include <boost/functional/hash.hpp>
// Forward declaration for adapter classes.
@@ -970,14 +970,10 @@ namespace storm {
};
- std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix) {
- std::set<storm::Variable> result;
- for(auto const& entry : matrix) {
- entry.probability.gatherVariables(result);
- }
- return result;
- }
-
+#ifdef STORM_HAVE_CARL
+ std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix);
+#endif
+
} // namespace storage
} // namespace storm
diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
index 193b0ff28..bac64948f 100644
--- a/src/utility/graph.cpp
+++ b/src/utility/graph.cpp
@@ -986,9 +986,10 @@ namespace storm {
template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
- template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
- template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
-
+ template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#ifdef STORM_HAVE_CARL
+ template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
@@ -1004,19 +1005,24 @@ namespace storm {
template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#ifdef STORM_HAVE_CARL
template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#ifdef STORM_HAVE_CARL
template storm::storage::BitVector performProb1A(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<double> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<double>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
- template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
-
+#ifdef STORM_HAVE_CARL
+ template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
+#endif
template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<double> const& matrix) ;
diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
index 04f706221..4d87796b8 100644
--- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
@@ -10,6 +10,9 @@
#include "src/models/sparse/StandardRewardModel.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+
+#ifdef STORM_HAVE_MSAT
+
TEST(SmtPermissiveSchedulerTest, DieSelection) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
@@ -58,3 +61,5 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
//
}
+
+#endif // STORM_HAVE_MSAT