Bump version

[yosys.git] / libs / subcircuit / subcircuit.cc

/*
 *  SubCircuit -- An implementation of the Ullmann Subgraph Isomorphism
 *                algorithm for coarse grain logic networks
 *
 *  Copyright (C) 2013  Claire Xenia Wolf <claire@yosyshq.com>
 *
 *  Permission to use, copy, modify, and/or distribute this software for any
 *  purpose with or without fee is hereby granted, provided that the above
 *  copyright notice and this permission notice appear in all copies.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *
 */

#include "subcircuit.h"

#include <algorithm>
#include <assert.h>
#include <stdarg.h>
#include <stdio.h>

#ifdef _YOSYS_
#  include "kernel/yosys.h"
#  define my_printf YOSYS_NAMESPACE_PREFIX log
#else
#  define my_printf printf
#endif

using namespace SubCircuit;

#ifndef _YOSYS_
static std::string my_stringf(const char *fmt, ...)
{
        std::string string;
        char *str = NULL;
        va_list ap;

        va_start(ap, fmt);
        if (vasprintf(&str, fmt, ap) < 0)
                str = NULL;
        va_end(ap);

        if (str != NULL) {
                string = str;
                free(str);
        }

        return string;
}
#else
#  define my_stringf YOSYS_NAMESPACE_PREFIX stringf
#endif

SubCircuit::Graph::Graph(const Graph &other, const std::vector<std::string> &otherNodes)
{
        allExtern = other.allExtern;

        std::map<int, int> other2this;
        for (int i = 0; i < int(otherNodes.size()); i++) {
                assert(other.nodeMap.count(otherNodes[i]) > 0);
                other2this[other.nodeMap.at(otherNodes[i])] = i;
                nodeMap[otherNodes[i]] = i;
        }

        std::map<int, int> edges2this;
        for (auto &i1 : other2this)
        for (auto &i2 : other.nodes[i1.first].ports)
        for (auto &i3 : i2.bits)
                if (edges2this.count(i3.edgeIdx) == 0) {
                        int next_idx = edges2this.size();
                        edges2this[i3.edgeIdx] = next_idx;
                }

        edges.resize(edges2this.size());
        for (auto &it : edges2this) {
                for (auto &bit : other.edges[it.first].portBits)
                        if (other2this.count(bit.nodeIdx) > 0)
                                edges[it.second].portBits.insert(BitRef(other2this[bit.nodeIdx], bit.portIdx, bit.bitIdx));
                edges[it.second].constValue = other.edges[it.first].constValue;
                edges[it.second].isExtern = other.edges[it.first].isExtern;
        }

        nodes.resize(other2this.size());
        for (auto &it : other2this) {
                nodes[it.second] = other.nodes[it.first];
                for (auto &i2 : nodes[it.second].ports)
                for (auto &i3 : i2.bits)
                        i3.edgeIdx = edges2this.at(i3.edgeIdx);
        }
}

bool SubCircuit::Graph::BitRef::operator < (const BitRef &other) const
{
        if (nodeIdx != other.nodeIdx)
                return nodeIdx < other.nodeIdx;
        if (portIdx != other.portIdx)
                return portIdx < other.portIdx;
        return bitIdx < other.bitIdx;
}

void  SubCircuit::Graph::createNode(std::string nodeId, std::string typeId, void *userData, bool shared)
{
        assert(nodeMap.count(nodeId) == 0);
        nodeMap[nodeId] = nodes.size();
        nodes.push_back(Node());

        Node &newNode = nodes.back();
        newNode.nodeId = nodeId;
        newNode.typeId = typeId;
        newNode.userData = userData;
        newNode.shared = shared;
}

void SubCircuit::Graph::createPort(std::string nodeId, std::string portId, int width, int minWidth)
{
        assert(nodeMap.count(nodeId) != 0);
        int nodeIdx = nodeMap[nodeId];
        Node &node = nodes[nodeIdx];

        assert(node.portMap.count(portId) == 0);

        int portIdx = node.ports.size();
        node.portMap[portId] = portIdx;
        node.ports.push_back(Port());
        Port &port = node.ports.back();

        port.portId = portId;
        port.minWidth = minWidth < 0 ? width : minWidth;
        port.bits.insert(port.bits.end(), width, PortBit());

        for (int i = 0; i < width; i++) {
                port.bits[i].edgeIdx = edges.size();
                edges.push_back(Edge());
                edges.back().portBits.insert(BitRef(nodeIdx, portIdx, i));
        }
}

void SubCircuit::Graph::createConnection(std::string fromNodeId, std::string fromPortId, int fromBit, std::string toNodeId, std::string toPortId, int toBit, int width)
{
        assert(nodeMap.count(fromNodeId) != 0);
        assert(nodeMap.count(toNodeId) != 0);

        int fromNodeIdx = nodeMap[fromNodeId];
        Node &fromNode = nodes[fromNodeIdx];

        int toNodeIdx = nodeMap[toNodeId];
        Node &toNode = nodes[toNodeIdx];

        assert(fromNode.portMap.count(fromPortId) != 0);
        assert(toNode.portMap.count(toPortId) != 0);

        int fromPortIdx = fromNode.portMap[fromPortId];
        Port &fromPort = fromNode.ports[fromPortIdx];

        int toPortIdx = toNode.portMap[toPortId];
        Port &toPort = toNode.ports[toPortIdx];

        if (width < 0) {
                assert(fromBit == 0 && toBit == 0);
                assert(fromPort.bits.size() == toPort.bits.size());
                width = fromPort.bits.size();
        }

        assert(fromBit >= 0 && toBit >= 0);
        for (int i = 0; i < width; i++)
        {
                assert(fromBit + i < int(fromPort.bits.size()));
                assert(toBit + i < int(toPort.bits.size()));

                int fromEdgeIdx = fromPort.bits[fromBit + i].edgeIdx;
                int toEdgeIdx = toPort.bits[toBit + i].edgeIdx;

                if (fromEdgeIdx == toEdgeIdx)
                        continue;

                // merge toEdge into fromEdge
                if (edges[toEdgeIdx].isExtern)
                        edges[fromEdgeIdx].isExtern = true;
                if (edges[toEdgeIdx].constValue) {
                        assert(edges[fromEdgeIdx].constValue == 0);
                        edges[fromEdgeIdx].constValue = edges[toEdgeIdx].constValue;
                }
                for (const auto &ref : edges[toEdgeIdx].portBits) {
                        edges[fromEdgeIdx].portBits.insert(ref);
                        nodes[ref.nodeIdx].ports[ref.portIdx].bits[ref.bitIdx].edgeIdx = fromEdgeIdx;
                }

                // remove toEdge (move last edge over toEdge if needed)
                if (toEdgeIdx+1 != int(edges.size())) {
                        edges[toEdgeIdx] = edges.back();
                        for (const auto &ref : edges[toEdgeIdx].portBits)
                                nodes[ref.nodeIdx].ports[ref.portIdx].bits[ref.bitIdx].edgeIdx = toEdgeIdx;
                }
                edges.pop_back();
        }
}

void SubCircuit::Graph::createConnection(std::string fromNodeId, std::string fromPortId, std::string toNodeId, std::string toPortId)
{
        createConnection(fromNodeId, fromPortId, 0, toNodeId, toPortId, 0, -1);
}

void SubCircuit::Graph::createConstant(std::string toNodeId, std::string toPortId, int toBit, int constValue)
{
        assert(nodeMap.count(toNodeId) != 0);
        int toNodeIdx = nodeMap[toNodeId];
        Node &toNode = nodes[toNodeIdx];

        assert(toNode.portMap.count(toPortId) != 0);
        int toPortIdx = toNode.portMap[toPortId];
        Port &toPort = toNode.ports[toPortIdx];

        assert(toBit >= 0 && toBit < int(toPort.bits.size()));
        int toEdgeIdx = toPort.bits[toBit].edgeIdx;

        assert(edges[toEdgeIdx].constValue == 0);
        edges[toEdgeIdx].constValue = constValue;
}

void SubCircuit::Graph::createConstant(std::string toNodeId, std::string toPortId, int constValue)
{
        assert(nodeMap.count(toNodeId) != 0);
        int toNodeIdx = nodeMap[toNodeId];
        Node &toNode = nodes[toNodeIdx];

        assert(toNode.portMap.count(toPortId) != 0);
        int toPortIdx = toNode.portMap[toPortId];
        Port &toPort = toNode.ports[toPortIdx];

        for (int i = 0; i < int(toPort.bits.size()); i++) {
                int toEdgeIdx = toPort.bits[i].edgeIdx;
                assert(edges[toEdgeIdx].constValue == 0);
                edges[toEdgeIdx].constValue = constValue % 2 ? '1' : '0';
                constValue = constValue >> 1;
        }
}

void SubCircuit::Graph::markExtern(std::string nodeId, std::string portId, int bit)
{
        assert(nodeMap.count(nodeId) != 0);
        Node &node = nodes[nodeMap[nodeId]];

        assert(node.portMap.count(portId) != 0);
        Port &port = node.ports[node.portMap[portId]];

        if (bit < 0) {
                for (const auto portBit : port.bits)
                        edges[portBit.edgeIdx].isExtern = true;
        } else {
                assert(bit < int(port.bits.size()));
                edges[port.bits[bit].edgeIdx].isExtern = true;
        }
}

void SubCircuit::Graph::markAllExtern()
{
        allExtern = true;
}

void SubCircuit::Graph::print()
{
        for (int i = 0; i < int(nodes.size()); i++) {
                const Node &node = nodes[i];
                my_printf("NODE %d: %s (%s)\n", i, node.nodeId.c_str(), node.typeId.c_str());
                for (int j = 0; j < int(node.ports.size()); j++) {
                        const Port &port = node.ports[j];
                        my_printf("  PORT %d: %s (%d/%d)\n", j, port.portId.c_str(), port.minWidth, int(port.bits.size()));
                        for (int k = 0; k < int(port.bits.size()); k++) {
                                int edgeIdx = port.bits[k].edgeIdx;
                                my_printf("    BIT %d (%d):", k, edgeIdx);
                                for (const auto &ref : edges[edgeIdx].portBits)
                                        my_printf(" %d.%d.%d", ref.nodeIdx, ref.portIdx, ref.bitIdx);
                                if (edges[edgeIdx].isExtern)
                                        my_printf(" [extern]");
                                my_printf("\n");
                        }
                }
        }
}

class SubCircuit::SolverWorker
{
        // basic internal data structures

        typedef std::vector<std::map<int, int>> adjMatrix_t;

        struct GraphData {
                std::string graphId;
                Graph graph;
                adjMatrix_t adjMatrix;
                std::vector<bool> usedNodes;
        };

        static void printAdjMatrix(const adjMatrix_t &matrix)
        {
                my_printf("%7s", "");
                for (int i = 0; i < int(matrix.size()); i++)
                        my_printf("%4d:", i);
                my_printf("\n");
                for (int i = 0; i < int(matrix.size()); i++) {
                        my_printf("%5d:", i);
                        for (int j = 0; j < int(matrix.size()); j++)
                                if (matrix.at(i).count(j) == 0)
                                        my_printf("%5s", "-");
                                else
                                        my_printf("%5d", matrix.at(i).at(j));
                        my_printf("\n");
                }
        }

        // helper functions for handling permutations

        static constexpr int maxPermutationsLimit = 1000000;

        static int numberOfPermutations(const std::vector<std::string> &list)
        {
                constexpr size_t mappedPermutationsSize = 10;
                constexpr int mappedPermutations[mappedPermutationsSize] = {1, 1, 2, 6, 24, 120, 720, 5040, 40320, 362880};
                assert(list.size() < mappedPermutationsSize);
                return mappedPermutations[list.size()];
        }

        static void permutateVectorToMap(std::map<std::string, std::string> &map, const std::vector<std::string> &list, int idx)
        {
                // convert idx to a list.size() digits factoradic number

                std::vector<int> factoradicDigits;
                for (int i = 0; i < int(list.size()); i++) {
                        factoradicDigits.push_back(idx % (i+1));
                        idx = idx / (i+1);
                }

                // construct permutation

                std::vector<std::string> pool = list;
                std::vector<std::string> permutation;

                while (!factoradicDigits.empty()) {
                        int i = factoradicDigits.back();
                        factoradicDigits.pop_back();
                        permutation.push_back(pool[i]);
                        pool.erase(pool.begin() + i);
                }

                // update map

                for (int i = 0; i < int(list.size()); i++)
                        map[list[i]] = permutation[i];
        }

        static int numberOfPermutationsArray(const std::vector<std::vector<std::string>> &list)
        {
                int numPermutations = 1;
                for (const auto &it : list) {
                        int thisPermutations = numberOfPermutations(it);
                        assert(float(numPermutations) * float(thisPermutations) < maxPermutationsLimit);
                        numPermutations *= thisPermutations;
                }
                return numPermutations;
        }

        static void permutateVectorToMapArray(std::map<std::string, std::string> &map, const std::vector<std::vector<std::string>> &list, int idx)
        {
                for (const auto &it : list) {
                        int thisPermutations = numberOfPermutations(it);
                        int thisIdx = idx % thisPermutations;
                        permutateVectorToMap(map, it, thisIdx);
                        idx /= thisPermutations;
                }
        }

        static void applyPermutation(std::map<std::string, std::string> &map, const std::map<std::string, std::string> &permutation)
        {
                std::vector<std::pair<std::string, std::string>> changeLog;
                for (const auto &it : permutation)
                        if (map.count(it.second))
                                changeLog.push_back(std::pair<std::string, std::string>(it.first, map.at(it.second)));
                        else
                                changeLog.push_back(std::pair<std::string, std::string>(it.first, it.second));
                for (const auto &it : changeLog)
                        map[it.first] = it.second;
        }

        // classes for internal digraph representation

        struct DiBit
        {
                std::string fromPort, toPort;
                int fromBit, toBit;

                DiBit() : fromPort(), toPort(), fromBit(-1), toBit(-1) { }
                DiBit(std::string fromPort, int fromBit, std::string toPort, int toBit) : fromPort(fromPort), toPort(toPort), fromBit(fromBit), toBit(toBit) { }

                bool operator < (const DiBit &other) const
                {
                        if (fromPort != other.fromPort)
                                return fromPort < other.fromPort;
                        if (toPort != other.toPort)
                                return toPort < other.toPort;
                        if (fromBit != other.fromBit)
                                return fromBit < other.fromBit;
                        return toBit < other.toBit;
                }

                std::string toString() const
                {
                        return my_stringf("%s[%d]:%s[%d]", fromPort.c_str(), fromBit, toPort.c_str(), toBit);
                }
        };

        struct DiNode
        {
                std::string typeId;
                std::map<std::string, int> portSizes;

                DiNode()
                {
                }

                DiNode(const Graph &graph, int nodeIdx)
                {
                        const Graph::Node &node = graph.nodes.at(nodeIdx);
                        typeId = node.typeId;
                        for (const auto &port : node.ports)
                                portSizes[port.portId] = port.bits.size();
                }

                bool operator < (const DiNode &other) const
                {
                        if (typeId != other.typeId)
                                return typeId < other.typeId;
                        return portSizes < other.portSizes;
                }

                std::string toString() const
                {
                        std::string str;
                        bool firstPort = true;
                        for (const auto &it : portSizes) {
                                str += my_stringf("%s%s[%d]", firstPort ? "" : ",", it.first.c_str(), it.second);
                                firstPort = false;
                        }
                        return typeId + "(" + str + ")";
                }
        };

        struct DiEdge
        {
                DiNode fromNode, toNode;
                std::set<DiBit> bits;
                std::string userAnnotation;

                bool operator < (const DiEdge &other) const
                {
                        if (fromNode < other.fromNode || other.fromNode < fromNode)
                                return fromNode < other.fromNode;
                        if (toNode < other.toNode || other.toNode < toNode)
                                return toNode < other.toNode;
                        if (bits < other.bits || other.bits < bits)
                                return bits < other.bits;
                        return userAnnotation < other.userAnnotation;
                }

                bool compare(const DiEdge &other, const std::map<std::string, std::string> &mapFromPorts, const std::map<std::string, std::string> &mapToPorts) const
                {
                        // Rules for matching edges:
                        //
                        // For all bits in the needle edge:
                        //   - ignore if needle ports don't exist in haystack edge
                        //   - otherwise: matching bit in haystack edge must exist
                        //
                        // There is no need to check in the other direction, as checking
                        // of the isExtern properties is already performed in node matching.
                        //
                        // Note: "this" is needle, "other" is haystack

                        for (auto bit : bits)
                        {
                                if (mapFromPorts.count(bit.fromPort) > 0)
                                        bit.fromPort = mapFromPorts.at(bit.fromPort);
                                if (mapToPorts.count(bit.toPort) > 0)
                                        bit.toPort = mapToPorts.at(bit.toPort);

                                if (other.fromNode.portSizes.count(bit.fromPort) == 0)
                                        continue;
                                if (other.toNode.portSizes.count(bit.toPort) == 0)
                                        continue;

                                if (bit.fromBit >= other.fromNode.portSizes.at(bit.fromPort))
                                        continue;
                                if (bit.toBit >= other.toNode.portSizes.at(bit.toPort))
                                        continue;

                                if (other.bits.count(bit) == 0)
                                        return false;
                        }

                        return true;
                }

                bool compareWithFromAndToPermutations(const DiEdge &other, const std::map<std::string, std::string> &mapFromPorts, const std::map<std::string, std::string> &mapToPorts,
                                const std::map<std::string, std::set<std::map<std::string, std::string>>> &swapPermutations) const
                {
                        if (swapPermutations.count(fromNode.typeId) > 0)
                                for (const auto &permutation : swapPermutations.at(fromNode.typeId)) {
                                        std::map<std::string, std::string> thisMapFromPorts = mapFromPorts;
                                        applyPermutation(thisMapFromPorts, permutation);
                                        if (compareWithToPermutations(other, thisMapFromPorts, mapToPorts, swapPermutations))
                                                return true;
                                }
                        return compareWithToPermutations(other, mapFromPorts, mapToPorts, swapPermutations);
                }

                bool compareWithToPermutations(const DiEdge &other, const std::map<std::string, std::string> &mapFromPorts, const std::map<std::string, std::string> &mapToPorts,
                                const std::map<std::string, std::set<std::map<std::string, std::string>>> &swapPermutations) const
                {
                        if (swapPermutations.count(toNode.typeId) > 0)
                                for (const auto &permutation : swapPermutations.at(toNode.typeId)) {
                                        std::map<std::string, std::string> thisMapToPorts = mapToPorts;
                                        applyPermutation(thisMapToPorts, permutation);
                                        if (compare(other, mapFromPorts, thisMapToPorts))
                                                return true;
                                }
                        return compare(other, mapFromPorts, mapToPorts);
                }

                bool compare(const DiEdge &other, const std::map<std::string, std::set<std::set<std::string>>> &swapPorts,
                                const std::map<std::string, std::set<std::map<std::string, std::string>>> &swapPermutations) const
                {
                        // brute force method for port swapping: try all variations

                        std::vector<std::vector<std::string>> swapFromPorts;
                        std::vector<std::vector<std::string>> swapToPorts;

                        // only use groups that are relevant for this edge

                        if (swapPorts.count(fromNode.typeId) > 0)
                                for (const auto &ports : swapPorts.at(fromNode.typeId)) {
                                        for (const auto &bit : bits)
                                                if (ports.count(bit.fromPort))
                                                        goto foundFromPortMatch;
                                        if (0) {
                                foundFromPortMatch:
                                                std::vector<std::string> portsVector;
                                                for (const auto &port : ports)
                                                        portsVector.push_back(port);
                                                swapFromPorts.push_back(portsVector);
                                        }
                                }

                        if (swapPorts.count(toNode.typeId) > 0)
                                for (const auto &ports : swapPorts.at(toNode.typeId)) {
                                        for (const auto &bit : bits)
                                                if (ports.count(bit.toPort))
                                                        goto foundToPortMatch;
                                        if (0) {
                                foundToPortMatch:
                                                std::vector<std::string> portsVector;
                                                for (const auto &port : ports)
                                                        portsVector.push_back(port);
                                                swapToPorts.push_back(portsVector);
                                        }
                                }

                        // try all permutations

                        std::map<std::string, std::string> mapFromPorts, mapToPorts;
                        int fromPortsPermutations = numberOfPermutationsArray(swapFromPorts);
                        int toPortsPermutations = numberOfPermutationsArray(swapToPorts);

                        for (int i = 0; i < fromPortsPermutations; i++)
                        {
                                permutateVectorToMapArray(mapFromPorts, swapFromPorts, i);

                                for (int j = 0; j < toPortsPermutations; j++) {
                                        permutateVectorToMapArray(mapToPorts, swapToPorts, j);
                                        if (compareWithFromAndToPermutations(other, mapFromPorts, mapToPorts, swapPermutations))
                                                return true;
                                }
                        }

                        return false;
                }

                bool compare(const DiEdge &other, const std::map<std::string, std::string> &mapFromPorts, const std::map<std::string, std::set<std::set<std::string>>> &swapPorts,
                                const std::map<std::string, std::set<std::map<std::string, std::string>>> &swapPermutations) const
                {
                        // strip-down version of the last function: only try permutations for mapToPorts, mapFromPorts is already provided by the caller

                        std::vector<std::vector<std::string>> swapToPorts;

                        if (swapPorts.count(toNode.typeId) > 0)
                                for (const auto &ports : swapPorts.at(toNode.typeId)) {
                                        for (const auto &bit : bits)
                                                if (ports.count(bit.toPort))
                                                        goto foundToPortMatch;
                                        if (0) {
                                foundToPortMatch:
                                                std::vector<std::string> portsVector;
                                                for (const auto &port : ports)
                                                        portsVector.push_back(port);
                                                swapToPorts.push_back(portsVector);
                                        }
                                }

                        std::map<std::string, std::string> mapToPorts;
                        int toPortsPermutations = numberOfPermutationsArray(swapToPorts);

                        for (int j = 0; j < toPortsPermutations; j++) {
                                permutateVectorToMapArray(mapToPorts, swapToPorts, j);
                                if (compareWithToPermutations(other, mapFromPorts, mapToPorts, swapPermutations))
                                        return true;
                        }

                        return false;
                }

                std::string toString() const
                {
                        std::string buffer = fromNode.toString() + " " + toNode.toString();
                        for (const auto &bit : bits)
                                buffer += " " + bit.toString();
                        if (!userAnnotation.empty())
                                buffer += " " + userAnnotation;
                        return buffer;
                }

                static void findEdgesInGraph(const Graph &graph, std::map<std::pair<int, int>, DiEdge> &edges)
                {
                        edges.clear();
                        for (const auto &edge : graph.edges) {
                                if (edge.constValue != 0)
                                        continue;
                                for (const auto &fromBit : edge.portBits)
                                for (const auto &toBit : edge.portBits)
                                        if (&fromBit != &toBit) {
                                                DiEdge &de = edges[std::pair<int, int>(fromBit.nodeIdx, toBit.nodeIdx)];
                                                de.fromNode = DiNode(graph, fromBit.nodeIdx);
                                                de.toNode = DiNode(graph, toBit.nodeIdx);
                                                std::string fromPortId = graph.nodes[fromBit.nodeIdx].ports[fromBit.portIdx].portId;
                                                std::string toPortId = graph.nodes[toBit.nodeIdx].ports[toBit.portIdx].portId;
                                                de.bits.insert(DiBit(fromPortId, fromBit.bitIdx, toPortId, toBit.bitIdx));
                                        }
                        }
                }
        };

        struct DiCache
        {
                std::map<DiEdge, int> edgeTypesMap;
                std::vector<DiEdge> edgeTypes;
                std::map<std::pair<int, int>, bool> compareCache;

                void add(const Graph &graph, adjMatrix_t &adjMatrix, const std::string &graphId, Solver *userSolver)
                {
                        std::map<std::pair<int, int>, DiEdge> edges;
                        DiEdge::findEdgesInGraph(graph, edges);

                        adjMatrix.clear();
                        adjMatrix.resize(graph.nodes.size());

                        for (auto &it : edges) {
                                const Graph::Node &fromNode = graph.nodes[it.first.first];
                                const Graph::Node &toNode = graph.nodes[it.first.second];
                                it.second.userAnnotation = userSolver->userAnnotateEdge(graphId, fromNode.nodeId, fromNode.userData, toNode.nodeId, toNode.userData);
                        }

                        for (const auto &it : edges) {
                                if (edgeTypesMap.count(it.second) == 0) {
                                        edgeTypesMap[it.second] = edgeTypes.size();
                                        edgeTypes.push_back(it.second);
                                }
                                adjMatrix[it.first.first][it.first.second] = edgeTypesMap[it.second];
                        }
                }

                bool compare(int needleEdge, int haystackEdge, const std::map<std::string, std::set<std::set<std::string>>> &swapPorts,
                                const std::map<std::string, std::set<std::map<std::string, std::string>>> &swapPermutations)
                {
                        std::pair<int, int> key(needleEdge, haystackEdge);
                        if (!compareCache.count(key))
                                compareCache[key] = edgeTypes.at(needleEdge).compare(edgeTypes.at(haystackEdge), swapPorts, swapPermutations);
                        return compareCache[key];
                }

                bool compare(int needleEdge, int haystackEdge, const std::map<std::string, std::string> &mapFromPorts, const std::map<std::string, std::set<std::set<std::string>>> &swapPorts,
                                const std::map<std::string, std::set<std::map<std::string, std::string>>> &swapPermutations) const
                {
                        return edgeTypes.at(needleEdge).compare(edgeTypes.at(haystackEdge), mapFromPorts, swapPorts, swapPermutations);
                }

                bool compare(int needleEdge, int haystackEdge, const std::map<std::string, std::string> &mapFromPorts, const std::map<std::string, std::string> &mapToPorts) const
                {
                        return edgeTypes.at(needleEdge).compare(edgeTypes.at(haystackEdge), mapFromPorts, mapToPorts);
                }

                void printEdgeTypes() const
                {
                        for (int i = 0; i < int(edgeTypes.size()); i++)
                                my_printf("%5d: %s\n", i, edgeTypes[i].toString().c_str());
                }
        };

        // solver state variables

        Solver *userSolver;
        std::map<std::string, GraphData> graphData;
        std::map<std::string, std::set<std::string>> compatibleTypes;
        std::map<int, std::set<int>> compatibleConstants;
        std::map<std::string, std::set<std::set<std::string>>> swapPorts;
        std::map<std::string, std::set<std::map<std::string, std::string>>> swapPermutations;
        DiCache diCache;
        bool verbose;

        // main solver functions

        bool matchNodePorts(const Graph &needle, int needleNodeIdx, const Graph &haystack, int haystackNodeIdx, const std::map<std::string, std::string> &swaps) const
        {
                const Graph::Node &nn = needle.nodes[needleNodeIdx];
                const Graph::Node &hn = haystack.nodes[haystackNodeIdx];
                assert(nn.ports.size() == hn.ports.size());

                for (int i = 0; i < int(nn.ports.size()); i++)
                {
                        std::string hnPortId = nn.ports[i].portId;
                        if (swaps.count(hnPortId) > 0)
                                hnPortId = swaps.at(hnPortId);

                        if (hn.portMap.count(hnPortId) == 0)
                                return false;

                        const Graph::Port &np = nn.ports[i];
                        const Graph::Port &hp = hn.ports[hn.portMap.at(hnPortId)];

                        if (int(hp.bits.size()) < np.minWidth || hp.bits.size() > np.bits.size())
                                return false;

                        for (int j = 0; j < int(hp.bits.size()); j++)
                        {
                                const Graph::Edge &ne = needle.edges[np.bits[j].edgeIdx];
                                const Graph::Edge &he = haystack.edges[hp.bits[j].edgeIdx];

                                if (ne.constValue || he.constValue) {
                                        if (ne.constValue != he.constValue)
                                                if (compatibleConstants.count(ne.constValue) == 0 || compatibleConstants.at(ne.constValue).count(he.constValue) == 0)
                                                        return false;
                                        continue;
                                }

                                if (ne.isExtern || needle.allExtern) {
                                        if (he.portBits.size() < ne.portBits.size())
                                                return false;
                                } else {
                                        if (he.portBits.size() != ne.portBits.size())
                                                return false;
                                        if (he.isExtern || haystack.allExtern)
                                                return false;
                                }
                        }
                }

                return true;
        }

        bool matchNodes(const GraphData &needle, int needleNodeIdx, const GraphData &haystack, int haystackNodeIdx) const
        {
                // Rules for matching nodes:
                //
                // 1. their typeId must be identical or compatible
                //    (this is checked before calling this function)
                //
                // 2. they must have the same ports and the haystack port
                //    widths must match the needle port width range
                //
                // 3. All edges from the needle must match the haystack:
                //    a) if the needle edge is extern:
                //         - the haystack edge must have at least as many components as the needle edge
                //    b) if the needle edge is not extern:
                //         - the haystack edge must have the same number of components as the needle edge
                //         - the haystack edge must not be extern

                const Graph::Node &nn = needle.graph.nodes[needleNodeIdx];
                const Graph::Node &hn = haystack.graph.nodes[haystackNodeIdx];

                assert(nn.typeId == hn.typeId || (compatibleTypes.count(nn.typeId) > 0 && compatibleTypes.at(nn.typeId).count(hn.typeId) > 0));

                if (nn.ports.size() != hn.ports.size())
                        return false;

                std::map<std::string, std::string> currentCandidate;

                for (const auto &port : needle.graph.nodes[needleNodeIdx].ports)
                        currentCandidate[port.portId] = port.portId;

                if (swapPorts.count(needle.graph.nodes[needleNodeIdx].typeId) == 0)
                {
                        if (matchNodePorts(needle.graph, needleNodeIdx, haystack.graph, haystackNodeIdx, currentCandidate) &&
                                        userSolver->userCompareNodes(needle.graphId, nn.nodeId, nn.userData, haystack.graphId, hn.nodeId, hn.userData, currentCandidate))
                                return true;

                        if (swapPermutations.count(needle.graph.nodes[needleNodeIdx].typeId) > 0)
                                for (const auto &permutation : swapPermutations.at(needle.graph.nodes[needleNodeIdx].typeId)) {
                                        std::map<std::string, std::string> currentSubCandidate = currentCandidate;
                                        applyPermutation(currentSubCandidate, permutation);
                                        if (matchNodePorts(needle.graph, needleNodeIdx, haystack.graph, haystackNodeIdx, currentCandidate) &&
                                                        userSolver->userCompareNodes(needle.graphId, nn.nodeId, nn.userData, haystack.graphId, hn.nodeId, hn.userData, currentCandidate))
                                                return true;
                                }
                }
                else
                {
                        std::vector<std::vector<std::string>> thisSwapPorts;
                        for (const auto &ports : swapPorts.at(needle.graph.nodes[needleNodeIdx].typeId)) {
                                std::vector<std::string> portsVector;
                                for (const auto &port : ports)
                                        portsVector.push_back(port);
                                thisSwapPorts.push_back(portsVector);
                        }

                        int thisPermutations = numberOfPermutationsArray(thisSwapPorts);
                        for (int i = 0; i < thisPermutations; i++)
                        {
                                permutateVectorToMapArray(currentCandidate, thisSwapPorts, i);

                                if (matchNodePorts(needle.graph, needleNodeIdx, haystack.graph, haystackNodeIdx, currentCandidate) &&
                                                userSolver->userCompareNodes(needle.graphId, nn.nodeId, nn.userData, haystack.graphId, hn.nodeId, hn.userData, currentCandidate))
                                        return true;

                                if (swapPermutations.count(needle.graph.nodes[needleNodeIdx].typeId) > 0)
                                        for (const auto &permutation : swapPermutations.at(needle.graph.nodes[needleNodeIdx].typeId)) {
                                                std::map<std::string, std::string> currentSubCandidate = currentCandidate;
                                                applyPermutation(currentSubCandidate, permutation);
                                                if (matchNodePorts(needle.graph, needleNodeIdx, haystack.graph, haystackNodeIdx, currentCandidate) &&
                                                                userSolver->userCompareNodes(needle.graphId, nn.nodeId, nn.userData, haystack.graphId, hn.nodeId, hn.userData, currentCandidate))
                                                        return true;
                                        }
                        }
                }

                return false;
        }

        void generateEnumerationMatrix(std::vector<std::set<int>> &enumerationMatrix, const GraphData &needle, const GraphData &haystack, const std::map<std::string, std::set<std::string>> &initialMappings) const
        {
                std::map<std::string, std::set<int>> haystackNodesByTypeId;
                for (int i = 0; i < int(haystack.graph.nodes.size()); i++)
                        haystackNodesByTypeId[haystack.graph.nodes[i].typeId].insert(i);

                enumerationMatrix.clear();
                enumerationMatrix.resize(needle.graph.nodes.size());
                for (int i = 0; i < int(needle.graph.nodes.size()); i++)
                {
                        const Graph::Node &nn = needle.graph.nodes[i];

                        for (int j : haystackNodesByTypeId[nn.typeId]) {
                                const Graph::Node &hn = haystack.graph.nodes[j];
                                if (initialMappings.count(nn.nodeId) > 0 && initialMappings.at(nn.nodeId).count(hn.nodeId) == 0)
                                        continue;
                                if (!matchNodes(needle, i, haystack, j))
                                        continue;
                                enumerationMatrix[i].insert(j);
                        }

                        if (compatibleTypes.count(nn.typeId) > 0)
                                for (const std::string &compatibleTypeId : compatibleTypes.at(nn.typeId))
                                        for (int j : haystackNodesByTypeId[compatibleTypeId]) {
                                                const Graph::Node &hn = haystack.graph.nodes[j];
                                                if (initialMappings.count(nn.nodeId) > 0 && initialMappings.at(nn.nodeId).count(hn.nodeId) == 0)
                                                        continue;
                                                if (!matchNodes(needle, i, haystack, j))
                                                        continue;
                                                enumerationMatrix[i].insert(j);
                                        }
                }
        }

        bool checkEnumerationMatrix(std::vector<std::set<int>> &enumerationMatrix, int i, int j, const GraphData &needle, const GraphData &haystack)
        {
                for (const auto &it_needle : needle.adjMatrix.at(i))
                {
                        int needleNeighbour = it_needle.first;
                        int needleEdgeType = it_needle.second;

                        for (int haystackNeighbour : enumerationMatrix[needleNeighbour])
                                if (haystack.adjMatrix.at(j).count(haystackNeighbour) > 0) {
                                        int haystackEdgeType = haystack.adjMatrix.at(j).at(haystackNeighbour);
                                        if (diCache.compare(needleEdgeType, haystackEdgeType, swapPorts, swapPermutations)) {
                                                const Graph::Node &needleFromNode = needle.graph.nodes[i];
                                                const Graph::Node &needleToNode = needle.graph.nodes[needleNeighbour];
                                                const Graph::Node &haystackFromNode = haystack.graph.nodes[j];
                                                const Graph::Node &haystackToNode = haystack.graph.nodes[haystackNeighbour];
                                                if (userSolver->userCompareEdge(needle.graphId, needleFromNode.nodeId,  needleFromNode.userData, needleToNode.nodeId,  needleToNode.userData,
                                                                haystack.graphId, haystackFromNode.nodeId, haystackFromNode.userData, haystackToNode.nodeId, haystackToNode.userData))
                                                        goto found_match;
                                        }
                                }

                        return false;
                found_match:;
                }

                return true;
        }

        bool pruneEnumerationMatrix(std::vector<std::set<int>> &enumerationMatrix, const GraphData &needle, const GraphData &haystack, int &nextRow, bool allowOverlap)
        {
                bool didSomething = true;
                while (didSomething)
                {
                        nextRow = -1;
                        didSomething = false;
                        for (int i = 0; i < int(enumerationMatrix.size()); i++) {
                                std::set<int> newRow;
                                for (int j : enumerationMatrix[i]) {
                                        if (!checkEnumerationMatrix(enumerationMatrix, i, j, needle, haystack))
                                                didSomething = true;
                                        else if (!allowOverlap && haystack.usedNodes[j])
                                                didSomething = true;
                                        else
                                                newRow.insert(j);
                                }
                                if (newRow.size() == 0)
                                        return false;
                                if (newRow.size() >= 2 && (nextRow < 0 || needle.adjMatrix.at(nextRow).size() < needle.adjMatrix.at(i).size()))
                                        nextRow = i;
                                enumerationMatrix[i].swap(newRow);
                        }
                }
                return true;
        }

        void printEnumerationMatrix(const std::vector<std::set<int>> &enumerationMatrix, int maxHaystackNodeIdx = -1) const
        {
                if (maxHaystackNodeIdx < 0) {
                        for (const auto &it : enumerationMatrix)
                                for (int idx : it)
                                        maxHaystackNodeIdx = std::max(maxHaystackNodeIdx, idx);
                }

                my_printf("       ");
                for (int j = 0; j < maxHaystackNodeIdx; j += 5)
                        my_printf("%-6d", j);
                my_printf("\n");

                for (int i = 0; i < int(enumerationMatrix.size()); i++)
                {
                        my_printf("%5d:", i);
                        for (int j = 0; j < maxHaystackNodeIdx; j++) {
                                if (j % 5 == 0)
                                        my_printf(" ");
                                my_printf("%c", enumerationMatrix[i].count(j) > 0 ? '*' : '.');
                        }
                        my_printf("\n");
                }
        }

        bool checkPortmapCandidate(const std::vector<std::set<int>> &enumerationMatrix, const GraphData &needle,  const GraphData &haystack, int idx, const std::map<std::string, std::string> &currentCandidate)
        {
                assert(enumerationMatrix[idx].size() == 1);
                int idxHaystack = *enumerationMatrix[idx].begin();

                const Graph::Node &nn = needle.graph.nodes[idx];
                const Graph::Node &hn = haystack.graph.nodes[idxHaystack];

                if (!matchNodePorts(needle.graph, idx, haystack.graph, idxHaystack, currentCandidate) ||
                                !userSolver->userCompareNodes(needle.graphId, nn.nodeId, nn.userData, haystack.graphId, hn.nodeId, hn.userData, currentCandidate))
                        return false;

                for (const auto &it_needle : needle.adjMatrix.at(idx))
                {
                        int needleNeighbour = it_needle.first;
                        int needleEdgeType = it_needle.second;

                        assert(enumerationMatrix[needleNeighbour].size() == 1);
                        int haystackNeighbour = *enumerationMatrix[needleNeighbour].begin();

                        assert(haystack.adjMatrix.at(idxHaystack).count(haystackNeighbour) > 0);
                        int haystackEdgeType = haystack.adjMatrix.at(idxHaystack).at(haystackNeighbour);
                        if (!diCache.compare(needleEdgeType, haystackEdgeType, currentCandidate, swapPorts, swapPermutations))
                                return false;
                }

                return true;
        }

        void generatePortmapCandidates(std::set<std::map<std::string, std::string>> &portmapCandidates, const std::vector<std::set<int>> &enumerationMatrix,
                        const GraphData &needle, const GraphData &haystack, int idx)
        {
                std::map<std::string, std::string> currentCandidate;

                for (const auto &port : needle.graph.nodes[idx].ports)
                        currentCandidate[port.portId] = port.portId;

                if (swapPorts.count(needle.graph.nodes[idx].typeId) == 0)
                {
                        if (checkPortmapCandidate(enumerationMatrix, needle, haystack, idx, currentCandidate))
                                portmapCandidates.insert(currentCandidate);

                        if (swapPermutations.count(needle.graph.nodes[idx].typeId) > 0)
                                for (const auto &permutation : swapPermutations.at(needle.graph.nodes[idx].typeId)) {
                                        std::map<std::string, std::string> currentSubCandidate = currentCandidate;
                                        applyPermutation(currentSubCandidate, permutation);
                                        if (checkPortmapCandidate(enumerationMatrix, needle, haystack, idx, currentSubCandidate))
                                                portmapCandidates.insert(currentSubCandidate);
                                }
                }
                else
                {
                        std::vector<std::vector<std::string>> thisSwapPorts;
                        for (const auto &ports : swapPorts.at(needle.graph.nodes[idx].typeId)) {
                                std::vector<std::string> portsVector;
                                for (const auto &port : ports)
                                        portsVector.push_back(port);
                                thisSwapPorts.push_back(portsVector);
                        }

                        int thisPermutations = numberOfPermutationsArray(thisSwapPorts);
                        for (int i = 0; i < thisPermutations; i++)
                        {
                                permutateVectorToMapArray(currentCandidate, thisSwapPorts, i);

                                if (checkPortmapCandidate(enumerationMatrix, needle, haystack, idx, currentCandidate))
                                        portmapCandidates.insert(currentCandidate);

                                if (swapPermutations.count(needle.graph.nodes[idx].typeId) > 0)
                                        for (const auto &permutation : swapPermutations.at(needle.graph.nodes[idx].typeId)) {
                                                std::map<std::string, std::string> currentSubCandidate = currentCandidate;
                                                applyPermutation(currentSubCandidate, permutation);
                                                if (checkPortmapCandidate(enumerationMatrix, needle, haystack, idx, currentSubCandidate))
                                                        portmapCandidates.insert(currentSubCandidate);
                                        }
                        }
                }
        }

        bool prunePortmapCandidates(std::vector<std::set<std::map<std::string, std::string>>> &portmapCandidates, std::vector<std::set<int>> enumerationMatrix, const GraphData &needle, const GraphData &haystack)
        {
                bool didSomething = false;

                // strategy #1: prune impossible port mappings

                for (int i = 0; i < int(needle.graph.nodes.size()); i++)
                {
                        assert(enumerationMatrix[i].size() == 1);
                        int j = *enumerationMatrix[i].begin();

                        std::set<std::map<std::string, std::string>> thisCandidates;
                        portmapCandidates[i].swap(thisCandidates);

                        for (const auto &testCandidate : thisCandidates)
                        {
                                for (const auto &it_needle : needle.adjMatrix.at(i))
                                {
                                        int needleNeighbour = it_needle.first;
                                        int needleEdgeType = it_needle.second;

                                        assert(enumerationMatrix[needleNeighbour].size() == 1);
                                        int haystackNeighbour = *enumerationMatrix[needleNeighbour].begin();

                                        assert(haystack.adjMatrix.at(j).count(haystackNeighbour) > 0);
                                        int haystackEdgeType = haystack.adjMatrix.at(j).at(haystackNeighbour);

                                        std::set<std::map<std::string, std::string>> &candidates =
                                                        i == needleNeighbour ? thisCandidates : portmapCandidates[needleNeighbour];

                                        for (const auto &otherCandidate : candidates) {
                                                if (diCache.compare(needleEdgeType, haystackEdgeType, testCandidate, otherCandidate))
                                                        goto found_match;
                                        }

                                        didSomething = true;
                                        goto purgeCandidate;
                                found_match:;
                                }

                                portmapCandidates[i].insert(testCandidate);
                        purgeCandidate:;
                        }

                        if (portmapCandidates[i].size() == 0)
                                return false;
                }

                if (didSomething)
                        return true;

                // strategy #2: prune a single random port mapping

                for (int i = 0; i < int(needle.graph.nodes.size()); i++)
                        if (portmapCandidates[i].size() > 1) {
                                // remove last mapping. this keeps ports unswapped in don't-care situations
                                portmapCandidates[i].erase(--portmapCandidates[i].end());
                                return true;
                        }

                return false;
        }

        void ullmannRecursion(std::vector<Solver::Result> &results, std::vector<std::set<int>> &enumerationMatrix, int iter, const GraphData &needle, GraphData &haystack, bool allowOverlap, int limitResults)
        {
                int i = -1;
                if (!pruneEnumerationMatrix(enumerationMatrix, needle, haystack, i, allowOverlap))
                        return;

                if (i < 0)
                {
                        Solver::Result result;
                        result.needleGraphId = needle.graphId;
                        result.haystackGraphId = haystack.graphId;

                        std::vector<std::set<std::map<std::string, std::string>>> portmapCandidates;
                        portmapCandidates.resize(enumerationMatrix.size());

                        for (int j = 0; j < int(enumerationMatrix.size()); j++) {
                                Solver::ResultNodeMapping mapping;
                                mapping.needleNodeId = needle.graph.nodes[j].nodeId;
                                mapping.needleUserData = needle.graph.nodes[j].userData;
                                mapping.haystackNodeId = haystack.graph.nodes[*enumerationMatrix[j].begin()].nodeId;
                                mapping.haystackUserData = haystack.graph.nodes[*enumerationMatrix[j].begin()].userData;
                                generatePortmapCandidates(portmapCandidates[j], enumerationMatrix, needle, haystack, j);
                                result.mappings[needle.graph.nodes[j].nodeId] = mapping;
                        }

                        while (prunePortmapCandidates(portmapCandidates, enumerationMatrix, needle, haystack)) { }

                        if (verbose) {
                                my_printf("\nPortmapper results:\n");
                                for (int j = 0; j < int(enumerationMatrix.size()); j++) {
                                        my_printf("%5d: %s\n", j, needle.graph.nodes[j].nodeId.c_str());
                                        int variantCounter = 0;
                                        for (auto &i2 : portmapCandidates.at(j)) {
                                                my_printf("%*s variant %2d:", 6, "", variantCounter++);
                                                int mapCounter = 0;
                                                for (auto &i3 : i2)
                                                        my_printf("%s %s -> %s", mapCounter++ ? "," : "", i3.first.c_str(), i3.second.c_str());
                                                my_printf("\n");
                                        }
                                }
                        }

                        for (int j = 0; j < int(enumerationMatrix.size()); j++) {
                                if (portmapCandidates[j].size() == 0) {
                                        if (verbose) {
                                                my_printf("\nSolution (rejected by portmapper):\n");
                                                printEnumerationMatrix(enumerationMatrix, haystack.graph.nodes.size());
                                        }
                                        return;
                                }
                                result.mappings[needle.graph.nodes[j].nodeId].portMapping = *portmapCandidates[j].begin();
                        }

                        if (!userSolver->userCheckSolution(result)) {
                                if (verbose) {
                                        my_printf("\nSolution (rejected by userCheckSolution):\n");
                                        printEnumerationMatrix(enumerationMatrix, haystack.graph.nodes.size());
                                }
                                return;
                        }

                        for (int j = 0; j < int(enumerationMatrix.size()); j++)
                                if (!haystack.graph.nodes[*enumerationMatrix[j].begin()].shared)
                                        haystack.usedNodes[*enumerationMatrix[j].begin()] = true;

                        if (verbose) {
                                my_printf("\nSolution:\n");
                                printEnumerationMatrix(enumerationMatrix, haystack.graph.nodes.size());
                        }

                        results.push_back(result);
                        return;
                }

                if (verbose) {
                        my_printf("\n");
                        my_printf("Enumeration Matrix at recursion level %d (%d):\n", iter, i);
                        printEnumerationMatrix(enumerationMatrix, haystack.graph.nodes.size());
                }

                std::set<int> activeRow;
                enumerationMatrix[i].swap(activeRow);

                for (int j : activeRow)
                {
                        // found enough?
                        if (limitResults >= 0 && int(results.size()) >= limitResults)
                                return;

                        // already used by other solution -> try next
                        if (!allowOverlap && haystack.usedNodes[j])
                                continue;

                        // create enumeration matrix for child in recursion tree
                        std::vector<std::set<int>> nextEnumerationMatrix = enumerationMatrix;
                        for (int k = 0; k < int(nextEnumerationMatrix.size()); k++)
                                nextEnumerationMatrix[k].erase(j);
                        nextEnumerationMatrix[i].insert(j);

                        // recursion
                        ullmannRecursion(results, nextEnumerationMatrix, iter+1, needle, haystack, allowOverlap, limitResults);

                        // we just have found something -> unroll to top recursion level
                        if (!allowOverlap && haystack.usedNodes[j] && iter > 0)
                                return;
                }
        }

        // additional data structes and functions for mining

        struct NodeSet {
                std::string graphId;
                std::set<int> nodes;
                NodeSet(std::string graphId, int node1, int node2) {
                        this->graphId = graphId;
                        nodes.insert(node1);
                        nodes.insert(node2);
                }
                NodeSet(std::string graphId, const std::vector<int> &nodes) {
                        this->graphId = graphId;
                        for (int node : nodes)
                                this->nodes.insert(node);
                }
                void extend(const NodeSet &other) {
                        assert(this->graphId == other.graphId);
                        for (int node : other.nodes)
                                nodes.insert(node);
                }
                int extendCandidate(const NodeSet &other) const {
                        if (graphId != other.graphId)
                                return 0;
                        int newNodes = 0;
                        bool intersect = false;
                        for (int node : other.nodes)
                                if (nodes.count(node) > 0)
                                        intersect = true;
                                else
                                        newNodes++;
                        return intersect ? newNodes : 0;
                }
                bool operator <(const NodeSet &other) const {
                        if (graphId != other.graphId)
                                return graphId < other.graphId;
                        return nodes < other.nodes;
                }
                std::string to_string() const {
                        std::string str = graphId + "(";
                        bool first = true;
                        for (int node : nodes) {
                                str += my_stringf("%s%d", first ? "" : " ", node);
                                first = false;
                        }
                        return str + ")";
                }
        };

        void solveForMining(std::vector<Solver::Result> &results, const GraphData &needle)
        {
                bool backupVerbose = verbose;
                verbose = false;

                for (auto &it : graphData)
                {
                        GraphData &haystack = it.second;

                        std::vector<std::set<int>> enumerationMatrix;
                        std::map<std::string, std::set<std::string>> initialMappings;
                        generateEnumerationMatrix(enumerationMatrix, needle, haystack, initialMappings);

                        haystack.usedNodes.resize(haystack.graph.nodes.size());
                        ullmannRecursion(results, enumerationMatrix, 0, needle, haystack, true, -1);
                }

                verbose = backupVerbose;
        }

        int testForMining(std::vector<Solver::MineResult> &results, std::set<NodeSet> &usedSets, std::set<NodeSet> &nextPool, NodeSet &testSet,
                        const std::string &graphId, const Graph &graph, int minNodes, int minMatches, int limitMatchesPerGraph)
        {
                // my_printf("test: %s\n", testSet.to_string().c_str());

                GraphData needle;
                std::vector<std::string> needle_nodes;
                for (int nodeIdx : testSet.nodes)
                        needle_nodes.push_back(graph.nodes[nodeIdx].nodeId);
                needle.graph = Graph(graph, needle_nodes);
                needle.graph.markAllExtern();
                diCache.add(needle.graph, needle.adjMatrix, graphId, userSolver);

                std::vector<Solver::Result> ullmannResults;
                solveForMining(ullmannResults, needle);

                int matches = 0;
                std::map<std::string, int> matchesPerGraph;
                std::set<NodeSet> thisNodeSetSet;

                for (auto &it : ullmannResults)
                {
                        std::vector<int> resultNodes;
                        for (auto &i2 : it.mappings)
                                resultNodes.push_back(graphData[it.haystackGraphId].graph.nodeMap[i2.second.haystackNodeId]);
                        NodeSet resultSet(it.haystackGraphId, resultNodes);

                        // my_printf("match: %s%s\n", resultSet.to_string().c_str(), usedSets.count(resultSet) > 0 ? " (dup)" : "");

#if 0
                        if (usedSets.count(resultSet) > 0) {
                                // Because of shorted pins isomorphisim is not always bidirectional!
                                //
                                // This means that the following assert is not true in all cases and subgraph A might
                                // show up in the matches for subgraph B but not vice versa... This also means that the
                                // order in which subgraphs are processed has an impact on the results set.
                                //
                                assert(thisNodeSetSet.count(resultSet) > 0);
                                continue;
                        }
#else
                        if (thisNodeSetSet.count(resultSet) > 0)
                                continue;
#endif

                        usedSets.insert(resultSet);
                        thisNodeSetSet.insert(resultSet);

                        matchesPerGraph[it.haystackGraphId]++;
                        if (limitMatchesPerGraph < 0 || matchesPerGraph[it.haystackGraphId] < limitMatchesPerGraph)
                                matches++;
                }

                if (matches < minMatches)
                        return matches;

                if (minNodes <= int(testSet.nodes.size()))
                {
                        Solver::MineResult result;
                        result.graphId = graphId;
                        result.totalMatchesAfterLimits = matches;
                        result.matchesPerGraph = matchesPerGraph;
                        for (int nodeIdx : testSet.nodes) {
                                Solver::MineResultNode resultNode;
                                resultNode.nodeId = graph.nodes[nodeIdx].nodeId;
                                resultNode.userData = graph.nodes[nodeIdx].userData;
                                result.nodes.push_back(resultNode);
                        }
                        results.push_back(result);
                }

                nextPool.insert(thisNodeSetSet.begin(), thisNodeSetSet.end());
                return matches;
        }

        void findNodePairs(std::vector<Solver::MineResult> &results, std::set<NodeSet> &nodePairs, int minNodes, int minMatches, int limitMatchesPerGraph)
        {
                int groupCounter = 0;
                std::set<NodeSet> usedPairs;
                nodePairs.clear();

                if (verbose)
                        my_printf("\nMining for frequent node pairs:\n");

                for (auto &graph_it : graphData)
                for (int node1 = 0; node1 < int(graph_it.second.graph.nodes.size()); node1++)
                for (auto &adj_it : graph_it.second.adjMatrix.at(node1))
                {
                        const std::string &graphId = graph_it.first;
                        const auto &graph = graph_it.second.graph;
                        int node2 = adj_it.first;

                        if (node1 == node2)
                                continue;

                        NodeSet pair(graphId, node1, node2);

                        if (usedPairs.count(pair) > 0)
                                continue;

                        int matches = testForMining(results, usedPairs, nodePairs, pair, graphId, graph, minNodes, minMatches, limitMatchesPerGraph);

                        if (verbose)
                                my_printf("Pair %s[%s,%s] -> %d%s\n", graphId.c_str(), graph.nodes[node1].nodeId.c_str(),
                                                graph.nodes[node2].nodeId.c_str(), matches, matches < minMatches ? "  *purge*" : "");

                        if (minMatches <= matches)
                                groupCounter++;
                }

                if (verbose)
                        my_printf("Found a total of %d subgraphs in %d groups.\n", int(nodePairs.size()), groupCounter);
        }

        void findNextPool(std::vector<Solver::MineResult> &results, std::set<NodeSet> &pool,
                        int oldSetSize, int increment, int minNodes, int minMatches, int limitMatchesPerGraph)
        {
                int groupCounter = 0;
                std::map<std::string, std::vector<const NodeSet*>> poolPerGraph;
                std::set<NodeSet> nextPool;

                for (auto &it : pool)
                        poolPerGraph[it.graphId].push_back(&it);

                if (verbose)
                        my_printf("\nMining for frequent subcircuits of size %d using increment %d:\n", oldSetSize+increment, increment);

                int count = 0;
                for (auto &it : poolPerGraph)
                {
                        std::map<int, std::set<int>> node2sets;
                        std::set<NodeSet> usedSets;

                        for (int idx = 0; idx < int(it.second.size()); idx++) {
                                for (int node : it.second[idx]->nodes)
                                        node2sets[node].insert(idx);
                        }

                        for (int idx1 = 0; idx1 < int(it.second.size()); idx1++, count++)
                        {
                                std::set<int> idx2set;

                                for (int node : it.second[idx1]->nodes)
                                        for (int idx2 : node2sets[node])
                                                if (idx2 > idx1)
                                                        idx2set.insert(idx2);

                                for (int idx2 : idx2set)
                                {
                                        if (it.second[idx1]->extendCandidate(*it.second[idx2]) != increment)
                                                continue;

                                        NodeSet mergedSet = *it.second[idx1];
                                        mergedSet.extend(*it.second[idx2]);

                                        if (usedSets.count(mergedSet) > 0)
                                                continue;

                                        const std::string &graphId = it.first;
                                        const auto &graph = graphData[it.first].graph;

                                        if (verbose) {
                                                my_printf("<%d%%/%d> Found %s[", int(100*count/pool.size()), oldSetSize+increment, graphId.c_str());
                                                bool first = true;
                                                for (int nodeIdx : mergedSet.nodes) {
                                                        my_printf("%s%s", first ? "" : ",", graph.nodes[nodeIdx].nodeId.c_str());
                                                        first = false;
                                                }
                                                my_printf("] ->");
                                        }

                                        int matches = testForMining(results, usedSets, nextPool, mergedSet, graphId, graph, minNodes, minMatches, limitMatchesPerGraph);

                                        if (verbose)
                                                my_printf(" %d%s\n", matches, matches < minMatches ? "  *purge*" : "");

                                        if (minMatches <= matches)
                                                groupCounter++;
                                }
                        }
                }

                pool.swap(nextPool);

                if (verbose)
                        my_printf("Found a total of %d subgraphs in %d groups.\n", int(pool.size()), groupCounter);
        }

        // interface to the public solver class

protected:
        SolverWorker(Solver *userSolver) : userSolver(userSolver), verbose(false)
        {
        }

        void setVerbose()
        {
                verbose = true;
        }

        void addGraph(std::string graphId, const Graph &graph)
        {
                assert(graphData.count(graphId) == 0);

                GraphData &gd = graphData[graphId];
                gd.graphId = graphId;
                gd.graph = graph;
                diCache.add(gd.graph, gd.adjMatrix, graphId, userSolver);
        }

        void addCompatibleTypes(std::string needleTypeId, std::string haystackTypeId)
        {
                compatibleTypes[needleTypeId].insert(haystackTypeId);
        }

        void addCompatibleConstants(int needleConstant, int haystackConstant)
        {
                compatibleConstants[needleConstant].insert(haystackConstant);
        }

        void addSwappablePorts(std::string needleTypeId, const std::set<std::string> &ports)
        {
                swapPorts[needleTypeId].insert(ports);
                diCache.compareCache.clear();
        }

        void addSwappablePortsPermutation(std::string needleTypeId, const std::map<std::string, std::string> &portMapping)
        {
                swapPermutations[needleTypeId].insert(portMapping);
                diCache.compareCache.clear();
        }

        void solve(std::vector<Solver::Result> &results, std::string needleGraphId, std::string haystackGraphId,
                        const std::map<std::string, std::set<std::string>> &initialMappings, bool allowOverlap, int maxSolutions)
        {
                assert(graphData.count(needleGraphId) > 0);
                assert(graphData.count(haystackGraphId) > 0);

                const GraphData &needle = graphData[needleGraphId];
                GraphData &haystack = graphData[haystackGraphId];

                std::vector<std::set<int>> enumerationMatrix;
                generateEnumerationMatrix(enumerationMatrix, needle, haystack, initialMappings);

                if (verbose)
                {
                        my_printf("\n");
                        my_printf("Needle nodes:\n");
                        for (int i = 0; i < int(needle.graph.nodes.size()); i++)
                                my_printf("%5d: %s (%s)\n", i, needle.graph.nodes[i].nodeId.c_str(), needle.graph.nodes[i].typeId.c_str());

                        my_printf("\n");
                        my_printf("Haystack nodes:\n");
                        for (int i = 0; i < int(haystack.graph.nodes.size()); i++)
                                my_printf("%5d: %s (%s)\n", i, haystack.graph.nodes[i].nodeId.c_str(), haystack.graph.nodes[i].typeId.c_str());

                        my_printf("\n");
                        my_printf("Needle Adjecency Matrix:\n");
                        printAdjMatrix(needle.adjMatrix);

                        my_printf("\n");
                        my_printf("Haystack Adjecency Matrix:\n");
                        printAdjMatrix(haystack.adjMatrix);

                        my_printf("\n");
                        my_printf("Edge Types:\n");
                        diCache.printEdgeTypes();

                        my_printf("\n");
                        my_printf("Enumeration Matrix (haystack nodes at column indices):\n");
                        printEnumerationMatrix(enumerationMatrix, haystack.graph.nodes.size());
                }

                haystack.usedNodes.resize(haystack.graph.nodes.size());
                ullmannRecursion(results, enumerationMatrix, 0, needle, haystack, allowOverlap, maxSolutions > 0 ? results.size() + maxSolutions : -1);
        }

        void mine(std::vector<Solver::MineResult> &results, int minNodes, int maxNodes, int minMatches, int limitMatchesPerGraph)
        {
                int nodeSetSize = 2;
                std::set<NodeSet> pool;
                findNodePairs(results, pool, minNodes, minMatches, limitMatchesPerGraph);

                while ((maxNodes < 0 || nodeSetSize < maxNodes) && pool.size() > 0)
                {
                        int increment = nodeSetSize - 1;
                        if (nodeSetSize + increment >= minNodes)
                                increment = minNodes - nodeSetSize;
                        if (nodeSetSize >= minNodes)
                                increment = 1;

                        findNextPool(results, pool, nodeSetSize, increment, minNodes, minMatches, limitMatchesPerGraph);
                        nodeSetSize += increment;
                }
        }

        void clearOverlapHistory()
        {
                for (auto &it : graphData)
                        it.second.usedNodes.clear();
        }

        void clearConfig()
        {
                compatibleTypes.clear();
                compatibleConstants.clear();
                swapPorts.clear();
                swapPermutations.clear();
                diCache.compareCache.clear();
        }

        friend class Solver;
};

bool Solver::userCompareNodes(const std::string&, const std::string&, void*, const std::string&, const std::string&, void*, const std::map<std::string, std::string>&)
{
        return true;
}

std::string Solver::userAnnotateEdge(const std::string&, const std::string&, void*, const std::string&, void*)
{
        return std::string();
}

bool Solver::userCompareEdge(const std::string&, const std::string&, void*, const std::string&, void*, const std::string&, const std::string&, void*, const std::string&, void*)
{
        return true;
}

bool Solver::userCheckSolution(const Result&)
{
        return true;
}

SubCircuit::Solver::Solver()
{
        worker = new SolverWorker(this);
}

SubCircuit::Solver::~Solver()
{
        delete worker;
}

void SubCircuit::Solver::setVerbose()
{
        worker->setVerbose();
}

void SubCircuit::Solver::addGraph(std::string graphId, const Graph &graph)
{
        worker->addGraph(graphId, graph);
}

void SubCircuit::Solver::addCompatibleTypes(std::string needleTypeId, std::string haystackTypeId)
{
        worker->addCompatibleTypes(needleTypeId, haystackTypeId);
}

void SubCircuit::Solver::addCompatibleConstants(int needleConstant, int haystackConstant)
{
        worker->addCompatibleConstants(needleConstant, haystackConstant);
}

void SubCircuit::Solver::addSwappablePorts(std::string needleTypeId, std::string portId1, std::string portId2, std::string portId3, std::string portId4)
{
        std::set<std::string> ports;
        ports.insert(portId1);
        ports.insert(portId2);
        ports.insert(portId3);
        ports.insert(portId4);
        ports.erase(std::string());
        addSwappablePorts(needleTypeId, ports);
}

void SubCircuit::Solver::addSwappablePorts(std::string needleTypeId, std::set<std::string> ports)
{
        worker->addSwappablePorts(needleTypeId, ports);
}

void SubCircuit::Solver::addSwappablePortsPermutation(std::string needleTypeId, std::map<std::string, std::string> portMapping)
{
        worker->addSwappablePortsPermutation(needleTypeId, portMapping);
}

void SubCircuit::Solver::solve(std::vector<Result> &results, std::string needleGraphId, std::string haystackGraphId, bool allowOverlap, int maxSolutions)
{
        std::map<std::string, std::set<std::string>> emptyInitialMapping;
        worker->solve(results, needleGraphId, haystackGraphId, emptyInitialMapping, allowOverlap, maxSolutions);
}

void SubCircuit::Solver::solve(std::vector<Result> &results, std::string needleGraphId, std::string haystackGraphId,
                const std::map<std::string, std::set<std::string>> &initialMappings, bool allowOverlap, int maxSolutions)
{
        worker->solve(results, needleGraphId, haystackGraphId, initialMappings, allowOverlap, maxSolutions);
}

void SubCircuit::Solver::mine(std::vector<MineResult> &results, int minNodes, int maxNodes, int minMatches, int limitMatchesPerGraph)
{
        worker->mine(results, minNodes, maxNodes, minMatches, limitMatchesPerGraph);
}

void SubCircuit::Solver::clearOverlapHistory()
{
        worker->clearOverlapHistory();
}

void SubCircuit::Solver::clearConfig()
{
        worker->clearConfig();
}