//---------------------------------------------------------------------------

#include "stdafx.h"

#ifdef _MSC_VER
#pragma hdrstop
#endif

using namespace std;

#include "../../Kernel/kernelincludes.h"

#include "../../Multilevel/Blif.h"
#include "../../Multilevel/Node.h"
#include "../../Multilevel/Signal.h"
#include "../../Multilevel/Network.h"
//#include "TimeStamp.h"
#include "Resynthesis.h"
//---------------------------------------------------------------------------

Resynthesis::Resynthesis( Network *src )
{
    source = src;
	stripped = NULL;
	improvement = false;
	method = 0;
	optcrit = 0;
	stoplimit = 10;
	sizelimit = 1;
	size = UINT_MAX;
	fanin = 0;
	fanout = 0;
	c_size = 0;
	r_size = 0;
	accept = false;
	real_fanin_rad = 0;
	real_fanout_rad = 0;
}

Resynthesis::~Resynthesis(void)
{
	delete stripped;
}

bool Resynthesis::Nondisjoint( const list<Node>::iterator ndi1, const list<Node>::iterator ndi2 ) const
{
	unsigned int i, j;
	bool nondisjoint = false;

	for ( i = 0; i < (*ndi1).getData()->inputs(); i++ ) {
		for ( j = 0; j < (*ndi2).getData()->inputs(); j++ )
			if ( (*ndi1).getData()->getIName(i) == (*ndi2).getData()->getIName(j) ) {
				nondisjoint = true;
				break;
			}
		if ( nondisjoint ) break;
	}
	return nondisjoint;
}

bool Resynthesis::Nondisjoint( Network *net, const list<Node>::iterator ndi ) const
{
	unsigned int j;

	for ( j = 0; j < (*ndi).inputs(); j++ )
		if ( net->IsSignalThere( (*ndi).getData()->getIName(j) )) return true;
	for ( j = 0; j < (*ndi).outputs(); j++ )
		if ( net->IsSignalThere( (*ndi).getData()->getOName(j) )) return true;
	return false;
}

void Resynthesis::EspressoResynth(void)
{
	unsigned int i, j, k;
	unsigned int limit;
	list<Node>::iterator ndi, endnode;
	bool first = true;
	PLA *res;

	limit = source->GetNodes()/2;
	for ( i = 0; i < limit; i++ ) {
		do {
			j = rand() % source->GetNodes();
			k = rand() % source->GetNodes();
		} while ( j == k || !Nondisjoint( source->GetNodeByIndex(j), source->GetNodeByIndex(k) ) );
		source->MergeNodes( source->GetNodeByIndex(j), source->GetNodeByIndex(k) );
	}
	ndi = source->getData()->begin();
	endnode = source->getData()->end();
	endnode--;
	do {
		if ( (*ndi).outputs() > 1 ) {
			(*ndi).getData()->SavePLA("to_min.pla");
			system(DELFILE("from_min.pla"));
			system( "espresso to_min.pla > from.min.pla" );
			res = new PLA();
			res->LoadPLA("from_min.pla");
			ndi = source->DeleteNode(ndi);
			source->AddNode(*res);
			if ( first ) {
				endnode = source->getData()->end();
				endnode--;
				first = false;
			}
			delete res;
		} else ndi++;
	} while ( ndi != endnode );
}

void Resynthesis::GenerateNeighbors( list<Node>::iterator ndi )
// Generates neighbors of the node in "source" and stores them into "neighbors"
{
	unsigned int i;
	pair<bool, list<Signal>::iterator> findres;
	list<Node>::iterator ndi2;
	list<pair<list<Node>::iterator, unsigned int> >::iterator destit;

	// process node inputs
	for ( i = 0; i < (*ndi).inputs(); i++ ) {
		findres = source->FindSignal( (*ndi).getData()->getIName(i) );
		if ( findres.first ) {
			if ( !(*findres.second).IsPI() && !(*findres.second).IsConstant() ) {
				ndi2 = (*findres.second).GetSource()->first;
				if ( (*ndi2).tmp2 == 0 ) {
					neighbors.push_back(ndi2);
					(*ndi2).tmp2 = 1;
				}
				for ( destit = (*findres.second).GetDest()->begin(); destit != (*findres.second).GetDest()->end(); destit++ ) {
					ndi2 = (*destit).first;
					if ( (*ndi2).tmp2 == 0 && ndi2 != ndi ) {
						neighbors.push_back(ndi2);
						(*ndi2).tmp2 = 1;
					}
				}
			}
		}
	}
	// process node outputs
	for ( i = 0; i < (*ndi).outputs(); i++ ) {
		findres = source->FindSignal( (*ndi).getData()->getOName(i) );
		if ( !findres.first ) throw RuntimeException( "Resynthesis::GenerateNeighbors: Signal not found - very strange" );
		for ( destit = (*findres.second).GetDest()->begin(); destit != (*findres.second).GetDest()->end(); destit++ ) {
			ndi2 = (*destit).first;
			if ( (*ndi2).tmp2 == 0 ) {
				neighbors.push_back(ndi2);
				(*ndi2).tmp2 = 1;
			}
		}
	}
}

bool Resynthesis::FeedsNode( const string &name )
// is this a name of some input in source?
{
	pair<bool, list<Signal>::iterator> findres;

	findres = source->FindSignal(name);
	if ( !findres.first ) throw RuntimeException( "Resynthesis::FeedsNode: Signal not found. Something's very wrong" );
	return !(*findres.second).GetDest()->empty();
}

bool Resynthesis::RandomSelect(void)
// Randomly selects a non-disjoint node and moves it from this->source to this->parted
{
	unsigned int i, j;
	list<Node>::iterator ndi;

	j = source->GetNodes() * stoplimit;
	do {
		i = rand() % source->GetNodes();
		j--;
		ndi = source->GetNodeByIndex(i);
	} while ( j > 0 && ((!stripped->empty() && !Nondisjoint( stripped, ndi )) || ( stripped->empty() && (*ndi).inputs() == 1 && (*ndi).getData()->getTerms() == 1 && (*ndi).getData()->getData()->begin()->getCube() == "-" )));   // do not select constants as the first node
	if ( j != 0 ) {
		stripped->AddNode(*source->GetNodeByIndex(i));
		if ( (*source->GetNodeByIndex(i)).inputs() != 1 ) stripped->tmp = 0;
		else if ( (*source->GetNodeByIndex(i)).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
		source->DeleteNode(source->GetNodeByIndex(i));
	}
	return ( j != 0 );
}

bool Resynthesis::FaninSelect(void)
// Selects a node and moves it from this->source to this->stripped
// Nodes inducing minimum this->stripped fanin are prefered
{
	unsigned int i;
	list<Node>::iterator ndi;
	vector<unsigned int> candidates;
	unsigned int val, minval;

	if ( stripped->empty() ) {		// if stripped is empty, select one randomly
		RandomSelect();
		return true;
	}
	minval = UINT_MAX;
	for ( ndi = source->getData()->begin(); ndi != source->getData()->end(); ndi++ ) 
		if ( Nondisjoint( stripped, ndi ) || stripped->empty() ) {
			val = 0;
			for ( i = 0; i < (*ndi).inputs(); i++ )
				if ( !stripped->IsSignalThere((*ndi).getData()->getIName(i))) val++;		// this input is not in stripped. It will induce a PI
			if ( val == minval )
				candidates.push_back( source->getIndex(ndi) );
			else if ( val < minval ) {
				candidates.clear();
				candidates.push_back( source->getIndex(ndi) );
				minval = val;
			}
		}
	if ( candidates.empty() ) return false;
	i = candidates[rand() % candidates.size()];
	stripped->AddNode(*source->GetNodeByIndex(i));
	if ( (*source->GetNodeByIndex(i)).inputs() != 1 ) stripped->tmp = 0;
	else if ( (*source->GetNodeByIndex(i)).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
	source->DeleteNode(source->GetNodeByIndex(i));
	return true;
}

bool Resynthesis::FanoutSelect(void)
// Selects a node and moves it from this->source to this->stripped
// Nodes inducing minimum this->stripped fanout are prefered
{
	unsigned int i;
	list<Node>::iterator ndi;
	vector<unsigned int> candidates;
	unsigned int val, minval;

	if ( stripped->empty() ) {		// if stripped is empty, select one randomly
		RandomSelect();
		return true;
	}
	minval = UINT_MAX;
	for ( ndi = source->getData()->begin(); ndi != source->getData()->end(); ndi++ )
		if ( Nondisjoint( stripped, ndi ) || stripped->empty() ) {
			val = 0;
			for ( i = 0; i < (*ndi).outputs(); i++ ) {
				if ( source->isPO((*ndi).getData()->getOName(i)) ) val++;  // this is a PO
				else if ( FeedsNode((*ndi).getData()->getOName(i)) ) val++;	// this output feeds a node in source. It could induce extra output in stripped
			}
			if ( val == minval )
				candidates.push_back( source->getIndex(ndi) );
			else if ( val < minval ) {
				candidates.clear();
				candidates.push_back( source->getIndex(ndi) );
				minval = val;
			}
		}
	if ( candidates.empty() ) return false;
	i = candidates[rand() % candidates.size()];
	stripped->AddNode(*source->GetNodeByIndex(i));
	if ( (*source->GetNodeByIndex(i)).inputs() != 1 ) stripped->tmp = 0;
	else if ( (*source->GetNodeByIndex(i)).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
	source->DeleteNode(source->GetNodeByIndex(i));
	return true;
}

bool Resynthesis::FaninFanoutSelect(void)
// Selects a non-disjoint node and moves it from this->source to this->stripped
// Nodes inducing minimum sum of inputs and outputs in this->stripped are prefered
{
	unsigned int i;
	list<Node>::iterator ndi;
	vector<unsigned int> candidates;
	unsigned int val, minval;

	if ( stripped->empty() ) {		// if stripped is empty, select one randomly
		RandomSelect();
		return true;
	}
	minval = UINT_MAX;
	for ( ndi = source->getData()->begin(); ndi != source->getData()->end(); ndi++ )
		if ( Nondisjoint( stripped, ndi ) || stripped->empty() ) {
			val = 0;
			for ( i = 0; i < (*ndi).inputs(); i++ )
				if ( !stripped->IsSignalThere( (*ndi).getData()->getIName(i) ) ) val++;		// this input is not there
			for ( i = 0; i < (*ndi).outputs(); i++ ) {
				if ( source->isPO((*ndi).getData()->getOName(i)) ) val++;  // this is a PO
				else if ( FeedsNode((*ndi).getData()->getOName(i)) ) val++;	// this output feeds a node in source. It could induce extra output in stripped
			}
			if ( val == minval )
				candidates.push_back( source->getIndex(ndi) );
			else if ( val < minval ) {
				candidates.clear();
				candidates.push_back( source->getIndex(ndi) );
				minval = val;
			}
		}

	if ( candidates.empty() ) return false;
	i = candidates[rand() % candidates.size()];
	stripped->AddNode(*source->GetNodeByIndex(i));
	if ( (*source->GetNodeByIndex(i)).inputs() != 1 ) stripped->tmp = 0;
	else if ( (*source->GetNodeByIndex(i)).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
	source->DeleteNode(source->GetNodeByIndex(i));
	return true;
}

bool Resynthesis::RandomSelect2(void)
// Randomly selects a non-disjoint node and moves it from this->source to this->parted
{
	unsigned int i, j;
	list<Node>::iterator ndi;
	list<list<Node>::iterator>::iterator neighit;

	if ( source->empty() ) return false;
	if ( !stripped->empty() && neighbors.empty() ) return false;

	// select the first node randomly
	if ( neighbors.empty() ) {
		i = rand() % source->GetNodes();
		ndi = source->GetNodeByIndex(i);
	}
	else {
		i = rand() % neighbors.size();
		neighit = neighbors.begin();
		for ( j = 0; j < i; j++ ) neighit++;
		ndi = *neighit;
		neighbors.erase(neighit);
	}
	stripped->AddNode(*ndi);
	if ( (*ndi).inputs() != 1 ) stripped->tmp = 0;
	else if ( (*ndi).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
	GenerateNeighbors(ndi);
	source->DeleteNode(ndi);
	return true;
}

bool Resynthesis::FaninSelect2(void)
// Selects a node and moves it from this->source to this->stripped
// Nodes inducing minimum this->stripped fanin are prefered
// Uses neighbors instead of processing all nodes and checking Nondisjoint. As a result, it is slower
{
	unsigned int i, minval, val;
	list<Node>::iterator ndi;
	list<list<Node>::iterator>::iterator neighit;
	vector<list<list<Node>::iterator>::iterator> candidates;

	if ( source->empty() ) return false;
	if ( !stripped->empty() && neighbors.empty() ) return false;

	// select the first node randomly
	if ( neighbors.empty() ) {
		i = rand() % source->GetNodes();
		ndi = source->GetNodeByIndex(i);
	}
	else {
		minval = UINT_MAX;
		for ( neighit = neighbors.begin(); neighit != neighbors.end(); neighit++ ) {
			ndi = *neighit;
			val = 0;
			for ( i = 0; i < (*ndi).inputs(); i++ )
				if ( !stripped->IsSignalThere((*ndi).getData()->getIName(i))) val++;		// this input is not in stripped. It will induce a PI
			if ( val == minval )
				candidates.push_back( neighit );
			else if ( val < minval ) {
				candidates.clear();
				candidates.push_back( neighit );
				minval = val;
			}
		}
		if ( candidates.empty() ) return false;
		neighit = candidates[rand() % candidates.size()];
		ndi = *neighit;
		neighbors.erase(neighit);
	}
	stripped->AddNode(*ndi);
	if ( (*ndi).inputs() != 1 ) stripped->tmp = 0;
	else if ( (*ndi).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
	GenerateNeighbors(ndi);
	source->DeleteNode(ndi);
	return true;
}

bool Resynthesis::FanoutSelect2(void)
// Selects a node and moves it from this->source to this->stripped
// Nodes inducing minimum this->stripped fanout are prefered
// Uses neighbors instead of processing all nodes and checking Nondisjoint. As a result, it is slower
{
	unsigned int i, minval, val;
	list<Node>::iterator ndi;
	list<list<Node>::iterator>::iterator neighit;
	vector<list<list<Node>::iterator>::iterator> candidates;

	if ( source->empty() ) return false;
	if ( !stripped->empty() && neighbors.empty() ) return false;

	// select the first node randomly
	if ( neighbors.empty() ) {
		i = rand() % source->GetNodes();
		ndi = source->GetNodeByIndex(i);
	}
	else {
		minval = UINT_MAX;
		for ( neighit = neighbors.begin(); neighit != neighbors.end(); neighit++ ) {
			ndi = *neighit;
			val = 0;
			for ( i = 0; i < (*ndi).outputs(); i++ ) {
				if ( source->isPO((*ndi).getData()->getOName(i)) ) val++;  // this is a PO
				else if ( FeedsNode((*ndi).getData()->getOName(i)) ) val++;	// this output feeds a node in source. It could induce extra output in stripped
			}
			if ( val == minval )
				candidates.push_back( neighit );
			else if ( val < minval ) {
				candidates.clear();
				candidates.push_back( neighit );
				minval = val;
			}
		}
		if ( candidates.empty() ) return false;
		neighit = candidates[rand() % candidates.size()];
		ndi = *neighit;
		neighbors.erase(neighit);
	}
	stripped->AddNode(*ndi);
	if ( (*ndi).inputs() != 1 ) stripped->tmp = 0;
	else if ( (*ndi).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
	GenerateNeighbors(ndi);
	source->DeleteNode(ndi);
	return true;
}

bool Resynthesis::FaninFanoutSelect2(void)
// Selects a non-disjoint node and moves it from this->source to this->stripped
// Nodes inducing minimum sum of inputs and outputs in this->stripped are prefered
// Uses neighbors instead of processing all nodes and checking Nondisjoint. As a result, it is slower
{
	unsigned int i, minval, val;
	list<Node>::iterator ndi;
	list<list<Node>::iterator>::iterator neighit;
	vector<list<list<Node>::iterator>::iterator> candidates;

	if ( source->empty() ) return false;
	if ( !stripped->empty() && neighbors.empty() ) return false;

	// select the first node randomly
	if ( neighbors.empty() ) {
		i = rand() % source->GetNodes();
		ndi = source->GetNodeByIndex(i);
	}
	else {
		minval = UINT_MAX;
		for ( neighit = neighbors.begin(); neighit != neighbors.end(); neighit++ ) {
			ndi = *neighit;
			val = 0;
			for ( i = 0; i < (*ndi).inputs(); i++ )
				if ( !stripped->IsSignalThere((*ndi).getData()->getIName(i))) val++;		// this input is not in stripped. It will induce a PI
			for ( i = 0; i < (*ndi).outputs(); i++ ) {
				if ( source->isPO((*ndi).getData()->getOName(i)) ) val++;  // this is a PO
				else if ( FeedsNode((*ndi).getData()->getOName(i)) ) val++;	// this output feeds a node in source. It could induce extra output in stripped
			}
			if ( val == minval )
				candidates.push_back( neighit );
			else if ( val < minval ) {
				candidates.clear();
				candidates.push_back( neighit );
				minval = val;
			}
		}
		if ( candidates.empty() ) return false;
		neighit = candidates[rand() % candidates.size()];
		ndi = *neighit;
		neighbors.erase(neighit);
	}
	stripped->AddNode(*ndi);
	if ( (*ndi).inputs() != 1 ) stripped->tmp = 0;
	else if ( (*ndi).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
	GenerateNeighbors(ndi);
	source->DeleteNode(ndi);
	return true;
}

void Resynthesis::RadiusSelect(void)
// Selects one node randomly, then all nodes reachable by a given number of steps (nodes)
{
	unsigned int i;
	list<Node>::iterator ndi, ndi1;
	queue< list<Node>::iterator > node_queue;
	queue< list<Node>::iterator > proc_node_queue;
	list<Signal>::iterator sig;
	list<pair<list<Node>::iterator, unsigned int> > *destlist; 
	list<pair<list<Node>::iterator, unsigned int> >::iterator destlist_it; 
	pair<bool, list<Signal>::iterator> findres;

	for ( ndi = source->getData()->begin(); ndi != source->getData()->end(); ++ndi )
		ndi->tmp = -1;		// set as unprocessed
	
	// randomly select pivot node
	do {
		i = rand() % source->GetNodes();
		ndi = source->GetNodeByIndex(i);
	} while ( ndi->getData()->isConstant() );	// do not select constants

	ndi->tmp = 0;
	ndi->tmp2 = 0;			// distance = 0
	node_queue.push(ndi);

	while ( !node_queue.empty() ) {
		ndi = node_queue.front();			// take unprocessed node 
		node_queue.pop();
		proc_node_queue.push(ndi);		// put it into cut
		if ( proc_node_queue.size() == limit ) break;		// window size limit reached
		if ( (unsigned int)ndi->tmp < size ) {
			for ( i = 0; i < ndi->inputs(); i++ ) {		// enque node fan-ins
				findres = source->FindSignal( ndi->getData()->getIName(i) );
				if ( !findres.first ) throw RuntimeException( "Resynthesis::RadiusSelect: Signal not found. Some inconsistency in signals" );
				else sig = findres.second;
				if ( !sig->IsPI() && !sig->IsConstant() ) {
					ndi1 = sig->GetSource()->first;
					if ( ndi1->tmp == -1 ) {
						ndi1->tmp = ndi->tmp + 1;
						ndi1->tmp2 = ndi->tmp2 - 1;
						if ( -ndi1->tmp2 > (int)this->real_fanin_rad ) this->real_fanin_rad = -ndi1->tmp2;
						node_queue.push(ndi1);
					}
				}
			}
			for ( i = 0; i < ndi->outputs(); i++ ) {		// enque node fan-outs
				sig = source->FindSignal( ndi->getData()->getOName(i) ).second;
				destlist = sig->GetDest();
				for ( destlist_it = destlist->begin(); destlist_it != destlist->end(); ++destlist_it ) {
					ndi1 = destlist_it->first;
					if ( ndi1->tmp == -1 ) {
						ndi1->tmp = ndi->tmp + 1;
						ndi1->tmp2 = ndi->tmp2 + 1;
						if ( ndi1->tmp2 > (int)this->real_fanout_rad ) this->real_fanout_rad = ndi1->tmp2;
						node_queue.push(ndi1);
					}
				}
			}
		}
	}
			// move selected nodes to stripped
	while ( !proc_node_queue.empty() ) {
		ndi = proc_node_queue.front();
		proc_node_queue.pop();
		stripped->AddNode(*ndi);
		if ( ndi->inputs() != 1 ) stripped->tmp = 0;
		else if ( !ndi->getData()->isConstant() ) stripped->tmp = 0;
		source->DeleteNode(ndi);
	}
}

void Resynthesis::WindowingSelect(void)
// Selects one node randomly, finds the transitive fan-in and fan-out to a limited depth,
// then the transitive fan-in of the fan-out, to the minimum fan-in level
{
	unsigned int i;
	list<Node>::iterator pivot_ndi, ndi, ndi1;
	queue< list<Node>::iterator > node_queue;
	queue< list<Node>::iterator > node_queue2;
	queue< list<Node>::iterator > proc_node_queue;
	list<Signal>::iterator sig;
	list<pair<list<Node>::iterator, unsigned int> > *destlist; 
	list<pair<list<Node>::iterator, unsigned int> >::iterator destlist_it; 
	pair<bool, list<Signal>::iterator> findres;
	unsigned int minlevel;
	set<string> processed;
	bool lastflag;

	for ( ndi = source->getData()->begin(); ndi != source->getData()->end(); ndi++ )
		(*ndi).tmp = -1;		// set as unprocessed
	
	// randomly select starting node
	do {
		i = rand() % source->GetNodes();
		pivot_ndi = source->GetNodeByIndex(i);
	} while ( (*pivot_ndi).inputs() == 1 && (*pivot_ndi).getData()->getTerms() == 1 && (*pivot_ndi).getData()->getData()->begin()->getCube() == "-"  );	// do not select constants

	(*pivot_ndi).tmp = 0;

	// compute minimum limited fan-in level
	minlevel = source->GetNodeLevel(pivot_ndi);
	if ( minlevel - size < 2 ) minlevel = 1;		// the TFI it goes to PIs
	else {
		node_queue.push(pivot_ndi);
		while ( !node_queue.empty() ) {
			if ( minlevel == 1 ) break;
			ndi = node_queue.front();			// take unprocessed node
			node_queue.pop();
			if ( (unsigned int)(*ndi).tmp < size ) {
				for ( i = 0; i < (*ndi).inputs(); i++ ) {
					findres = source->FindSignal( (*ndi).getData()->getIName(i) );
					if ( !findres.first ) throw RuntimeException( "Resynthesis::WindowingSelect: Signal not found. Some inconsistency in signals" );
					else sig = findres.second;
					if ( !(*sig).IsPI() && !sig->IsConstant() ) {
						ndi1 = (*sig).GetSource()->first;
						if ( (*ndi1).tmp == -1 ) {
							(*ndi1).tmp = (*ndi).tmp + 1;
							node_queue.push(ndi1);
							if ( source->GetNodeLevel(ndi1) < minlevel ) minlevel = source->GetNodeLevel(ndi1);
							if ( minlevel == 1 ) break;
						}
					}
				}
			}
		}
		while ( !node_queue.empty() ) node_queue.pop();
	}

	// generate fan-out of the pivot
	node_queue.push(pivot_ndi);

	while ( !node_queue.empty() ) {
		ndi = node_queue.front();			// take unprocessed node
		node_queue.pop();
		if ( (unsigned int)(*ndi).tmp < size ) {
			lastflag = true;
			for ( i = 0; i < (*ndi).outputs(); i++ ) {		// enque node fan-outs
				sig = source->FindSignal( (*ndi).getData()->getOName(i) ).second;
				destlist = sig->GetDest();
				for ( destlist_it = destlist->begin(); destlist_it != destlist->end(); destlist_it++ ) {
					lastflag = false;
					ndi1 = (*destlist_it).first;
					if ( (*ndi1).tmp == -1 ) {
						(*ndi1).tmp = (*ndi).tmp + 1;
						if ( (unsigned int)(*ndi1).tmp == size ) node_queue2.push(ndi1);
						else node_queue.push(ndi1);
					}
				}
			}
			if ( lastflag ) node_queue2.push(ndi);  // this is the last node
		}
	}

	// generate fan-in of the fan-out nodes up to minlevel
	proc_node_queue.push(node_queue2.front());
	processed.insert((*(node_queue2.front())).getData()->getOName(0));
	while ( !node_queue2.empty() ) {
		if ( proc_node_queue.size() >= limit ) break;		// node limit reached
		ndi = node_queue2.front();			// take unprocessed node
		node_queue2.pop();
		if ( source->GetNodeLevel(ndi) == 1 ) continue;
		for ( i = 0; i < (*ndi).inputs(); i++ ) {
			findres = source->FindSignal( (*ndi).getData()->getIName(i) );
			if ( !findres.first ) throw RuntimeException( "Resynthesis::WindowingSelect: Signal not found. Some inconsistency in signals" );
			else sig = findres.second;
			if ( !(*sig).IsPI() && !sig->IsConstant() ) {
				ndi1 = (*sig).GetSource()->first;
				if ( processed.find( (*ndi1).getData()->getOName(0) ) == processed.end() ) {
					if ( source->GetNodeLevel(ndi1) >= minlevel ) {
						node_queue2.push(ndi1);
						processed.insert((*ndi1).getData()->getOName(0));
						proc_node_queue.push(ndi1);
						if ( proc_node_queue.size() >= limit ) break;		// node limit reached
					}
				}
			}
		}
	}

	// move selected nodes to stripped
	while ( !proc_node_queue.empty() ) {
		ndi = proc_node_queue.front();
		proc_node_queue.pop();
		stripped->AddNode(*ndi);
		if ( (*ndi).inputs() != 1 ) stripped->tmp = 0;
		else if ( (*ndi).getData()->getData()->front().getCube() != "-" ) stripped->tmp = 0;
		source->DeleteNode(ndi);
	}
}

void Resynthesis::MultilevelResynth(void)
// Performs one resynthesis step
// Extract several nodes from the source network,
//    runs external resynthesis tool and returns the resynthesized network back
{
	unsigned int i;
	list<Node>::iterator ndi, endnode;
	Network *newnet;
	Blif resynblif;
	list<string> voidnodes;
	list<string>::iterator nameit;
	list<Signal>::const_iterator sigit;
	string newname;
	Blif *bliffile;
	bool terminate;
	ifstream testfile;
	stringstream ss;
	char s[10];

	if ( sizelimit > 1 ) limit = (unsigned int)sizelimit;
	else limit = (unsigned int)((float)source->GetNodes()*sizelimit);

	source->GenerateSignals();
		// create stripped network

	delete stripped;
	stripped = new Network();
	stripped->SetModel("tmp");
	stripped->tmp = 1;			// set "all constant nodes" to true
	neighbors.clear();
	for ( ndi = source->getData()->begin(); ndi != source->getData()->end(); ++ndi ) ndi->tmp2 = 0;		// not in neighbors

	if ( method < 4 )
		for ( i = 0; i < limit; i++ ) {	
			switch (method) {
				case 0: terminate = !RandomSelect();
					break;
				case 1: terminate = !FaninSelect();
					break;
				case 2: terminate = !FanoutSelect();
					break;
				case 3: terminate = !FaninFanoutSelect();
					break;
			}
			if ( terminate ) break;
			if ( source->empty() ) break;
			if ( i == 0 ) stripped->GenerateSignals();
		}
	else switch ( method ) {
		case 4: RadiusSelect();
			break;
		case 5: WindowingSelect();
			break;
		default: throw RuntimeException( "MultilevelResynth:: Unknown cut selection method" );
	}

	if ( stripped->tmp == 1 ) {		// all constant nodes produced, do not resynthesize
		source->SpliceNetworks(*stripped);
		delete stripped;
		stripped = NULL;
		fanin = 0;
		fanout = 0;
		c_size = 0;
		r_size = 0;
		return;
	}
	stripped->DerivePorts();		// derive primary inputs and outputs
//	cout << stripped->inputs() << " " << stripped->outputs();
	voidnodes = source->FindVoidSignals();		// signals, that remained unfed in original network

	for ( nameit = voidnodes.begin(); nameit != voidnodes.end(); nameit++ )
		if ( !stripped->isPO(*nameit) ) stripped->AddOutput(*nameit);

	//	to_backup = source->ToBlif();
//	to_backup->SaveBlif("reminder.blif");
//	delete to_backup;

	fanin = stripped->inputs();
	fanout = stripped->outputs();
	c_size = stripped->GetNodes();

		// run external resynthesis
	bliffile = stripped->ToBlif();
	bliffile->SaveBlif("to_resyn.blif");
	delete bliffile;
	system( RUNSCRIPT("resyn.bat") );

	// try, if the resynthesis passed
	testfile.open("from_resyn.blif");	
	if (!testfile.is_open()) {		// resynthesis failed, put stripped back
		source->SpliceNetworks(*stripped);
		fanin = 0;
		fanout = 0;
		c_size = 0;
		r_size = 0;
		delete stripped;
		stripped = NULL;
		return;
	}
	testfile.close();

	resynblif.LoadBlif("from_resyn.blif");
	newnet = new Network(resynblif);
	r_size = newnet->GetNodes();

	accept = true;
	if ( improvement ) {
		switch ( optcrit ) {
			case 0: accept = ( stripped->GetNodes() >= newnet->GetNodes() );
				break;
			case 1: accept = ( stripped->getLiterals() >= newnet->getLiterals() );
				break;
			default: throw RuntimeException("Resynthesis::MultilevelResynth: unknown optimization criterion" );
		}
	}
	if ( accept ) {
			// Rename new internal signals
		i = 0;
		for ( sigit = newnet->GetSignals()->begin(); sigit != newnet->GetSignals()->end(); ++sigit )
			if ( !sigit->IsPI() && !sigit->IsPO() ) {
				if ( source->FindSignal(sigit->getName()).first ) {
					do {
						//ss.clear();
						//ss << i++;
						itoa(i++, s, 10);
						newname = "nd_" + string(s);
					} while ( source->FindSignal(newname).first || newnet->FindSignal(newname).first );
					newnet->Rename( sigit->getName(), newname );
				}
			}

			// splice networks
		source->SpliceNetworks(*newnet);
		delete newnet;
	}
	else {					// worse result, not accepted. Put the old network back.
		source->SpliceNetworks(*stripped);
	}
	delete stripped;
	stripped = NULL;
}

void Resynthesis::Run(void)
{
	real_fanin_rad = 0;
	real_fanout_rad = 0;

	MultilevelResynth();
}
