/*
 *  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 <cstdlib>
#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();
}