diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index d4aa08590..d6096e750 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -91,12 +91,12 @@ namespace storm {
if (actualIndexBucketPair.first == newIndex) {
if (options.explorationOrder == ExplorationOrder::Dfs) {
- statesToExplore.push_front(state);
+ statesToExplore.emplace_front(state, actualIndexBucketPair.first);
// Reserve one slot for the new state in the remapping.
stateRemapping.get().push_back(storm::utility::zero<StateType>());
} else if (options.explorationOrder == ExplorationOrder::Bfs) {
- statesToExplore.push_back(state);
+ statesToExplore.emplace_back(state, actualIndexBucketPair.first);
} else {
STORM_LOG_ASSERT(false, "Invalid exploration order.");
}
@@ -139,8 +139,8 @@ namespace storm {
// Perform a search through the model.
while (!statesToExplore.empty()) {
// Get the first state in the queue.
- CompressedState currentState = statesToExplore.front();
- StateType currentIndex = stateStorage.stateToId.getValue(currentState);
+ CompressedState currentState = statesToExplore.front().first;
+ StateType currentIndex = statesToExplore.front().second;
statesToExplore.pop_front();
// If the exploration order differs from breadth-first, we remember that this row group was actually
diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h
index ef5da691b..9440b7e08 100644
--- a/src/storm/builder/ExplicitModelBuilder.h
+++ b/src/storm/builder/ExplicitModelBuilder.h
@@ -136,7 +136,7 @@ namespace storm {
storm::storage::sparse::StateStorage<StateType> stateStorage;
/// A set of states that still need to be explored.
- std::deque<CompressedState> statesToExplore;
+ std::deque<std::pair<CompressedState, StateType>> statesToExplore;
/// An optional mapping from state indices to the row groups in which they actually reside. This needs to be
/// built in case the exploration order is not BFS.
diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp
index f2c4a483d..b33a332df 100644
--- a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp
+++ b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp
@@ -29,7 +29,6 @@ namespace storm {
return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
}
-
bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const {
return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp";
}
diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp
index 9cec1aa20..434ab6906 100644
--- a/src/storm/storage/BitVectorHashMap.cpp
+++ b/src/storm/storage/BitVectorHashMap.cpp
@@ -210,6 +210,11 @@ namespace storm {
return values[flagBucketPair.second];
}
+ template<class ValueType, class Hash>
+ ValueType BitVectorHashMap<ValueType, Hash>::getValue(std::size_t bucket) const {
+ return values[bucket];
+ }
+
template<class ValueType, class Hash>
bool BitVectorHashMap<ValueType, Hash>::contains(storm::storage::BitVector const& key) const {
return findBucket(key).first;
diff --git a/src/storm/storage/BitVectorHashMap.h b/src/storm/storage/BitVectorHashMap.h
index e2ca51a5e..7c400c1cd 100644
--- a/src/storm/storage/BitVectorHashMap.h
+++ b/src/storm/storage/BitVectorHashMap.h
@@ -113,6 +113,13 @@ namespace storm {
* @return The value associated with the given key (if any).
*/
ValueType getValue(storm::storage::BitVector const& key) const;
+
+ /*!
+ * Retrieves the value associated with the given bucket.
+ *
+ * @return The value associated with the given bucket (if any).
+ */
+ ValueType getValue(std::size_t bucket) const;
/*!
* Checks if the given key is already contained in the map.
diff --git a/src/storm/storage/expressions/CompiledExpression.cpp b/src/storm/storage/expressions/CompiledExpression.cpp
new file mode 100644
index 000000000..759ea899c
--- /dev/null
+++ b/src/storm/storage/expressions/CompiledExpression.cpp
@@ -0,0 +1,21 @@
+#include "storm/storage/expressions/CompiledExpression.h"
+
+#include "storm/storage/expressions/ExprtkCompiledExpression.h"
+
+namespace storm {
+ namespace expressions {
+
+ bool CompiledExpression::isExprtkCompiledExpression() const {
+ return false;
+ }
+
+ ExprtkCompiledExpression& CompiledExpression::asExprtkCompiledExpression() {
+ return static_cast<ExprtkCompiledExpression&>(*this);
+ }
+
+ ExprtkCompiledExpression const& CompiledExpression::asExprtkCompiledExpression() const {
+ return static_cast<ExprtkCompiledExpression const&>(*this);
+ }
+
+ }
+}
diff --git a/src/storm/storage/expressions/CompiledExpression.h b/src/storm/storage/expressions/CompiledExpression.h
new file mode 100644
index 000000000..786408c94
--- /dev/null
+++ b/src/storm/storage/expressions/CompiledExpression.h
@@ -0,0 +1,20 @@
+#pragma once
+
+namespace storm {
+ namespace expressions {
+
+ class ExprtkCompiledExpression;
+
+ class CompiledExpression {
+ public:
+
+ virtual bool isExprtkCompiledExpression() const;
+ ExprtkCompiledExpression& asExprtkCompiledExpression();
+ ExprtkCompiledExpression const& asExprtkCompiledExpression() const;
+
+ private:
+ // Currently empty.
+ };
+
+ }
+}
diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index 95c4f69e0..ed00728f0 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -9,6 +9,7 @@
#include "storm/storage/expressions/ChangeManagerVisitor.h"
#include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h"
#include "storm/storage/expressions/Expressions.h"
+#include "storm/storage/expressions/CompiledExpression.h"
#include "storm/exceptions/InvalidTypeException.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/utility/macros.h"
@@ -26,6 +27,11 @@ namespace storm {
STORM_LOG_THROW(a.getManager() == b.getManager(), storm::exceptions::InvalidArgumentException, "Expressions are managed by different manager.");
}
+ // Spell out destructor explicitly so we can use forward declarations in the header.
+ Expression::~Expression() {
+ // Intentionally left empty.
+ }
+
Expression::Expression(std::shared_ptr<BaseExpression const> const& expressionPtr) : expressionPtr(expressionPtr) {
// Intentionally left empty.
}
@@ -196,7 +202,19 @@ namespace storm {
return true;
}
SyntacticalEqualityCheckVisitor checker;
- return checker.isSyntaticallyEqual(*this, other);
+ return checker.isSyntacticallyEqual(*this, other);
+ }
+
+ bool Expression::hasCompiledExpression() const {
+ return static_cast<bool>(compiledExpression);
+ }
+
+ void Expression::setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const {
+ this->compiledExpression = compiledExpression;
+ }
+
+ CompiledExpression const& Expression::getCompiledExpression() const {
+ return *compiledExpression;
}
std::string Expression::toString() const {
diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h
index 26d6033c6..98a2e6417 100644
--- a/src/storm/storage/expressions/Expression.h
+++ b/src/storm/storage/expressions/Expression.h
@@ -15,6 +15,7 @@ namespace storm {
class ExpressionManager;
class Variable;
class ExpressionVisitor;
+ class CompiledExpression;
class Expression {
public:
@@ -58,6 +59,7 @@ namespace storm {
friend Expression maximum(Expression const& first, Expression const& second);
Expression() = default;
+ ~Expression();
/*!
* Creates an expression representing the given variable.
@@ -358,11 +360,29 @@ namespace storm {
*/
bool isSyntacticallyEqual(storm::expressions::Expression const& other) const;
+ /*!
+ * Retrieves whether this expression object has an associated compiled expression.
+ */
+ bool hasCompiledExpression() const;
+
+ /*!
+ * Associates the given compiled expression with this expression object.
+ */
+ void setCompiledExpression(std::shared_ptr<CompiledExpression> const& compiledExpression) const;
+
+ /*!
+ * Retrieves the associated compiled expression object (if there is any).
+ */
+ CompiledExpression const& getCompiledExpression() const;
+
friend std::ostream& operator<<(std::ostream& stream, Expression const& expression);
private:
// A pointer to the underlying base expression.
std::shared_ptr<BaseExpression const> expressionPtr;
+
+ // A pointer to an associated compiled expression object (if any).
+ mutable std::shared_ptr<CompiledExpression> compiledExpression;
};
// Provide operator overloads to conveniently construct new expressions from other expressions.
diff --git a/src/storm/storage/expressions/ExprtkCompiledExpression.cpp b/src/storm/storage/expressions/ExprtkCompiledExpression.cpp
new file mode 100644
index 000000000..2dda7945d
--- /dev/null
+++ b/src/storm/storage/expressions/ExprtkCompiledExpression.cpp
@@ -0,0 +1,19 @@
+#include "storm/storage/expressions/ExprtkCompiledExpression.h"
+
+namespace storm {
+ namespace expressions {
+
+ ExprtkCompiledExpression::ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression) : exprtkCompiledExpression(exprtkCompiledExpression) {
+ // Intentionally left empty.
+ }
+
+ ExprtkCompiledExpression::CompiledExpressionType const& ExprtkCompiledExpression::getCompiledExpression() const {
+ return exprtkCompiledExpression;
+ }
+
+ bool ExprtkCompiledExpression::isExprtkCompiledExpression() const {
+ return true;
+ }
+
+ }
+}
diff --git a/src/storm/storage/expressions/ExprtkCompiledExpression.h b/src/storm/storage/expressions/ExprtkCompiledExpression.h
new file mode 100644
index 000000000..b2c98fc2b
--- /dev/null
+++ b/src/storm/storage/expressions/ExprtkCompiledExpression.h
@@ -0,0 +1,25 @@
+#pragma once
+
+#include "storm/storage/expressions/CompiledExpression.h"
+
+#include "storm/utility/exprtk.h"
+
+namespace storm {
+ namespace expressions {
+
+ class ExprtkCompiledExpression : public CompiledExpression {
+ public:
+ typedef exprtk::expression<double> CompiledExpressionType;
+
+ ExprtkCompiledExpression(CompiledExpressionType const& exprtkCompiledExpression);
+
+ CompiledExpressionType const& getCompiledExpression() const;
+
+ virtual bool isExprtkCompiledExpression() const override;
+
+ private:
+ CompiledExpressionType exprtkCompiledExpression;
+ };
+
+ }
+}
diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp
index 70cd6e162..3b8b3ea70 100755
--- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp
+++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp
@@ -26,34 +26,26 @@ namespace storm {
template<typename RationalType>
bool ExprtkExpressionEvaluatorBase<RationalType>::asBool(Expression const& expression) const {
- std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer();
- auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer());
- if (expressionPair == this->compiledExpressions.end()) {
- CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression);
- return compiledExpression.value() == ValueType(1);
- }
- return expressionPair->second.value() == ValueType(1);
+ auto const& compiledExpression = getCompiledExpression(expression);
+ return compiledExpression.value() == ValueType(1);
}
template<typename RationalType>
int_fast64_t ExprtkExpressionEvaluatorBase<RationalType>::asInt(Expression const& expression) const {
- std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer();
- auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer());
- if (expressionPair == this->compiledExpressions.end()) {
- CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression);
- return static_cast<int_fast64_t>(compiledExpression.value());
- }
- return static_cast<int_fast64_t>(expressionPair->second.value());
+ auto const& compiledExpression = getCompiledExpression(expression);
+ return static_cast<int_fast64_t>(compiledExpression.value());
}
template<typename RationalType>
- typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const {
- std::pair<CacheType::iterator, bool> result = this->compiledExpressions.emplace(expression.getBaseExpressionPointer(), CompiledExpressionType());
- CompiledExpressionType& compiledExpression = result.first->second;
- compiledExpression.register_symbol_table(*symbolTable);
- bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
- STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")");
- return compiledExpression;
+ typename ExprtkExpressionEvaluatorBase<RationalType>::CompiledExpressionType const& ExprtkExpressionEvaluatorBase<RationalType>::getCompiledExpression(storm::expressions::Expression const& expression) const {
+ if (!expression.hasCompiledExpression() || !expression.getCompiledExpression().isExprtkCompiledExpression()) {
+ CompiledExpressionType compiledExpression;
+ compiledExpression.register_symbol_table(*symbolTable);
+ bool parsingOk = parser->compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
+ STORM_LOG_THROW(parsingOk, storm::exceptions::UnexpectedException, "Expression was not properly parsed by ExprTk: " << expression << ". (Returned error: " << parser->error() << ")");
+ expression.setCompiledExpression(std::make_shared<ExprtkCompiledExpression>(compiledExpression));
+ }
+ return expression.getCompiledExpression().asExprtkCompiledExpression().getCompiledExpression();
}
template<typename RationalType>
@@ -76,13 +68,8 @@ namespace storm {
}
double ExprtkExpressionEvaluator::asRational(Expression const& expression) const {
- std::shared_ptr<BaseExpression const> expressionPtr = expression.getBaseExpressionPointer();
- auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer());
- if (expressionPair == this->compiledExpressions.end()) {
- CompiledExpressionType const& compiledExpression = this->getCompiledExpression(expression);
- return static_cast<double>(compiledExpression.value());
- }
- return static_cast<double>(expressionPair->second.value());
+ auto const& compiledExpression = getCompiledExpression(expression);
+ return static_cast<double>(compiledExpression.value());
}
template class ExprtkExpressionEvaluatorBase<double>;
diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.h b/src/storm/storage/expressions/ExprtkExpressionEvaluator.h
index 1eefe163b..e6a7c6fb4 100755
--- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.h
+++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.h
@@ -6,18 +6,12 @@
#include "storm/storage/expressions/ExpressionEvaluatorBase.h"
-#pragma clang diagnostic push
-#pragma clang diagnostic ignored "-Wunused-variable"
-
-#pragma GCC diagnostic push
-
-#include "exprtk.hpp"
-
-#pragma GCC diagnostic pop
-#pragma clang diagnostic pop
+#include "storm/utility/exprtk.h"
#include "storm/storage/expressions/ToExprtkStringVisitor.h"
+#include "storm/storage/expressions/ExprtkCompiledExpression.h"
+
namespace storm {
namespace expressions {
template <typename RationalType>
@@ -34,15 +28,14 @@ namespace storm {
protected:
typedef double ValueType;
- typedef exprtk::expression<ValueType> CompiledExpressionType;
- typedef std::unordered_map<std::shared_ptr<BaseExpression const>, CompiledExpressionType> CacheType;
+ typedef ExprtkCompiledExpression::CompiledExpressionType CompiledExpressionType;
/*!
- * Adds a compiled version of the given expression to the internal storage.
+ * Retrieves a compiled version of the given expression.
*
* @param expression The expression that is to be compiled.
*/
- CompiledExpressionType& getCompiledExpression(storm::expressions::Expression const& expression) const;
+ CompiledExpressionType const& getCompiledExpression(storm::expressions::Expression const& expression) const;
// The parser used.
mutable std::unique_ptr<exprtk::parser<ValueType>> parser;
@@ -54,9 +47,6 @@ namespace storm {
std::vector<ValueType> booleanValues;
std::vector<ValueType> integerValues;
std::vector<ValueType> rationalValues;
-
- // A mapping of expressions to their compiled counterpart.
- mutable CacheType compiledExpressions;
};
class ExprtkExpressionEvaluator : public ExprtkExpressionEvaluatorBase<double> {
diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
index c1133c9db..7f45240d7 100644
--- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
+++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp
@@ -5,7 +5,7 @@
namespace storm {
namespace expressions {
- bool SyntacticalEqualityCheckVisitor::isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) {
+ bool SyntacticalEqualityCheckVisitor::isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2) {
return boost::any_cast<bool>(expression1.accept(*this, std::ref(expression2.getBaseExpression())));
}
diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h
index ef556d827..2c255b5c2 100644
--- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h
+++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.h
@@ -9,7 +9,7 @@ namespace storm {
class SyntacticalEqualityCheckVisitor : public ExpressionVisitor {
public:
- bool isSyntaticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2);
+ bool isSyntacticallyEqual(storm::expressions::Expression const& expression1, storm::expressions::Expression const& expression2);
virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
diff --git a/src/storm/utility/exprtk.h b/src/storm/utility/exprtk.h
new file mode 100644
index 000000000..3aba1b8db
--- /dev/null
+++ b/src/storm/utility/exprtk.h
@@ -0,0 +1,11 @@
+#pragma once
+
+#pragma clang diagnostic push
+#pragma clang diagnostic ignored "-Wunused-variable"
+
+#pragma GCC diagnostic push
+
+#include "exprtk.hpp"
+
+#pragma GCC diagnostic pop
+#pragma clang diagnostic pop