DftSymmetries.h

Go to the documentation of this file.

#pragma once
 
#include <cstddef>
#include <iostream>
#include <map>
#include <vector>
 
namespace storm::dft {
namespace storage {
 
class DftSymmetries {
   public:
    DftSymmetries() = default;
 
    DftSymmetries(std::map<size_t, std::vector<std::vector<size_t>>> groups);
 
    size_t nrSymmetries() const;
 
    std::vector<size_t>::const_iterator begin() const;
 
    std::vector<size_t>::const_iterator end() const;
 
    std::vector<std::vector<size_t>> const& getSymmetryGroup(size_t index) const;
 
    friend std::ostream& operator<<(std::ostream& out, DftSymmetries const& symmetries);
 
   private:
    bool existsInFirstSymmetry(size_t index, size_t value) const;
 
    bool existsInSymmetry(size_t index, size_t value) const;
 
    int applySymmetry(std::vector<std::vector<size_t>> const& symmetry, size_t value, size_t index) const;
 
    std::vector<std::vector<size_t>> createSymmetry(std::vector<std::vector<size_t>> parentSymmetry, std::vector<std::vector<size_t>> childSymmetry,
                                                    size_t index);
 
    void sortHierarchical(size_t parent, std::vector<size_t>& candidates);
 
    // Symmetry groups: top level element of group -> symmetry
    // Each symmetry is given by a list of the equivalence classes
    // Each equivalence class is given by all symmetric elements
    std::map<size_t, std::vector<std::vector<size_t>>> groups;
 
    // Top element of groups sorted by their size in increasing order
    std::vector<size_t> sortedSymmetries;
};
 
}  // namespace storage
}  // namespace storm::dft