diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp new file mode 100644 index 000000000..62510a035 --- /dev/null +++ b/src/storage/dd/Add.cpp @@ -0,0 +1,8 @@ +#include "src/storage/dd/Add.h" + +namespace storm { + namespace dd { + + template class Add; + } +} \ No newline at end of file diff --git a/src/storage/dd/Add.h b/src/storage/dd/Add.h index 0c12fd586..68fda1a8f 100644 --- a/src/storage/dd/Add.h +++ b/src/storage/dd/Add.h @@ -6,8 +6,10 @@ namespace storm { namespace dd { - // Declare Add class so we can then specialize it for the different ADD types. - template class Add; + template + class Add { + + }; } } diff --git a/src/storage/dd/Bdd.cpp b/src/storage/dd/Bdd.cpp new file mode 100644 index 000000000..2bc04d168 --- /dev/null +++ b/src/storage/dd/Bdd.cpp @@ -0,0 +1,238 @@ +#include "src/storage/dd/Bdd.h" +#include "src/storage/dd/Add.h" +#include "src/storage/dd/Odd.h" + +#include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/dd/DdManager.h" + +#include "src/storage/BitVector.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace dd { + + template + Bdd::Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), internalBdd(internalBdd) { + // Intentionally left empty. + } + + template + Bdd::Bdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value) { + switch (comparisonType) { + case storm::logic::ComparisonType::Less: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::LessEqual: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::Greater: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::GreaterEqual: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal(), value, std::placeholders::_1)); + break; + } + + } + + template + bool Bdd::operator==(Bdd const& other) const { + return internalBdd == other.internalBdd; + } + + template + bool Bdd::operator!=(Bdd const& other) const { + return internalBdd != other.internalBdd; + } + + template + Bdd Bdd::ite(Bdd const& thenBdd, Bdd const& elseBdd) const { + std::set metaVariables = Dd::joinMetaVariables(*this, thenBdd); + metaVariables.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); + return Bdd(this->getDdManager(), internalBdd.ite(thenBdd.internalBdd, elseBdd.internalBdd), metaVariables); + } + + template + Bdd Bdd::operator||(Bdd const& other) const { + return Bdd(this->getDdManager(), internalBdd || other.internalBdd, Dd::joinMetaVariables(*this, other)); + } + + template + Bdd& Bdd::operator|=(Bdd const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + internalBdd |= other.internalBdd; + return *this; + } + + template + Bdd Bdd::operator&&(Bdd const& other) const { + return Bdd(this->getDdManager(), internalBdd && other.internalBdd, Dd::joinMetaVariables(*this, other)); + } + + template + Bdd& Bdd::operator&=(Bdd const& other) { + this->addMetaVariables(other.getContainedMetaVariables()); + internalBdd &= other.internalBdd; + return *this; + } + + template + Bdd Bdd::iff(Bdd const& other) const { + return Bdd(this->getDdManager(), internalBdd.iff(other.internalBdd), Dd::joinMetaVariables(*this, other)); + } + + template + Bdd Bdd::exclusiveOr(Bdd const& other) const { + return Bdd(this->getDdManager(), internalBdd.exclusiveOr(other.internalBdd), Dd::joinMetaVariables(*this, other)); + } + + template + Bdd Bdd::implies(Bdd const& other) const { + return Bdd(this->getDdManager(), internalBdd.implies(other.internalBdd), Dd::joinMetaVariables(*this, other)); + } + + template + Bdd Bdd::operator!() const { + return Bdd(this->getDdManager(), !internalBdd, this->getContainedMetaVariables()); + } + + template + Bdd& Bdd::complement() { + internalBdd.complement(); + return *this; + } + + template + Bdd Bdd::existsAbstract(std::set const& metaVariables) const { + Bdd cubeBdd = this->getDdManager()->getBddOne(); + + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the BDD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeBdd &= ddMetaVariable.getCube(); + } + + return Bdd(internalBdd.existsAbstract(cubeBdd)); + } + + template + Bdd Bdd::universalAbstract(std::set const& metaVariables) const { + InternalBdd cubeBdd = this->getDdManager()->getBddOne(); + + std::set newMetaVariables = this->getContainedMetaVariables(); + for (auto const& metaVariable : metaVariables) { + // First check whether the BDD contains the meta variable and erase it, if this is the case. + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); + newMetaVariables.erase(metaVariable); + + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeBdd &= ddMetaVariable.getCube(); + } + + return Bdd(internalBdd.universalAbstract(cubeBdd)); + } + + template + Bdd Bdd::andExists(Bdd const& other, std::set const& existentialVariables) const { + InternalBdd cubeBdd(this->getDdManager()->getBddOne()); + for (auto const& metaVariable : existentialVariables) { + DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); + cubeBdd &= ddMetaVariable.getCube(); + } + + std::set unionOfMetaVariables; + std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); + std::set containedMetaVariables; + std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); + + return Bdd(internalBdd.andExists(other.internalBdd, cubeBdd)); + } + + template + Bdd Bdd::constrain(Bdd const& constraint) const { + this->addMetaVariables(constraint.getContainedMetaVariables()); + return internalBdd.constraint(constraint.internalBdd); + } + + template + Bdd Bdd::restrict(Bdd const& constraint) const { + this->addMetaVariables(constraint.getContainedMetaVariables()); + return internalBdd.constraint(constraint.internalBdd); + } + + template + Bdd Bdd::swapVariables(std::vector> const& metaVariablePairs) const { + std::set newContainedMetaVariables; + std::vector const>, std::reference_wrapper const>>> fromTo; + for (auto const& metaVariablePair : metaVariablePairs) { + std::reference_wrapper const> variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); + std::reference_wrapper const> variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); + fromTo.push_back(std::make_pair(variable1, variable2)); + } + return Bdd(internalBdd.swapVariables(fromTo)); + } + + template + template + Add Bdd::toAdd() const { + return Add(internalBdd.template toAdd()); + } + + template + storm::storage::BitVector Bdd::toVector(storm::dd::Odd const& rowOdd) const { + return internalBdd.toVector(rowOdd); + } + + template + Bdd Bdd::getSupport() const { + return Bdd(internalBdd.getSupport()); + } + + template + uint_fast64_t Bdd::getNonZeroCount() const { + std::size_t numberOfDdVariables = 0; + for (auto const& metaVariable : this->getContainedMetaVariables()) { + numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); + } + return internalBdd.getNonZeroCount(numberOfDdVariables); + } + + template + uint_fast64_t Bdd::getLeafCount() const { + return internalBdd.getLeafCount(); + } + + template + uint_fast64_t Bdd::getNodeCount() const { + return internalBdd.getNodeCount(); + } + + template + uint_fast64_t Bdd::getIndex() const { + return internalBdd.getIndex(); + } + + template + bool Bdd::isOne() const { + return internalBdd.isOne(); + } + + template + bool Bdd::isZero() const { + return internalBdd.isZero(); + } + + template + void Bdd::exportToDot(std::string const& filename) const { + internalBdd.exportToDot(filename, this->getDdManager()->getDdVariableNames()); + } + + template class Bdd; + } +} \ No newline at end of file diff --git a/src/storage/dd/Bdd.h b/src/storage/dd/Bdd.h index 47c48474c..b116e95dd 100644 --- a/src/storage/dd/Bdd.h +++ b/src/storage/dd/Bdd.h @@ -4,10 +4,256 @@ #include "src/storage/dd/Dd.h" #include "src/storage/dd/DdType.h" +#include "src/storage/dd/cudd/InternalCuddBdd.h" + namespace storm { namespace dd { - // Declare Bdd class so we can then specialize it for the different BDD types. - template class Bdd; + template + class Add; + + template + class Bdd : public Dd { + public: + + // Instantiate all copy/move constructors/assignments with the default implementation. + Bdd() = default; + Bdd(Bdd const& other) = default; + Bdd& operator=(Bdd const& other) = default; + Bdd(Bdd&& other) = default; + Bdd& operator=(Bdd&& other) = default; + + /*! + * Retrieves whether the two BDDs represent the same function. + * + * @param other The BDD that is to be compared with the current one. + * @return True if the BDDs represent the same function. + */ + bool operator==(Bdd const& other) const; + + /*! + * Retrieves whether the two BDDs represent different functions. + * + * @param other The BDD that is to be compared with the current one. + * @return True if the BDDs represent the different functions. + */ + bool operator!=(Bdd const& other) const; + + /*! + * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero + * function value to the function values specified by the first DD and all others to the function values + * specified by the second DD. + * + * @param thenBdd The BDD defining the 'then' part. + * @param elseBdd The BDD defining the 'else' part. + * @return The resulting BDD. + */ + Bdd ite(Bdd const& thenBdd, Bdd const& elseBdd) const; + + /*! + * Performs a logical or of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical or of the operands. + */ + Bdd operator||(Bdd const& other) const; + + /*! + * Performs a logical or of the current and the given BDD and assigns it to the current BDD. + * + * @param other The second BDD used for the operation. + * @return A reference to the current BDD after the operation + */ + Bdd& operator|=(Bdd const& other); + + /*! + * Performs a logical and of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical and of the operands. + */ + Bdd operator&&(Bdd const& other) const; + + /*! + * Performs a logical and of the current and the given BDD and assigns it to the current BDD. + * + * @param other The second BDD used for the operation. + * @return A reference to the current BDD after the operation + */ + Bdd& operator&=(Bdd const& other); + + /*! + * Performs a logical iff of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical iff of the operands. + */ + Bdd iff(Bdd const& other) const; + + /*! + * Performs a logical exclusive-or of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical exclusive-or of the operands. + */ + Bdd exclusiveOr(Bdd const& other) const; + + /*! + * Performs a logical implication of the current and the given BDD. + * + * @param other The second BDD used for the operation. + * @return The logical implication of the operands. + */ + Bdd implies(Bdd const& other) const; + + /*! + * Logically inverts the current BDD. + * + * @return The resulting BDD. + */ + Bdd operator!() const; + + /*! + * Logically complements the current BDD. + * + * @return A reference to the current BDD after the operation. + */ + Bdd& complement(); + + /*! + * Existentially abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Bdd existsAbstract(std::set const& metaVariables) const; + + /*! + * Universally abstracts from the given meta variables. + * + * @param metaVariables The meta variables from which to abstract. + */ + Bdd universalAbstract(std::set const& metaVariables) const; + + /*! + * Computes the logical and of the current and the given BDD and existentially abstracts from the given set + * of variables. + * + * @param other The second BDD for the logical and. + * @param existentialVariables The variables from which to existentially abstract. + * @return A BDD representing the result. + */ + Bdd andExists(Bdd const& other, std::set const& existentialVariables) const; + + /*! + * Computes the constraint of the current BDD with the given constraint. That is, the function value of the + * resulting BDD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting BDD. + */ + Bdd constrain(Bdd const& constraint) const; + + /*! + * Computes the restriction of the current BDD with the given constraint. That is, the function value of the + * resulting DD will be the same as the current ones for all assignments mapping to one in the constraint + * and may be different otherwise. + * + * @param constraint The constraint to use for the operation. + * @return The resulting BDD. + */ + Bdd restrict(Bdd const& constraint) const; + + /*! + * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have + * the same number of underlying BDD variables. + * + * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. + * @return The resulting BDD. + */ + Bdd swapVariables(std::vector> const& metaVariablePairs) const; + + /*! + * Retrieves whether this DD represents the constant one function. + * + * @return True if this DD represents the constant one function. + */ + bool isOne() const; + + /*! + * Retrieves whether this DD represents the constant zero function. + * + * @return True if this DD represents the constant zero function. + */ + bool isZero() const; + + /*! + * Converts a BDD to an equivalent ADD. + * + * @return The corresponding ADD. + */ + template + Add toAdd() const; + + /*! + * Converts the BDD to a bit vector. The given offset-labeled DD is used to determine the correct row of + * each entry. + * + * @param rowOdd The ODD used for determining the correct row. + * @return The bit vector that is represented by this BDD. + */ + storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd) const; + + virtual Bdd getSupport() const override; + + virtual uint_fast64_t getNonZeroCount() const override; + + virtual uint_fast64_t getLeafCount() const override; + + virtual uint_fast64_t getNodeCount() const override; + + virtual uint_fast64_t getIndex() const override; + + virtual void exportToDot(std::string const& filename) const override; + + private: + /*! + * Creates a DD that encapsulates the given CUDD ADD. + * + * @param ddManager The manager responsible for this DD. + * @param cuddBdd The CUDD BDD to store. + * @param containedMetaVariables The meta variables that appear in the DD. + */ + Bdd(std::shared_ptr const> ddManager, InternalBdd const& internalBdd, std::set const& containedMetaVariables = std::set()); + + /*! + * Constructs a BDD representation of all encodings that are in the requested relation with the given value. + * + * @param ddManager The DD manager responsible for the resulting BDD. + * @param explicitValues The explicit values to compare to the given value. + * @param odd The ODD used for the translation from the explicit representation to a symbolic one. + * @param metaVariables The meta variables to use for the symbolic encoding. + * @param comparisonType The relation that needs to hold for the values (wrt. to the given value). + * @param value The value to compare with. + */ + Bdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); + + /*! + * Builds a BDD representing the values that make the given filter function evaluate to true. + * + * @param ddManager The manager responsible for the BDD. + * @param values The values that are to be checked against the filter function. + * @param odd The ODD used for the translation. + * @param metaVariables The meta variables used for the translation. + * @param filter The filter that evaluates whether an encoding is to be mapped to 0 or 1. + * @return The resulting (CUDD) BDD. + */ + template + static BDD fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter); + + + // The internal BDD that depends on the chosen library. + InternalBdd internalBdd; + }; } } diff --git a/src/storage/dd/Dd.cpp b/src/storage/dd/Dd.cpp new file mode 100644 index 000000000..5d0b32cef --- /dev/null +++ b/src/storage/dd/Dd.cpp @@ -0,0 +1,92 @@ +#include "src/storage/dd/Dd.h" + +#include + +#include "src/storage/dd/DdManager.h" + +namespace storm { + namespace dd { + template + Dd::Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) { + // Intentionally left empty. + } + + template + bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { + return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); + } + + template + bool Dd::containsMetaVariables(std::set const& metaVariables) const { + return std::includes(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end()); + } + + template + std::set const& Dd::getContainedMetaVariables() const { + return this->containedMetaVariables; + } + + template + std::set& Dd::getContainedMetaVariables() { + return this->containedMetaVariables; + } + + template + std::shared_ptr const> Dd::getDdManager() const { + return this->ddManager; + } + + template + void Dd::addMetaVariables(std::set const& metaVariables) { + std::set result; + std::set_union(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin())); + containedMetaVariables = std::move(result); + } + + template + void Dd::addMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().insert(metaVariable); + } + + template + void Dd::removeMetaVariable(storm::expressions::Variable const& metaVariable) { + this->getContainedMetaVariables().erase(metaVariable); + } + + template + void Dd::removeMetaVariables(std::set const& metaVariables) { + std::set result; + std::set_difference(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin())); + containedMetaVariables = std::move(result); + } + + template + std::vector Dd::getSortedVariableIndices() const { + return getSortedVariableIndices(*this->getDdManager(), this->getContainedMetaVariables()); + } + + template + std::vector Dd::getSortedVariableIndices(DdManager const& manager, std::set const& metaVariables) { + std::vector ddVariableIndices; + for (auto const& metaVariableName : metaVariables) { + auto const& metaVariable = manager.getMetaVariable(metaVariableName); + for (auto const& ddVariable : metaVariable.getDdVariables()) { + ddVariableIndices.push_back(ddVariable.getIndex()); + } + } + + // Next, we need to sort them, since they may be arbitrarily ordered otherwise. + std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); + return ddVariableIndices; + } + + template + std::set Dd::joinMetaVariables(storm::dd::Dd const& first, storm::dd::Dd const& second) { + std::set metaVariables; + std::set_union(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); + return metaVariables; + } + + template class Dd; + } +} \ No newline at end of file diff --git a/src/storage/dd/Dd.h b/src/storage/dd/Dd.h index bc7075f46..7d007153d 100644 --- a/src/storage/dd/Dd.h +++ b/src/storage/dd/Dd.h @@ -1,12 +1,180 @@ #ifndef STORM_STORAGE_DD_DD_H_ #define STORM_STORAGE_DD_DD_H_ +#include +#include +#include + #include "src/storage/dd/DdType.h" +#include "src/storage/expressions/Variable.h" namespace storm { namespace dd { - // Declare Dd class so we can then specialize it for the different DD types. - template class Dd; + // Forward-declare some classes. + template class DdManager; + template class Bdd; + + template + class Dd { + public: + // Declare the DdManager so it can access the internals of a DD. + friend class DdManager; + + // Instantiate all copy/move constructors/assignments with the default implementation. + Dd() = default; + Dd(Dd const& other) = default; + Dd& operator=(Dd const& other) = default; + Dd(Dd&& other) = default; + Dd& operator=(Dd&& other) = default; + + /*! + * Retrieves the support of the current DD. + * + * @return The support represented as a BDD. + */ + virtual Bdd getSupport() const = 0; + + /*! + * Retrieves the number of encodings that are mapped to a non-zero value. + * + * @return The number of encodings that are mapped to a non-zero value. + */ + virtual uint_fast64_t getNonZeroCount() const = 0; + + /*! + * Retrieves the number of leaves of the DD. + * + * @return The number of leaves of the DD. + */ + virtual uint_fast64_t getLeafCount() const = 0; + + /*! + * Retrieves the number of nodes necessary to represent the DD. + * + * @return The number of nodes in this DD. + */ + virtual uint_fast64_t getNodeCount() const = 0; + + /*! + * Retrieves the index of the topmost variable in the DD. + * + * @return The index of the topmost variable in DD. + */ + virtual uint_fast64_t getIndex() const = 0; + + /*! + * Retrieves whether the given meta variable is contained in the DD. + * + * @param metaVariable The meta variable for which to query membership. + * @return True iff the meta variable is contained in the DD. + */ + bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const; + + /*! + * Retrieves whether the given meta variables are all contained in the DD. + * + * @param metaVariables The meta variables for which to query membership. + * @return True iff all meta variables are contained in the DD. + */ + bool containsMetaVariables(std::set const& metaVariables) const; + + /*! + * Retrieves the set of all meta variables contained in the DD. + * + * @return The set of all meta variables contained in the DD. + */ + std::set const& getContainedMetaVariables() const; + + /*! + * Exports the DD to the given file in the dot format. + * + * @param filename The name of the file to which the DD is to be exported. + */ + virtual void exportToDot(std::string const& filename) const = 0; + + /*! + * Retrieves the manager that is responsible for this DD. + * + * A pointer to the manager that is responsible for this DD. + */ + std::shared_ptr const> getDdManager() const; + + /*! + * Retrieves the set of all meta variables contained in the DD. + * + * @return The set of all meta variables contained in the DD. + */ + std::set& getContainedMetaVariables(); + + protected: + /*! + * Retrieves the (sorted) list of the variable indices of DD variables contained in this DD. + * + * @return The sorted list of variable indices. + */ + std::vector getSortedVariableIndices() const; + + /*! + * Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set. + * + * @param manager The manager responsible for the DD. + * @param metaVariable The set of meta variables for which to retrieve the index list. + * @return The sorted list of variable indices. + */ + static std::vector getSortedVariableIndices(DdManager const& manager, std::set const& metaVariables); + + /*! + * Adds the given set of meta variables to the DD. + * + * @param metaVariables The set of meta variables to add. + */ + void addMetaVariables(std::set const& metaVariables); + + /*! + * Adds the given meta variable to the set of meta variables that are contained in this DD. + * + * @param metaVariable The name of the meta variable to add. + */ + void addMetaVariable(storm::expressions::Variable const& metaVariable); + + /*! + * Removes the given meta variable to the set of meta variables that are contained in this DD. + * + * @param metaVariable The name of the meta variable to remove. + */ + void removeMetaVariable(storm::expressions::Variable const& metaVariable); + + /*! + * Removes the given set of meta variables from the DD. + * + * @param metaVariables The set of meta variables to remove. + */ + void removeMetaVariables(std::set const& metaVariables); + + /*! + * Creates a DD with the given manager and meta variables. + * + * @param ddManager The manager responsible for this DD. + * @param containedMetaVariables The meta variables that appear in the DD. + */ + Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables = std::set()); + + /*! + * Retrieves the set of meta variables contained in both DDs. + * + * @param first The first DD. + * @param second The second DD. + * @return The set of all contained meta variables. + */ + static std::set joinMetaVariables(storm::dd::Dd const& first, storm::dd::Dd const& second); + + private: + // A pointer to the manager responsible for this DD. + std::shared_ptr const> ddManager; + + // The meta variables that appear in this DD. + std::set containedMetaVariables; + }; } } diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h index 53fde64bb..3c1d5e70c 100644 --- a/src/storage/dd/DdManager.h +++ b/src/storage/dd/DdManager.h @@ -2,11 +2,19 @@ #define STORM_STORAGE_DD_DDMANAGER_H_ #include "src/storage/dd/DdType.h" +#include "src/storage/dd/DdMetaVariable.h" +#include "src/storage/expressions/Variable.h" namespace storm { namespace dd { // Declare DdManager class so we can then specialize it for the different DD types. - template class DdManager; + template + class DdManager { + public: + Bdd getBddOne() const; + Bdd getBddZero() const; + DdMetaVariable const& getMetaVariable(storm::expressions::Variable const& variable) const; + }; } } diff --git a/src/storage/dd/DdMetaVariable.h b/src/storage/dd/DdMetaVariable.h index b85b23c1c..555569774 100644 --- a/src/storage/dd/DdMetaVariable.h +++ b/src/storage/dd/DdMetaVariable.h @@ -6,7 +6,11 @@ namespace storm { namespace dd { // Declare DdMetaVariable class so we can then specialize it for the different DD types. - template class DdMetaVariable; + template + class DdMetaVariable { + public: + InternalBdd getCube() const; + }; } } diff --git a/src/storage/dd/DdType.h b/src/storage/dd/DdType.h index feb2fe70a..d23933eed 100644 --- a/src/storage/dd/DdType.h +++ b/src/storage/dd/DdType.h @@ -4,7 +4,8 @@ namespace storm { namespace dd { enum class DdType { - CUDD + CUDD, + Sylvan }; } } diff --git a/src/storage/dd/InternalAdd.h b/src/storage/dd/InternalAdd.h new file mode 100644 index 000000000..1c69b41ec --- /dev/null +++ b/src/storage/dd/InternalAdd.h @@ -0,0 +1,14 @@ +#ifndef STORM_STORAGE_DD_INTERNALADD_H_ +#define STORM_STORAGE_DD_INTERNALADD_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + template + class InternalAdd; + } +} + + +#endif /* STORM_STORAGE_DD_INTERNALADD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/InternalBdd.h b/src/storage/dd/InternalBdd.h new file mode 100644 index 000000000..093008a85 --- /dev/null +++ b/src/storage/dd/InternalBdd.h @@ -0,0 +1,14 @@ +#ifndef STORM_STORAGE_DD_INTERNALBDD_H_ +#define STORM_STORAGE_DD_INTERNALBDD_H_ + +#include "src/storage/dd/DdType.h" + +namespace storm { + namespace dd { + template + class InternalBdd; + } +} + + +#endif /* STORM_STORAGE_DD_CUDD_INTERNALBDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/Odd.cpp b/src/storage/dd/Odd.cpp new file mode 100644 index 000000000..e69de29bb diff --git a/src/storage/dd/Odd.h b/src/storage/dd/Odd.h index 6a7231300..21e5fcc90 100644 --- a/src/storage/dd/Odd.h +++ b/src/storage/dd/Odd.h @@ -5,8 +5,10 @@ namespace storm { namespace dd { - // Declare Odd class so we can then specialize it for the different DD types. - template class Odd; + template + class Odd { + + }; } } diff --git a/src/storage/dd/cudd/CuddBdd.cpp b/src/storage/dd/cudd/CuddBdd.cpp deleted file mode 100644 index 0e0acb99f..000000000 --- a/src/storage/dd/cudd/CuddBdd.cpp +++ /dev/null @@ -1,384 +0,0 @@ -#include -#include -#include - -#include "src/storage/dd/cudd/CuddAdd.h" -#include "src/storage/dd/cudd/CuddBdd.h" -#include "src/storage/dd/cudd/CuddOdd.h" -#include "src/storage/dd/cudd/CuddDdManager.h" - -#include "src/storage/BitVector.h" - -#include "src/logic/ComparisonType.h" - -#include "src/utility/macros.h" -#include "src/exceptions/InvalidArgumentException.h" - -namespace storm { - namespace dd { - Bdd::Bdd(std::shared_ptr const> ddManager, BDD cuddBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), cuddBdd(cuddBdd) { - // Intentionally left empty. - } - - Bdd::Bdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd(ddManager, metaVariables) { - switch (comparisonType) { - case storm::logic::ComparisonType::Less: - this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater(), value, std::placeholders::_1)); - break; - case storm::logic::ComparisonType::LessEqual: - this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal(), value, std::placeholders::_1)); - break; - case storm::logic::ComparisonType::Greater: - this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less(), value, std::placeholders::_1)); - break; - case storm::logic::ComparisonType::GreaterEqual: - this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal(), value, std::placeholders::_1)); - break; - } - - } - - Add Bdd::toAdd() const { - return Add(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables()); - } - - BDD Bdd::getCuddBdd() const { - return this->cuddBdd; - } - - DdNode* Bdd::getCuddDdNode() const { - return this->getCuddBdd().getNode(); - } - - bool Bdd::operator==(Bdd const& other) const { - return this->getCuddBdd() == other.getCuddBdd(); - } - - bool Bdd::operator!=(Bdd const& other) const { - return !(*this == other); - } - - Bdd Bdd::ite(Bdd const& thenDd, Bdd const& elseDd) const { - std::set metaVariableNames; - std::set_union(thenDd.getContainedMetaVariables().begin(), thenDd.getContainedMetaVariables().end(), elseDd.getContainedMetaVariables().begin(), elseDd.getContainedMetaVariables().end(), std::inserter(metaVariableNames, metaVariableNames.begin())); - metaVariableNames.insert(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end()); - - return Bdd(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames); - } - - Bdd Bdd::operator!() const { - Bdd result(*this); - result.complement(); - return result; - } - - Bdd& Bdd::complement() { - this->cuddBdd = ~this->getCuddBdd(); - return *this; - } - - Bdd Bdd::operator&&(Bdd const& other) const { - Bdd result(*this); - result &= other; - return result; - } - - Bdd& Bdd::operator&=(Bdd const& other) { - this->addMetaVariables(other.getContainedMetaVariables()); - this->cuddBdd = this->getCuddBdd() & other.getCuddBdd(); - return *this; - } - - Bdd Bdd::operator||(Bdd const& other) const { - Bdd result(*this); - result |= other; - return result; - } - - Bdd& Bdd::operator|=(Bdd const& other) { - this->addMetaVariables(other.getContainedMetaVariables()); - this->cuddBdd = this->getCuddBdd() | other.getCuddBdd(); - return *this; - } - - Bdd Bdd::iff(Bdd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Bdd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); - } - - Bdd Bdd::exclusiveOr(Bdd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Bdd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); - } - - Bdd Bdd::implies(Bdd const& other) const { - std::set metaVariables(this->getContainedMetaVariables()); - metaVariables.insert(other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end()); - return Bdd(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables); - } - - Bdd Bdd::existsAbstract(std::set const& metaVariables) const { - Bdd cubeBdd = this->getDdManager()->getBddOne(); - - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the BDD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeBdd &= ddMetaVariable.getCube(); - } - - return Bdd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cubeBdd.getCuddBdd()), newMetaVariables); - } - - Bdd Bdd::universalAbstract(std::set const& metaVariables) const { - Bdd cubeBdd = this->getDdManager()->getBddOne(); - - std::set newMetaVariables = this->getContainedMetaVariables(); - for (auto const& metaVariable : metaVariables) { - // First check whether the BDD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); - newMetaVariables.erase(metaVariable); - - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeBdd &= ddMetaVariable.getCube(); - } - - return Bdd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cubeBdd.getCuddBdd()), newMetaVariables); - } - - Bdd Bdd::swapVariables(std::vector> const& metaVariablePairs) const { - std::set newContainedMetaVariables; - std::vector from; - std::vector to; - for (auto const& metaVariablePair : metaVariablePairs) { - DdMetaVariable const& variable1 = this->getDdManager()->getMetaVariable(metaVariablePair.first); - DdMetaVariable const& variable2 = this->getDdManager()->getMetaVariable(metaVariablePair.second); - - // Check if it's legal so swap the meta variables. - STORM_LOG_THROW(variable1.getNumberOfDdVariables() == variable2.getNumberOfDdVariables(), storm::exceptions::InvalidArgumentException, "Unable to swap meta variables with different size."); - - // Keep track of the contained meta variables in the DD. - if (this->containsMetaVariable(metaVariablePair.first)) { - newContainedMetaVariables.insert(metaVariablePair.second); - } - if (this->containsMetaVariable(metaVariablePair.second)) { - newContainedMetaVariables.insert(metaVariablePair.first); - } - - // Add the variables to swap to the corresponding vectors. - for (auto const& ddVariable : variable1.getDdVariables()) { - from.push_back(ddVariable.getCuddBdd()); - } - for (auto const& ddVariable : variable2.getDdVariables()) { - to.push_back(ddVariable.getCuddBdd()); - } - } - - // Finally, call CUDD to swap the variables. - return Bdd(this->getDdManager(), this->getCuddBdd().SwapVariables(from, to), newContainedMetaVariables); - } - - Bdd Bdd::andExists(Bdd const& other, std::set const& existentialVariables) const { - Bdd cubeBdd(this->getDdManager()->getBddOne()); - for (auto const& metaVariable : existentialVariables) { - DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); - cubeBdd &= ddMetaVariable.getCube(); - } - - std::set unionOfMetaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), other.getContainedMetaVariables().begin(), other.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin())); - std::set containedMetaVariables; - std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), existentialVariables.begin(), existentialVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin())); - - return Bdd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cubeBdd.getCuddBdd()), containedMetaVariables); - } - - Bdd Bdd::constrain(Bdd const& constraint) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Bdd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); - } - - Bdd Bdd::restrict(Bdd const& constraint) const { - std::set metaVariables; - std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), constraint.getContainedMetaVariables().begin(), constraint.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin())); - return Bdd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); - } - - Bdd Bdd::getSupport() const { - return Bdd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); - } - - uint_fast64_t Bdd::getNonZeroCount() const { - std::size_t numberOfDdVariables = 0; - for (auto const& metaVariable : this->getContainedMetaVariables()) { - numberOfDdVariables += this->getDdManager()->getMetaVariable(metaVariable).getNumberOfDdVariables(); - } - return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); - } - - uint_fast64_t Bdd::getLeafCount() const { - return static_cast(this->getCuddBdd().CountLeaves()); - } - - uint_fast64_t Bdd::getNodeCount() const { - return static_cast(this->getCuddBdd().nodeCount()); - } - - bool Bdd::isOne() const { - return this->getCuddBdd().IsOne(); - } - - bool Bdd::isZero() const { - return this->getCuddBdd().IsZero(); - } - - uint_fast64_t Bdd::getIndex() const { - return static_cast(this->getCuddBdd().NodeReadIndex()); - } - - void Bdd::exportToDot(std::string const& filename) const { - if (filename.empty()) { - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector); - } else { - // Build the name input of the DD. - std::vector ddNames; - std::string ddName("f"); - ddNames.push_back(new char[ddName.size() + 1]); - std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); - - // Now build the variables names. - std::vector ddVariableNamesAsStrings = this->getDdManager()->getDdVariableNames(); - std::vector ddVariableNames; - for (auto const& element : ddVariableNamesAsStrings) { - ddVariableNames.push_back(new char[element.size() + 1]); - std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); - } - - // Open the file, dump the DD and close it again. - FILE* filePointer = fopen(filename.c_str() , "w"); - std::vector cuddBddVector = { this->getCuddBdd() }; - this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); - fclose(filePointer); - - // Finally, delete the names. - for (char* element : ddNames) { - delete element; - } - for (char* element : ddVariableNames) { - delete element; - } - } - } - - template - BDD Bdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { - std::vector ddVariableIndices = getSortedVariableIndices(*ddManager, metaVariables); - uint_fast64_t offset = 0; - return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter)); - } - - template - DdNode* Bdd::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices, std::function const& filter) { - if (currentLevel == maxLevel) { - // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one - // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we - // need to copy the next value of the vector iff the then-offset is greater than zero. - if (odd.getThenOffset() > 0) { - if (filter(values[currentOffset++])) { - return Cudd_ReadOne(manager); - } else { - return Cudd_ReadLogicZero(manager); - } - } else { - return Cudd_ReadZero(manager); - } - } else { - // If the total offset is zero, we can just return the constant zero DD. - if (odd.getThenOffset() + odd.getElseOffset() == 0) { - return Cudd_ReadZero(manager); - } - - // Determine the new else-successor. - DdNode* elseSuccessor = nullptr; - if (odd.getElseOffset() > 0) { - elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices, filter); - } else { - elseSuccessor = Cudd_ReadLogicZero(manager); - } - Cudd_Ref(elseSuccessor); - - // Determine the new then-successor. - DdNode* thenSuccessor = nullptr; - if (odd.getThenOffset() > 0) { - thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices, filter); - } else { - thenSuccessor = Cudd_ReadLogicZero(manager); - } - Cudd_Ref(thenSuccessor); - - // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor); - DdNode* result = Cudd_bddIthVar(manager, static_cast(ddVariableIndices[currentLevel])); - Cudd_Ref(result); - DdNode* newResult = Cudd_bddIte(manager, result, thenSuccessor, elseSuccessor); - Cudd_Ref(newResult); - - // Dispose of the intermediate results - Cudd_RecursiveDeref(manager, result); - Cudd_RecursiveDeref(manager, thenSuccessor); - Cudd_RecursiveDeref(manager, elseSuccessor); - - // Before returning, we remove the protection imposed by the previous call to Cudd_Ref. - Cudd_Deref(newResult); - - return newResult; - } - } - - storm::storage::BitVector Bdd::toVector(storm::dd::Odd const& rowOdd) const { - std::vector ddVariableIndices = this->getSortedVariableIndices(); - storm::storage::BitVector result(rowOdd.getTotalOffset()); - this->toVectorRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices); - return result; - } - - void Bdd::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { - // If there are no more values to select, we can directly return. - if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) { - return; - } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) { - return; - } - - // If we are at the maximal level, the value to be set is stored as a constant in the DD. - if (currentRowLevel == maxLevel) { - result.set(currentRowOffset, true); - } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { - toVectorRec(dd, manager, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); - toVectorRec(dd, manager, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); - } else { - // Otherwise, we compute the ODDs for both the then- and else successors. - DdNode* elseDdNode = Cudd_E(dd); - DdNode* thenDdNode = Cudd_T(dd); - - // Determine whether we have to evaluate the successors as if they were complemented. - bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement; - bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement; - - toVectorRec(Cudd_Regular(elseDdNode), manager, result, rowOdd.getElseSuccessor(), elseComplemented, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); - toVectorRec(Cudd_Regular(thenDdNode), manager, result, rowOdd.getThenSuccessor(), thenComplemented, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); - } - } - - std::ostream& operator<<(std::ostream& out, const Bdd& bdd) { - bdd.exportToDot(); - return out; - } - } -} \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDd.cpp b/src/storage/dd/cudd/CuddDd.cpp deleted file mode 100644 index 1bf3d3d08..000000000 --- a/src/storage/dd/cudd/CuddDd.cpp +++ /dev/null @@ -1,70 +0,0 @@ -#include - -#include "src/storage/dd/cudd/CuddDd.h" -#include "src/storage/dd/cudd/CuddDdManager.h" - -namespace storm { - namespace dd { - Dd::Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables) : ddManager(ddManager), containedMetaVariables(containedMetaVariables) { - // Intentionally left empty. - } - - bool Dd::containsMetaVariable(storm::expressions::Variable const& metaVariable) const { - return containedMetaVariables.find(metaVariable) != containedMetaVariables.end(); - } - - bool Dd::containsMetaVariables(std::set const& metaVariables) const { - return std::includes(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end()); - } - - std::set const& Dd::getContainedMetaVariables() const { - return this->containedMetaVariables; - } - - std::set& Dd::getContainedMetaVariables() { - return this->containedMetaVariables; - } - - std::shared_ptr const> Dd::getDdManager() const { - return this->ddManager; - } - - void Dd::addMetaVariables(std::set const& metaVariables) { - std::set result; - std::set_union(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin())); - containedMetaVariables = std::move(result); - } - - void Dd::addMetaVariable(storm::expressions::Variable const& metaVariable) { - this->getContainedMetaVariables().insert(metaVariable); - } - - void Dd::removeMetaVariable(storm::expressions::Variable const& metaVariable) { - this->getContainedMetaVariables().erase(metaVariable); - } - - void Dd::removeMetaVariables(std::set const& metaVariables) { - std::set result; - std::set_difference(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin())); - containedMetaVariables = std::move(result); - } - - std::vector Dd::getSortedVariableIndices() const { - return getSortedVariableIndices(*this->getDdManager(), this->getContainedMetaVariables()); - } - - std::vector Dd::getSortedVariableIndices(DdManager const& manager, std::set const& metaVariables) { - std::vector ddVariableIndices; - for (auto const& metaVariableName : metaVariables) { - auto const& metaVariable = manager.getMetaVariable(metaVariableName); - for (auto const& ddVariable : metaVariable.getDdVariables()) { - ddVariableIndices.push_back(ddVariable.getIndex()); - } - } - - // Next, we need to sort them, since they may be arbitrarily ordered otherwise. - std::sort(ddVariableIndices.begin(), ddVariableIndices.end()); - return ddVariableIndices; - } - } -} \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddDd.h b/src/storage/dd/cudd/CuddDd.h deleted file mode 100644 index 0077bcc8a..000000000 --- a/src/storage/dd/cudd/CuddDd.h +++ /dev/null @@ -1,182 +0,0 @@ -#ifndef STORM_STORAGE_DD_CUDDDD_H_ -#define STORM_STORAGE_DD_CUDDDD_H_ - -#include -#include - -#include "src/storage/dd/Dd.h" -#include "src/storage/expressions/Variable.h" -#include "src/utility/OsDetection.h" - -// Include the C++-interface of CUDD. -#include "cuddObj.hh" - -namespace storm { - namespace dd { - // Forward-declare some classes. - template class DdManager; - template class Odd; - template class Bdd; - - template<> - class Dd { - public: - // Declare the DdManager so it can access the internals of a DD. - friend class DdManager; - - // Instantiate all copy/move constructors/assignments with the default implementation. - Dd() = default; - Dd(Dd const& other) = default; - Dd& operator=(Dd const& other) = default; -#ifndef WINDOWS - Dd(Dd&& other) = default; - Dd& operator=(Dd&& other) = default; -#endif - - /*! - * Retrieves the support of the current DD. - * - * @return The support represented as a BDD. - */ - virtual Bdd getSupport() const = 0; - - /*! - * Retrieves the number of encodings that are mapped to a non-zero value. - * - * @return The number of encodings that are mapped to a non-zero value. - */ - virtual uint_fast64_t getNonZeroCount() const = 0; - - /*! - * Retrieves the number of leaves of the DD. - * - * @return The number of leaves of the DD. - */ - virtual uint_fast64_t getLeafCount() const = 0; - - /*! - * Retrieves the number of nodes necessary to represent the DD. - * - * @return The number of nodes in this DD. - */ - virtual uint_fast64_t getNodeCount() const = 0; - - /*! - * Retrieves the index of the topmost variable in the DD. - * - * @return The index of the topmost variable in DD. - */ - virtual uint_fast64_t getIndex() const = 0; - - /*! - * Retrieves whether the given meta variable is contained in the DD. - * - * @param metaVariable The meta variable for which to query membership. - * @return True iff the meta variable is contained in the DD. - */ - bool containsMetaVariable(storm::expressions::Variable const& metaVariable) const; - - /*! - * Retrieves whether the given meta variables are all contained in the DD. - * - * @param metaVariables The meta variables for which to query membership. - * @return True iff all meta variables are contained in the DD. - */ - bool containsMetaVariables(std::set const& metaVariables) const; - - /*! - * Retrieves the set of all meta variables contained in the DD. - * - * @return The set of all meta variables contained in the DD. - */ - std::set const& getContainedMetaVariables() const; - - /*! - * Exports the DD to the given file in the dot format. - * - * @param filename The name of the file to which the DD is to be exported. - */ - virtual void exportToDot(std::string const& filename = "") const = 0; - - /*! - * Retrieves the manager that is responsible for this DD. - * - * A pointer to the manager that is responsible for this DD. - */ - std::shared_ptr const> getDdManager() const; - - /*! - * Retrieves the set of all meta variables contained in the DD. - * - * @return The set of all meta variables contained in the DD. - */ - std::set& getContainedMetaVariables(); - - protected: - - /*! - * Retrieves the (sorted) list of the variable indices of DD variables contained in this DD. - * - * @return The sorted list of variable indices. - */ - std::vector getSortedVariableIndices() const; - - /*! - * Retrieves the (sorted) list of the variable indices of the DD variables given by the meta variable set. - * - * @param manager The manager responsible for the DD. - * @param metaVariable The set of meta variables for which to retrieve the index list. - * @return The sorted list of variable indices. - */ - static std::vector getSortedVariableIndices(DdManager const& manager, std::set const& metaVariables); - - /*! - * Adds the given set of meta variables to the DD. - * - * @param metaVariables The set of meta variables to add. - */ - void addMetaVariables(std::set const& metaVariables); - - /*! - * Adds the given meta variable to the set of meta variables that are contained in this DD. - * - * @param metaVariable The name of the meta variable to add. - */ - void addMetaVariable(storm::expressions::Variable const& metaVariable); - - /*! - * Removes the given meta variable to the set of meta variables that are contained in this DD. - * - * @param metaVariable The name of the meta variable to remove. - */ - void removeMetaVariable(storm::expressions::Variable const& metaVariable); - - /*! - * Removes the given set of meta variables from the DD. - * - * @param metaVariables The set of meta variables to remove. - */ - void removeMetaVariables(std::set const& metaVariables); - - protected: - - /*! - * Creates a DD with the given manager and meta variables. - * - * @param ddManager The manager responsible for this DD. - * @param containedMetaVariables The meta variables that appear in the DD. - */ - Dd(std::shared_ptr const> ddManager, std::set const& containedMetaVariables = std::set()); - - private: - - // A pointer to the manager responsible for this DD. - std::shared_ptr const> ddManager; - - // The meta variables that appear in this DD. - std::set containedMetaVariables; - }; - } -} - -#endif /* STORM_STORAGE_DD_CUDDDD_H_ */ \ No newline at end of file diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp new file mode 100644 index 000000000..52db5fab3 --- /dev/null +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -0,0 +1,316 @@ +#include "src/storage/dd/cudd/InternalCuddBdd.h" + +namespace storm { + namespace dd { + bool InternalBdd::operator==(InternalBdd const& other) const { + return this->getCuddBdd() == other.getCuddBdd(); + } + + bool InternalBdd::operator!=(InternalBdd const& other) const { + return !(*this == other); + } + + InternalBdd InternalBdd::ite(InternalBdd const& thenDd, InternalBdd const& elseDd) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().Ite(thenDd.getCuddBdd(), elseDd.getCuddBdd()), metaVariableNames); + } + + InternalBdd InternalBdd::operator||(InternalBdd const& other) const { + InternalBdd result(*this); + result |= other; + return result; + } + + InternalBdd& InternalBdd::operator|=(InternalBdd const& other) { + this->cuddBdd = this->getCuddBdd() | other.getCuddBdd(); + return *this; + } + + InternalBdd InternalBdd::operator&&(InternalBdd const& other) const { + InternalBdd result(*this); + result &= other; + return result; + } + + InternalBdd& InternalBdd::operator&=(InternalBdd const& other) { + this->cuddBdd = this->getCuddBdd() & other.getCuddBdd(); + return *this; + } + + InternalBdd InternalBdd::iff(InternalBdd const& other) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().Xnor(other.getCuddBdd()), metaVariables); + } + + InternalBdd InternalBdd::exclusiveOr(InternalBdd const& other) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().Xor(other.getCuddBdd()), metaVariables); + } + + InternalBdd InternalBdd::implies(InternalBdd const& other) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().Ite(other.getCuddBdd(), this->getDdManager()->getBddOne().getCuddBdd()), metaVariables); + } + + InternalBdd InternalBdd::operator!() const { + InternalBdd result(*this); + result.complement(); + return result; + } + + InternalBdd& InternalBdd::complement() { + this->cuddBdd = ~this->getCuddBdd(); + return *this; + } + + InternalBdd InternalBdd::existsAbstract(InternalBdd const& cube) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().ExistAbstract(cube.getCuddBdd()), newMetaVariables); + } + + InternalBdd InternalBdd::universalAbstract(InternalBdd const& cube) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().UnivAbstract(cube.getCuddBdd()), newMetaVariables); + } + + InternalBdd InternalBdd::andExists(InternalBdd const& other, InternalBdd const& cube) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().AndAbstract(other.getCuddBdd(), cube.getCuddBdd()), containedMetaVariables); + } + + InternalBdd InternalBdd::constrain(InternalBdd const& constraint) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().Constrain(constraint.getCuddBdd()), metaVariables); + } + + InternalBdd InternalBdd::restrict(InternalBdd const& constraint) const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().Restrict(constraint.getCuddBdd()), metaVariables); + } + + InternalBdd InternalBdd::swapVariables(std::vector const>, std::reference_wrapper const>>> const& fromTo) const { + std::vector fromBdd; + std::vector toBdd; + for (auto const& metaVariablePair : fromTo) { + DdMetaVariable const& variable1 = metaVariablePair.first.get(); + DdMetaVariable const& variable2 = metaVariablePair.second.get(); + + // Add the variables to swap to the corresponding vectors. + for (auto const& ddVariable : variable1.getDdVariables()) { + fromBdd.push_back(ddVariable.getCuddBdd()); + } + for (auto const& ddVariable : variable2.getDdVariables()) { + toBdd.push_back(ddVariable.getCuddBdd()); + } + } + + // Finally, call CUDD to swap the variables. + return InternalBdd(this->getDdManager(), this->getCuddBdd().SwapVariables(fromBdd, toBdd), newContainedMetaVariables); + } + + InternalBdd InternalBdd::getSupport() const { + return InternalBdd(this->getDdManager(), this->getCuddBdd().Support(), this->getContainedMetaVariables()); + } + + uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); + } + + uint_fast64_t InternalBdd::getLeafCount() const { + return static_cast(this->getCuddBdd().CountLeaves()); + } + + uint_fast64_t InternalBdd::getNodeCount() const { + return static_cast(this->getCuddBdd().nodeCount()); + } + + bool InternalBdd::isOne() const { + return this->getCuddBdd().IsOne(); + } + + bool InternalBdd::isZero() const { + return this->getCuddBdd().IsZero(); + } + + uint_fast64_t InternalBdd::getIndex() const { + return static_cast(this->getCuddBdd().NodeReadIndex()); + } + + void InternalBdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const { + // Build the name input of the DD. + std::vector ddNames; + std::string ddName("f"); + ddNames.push_back(new char[ddName.size() + 1]); + std::copy(ddName.c_str(), ddName.c_str() + 2, ddNames.back()); + + // Now build the variables names. + std::vector ddVariableNames; + for (auto const& element : ddVariableNamesAsStrings) { + ddVariableNames.push_back(new char[element.size() + 1]); + std::copy(element.c_str(), element.c_str() + element.size() + 1, ddVariableNames.back()); + } + + // Open the file, dump the DD and close it again. + FILE* filePointer = fopen(filename.c_str() , "w"); + std::vector cuddBddVector = { this->getCuddBdd() }; + this->getDdManager()->getCuddManager().DumpDot(cuddBddVector, &ddVariableNames[0], &ddNames[0], filePointer); + fclose(filePointer); + + // Finally, delete the names. + for (char* element : ddNames) { + delete element; + } + for (char* element : ddVariableNames) { + delete element; + } + } + + BDD InternalBdd::getCuddBdd() const { + return this->cuddBdd; + } + + DdNode* InternalBdd::getCuddDdNode() const { + return this->getCuddBdd().getNode(); + } + + + + + + + + + Add InternalBdd::toAdd() const { + return Add(this->getDdManager(), this->getCuddBdd().Add(), this->getContainedMetaVariables()); + } + + + + + + + + + + + + + + + + + + template + BDD InternalBdd::fromVector(std::shared_ptr const> ddManager, std::vector const& values, Odd const& odd, std::set const& metaVariables, std::function const& filter) { + std::vector ddVariableIndices = getSortedVariableIndices(*ddManager, metaVariables); + uint_fast64_t offset = 0; + return BDD(ddManager->getCuddManager(), fromVectorRec(ddManager->getCuddManager().getManager(), offset, 0, ddVariableIndices.size(), values, odd, ddVariableIndices, filter)); + } + + template + DdNode* InternalBdd::fromVectorRec(::DdManager* manager, uint_fast64_t& currentOffset, uint_fast64_t currentLevel, uint_fast64_t maxLevel, std::vector const& values, Odd const& odd, std::vector const& ddVariableIndices, std::function const& filter) { + if (currentLevel == maxLevel) { + // If we are in a terminal node of the ODD, we need to check whether the then-offset of the ODD is one + // (meaning the encoding is a valid one) or zero (meaning the encoding is not valid). Consequently, we + // need to copy the next value of the vector iff the then-offset is greater than zero. + if (odd.getThenOffset() > 0) { + if (filter(values[currentOffset++])) { + return Cudd_ReadOne(manager); + } else { + return Cudd_ReadLogicZero(manager); + } + } else { + return Cudd_ReadZero(manager); + } + } else { + // If the total offset is zero, we can just return the constant zero DD. + if (odd.getThenOffset() + odd.getElseOffset() == 0) { + return Cudd_ReadZero(manager); + } + + // Determine the new else-successor. + DdNode* elseSuccessor = nullptr; + if (odd.getElseOffset() > 0) { + elseSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getElseSuccessor(), ddVariableIndices, filter); + } else { + elseSuccessor = Cudd_ReadLogicZero(manager); + } + Cudd_Ref(elseSuccessor); + + // Determine the new then-successor. + DdNode* thenSuccessor = nullptr; + if (odd.getThenOffset() > 0) { + thenSuccessor = fromVectorRec(manager, currentOffset, currentLevel + 1, maxLevel, values, odd.getThenSuccessor(), ddVariableIndices, filter); + } else { + thenSuccessor = Cudd_ReadLogicZero(manager); + } + Cudd_Ref(thenSuccessor); + + // Create a node representing ITE(currentVar, thenSuccessor, elseSuccessor); + DdNode* result = Cudd_bddIthVar(manager, static_cast(ddVariableIndices[currentLevel])); + Cudd_Ref(result); + DdNode* newResult = Cudd_bddIte(manager, result, thenSuccessor, elseSuccessor); + Cudd_Ref(newResult); + + // Dispose of the intermediate results + Cudd_RecursiveDeref(manager, result); + Cudd_RecursiveDeref(manager, thenSuccessor); + Cudd_RecursiveDeref(manager, elseSuccessor); + + // Before returning, we remove the protection imposed by the previous call to Cudd_Ref. + Cudd_Deref(newResult); + + return newResult; + } + } + + storm::storage::BitVector InternalBdd::toVector(storm::dd::Odd const& rowOdd) const { + std::vector ddVariableIndices = this->getSortedVariableIndices(); + storm::storage::BitVector result(rowOdd.getTotalOffset()); + this->toVectorRec(this->getCuddDdNode(), this->getDdManager()->getCuddManager(), result, rowOdd, Cudd_IsComplement(this->getCuddDdNode()), 0, ddVariableIndices.size(), 0, ddVariableIndices); + return result; + } + + void InternalBdd::toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const { + // If there are no more values to select, we can directly return. + if (dd == Cudd_ReadLogicZero(manager.getManager()) && !complement) { + return; + } else if (dd == Cudd_ReadOne(manager.getManager()) && complement) { + return; + } + + // If we are at the maximal level, the value to be set is stored as a constant in the DD. + if (currentRowLevel == maxLevel) { + result.set(currentRowOffset, true); + } else if (ddRowVariableIndices[currentRowLevel] < dd->index) { + toVectorRec(dd, manager, result, rowOdd.getElseSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); + toVectorRec(dd, manager, result, rowOdd.getThenSuccessor(), complement, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); + } else { + // Otherwise, we compute the ODDs for both the then- and else successors. + DdNode* elseDdNode = Cudd_E(dd); + DdNode* thenDdNode = Cudd_T(dd); + + // Determine whether we have to evaluate the successors as if they were complemented. + bool elseComplemented = Cudd_IsComplement(elseDdNode) ^ complement; + bool thenComplemented = Cudd_IsComplement(thenDdNode) ^ complement; + + toVectorRec(Cudd_Regular(elseDdNode), manager, result, rowOdd.getElseSuccessor(), elseComplemented, currentRowLevel + 1, maxLevel, currentRowOffset, ddRowVariableIndices); + toVectorRec(Cudd_Regular(thenDdNode), manager, result, rowOdd.getThenSuccessor(), thenComplemented, currentRowLevel + 1, maxLevel, currentRowOffset + rowOdd.getElseOffset(), ddRowVariableIndices); + } + } + + InternalBdd::InternalBdd(std::shared_ptr const> ddManager, BDD cuddBdd, std::set const& containedMetaVariables) : Dd(ddManager, containedMetaVariables), cuddBdd(cuddBdd) { + // Intentionally left empty. + } + + InternalBdd::InternalBdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value) : Dd(ddManager, metaVariables) { + switch (comparisonType) { + case storm::logic::ComparisonType::Less: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::LessEqual: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::greater_equal(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::Greater: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less(), value, std::placeholders::_1)); + break; + case storm::logic::ComparisonType::GreaterEqual: + this->cuddBdd = fromVector(ddManager, explicitValues, odd, metaVariables, std::bind(std::less_equal(), value, std::placeholders::_1)); + break; + } + + } + + } +} \ No newline at end of file diff --git a/src/storage/dd/cudd/CuddBdd.h b/src/storage/dd/cudd/InternalCuddBdd.h similarity index 77% rename from src/storage/dd/cudd/CuddBdd.h rename to src/storage/dd/cudd/InternalCuddBdd.h index 7aec05601..5a8209aa9 100644 --- a/src/storage/dd/cudd/CuddBdd.h +++ b/src/storage/dd/cudd/InternalCuddBdd.h @@ -1,9 +1,9 @@ -#ifndef STORM_STORAGE_DD_CUDDBDD_H_ -#define STORM_STORAGE_DD_CUDDBDD_H_ +#ifndef STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_ +#define STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_ -#include "src/storage/dd/Bdd.h" -#include "src/storage/dd/cudd/CuddDd.h" -#include "src/utility/OsDetection.h" +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/InternalBdd.h" +#include "src/storage/dd/InternalAdd.h" // Include the C++-interface of CUDD. #include "cuddObj.hh" @@ -20,18 +20,13 @@ namespace storm { namespace storage { class BitVector; } - - - + namespace dd { - // Forward-declare some classes. - template class DdManager; - template class Odd; - template class Add; - template class DdForwardIterator; + template + class Odd; template<> - class Bdd : public Dd { + class InternalBdd { public: /*! * Constructs a BDD representation of all encodings that are in the requested relation with the given value. @@ -43,30 +38,22 @@ namespace storm { * @param comparisonType The relation that needs to hold for the values (wrt. to the given value). * @param value The value to compare with. */ - Bdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); - - // Declare the DdManager and DdIterator class as friend so it can access the internals of a DD. - friend class DdManager; - friend class DdForwardIterator; - friend class Add; - friend class Odd; + InternalBdd(std::shared_ptr const> ddManager, std::vector const& explicitValues, storm::dd::Odd const& odd, std::set const& metaVariables, storm::logic::ComparisonType comparisonType, double value); // Instantiate all copy/move constructors/assignments with the default implementation. - Bdd() = default; - Bdd(Bdd const& other) = default; - Bdd& operator=(Bdd const& other) = default; -#ifndef WINDOWS - Bdd(Bdd&& other) = default; - Bdd& operator=(Bdd&& other) = default; -#endif - + InternalBdd() = default; + InternalBdd(InternalBdd const& other) = default; + InternalBdd& operator=(InternalBdd const& other) = default; + InternalBdd(InternalBdd&& other) = default; + InternalBdd& operator=(InternalBdd&& other) = default; + /*! * Retrieves whether the two BDDs represent the same function. * * @param other The BDD that is to be compared with the current one. * @return True if the BDDs represent the same function. */ - bool operator==(Bdd const& other) const; + bool operator==(InternalBdd const& other) const; /*! * Retrieves whether the two BDDs represent different functions. @@ -74,7 +61,7 @@ namespace storm { * @param other The BDD that is to be compared with the current one. * @return True if the BDDs represent the different functions. */ - bool operator!=(Bdd const& other) const; + bool operator!=(InternalBdd const& other) const; /*! * Performs an if-then-else with the given operands, i.e. maps all valuations that are mapped to a non-zero @@ -85,7 +72,7 @@ namespace storm { * @param elseBdd The BDD defining the 'else' part. * @return The resulting BDD. */ - Bdd ite(Bdd const& thenBdd, Bdd const& elseBdd) const; + InternalBdd ite(InternalBdd const& thenBdd, InternalBdd const& elseBdd) const; /*! * Performs a logical or of the current and the given BDD. @@ -93,7 +80,7 @@ namespace storm { * @param other The second BDD used for the operation. * @return The logical or of the operands. */ - Bdd operator||(Bdd const& other) const; + InternalBdd operator||(InternalBdd const& other) const; /*! * Performs a logical or of the current and the given BDD and assigns it to the current BDD. @@ -101,7 +88,7 @@ namespace storm { * @param other The second BDD used for the operation. * @return A reference to the current BDD after the operation */ - Bdd& operator|=(Bdd const& other); + InternalBdd& operator|=(InternalBdd const& other); /*! * Performs a logical and of the current and the given BDD. @@ -109,7 +96,7 @@ namespace storm { * @param other The second BDD used for the operation. * @return The logical and of the operands. */ - Bdd operator&&(Bdd const& other) const; + InternalBdd operator&&(InternalBdd const& other) const; /*! * Performs a logical and of the current and the given BDD and assigns it to the current BDD. @@ -117,7 +104,7 @@ namespace storm { * @param other The second BDD used for the operation. * @return A reference to the current BDD after the operation */ - Bdd& operator&=(Bdd const& other); + InternalBdd& operator&=(InternalBdd const& other); /*! * Performs a logical iff of the current and the given BDD. @@ -125,7 +112,7 @@ namespace storm { * @param other The second BDD used for the operation. * @return The logical iff of the operands. */ - Bdd iff(Bdd const& other) const; + InternalBdd iff(InternalBdd const& other) const; /*! * Performs a logical exclusive-or of the current and the given BDD. @@ -133,7 +120,7 @@ namespace storm { * @param other The second BDD used for the operation. * @return The logical exclusive-or of the operands. */ - Bdd exclusiveOr(Bdd const& other) const; + InternalBdd exclusiveOr(InternalBdd const& other) const; /*! * Performs a logical implication of the current and the given BDD. @@ -141,35 +128,35 @@ namespace storm { * @param other The second BDD used for the operation. * @return The logical implication of the operands. */ - Bdd implies(Bdd const& other) const; + InternalBdd implies(InternalBdd const& other) const; /*! * Logically inverts the current BDD. * * @return The resulting BDD. */ - Bdd operator!() const; + InternalBdd operator!() const; /*! * Logically complements the current BDD. * * @return A reference to the current BDD after the operation. */ - Bdd& complement(); + InternalBdd& complement(); /*! * Existentially abstracts from the given meta variables. * * @param metaVariables The meta variables from which to abstract. */ - Bdd existsAbstract(std::set const& metaVariables) const; + InternalBdd existsAbstract(InternalBdd const& cube) const; /*! * Universally abstracts from the given meta variables. * * @param metaVariables The meta variables from which to abstract. */ - Bdd universalAbstract(std::set const& metaVariables) const; + InternalBdd universalAbstract(InternalBdd const& cube) const; /*! * Swaps the given pairs of meta variables in the BDD. The pairs of meta variables must be guaranteed to have @@ -178,8 +165,8 @@ namespace storm { * @param metaVariablePairs A vector of meta variable pairs that are to be swapped for one another. * @return The resulting BDD. */ - Bdd swapVariables(std::vector> const& metaVariablePairs) const; - + InternalBdd swapVariables(std::vector> const& metaVariablePairs) const; + /*! * Computes the logical and of the current and the given BDD and existentially abstracts from the given set * of variables. @@ -188,7 +175,7 @@ namespace storm { * @param existentialVariables The variables from which to existentially abstract. * @return A BDD representing the result. */ - Bdd andExists(Bdd const& other, std::set const& existentialVariables) const; + InternalBdd andExists(InternalBdd const& other, std::set const& existentialVariables) const; /*! * Computes the constraint of the current BDD with the given constraint. That is, the function value of the @@ -198,7 +185,7 @@ namespace storm { * @param constraint The constraint to use for the operation. * @return The resulting BDD. */ - Bdd constrain(Bdd const& constraint) const; + InternalBdd constrain(InternalBdd const& constraint) const; /*! * Computes the restriction of the current BDD with the given constraint. That is, the function value of the @@ -208,35 +195,35 @@ namespace storm { * @param constraint The constraint to use for the operation. * @return The resulting BDD. */ - Bdd restrict(Bdd const& constraint) const; + InternalBdd restrict(InternalBdd const& constraint) const; /*! * Retrieves the support of the current BDD. * * @return The support represented as a BDD. */ - virtual Bdd getSupport() const override; + InternalBdd getSupport() const; /*! * Retrieves the number of encodings that are mapped to a non-zero value. * * @return The number of encodings that are mapped to a non-zero value. */ - virtual uint_fast64_t getNonZeroCount() const override; + uint_fast64_t getNonZeroCount() const; /*! * Retrieves the number of leaves of the DD. * * @return The number of leaves of the DD. */ - virtual uint_fast64_t getLeafCount() const override; + uint_fast64_t getLeafCount() const; /*! * Retrieves the number of nodes necessary to represent the DD. * * @return The number of nodes in this DD. */ - virtual uint_fast64_t getNodeCount() const override; + uint_fast64_t getNodeCount() const; /*! * Retrieves whether this DD represents the constant one function. @@ -257,23 +244,22 @@ namespace storm { * * @return The index of the topmost variable in BDD. */ - virtual uint_fast64_t getIndex() const override; + uint_fast64_t getIndex() const; /*! * Exports the BDD to the given file in the dot format. * * @param filename The name of the file to which the BDD is to be exported. */ - virtual void exportToDot(std::string const& filename = "") const override; - - friend std::ostream & operator<<(std::ostream& out, const Bdd& bdd); - + void exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const; + /*! * Converts a BDD to an equivalent ADD. * * @return The corresponding ADD. */ - Add toAdd() const; + template + InternalAdd toAdd() const; /*! * Converts the BDD to a bit vector. The given offset-labeled DD is used to determine the correct row of @@ -285,20 +271,6 @@ namespace storm { storm::storage::BitVector toVector(storm::dd::Odd const& rowOdd) const; private: - /*! - * Retrieves the CUDD BDD object associated with this DD. - * - * @return The CUDD BDD object associated with this DD. - */ - BDD getCuddBdd() const; - - /*! - * Retrieves the raw DD node of CUDD associated with this BDD. - * - * @return The DD node of CUDD associated with this BDD. - */ - DdNode* getCuddDdNode() const; - /*! * Creates a DD that encapsulates the given CUDD ADD. * @@ -306,7 +278,7 @@ namespace storm { * @param cuddBdd The CUDD BDD to store. * @param containedMetaVariables The meta variables that appear in the DD. */ - Bdd(std::shared_ptr const> ddManager, BDD cuddBdd, std::set const& containedMetaVariables = std::set()); + InternalBdd(std::shared_ptr const> ddManager, BDD cuddBdd, std::set const& containedMetaVariables = std::set()); /*! * Builds a BDD representing the values that make the given filter function evaluate to true. @@ -351,10 +323,23 @@ namespace storm { */ void toVectorRec(DdNode const* dd, Cudd const& manager, storm::storage::BitVector& result, Odd const& rowOdd, bool complement, uint_fast64_t currentRowLevel, uint_fast64_t maxLevel, uint_fast64_t currentRowOffset, std::vector const& ddRowVariableIndices) const; - // The BDD created by CUDD. + /*! + * Retrieves the CUDD BDD object associated with this DD. + * + * @return The CUDD BDD object associated with this DD. + */ + BDD getCuddBdd() const; + + /*! + * Retrieves the raw DD node of CUDD associated with this BDD. + * + * @return The DD node of CUDD associated with this BDD. + */ + DdNode* getCuddDdNode() const; + BDD cuddBdd; }; } } -#endif /* STORM_STORAGE_DD_CUDDBDD_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DD_CUDD_INTERNALCUDDBDD_H_ */ \ No newline at end of file