SylvanBddManager.h

Go to the documentation of this file.

#pragma once
 
#include <map>
 
#include "storm/adapters/sylvan.h"
#include "storm/storage/dd/sylvan/InternalSylvanDdManager.h"
#include "storm/utility/macros.h"
 
namespace storm::dft {
namespace storage {
 
class SylvanBddManager {
   public:
    SylvanBddManager() = default;
 
    // We can only initialize Sylvan once therefore no copy semantics
    SylvanBddManager(SylvanBddManager const &) = delete;
 
    SylvanBddManager(SylvanBddManager &&) = default;
    SylvanBddManager &operator=(SylvanBddManager &&) = default;
 
    ~SylvanBddManager() = default;
 
    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);
    }
 
    static void exportBddToDot(sylvan::Bdd const &bdd, std::string const &filename) {
        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);
        }
    }
 
   private:
    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{};
};
 
}  // namespace storage
}  // namespace storm::dft