several optimizations related to explicit model building

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

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.

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";
             }

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;

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.

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);
+        }
+        
+    }
+}

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.
+        };
+        
+    }
+}

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 {

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.

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;
+        }
+        
+    }
+}

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;
+        };
+        
+    }
+}

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>;

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> {

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())));
         }
         

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;

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