SylvanBddManager.h

Go to the documentation of this file.

#pragma once
 
#include <map>
 
#include "storm/adapters/sylvan.h"
#include "storm/environment/Environment.h"
#include "storm/environment/dd/DdEnvironment.h"
#include "storm/io/file.h"
#include "storm/storage/dd/sylvan/InternalSylvanDdManager.h"
#include "storm/utility/macros.h"
 
namespace storm::dft {
namespace storage {

class SylvanBddManager {
   public:
#ifdef STORM_HAVE_SYLVAN
    explicit SylvanBddManager(storm::Environment const &env) : internalManager{env.dd().get<storm::dd::DdType::Sylvan>()} {}
#else
    explicit SylvanBddManager(storm::Environment const &) {
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
    }
#endif

    static std::shared_ptr<SylvanBddManager> createWithDefaultEnvironment() {
        return std::make_shared<SylvanBddManager>(storm::Environment());
    }
 
    // We can only initialize Sylvan once therefore no copy semantics
    SylvanBddManager(SylvanBddManager const &) = delete;
 
    SylvanBddManager(SylvanBddManager &&) = default;
    SylvanBddManager &operator=(SylvanBddManager &&) = default;

    ~SylvanBddManager() = default;
 
#ifdef STORM_HAVE_SYLVAN
    void execute(std::function<void()> const &f) const {
        internalManager.execute(f);
    }

    uint32_t createVariable(std::string const name) {
        nameToIndex[name] = nextFreeVariableIndex;
        indexToName[nextFreeVariableIndex] = name;
        sylvan::Bdd::bddVar(nextFreeVariableIndex);
        return nextFreeVariableIndex++;
    }

    sylvan::Bdd getPositiveLiteral(std::string const name) const {
        return sylvan::Bdd::bddVar(nameToIndex.at(name));
    }

    sylvan::Bdd getNegativeLiteral(std::string const name) const {
        return !sylvan::Bdd::bddVar(nameToIndex.at(name));
    }

    sylvan::Bdd getPositiveLiteral(uint32_t const index) const {
        return sylvan::Bdd::bddVar(index);
    }

    sylvan::Bdd getNegativeLiteral(uint32_t const index) const {
        return !sylvan::Bdd::bddVar(index);
    }

    sylvan::Bdd getOne() {
        return sylvan::Bdd::bddOne();
    }

    sylvan::Bdd getZero() {
        return sylvan::Bdd::bddZero();
    }

    uint32_t getIndex(std::string const name) const {
        return nameToIndex.at(name);
    }

    std::string getName(uint32_t const index) const {
        return indexToName.at(index);
    }

    void exportBddToDot(sylvan::Bdd const &bdd, std::string const &filename) const {
        FILE *filePointer = fopen(filename.c_str(), "w+");
 
        // fopen returns a nullptr on failure
        if (filePointer == nullptr) {
            STORM_LOG_ERROR("Failure to open file: " << filename);
        } else {
            bdd.PrintDot(filePointer);
            fclose(filePointer);
            std::ofstream filestream;
            storm::io::openFile(filename, filestream, true);
            filestream << "// Mapping from BDD nodes to DFT BEs as follows: \n";
            for (auto const &[index, name] : indexToName) {
                filestream << "// " << index << " -> " << name << '\n';
            }
            storm::io::closeFile(filestream);
        }
    }
#else
    void execute(std::function<void()> const &f) const {
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
    }
 
    uint32_t createVariable(std::string const name) {
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
    }
 
    uint32_t getIndex(std::string const name) const {
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
    }
 
    std::string getName(uint32_t const index) const {
        STORM_LOG_THROW(false, storm::exceptions::MissingLibraryException,
                        "This version of Storm was compiled without support for Sylvan. Yet, a method was called that requires this support. Please choose a "
                        "version of Storm with Sylvan support.");
    }
#endif
 
   private:
#ifdef STORM_HAVE_SYLVAN
    storm::dd::InternalDdManager<storm::dd::DdType::Sylvan> internalManager;
    uint32_t nextFreeVariableIndex{0};
 
    std::map<std::string, uint32_t> nameToIndex{};
    std::map<uint32_t, std::string> indexToName{};
#endif
};
 
}  // namespace storage
}  // namespace storm::dft