tempest/src/storm/storage/dd/Dd.cpp

#include "storm/storage/dd/Dd.h"

#include <algorithm>

#include "storm/storage/dd/DdManager.h"

#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"

namespace storm {
    namespace dd {
        template<DdType LibraryType>
        Dd<LibraryType>::Dd(DdManager<LibraryType> const& ddManager, std::set<storm::expressions::Variable> const& containedMetaVariables) : ddManager(const_cast<DdManager<LibraryType>*>(&ddManager)), containedMetaVariables(containedMetaVariables) {
            // Intentionally left empty.
        }
        
        template<DdType LibraryType>
        bool Dd<LibraryType>::containsMetaVariable(storm::expressions::Variable const& metaVariable) const {
            return containedMetaVariables.find(metaVariable) != containedMetaVariables.end();
        }
        
        template<DdType LibraryType>
        bool Dd<LibraryType>::containsMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) const {
            return std::includes(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end());
        }
        
        template<DdType LibraryType>
        std::set<storm::expressions::Variable> const& Dd<LibraryType>::getContainedMetaVariables() const {
            return this->containedMetaVariables;
        }
        
        template<DdType LibraryType>
        std::set<storm::expressions::Variable>& Dd<LibraryType>::getContainedMetaVariables() {
            return this->containedMetaVariables;
        }
        
        template<DdType LibraryType>
        DdManager<LibraryType>& Dd<LibraryType>::getDdManager() const {
            return *this->ddManager;
        }
        
        template<DdType LibraryType>
        void Dd<LibraryType>::addMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
            std::set<storm::expressions::Variable> result;
            std::set_union(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin()));
            containedMetaVariables = std::move(result);
        }
        
        template<DdType LibraryType>
        void Dd<LibraryType>::addMetaVariable(storm::expressions::Variable const& metaVariable) {
            this->getContainedMetaVariables().insert(metaVariable);
        }
        
        template<DdType LibraryType>
        void Dd<LibraryType>::removeMetaVariable(storm::expressions::Variable const& metaVariable) {
            this->getContainedMetaVariables().erase(metaVariable);
        }
        
        template<DdType LibraryType>
        void Dd<LibraryType>::removeMetaVariables(std::set<storm::expressions::Variable> const& metaVariables) {
            std::set<storm::expressions::Variable> result;
            std::set_difference(containedMetaVariables.begin(), containedMetaVariables.end(), metaVariables.begin(), metaVariables.end(), std::inserter(result, result.begin()));
            containedMetaVariables = std::move(result);
        }
        
        template<DdType LibraryType>
        std::vector<uint_fast64_t> Dd<LibraryType>::getSortedVariableIndices() const {
            return this->getDdManager().getSortedVariableIndices(this->getContainedMetaVariables());
        }
        
        template<DdType LibraryType>
        std::set<storm::expressions::Variable> Dd<LibraryType>::joinMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
            std::set<storm::expressions::Variable> metaVariables;
            std::set_union(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
            return metaVariables;
        }
        
        template<DdType LibraryType>
        std::set<storm::expressions::Variable> Dd<LibraryType>::subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
            bool includesAllMetaVariables = std::includes(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end());
            STORM_LOG_THROW(includesAllMetaVariables, storm::exceptions::InvalidArgumentException, "Cannot subtract meta variables that are not contained in the DD.");
            std::set<storm::expressions::Variable> metaVariables;
            std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
            return metaVariables;
        }
        
        template class Dd<storm::dd::DdType::CUDD>;
        template class Dd<storm::dd::DdType::Sylvan>;
    }
}