fixed some issues with meta variables in DDs

src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp

@@ -29,11 +29,7 @@ namespace storm {
                     ++counter;
                 }
                 
-                if (metaVariable.getType() == storm::dd::MetaVariableType::Bool) {
-                    newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), 3);
-                } else {
-                    newMetaVariables = ddManager.addMetaVariable(newMetaVariableName + std::to_string(counter), metaVariable.getLow(), metaVariable.getHigh(), 3);
-                }
+                newMetaVariables = ddManager.cloneVariable(metaVariablePair.first, newMetaVariableName + std::to_string(counter), 3);
                 
                 newRowVariables.insert(newMetaVariables[0]);
                 newColumnVariables.insert(newMetaVariables[1]);

src/storm/storage/dd/DdManager.cpp

@@ -7,6 +7,7 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidOperationException.h"
 
 #include "storm-config.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
@@ -75,7 +76,7 @@ namespace storm {
         Bdd<LibraryType> DdManager<LibraryType>::getEncoding(storm::expressions::Variable const& variable, int_fast64_t value, bool mostSignificantBitAtTop) const {
             DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
             
-            STORM_LOG_THROW(value >= metaVariable.getLow() && value <= metaVariable.getHigh(), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'.");
+            STORM_LOG_THROW(metaVariable.canRepresent(value), storm::exceptions::InvalidArgumentException, "Illegal value " << value << " for meta variable '" << variable.getName() << "'.");
             
             // Now compute the encoding relative to the low value of the meta variable.
             value -= metaVariable.getLow();
@@ -121,6 +122,7 @@ namespace storm {
         template<DdType LibraryType>
         Bdd<LibraryType> DdManager<LibraryType>::getRange(storm::expressions::Variable const& variable) const {
             storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
+            STORM_LOG_THROW(metaVariable.hasHigh(), storm::exceptions::InvalidOperationException, "Cannot create range for meta variable.");
             
             Bdd<LibraryType> result = this->getBddZero();
             
@@ -135,6 +137,7 @@ namespace storm {
         template<typename ValueType>
         Add<LibraryType, ValueType> DdManager<LibraryType>::getIdentity(storm::expressions::Variable const& variable) const {
             storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
+            STORM_LOG_THROW(metaVariable.hasHigh(), storm::exceptions::InvalidOperationException, "Cannot create identity for meta variable.");
             
             Add<LibraryType, ValueType> result = this->getAddZero<ValueType>();
             for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) {
@@ -158,6 +161,20 @@ namespace storm {
             return result;
         }
         
+        template<DdType LibraryType>
+        std::vector<storm::expressions::Variable> DdManager<LibraryType>::cloneVariable(storm::expressions::Variable const& variable, std::string const& newMetaVariableName, boost::optional<uint64_t> const& numberOfLayers) {
+            std::vector<storm::expressions::Variable> newMetaVariables;
+            auto const& ddMetaVariable = this->getMetaVariable(variable);
+            if (ddMetaVariable.getType() == storm::dd::MetaVariableType::Bool) {
+                newMetaVariables = this->addMetaVariable(newMetaVariableName, 3);
+            } else if (ddMetaVariable.getType() == storm::dd::MetaVariableType::Int) {
+                newMetaVariables = this->addMetaVariable(newMetaVariableName, ddMetaVariable.getLow(), ddMetaVariable.getHigh(), 3);
+            } else if (ddMetaVariable.getType() == storm::dd::MetaVariableType::BitVector) {
+                newMetaVariables = this->addBitVectorMetaVariable(newMetaVariableName, ddMetaVariable.getNumberOfDdVariables(), 3);
+            }
+            return newMetaVariables;
+        }
+        
         template<DdType LibraryType>
         std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
             std::vector<storm::expressions::Variable> result = addMetaVariable(name, low, high, 2, position);
@@ -166,87 +183,33 @@ namespace storm {
         
         template<DdType LibraryType>
         std::vector<storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, uint64_t numberOfLayers, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
-            // Check whether number of layers is legal.
-            STORM_LOG_THROW(numberOfLayers >= 1, storm::exceptions::InvalidArgumentException, "Layers must be at least 1.");
-            
-            // Check whether the variable name is legal.
-            STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
-            
-            // Check whether a meta variable already exists.
-            STORM_LOG_THROW(!this->hasMetaVariable(name), storm::exceptions::InvalidArgumentException, "A meta variable '" << name << "' already exists.");
-            
-            // Check that the range is legal.
-            STORM_LOG_THROW(high >= low, storm::exceptions::InvalidArgumentException, "Illegal empty range for meta variable.");
-            
-            std::size_t numberOfBits = static_cast<std::size_t>(std::ceil(std::log2(high - low + 1)));
-            
-            // If a specific position was requested, we compute it now.
-            boost::optional<uint_fast64_t> level;
-            if (position) {
-                storm::dd::DdMetaVariable<LibraryType> beforeVariable = this->getMetaVariable(position.get().second);
-                level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits<uint_fast64_t>::max() : std::numeric_limits<uint_fast64_t>::min();
-                for (auto const& ddVariable : beforeVariable.getDdVariables()) {
-                    level = position.get().first == MetaVariablePosition::Above ? std::min(level.get(), ddVariable.getLevel()) : std::max(level.get(), ddVariable.getLevel());
-                }
-                if (position.get().first == MetaVariablePosition::Below) {
-                    ++level.get();
-                }
-            }
-            
-            // For the case where low and high coincide, we need to have a single bit.
-            if (numberOfBits == 0) {
-                ++numberOfBits;
-            }
-            
-            STORM_LOG_TRACE("Creating meta variable with " << numberOfBits << " bit(s) and " << numberOfLayers << " layer(s).");
-            
-            std::stringstream tmp1;
-            std::vector<storm::expressions::Variable> result;
-            for (uint64 layer = 0; layer < numberOfLayers; ++layer) {
-                result.emplace_back(manager->declareBitVectorVariable(name + tmp1.str(), numberOfBits));
-                tmp1 << "'";
-            }
-            
-            std::vector<std::vector<Bdd<LibraryType>>> variables(numberOfLayers);
-            
-            for (std::size_t i = 0; i < numberOfBits; ++i) {
-                std::vector<InternalBdd<LibraryType>> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level);
-                for (uint64 layer = 0; layer < numberOfLayers; ++layer) {
-                    variables[layer].emplace_back(Bdd<LibraryType>(*this, ddVariables[layer], {result[layer]}));
-                }
-                
-                // If we are inserting the variable at a specific level, we need to prepare the level for the next pair
-                // of variables.
-                if (level) {
-                    level.get() += numberOfLayers;
-                }
-            }
-            
-            std::stringstream tmp2;
-            for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
-                metaVariableMap.emplace(result[layer], DdMetaVariable<LibraryType>(name + tmp2.str(), low, high, variables[layer]));
-                tmp2 << "'";
-            }
-            
-            return result;
+            return this->addMetaVariableHelper(MetaVariableType::Int, name, std::max(static_cast<uint64_t>(std::ceil(std::log2(high - low + 1))), 1ull), numberOfLayers, position, std::make_pair(low, high));
         }
         
         template<DdType LibraryType>
         std::vector<storm::expressions::Variable> DdManager<LibraryType>::addBitVectorMetaVariable(std::string const& variableName, uint64_t bits, uint64_t numberOfLayers, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
-            return this->addMetaVariable(variableName, 0, (1ull << bits) - 1, numberOfLayers, position);
+            return this->addMetaVariableHelper(MetaVariableType::BitVector, variableName, bits, numberOfLayers, position);
         }
         
         template<DdType LibraryType>
         std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
-            std::vector<storm::expressions::Variable> result = addMetaVariable(name, 2, position);
+            std::vector<storm::expressions::Variable> result = this->addMetaVariableHelper(MetaVariableType::Bool, name, 1, 2, position);
             return std::make_pair(result[0], result[1]);
         }
         
         template<DdType LibraryType>
         std::vector<storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name, uint64_t numberOfLayers, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
+            return this->addMetaVariableHelper(MetaVariableType::Bool, name, 1, numberOfLayers, position);
+        }
+        
+        template<DdType LibraryType>
+        std::vector<storm::expressions::Variable> DdManager<LibraryType>::addMetaVariableHelper(MetaVariableType const& type, std::string const& name, uint64_t numberOfDdVariables, uint64_t numberOfLayers, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position, boost::optional<std::pair<int_fast64_t, int_fast64_t>> const& bounds) {
             // Check whether number of layers is legal.
             STORM_LOG_THROW(numberOfLayers >= 1, storm::exceptions::InvalidArgumentException, "Layers must be at least 1.");
             
+            // Check that the number of DD variables is legal.
+            STORM_LOG_THROW(numberOfDdVariables >= 1, storm::exceptions::InvalidArgumentException, "Illegal number of DD variables.");
+            
             // Check whether the variable name is legal.
             STORM_LOG_THROW(name != "" && name.back() != '\'', storm::exceptions::InvalidArgumentException, "Illegal name of meta variable: '" << name << "'.");
             
@@ -256,7 +219,6 @@ namespace storm {
             // If a specific position was requested, we compute it now.
             boost::optional<uint_fast64_t> level;
             if (position) {
-                STORM_LOG_THROW(this->supportsOrderedInsertion(), storm::exceptions::NotSupportedException, "Cannot add meta variable at position, because the manager does not support ordered insertion.");
                 storm::dd::DdMetaVariable<LibraryType> beforeVariable = this->getMetaVariable(position.get().second);
                 level = position.get().first == MetaVariablePosition::Above ? std::numeric_limits<uint_fast64_t>::max() : std::numeric_limits<uint_fast64_t>::min();
                 for (auto const& ddVariable : beforeVariable.getDdVariables()) {
@@ -267,24 +229,42 @@ namespace storm {
                 }
             }
             
+            STORM_LOG_TRACE("Creating meta variable with " << numberOfDdVariables << " bit(s) and " << numberOfLayers << " layer(s).");
+            
             std::stringstream tmp1;
             std::vector<storm::expressions::Variable> result;
             for (uint64 layer = 0; layer < numberOfLayers; ++layer) {
-                result.emplace_back(manager->declareBooleanVariable(name + tmp1.str()));
+                if (type == MetaVariableType::Int) {
+                    result.emplace_back(manager->declareIntegerVariable(name + tmp1.str()));
+                } else if (type == MetaVariableType::Bool) {
+                    result.emplace_back(manager->declareBooleanVariable(name + tmp1.str()));
+                } else if (type == MetaVariableType::BitVector) {
+                    result.emplace_back(manager->declareBitVectorVariable(name + tmp1.str(), numberOfDdVariables));
+                }
                 tmp1 << "'";
             }
             
             std::vector<std::vector<Bdd<LibraryType>>> variables(numberOfLayers);
+            for (std::size_t i = 0; i < numberOfDdVariables; ++i) {
+                std::vector<InternalBdd<LibraryType>> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level);
+                for (uint64 layer = 0; layer < numberOfLayers; ++layer) {
+                    variables[layer].emplace_back(Bdd<LibraryType>(*this, ddVariables[layer], {result[layer]}));
+                }
                 
-            std::vector<InternalBdd<LibraryType>> ddVariables = internalDdManager.createDdVariables(numberOfLayers, level);
-            
-            for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
-                variables[layer].emplace_back(Bdd<LibraryType>(*this, ddVariables[layer], {result[layer]}));
+                // If we are inserting the variable at a specific level, we need to prepare the level for the next pair
+                // of variables.
+                if (level) {
+                    level.get() += numberOfLayers;
+                }
             }
             
             std::stringstream tmp2;
             for (uint64_t layer = 0; layer < numberOfLayers; ++layer) {
-                metaVariableMap.emplace(result[layer], DdMetaVariable<LibraryType>(name + tmp2.str(), variables[layer]));
+                if (bounds) {
+                    metaVariableMap.emplace(result[layer], DdMetaVariable<LibraryType>(name + tmp2.str(), bounds.get().first, bounds.get().second, variables[layer]));
+                } else {
+                    metaVariableMap.emplace(result[layer], DdMetaVariable<LibraryType>(type, name + tmp2.str(), variables[layer]));
+                }
                 tmp2 << "'";
             }
             

src/storm/storage/dd/DdManager.h

@@ -147,6 +147,15 @@ namespace storm {
              */
             Bdd<LibraryType> getCube(std::set<storm::expressions::Variable> const& variables) const;
 
+            /*!
+             * Clones the given meta variable and optionally changes the number of layers of the variable.
+             *
+             * @param variable The variable to clone.
+             * @param newVariableName The name of the variable to crate.
+             * @param numberOfLayers The number of layers of the variable to crate
+             */
+            std::vector<storm::expressions::Variable> cloneVariable(storm::expressions::Variable const& variable, std::string const& newVariableName, boost::optional<uint64_t> const& numberOfLayers = boost::none);
+            
             /*!
              * Adds an integer meta variable with the given range with two layers (a 'normal' and a 'primed' one).
              *
@@ -297,6 +306,15 @@ namespace storm {
             void debugCheck() const;
 
         private:
+            /*!
+             * Creates a meta variable with the given number of DD variables and layers.
+             *
+             * @param type The type of the meta variable to create.
+             * @param name The name of the variable.
+             * @param numberOfLayers The number of layers of this variable (must be greater or equal 1).
+             */
+            std::vector<storm::expressions::Variable> addMetaVariableHelper(MetaVariableType const& type, std::string const& name, uint64_t numberOfDdVariables, uint64_t numberOfLayers, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position = boost::none, boost::optional<std::pair<int_fast64_t, int_fast64_t>> const& bounds = boost::none);
+            
             /*!
              * Retrieves a list of names of the DD variables in the order of their index.
              *

src/storm/storage/dd/DdMetaVariable.cpp

@@ -10,7 +10,16 @@ namespace storm {
         }
         
         template<DdType LibraryType>
-        DdMetaVariable<LibraryType>::DdMetaVariable(std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(MetaVariableType::Bool), low(0), high(1), ddVariables(ddVariables) {
+        DdMetaVariable<LibraryType>::DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables) : name(name), type(type), low(0), ddVariables(ddVariables) {
+            STORM_LOG_ASSERT(type == MetaVariableType::Bool || type == MetaVariableType::BitVector, "Cannot create this type of meta variable in this constructor.");
+            if (ddVariables.size() < 63) {
+                this->high = (1ull << ddVariables.size()) - 1;
+            }
+            
+            // Correct type in the case of boolean variables.
+            if (ddVariables.size() == 1) {
+                this->type = MetaVariableType::Bool;
+            }
             this->createCube();
         }
         
@@ -31,7 +40,21 @@ namespace storm {
         
         template<DdType LibraryType>
         int_fast64_t DdMetaVariable<LibraryType>::getHigh() const {
-            return this->high;
+            return this->high.get();
+        }
+        
+        template<DdType LibraryType>
+        bool DdMetaVariable<LibraryType>::hasHigh() const {
+            return static_cast<bool>(this->high);
+        }
+        
+        template<DdType LibraryType>
+        bool DdMetaVariable<LibraryType>::canRepresent(int_fast64_t value) const {
+            bool result = value >= this->low;
+            if (result && high) {
+                return value <= this->high;
+            }
+            return false;
         }
         
         template<DdType LibraryType>

src/storm/storage/dd/DdMetaVariable.h

@@ -16,7 +16,7 @@ namespace storm {
         class Add;
 
         // An enumeration for all legal types of meta variables.
-        enum class MetaVariableType { Bool, Int };
+        enum class MetaVariableType { Bool, Int, BitVector };
         
         // Declare DdMetaVariable class so we can then specialize it for the different DD types.
         template<DdType LibraryType>
@@ -52,6 +52,13 @@ namespace storm {
              */
             int_fast64_t getLow() const;
             
+            /*!
+             * Retrieves whether the variable has an upper bound.
+             *
+             * @return True iff the variable has an upper bound.
+             */
+            bool hasHigh() const;
+            
             /*!
              * Retrieves the highest value of the range of the variable.
              *
@@ -59,6 +66,14 @@ namespace storm {
              */
             int_fast64_t getHigh() const;
 
+            /*!
+             * Retrieves whether the meta variable can represent the given value.
+             *
+             * @param value The value to check for legality.
+             * @return True iff the value is legal.
+             */
+            bool canRepresent(int_fast64_t value) const;
+            
             /*!
              * Retrieves the number of DD variables for this meta variable.
              *
@@ -102,11 +117,12 @@ namespace storm {
 
             /*!
              * Creates a boolean meta variable with the given name.
+             * @param type The type of the meta variable.
              * @param name The name of the meta variable.
              * @param ddVariables The vector of variables used to encode this variable.
              * @param manager A pointer to the manager that is responsible for this meta variable.
              */
-            DdMetaVariable(std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables);
+            DdMetaVariable(MetaVariableType const& type, std::string const& name, std::vector<Bdd<LibraryType>> const& ddVariables);
             
             /*!
              * Retrieves the variables used to encode the meta variable.
@@ -130,7 +146,7 @@ namespace storm {
             int_fast64_t low;
             
             // The highest value of the range of the variable.
-            int_fast64_t high;
+            boost::optional<int_fast64_t> high;
             
             // The vector of variables that are used to encode the meta variable.
             std::vector<Bdd<LibraryType>> ddVariables;

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@@ -291,7 +291,7 @@ namespace storm {
                     }
                 }
                 
-                void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t sourceStateEncodingIndex, storm::storage::BitVector& sourceStateEncoding, storm::storage::BitVector const& nondeterminismEncoding, uint64_t factor = 1) {
+                void extractTransitionMatrixRec(DdNode* transitionMatrixNode, DdNode* sourcePartitionNode, DdNode* targetPartitionNode, uint64_t sourceStateEncodingIndex, storm::storage::BitVector& sourceStateEncoding, storm::storage::BitVector const& nondeterminismEncoding, ValueType factor = 1) {
                     // For the empty DD, we do not need to add any entries. Note that the partition nodes cannot be zero
                     // as all states of the model have to be contained.
                     if (transitionMatrixNode == Cudd_ReadZero(ddman)) {
@@ -392,7 +392,7 @@ namespace storm {
                         if (!skippedInTargetPartition) {
                             extractTransitionMatrixRec(et, sourceE, targetT, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, factor);
                         }
-                        extractTransitionMatrixRec(ee, sourceE, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedInTargetPartition ? factor << 1 : factor);
+                        extractTransitionMatrixRec(ee, sourceE, targetE, sourceStateEncodingIndex + 1, sourceStateEncoding, nondeterminismEncoding, skippedInTargetPartition ? 2 * factor : factor);
                     }
                 }