Manager.h

Go to the documentation of this file.

// A minimalistic BDD library, following Wolfgang Kunz lecture slides
//
// Created by Markus Wedler 2014
 
#ifndef VDSPROJECT_MANAGER_H
#define VDSPROJECT_MANAGER_H
 
#include "ManagerInterface.h"
#include <unordered_map>
#include <string>
#include <vector>
 
namespace ClassProject
{
 
    class Manager : public ManagerInterface
    {
    public:
        Manager();
 
        struct Node
        {
            BDD_ID TopVar;
            BDD_ID low;
            BDD_ID high;
            std::string label;
        };
 
        struct Unique_Table_Key
        {
            BDD_ID TopVar;
            BDD_ID low;
            BDD_ID high;
 
            bool operator==(const Unique_Table_Key &other) const
            {
                return TopVar == other.TopVar && low == other.low && high == other.high;
            }
        };
 
        /*struct Unique_Table_Entry
        {
            BDD_ID id;
        };*/
 
        struct KeyHash
        {
            std::size_t operator()(const Unique_Table_Key &k) const
            {
                // A hash function
                return ((std::hash<BDD_ID>()(k.TopVar) ^ (std::hash<BDD_ID>()(k.low) << 1)) >> 1) ^ (std::hash<BDD_ID>()(k.high) << 1);
            }
        };
 
        std::unordered_map<Unique_Table_Key, BDD_ID, KeyHash> Table;
        std::vector<Node> id_table;
        std::unordered_map<Unique_Table_Key,BDD_ID,KeyHash> computed_table;
 
        BDD_ID createVar(const std::string &label) override;
        const BDD_ID &True() override;
        const BDD_ID &False() override;
        bool isConstant(BDD_ID f) override;
        bool isVariable(BDD_ID x) override;
        BDD_ID topVar(BDD_ID f) override;
        std::string getTopVarName(const BDD_ID &root) override;
        BDD_ID coFactorTrue(BDD_ID f, BDD_ID x) override;
        BDD_ID coFactorFalse(BDD_ID f, BDD_ID x) override;
        BDD_ID coFactorTrue(BDD_ID f) override;
        BDD_ID coFactorFalse(BDD_ID f) override;
        BDD_ID ite(BDD_ID i, BDD_ID t, BDD_ID e) override;
        void findNodes(const BDD_ID &root, std::set<BDD_ID> &nodes_of_root) override;
        void findVars(const BDD_ID &root, std::set<BDD_ID> &vars_of_root) override;
        size_t uniqueTableSize() override;
        BDD_ID neg(BDD_ID a) override;
        BDD_ID and2(BDD_ID a, BDD_ID b) override;
        BDD_ID or2(BDD_ID a, BDD_ID b) override;
        BDD_ID xor2(BDD_ID a, BDD_ID b) override;
        BDD_ID nand2(BDD_ID a, BDD_ID b) override;
        BDD_ID nor2(BDD_ID a, BDD_ID b) override;
        BDD_ID xnor2(BDD_ID a, BDD_ID b) override;
        void visualizeBDD(std::string filepath, BDD_ID &root) override;
    };
}
 
#endif