From 3887cb57aab63560dc54f74a0c0533321d78b79c Mon Sep 17 00:00:00 2001
From: David_Korzeniewski <david.korzeniewski@rwth-aachen.de>
Date: Wed, 2 Jul 2014 17:13:21 +0200
Subject: [PATCH] Fix for temporaries and non const references
Former-commit-id: 4eadf6cdab1e6be56e4c2c127d520953d3319e8c
---
src/solver/SmtSolver.h | 12 ++++++------
src/solver/Z3SmtSolver.cpp | 8 ++++----
src/solver/Z3SmtSolver.h | 8 ++++----
3 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h
index 914860bbc..c34c8a440 100644
--- a/src/solver/SmtSolver.h
+++ b/src/solver/SmtSolver.h
@@ -59,11 +59,11 @@ namespace storm {
//! assert an expression in the solver
//! @param e the asserted expression, the return type has to be bool
//! @throws IllegalArgumentTypeException if the return type of the expression is not bool
- virtual void assertExpression(storm::expressions::Expression &e) = 0;
+ virtual void assertExpression(storm::expressions::Expression const& e) = 0;
//! assert a set of expressions in the solver
//! @param es the asserted expressions
//! @see assert(storm::expressions::Expression &e)
- virtual void assertExpression(std::set<storm::expressions::Expression> &es) {
+ virtual void assertExpression(std::set<storm::expressions::Expression> const& es) {
for (storm::expressions::Expression e : es) {
this->assertExpression(e);
}
@@ -80,7 +80,7 @@ namespace storm {
//! assert a set of expressions in the solver
//! @param es the asserted expressions
//! @see assert(storm::expressions::Expression &e)
- virtual void assertExpression(std::initializer_list<storm::expressions::Expression> &es) {
+ virtual void assertExpression(std::initializer_list<storm::expressions::Expression> const& es) {
for (storm::expressions::Expression e : es) {
this->assertExpression(e);
}
@@ -98,7 +98,7 @@ namespace storm {
//! @param es the asserted expressions
//! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool
//! @see check()
- virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions) = 0;
+ virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) = 0;
//! check satisfiability of the conjunction of the currently asserted expressions and the provided assumptions
//! @param es the asserted expressions
//! @throws IllegalArgumentTypeException if the return type of one of the expressions is not bool
@@ -138,7 +138,7 @@ namespace storm {
* @throws IllegalFunctionCallException if model generation is not configured for this solver
* @throws NotImplementedException if model generation is not implemented with this solver class
*/
- virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> important) {
+ virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) {
throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
}
@@ -154,7 +154,7 @@ namespace storm {
* @throws IllegalFunctionCallException if model generation is not configured for this solver
* @throws NotImplementedException if model generation is not implemented with this solver class
*/
- virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback) {
+ virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) {
throw storm::exceptions::NotImplementedException("This subclass of SmtSolver does not support model generation.");
}
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index 6c13941e0..c2d58367b 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -52,7 +52,7 @@ namespace storm {
#endif
}
- void Z3SmtSolver::assertExpression(storm::expressions::Expression &e)
+ void Z3SmtSolver::assertExpression(storm::expressions::Expression const& e)
{
#ifdef STORM_HAVE_Z3
this->m_solver.add(m_adapter.translateExpression(e, true));
@@ -82,7 +82,7 @@ namespace storm {
#endif
}
- SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions)
+ SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions)
{
#ifdef STORM_HAVE_Z3
lastCheckAssumptions = true;
@@ -179,7 +179,7 @@ namespace storm {
#endif
}
- std::vector<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> important)
+ std::vector<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important)
{
#ifdef STORM_HAVE_Z3
@@ -194,7 +194,7 @@ namespace storm {
#endif
}
- uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback)
+ uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback)
{
#ifdef STORM_HAVE_Z3
for (storm::expressions::Expression e : important) {
diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h
index a34c5d412..b3b20a46a 100644
--- a/src/solver/Z3SmtSolver.h
+++ b/src/solver/Z3SmtSolver.h
@@ -23,19 +23,19 @@ namespace storm {
virtual void reset() override;
- virtual void assertExpression(storm::expressions::Expression &e) override;
+ virtual void assertExpression(storm::expressions::Expression const& e) override;
virtual CheckResult check() override;
- virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> &assumptions) override;
+ virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions) override;
virtual storm::expressions::SimpleValuation getModel() override;
- virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> important) override;
+ virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) override;
- virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
+ virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> callback) override;
virtual std::vector<storm::expressions::Expression> getUnsatAssumptions() override;