
/**CFile***********************************************************************

  FileName    [cuddMini.c]

  PackageName [cudd]

  Synopsis    [Minimizition via BDD and MDD]

  Description [External procedures included in this file:
		<ul>
		<li> Cudd_ddMinimization()
		</ul>]

  Author      [Pavel Cerny]

  Copyright   [Copyright (c) 2008, CVUT FEL

  All rights reserved.

  Redistribution and use in source and binary forms, with or without
  modification, are permitted provided that the following conditions
  are met:

  Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

  Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

  Neither the name of the University of Colorado nor the names of its
  contributors may be used to endorse or promote products derived from
  this software without specific prior written permission.

  THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
  "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
  LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
  FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
  COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
  INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
  BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
  LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
  CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
  LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
  ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
  POSSIBILITY OF SUCH DAMAGE.]

******************************************************************************/

#include "../include/util.h"
#include "../include/cuddInt.h"

#include <time.h>
#include <sys/types.h>
#include <sys/timeb.h>

#if DD_MINIMIZATION == 1

//
// Add character string to DdString
//

int cuddStringAddCharString( 
	DdString * dest, 
	char *     src,
	int        destpos )
{
	int				srclen = (int)strlen( src );
	int				srcpos = 0;
	int             writelen;
	DdSubstring *	actual = dest->first;

	// check validity of destination position
	if ( destpos > dest->length || actual == NULL )
		return FALSE;
	// find dest. position substring
	while ( destpos >= MINI_SUBSTRING_LEN ) {
		actual = actual->next;
		if ( actual == NULL )
			return FALSE;
		destpos -= MINI_SUBSTRING_LEN;
	}
	dest->length  = destpos + srclen;
	writelen      = MINI_SUBSTRING_LEN - destpos;
	while ( srclen > writelen ) {
		// write part of source
		memcpy( &actual->data[destpos], &src[srcpos], writelen );
		// check existence of next substring
		if ( actual->next == NULL ) {
			// alloc next substring 
			actual->next = malloc( sizeof(DdSubstring) );
			actual       = actual->next;
			if ( actual == NULL ) {
				dest->length = 0;
				return FALSE;
			}
			actual->data = malloc( sizeof(char) * MINI_SUBSTRING_LEN );
			if ( actual->data == NULL ) {
				dest->length = 0;
				return FALSE;
			}
		}
		else
			actual = actual->next;

		srclen  -= writelen;
		srcpos  += writelen;
		destpos  = 0;
		writelen = MINI_SUBSTRING_LEN;
	}
	// write modulo MINI_SUBSTRING_LEN remain
	strcpy( &actual->data[destpos], &src[srcpos] );
	return TRUE;
}


//
// Add character string to DdString
//

int cuddStringAddChar(
	DdString * dest, 
	char       src,
	int        destpos,
	int        count )
{
	int				i;
	int             writelen;
	char *          data;
	DdSubstring *	actual = dest->first;

	// check validity of destination position
	if ( destpos > dest->length || actual == NULL )
		return FALSE;
	// find dest. position substring
	while ( destpos >= MINI_SUBSTRING_LEN ) {
		actual = actual->next;
		if ( actual == NULL )
			return FALSE;
		destpos -= MINI_SUBSTRING_LEN;
	}
	dest->length  = destpos + count;
	writelen      = MINI_SUBSTRING_LEN - destpos;
	while ( count > writelen ) {
		data = actual->data;
		// write part of source
		for ( i = destpos; i < MINI_SUBSTRING_LEN; i++ )
			data[i] = src;
		// check existence of next substring
		if ( actual->next == NULL ) {
			// alloc next substring 
			actual->next = malloc( sizeof(DdSubstring) );
			actual       = actual->next;
			if ( actual == NULL ) {
				dest->length = 0;
				return FALSE;
			}
			actual->data = malloc( sizeof(char) * MINI_SUBSTRING_LEN );
			if ( actual->data == NULL ) {
				dest->length = 0;
				return FALSE;
			}
		}
		else
			actual = actual->next;
		count   -= writelen;
		destpos  = 0;
		writelen = MINI_SUBSTRING_LEN;
	}
	// write modulo MINI_SUBSTRING_LEN remain
	data = actual->data;
	for ( i = destpos; i < count; i++ )
		data[i] = src;
	data[i] = '\0';
	return TRUE;
}

//
// Init DdString
//

int cuddStringInit( DdString * dest )
{
	DdSubstring * actual;

	dest->length = 0;
	dest->first  = malloc( sizeof(DdSubstring) );
	actual       = dest->first;
	if ( actual == NULL )
		return FALSE;
	actual->next = NULL;
	actual->data = malloc( sizeof(char) * MINI_SUBSTRING_LEN );
	if ( actual->data == NULL ) {
		free( actual );
		dest->first = NULL;
		return FALSE;
	}
	return TRUE;
}

//
// Free DdString
//

void cuddStringFree( DdString * dest )
{
	DdSubstring * actual = dest->first;
	DdSubstring * next;

	while ( actual != NULL ) {
		next   = actual->next;
		free( actual->data );
		free( actual );
		actual = next;
	}
	dest->length = 0;
	dest->first  = NULL;
}

//
// Multiple-referenced nodes initialization
//

int cuddDdMinimizitionInit( 
	DdManager *				dd,
	DdNode **               roots,
	const unsigned int      inputs,
	const unsigned int      outputs,
	DdMinimizStackEntry	*	stack )
{
	DdNode *				node;		// Actual node ( on the top of stack )
	DdNode *				son;		// Son of actual node
	DdMinimizStackEntry		top;		// Actual top of stack
	DdMinimizationData *	data;
	char					bCheck;		// Check table of multiply-referenced nodes flag
	char					bComplement;// Table entry flag
	int						idx;		// General purpose variable
	int						stackIdx;	// Stack top position
	unsigned int            f;

	// Go through all functions of vector
	for ( f = 0; f < outputs; f++ ) 
	{
		// Check constant case
		if ( Cudd_IsConstant(roots[f]) )
			continue;

		// Push i-th function node on empty stack

		top.node            = roots[f];
		top.son[MINI_L_IDX] = 
		top.son[MINI_R_IDX] = MINI_STACK_SON_NINIT;
		stackIdx            = 0;
		stack[stackIdx]     = top;
		bCheck              = TRUE;

		// Loop until given function minimilized
		do 
		{
			// Get actual context from top of the stack
			top         = stack[stackIdx];
			node        = top.node;
			bComplement = Cudd_IsComplement(node);

			// Should check node minimization data ?
			if ( bCheck ) {
				data = Cudd_Regular(node)->data;
				idx  = MINI_REGULAR_IDX + bComplement;
				// If node is multiple-referenced in minimized BDDarrays
				if ( data != NULL && data->refsCnt[idx] > 0 ) {
					data->refsCnt[idx]++;
					stackIdx--;
					bCheck = FALSE;
					continue;
				}
			}
			// Check direction of depth search
			if      ( Mini_StackGoL(top) ) {
				son = Cudd_NotCond( Mini_CuddLSon(node), bComplement );
				idx = MINI_L_IDX;
			} 
			else if ( Mini_StackGoR(top) ) {
				son = Cudd_NotCond( Mini_CuddRSon(node), bComplement );
				idx = MINI_R_IDX;
			} 
			else { // Mini_StackGoB(top) == TRUE
				// Move back in recursion tree
				if ( Cudd_Regular(node)->ref > 1 ) {
					// Node is multiply-referenced, store it into table
					data = Cudd_Regular(node)->data;
					idx  = MINI_REGULAR_IDX + bComplement;
					if ( data == NULL ) {
						data = malloc( sizeof(DdMinimizationData) );
						if ( data != NULL ) {
							data->refs[MINI_REGULAR_IDX] = 
							data->refs[MINI_COMPLEM_IDX] = 0;
							data->refsCnt[idx]           = 1;
							data->refsCnt[1-idx]         = 0;
							data->flags                  = 0;
							Cudd_Regular(node)->data     = data;
						}
						else
							return FALSE;
					}
					else
						data->refsCnt[idx]++;
				}
				stackIdx--;
				bCheck = FALSE;
				continue;
			}
			if ( Cudd_IsConstant(son) ) {
				// Son node ~ constant function
				stack[stackIdx].son[idx] = MINI_STACK_SON_X;
				bCheck                   = FALSE;
				continue;
			}
			// Son node ~ non-constant function, go to depth
			stack[stackIdx].son[idx] = MINI_STACK_SON_NCONST;
			top.node                 = son;
			top.son[MINI_L_IDX]      = 
			top.son[MINI_R_IDX]      = MINI_STACK_SON_NINIT;
			stack[++stackIdx]        = top;
			bCheck                   = TRUE;
		} 
		while ( stackIdx >= 0 );

		node = roots[f];
		// If node is multiply-referenced, store it into table
		if ( Cudd_Regular(node)->ref > 1 ) {
			idx  = MINI_REGULAR_IDX + Cudd_IsComplement(node);
			if ( data == NULL ) {
				data = malloc( sizeof(DdMinimizationData) );
				if ( data != NULL ) {
					data->refs[MINI_REGULAR_IDX] = 
					data->refs[MINI_COMPLEM_IDX] = 0;
					data->refsCnt[idx]           = 1;
					data->refsCnt[1-idx]         = 0;
					data->flags                  = 0;
					Cudd_Regular(node)->data     = data;
				}
				else
					return FALSE;
			}
			else
				data->refsCnt[idx]++;
		}
	}
	return TRUE;
}

//
// Read PLA from file and update it
//

int cuddDdMinimizationReadPla(
	const DdNode *   son,
	const char       sonType,
	const int        vCnt,
	int *            cCnt,
	DdString *       str )
{
	int						i;					// Auxiliary value
	int						vCntSon;			// Count of variables of son PLA
	int						cCntSon;			// Count of clauses of son PLA
	char					szBuf[MINI_BUFSIZE_L];// Read buffer
	char					szPrefix[MINI_BUFSIZE_L];// Read buffer
	char *					szEnd;				// Auxiliary character pointer
	FILE *					fp;					// Input file stream

	// Set file name and open file
	sprintf( szBuf, "%d.pla", (unsigned long)son );
	if ( fopen_s( &fp, szBuf, "r" ) ) {
		fprintf( stderr, "\nunable to open pla for read: %s", szBuf ); 
		return FALSE;
	}

	// Read number of input variables
	fgets( szBuf, MINI_BUFSIZE_L, fp );
	if ( szBuf[0] != '.' || szBuf[1] != 'i' ) {
		fprintf( stderr, "\nbad flag .i position in pla: %d.pla", (unsigned long)son ); 
		goto MINI_PLA_READ_FAIL_LABEL;
	}
	vCntSon = (int)( strtod( &szBuf[3], &szEnd ) );
	if ( vCntSon == 0 ) {
		fprintf( stderr, "\nillegal variable count in pla: %d.pla", (unsigned long)son ); 
		goto MINI_PLA_READ_FAIL_LABEL;
	}

	// Read number of output variables
	fgets( szBuf, MINI_BUFSIZE_L, fp );
	if ( szBuf[0] != '.' || szBuf[1] != 'o' ) {
		fprintf( stderr, "\nbad flag .o position in pla: %d.pla", (unsigned long)son ); 
		goto MINI_PLA_READ_FAIL_LABEL;
	}

	// Read number of clauses
	fgets( szBuf, MINI_BUFSIZE_L, fp );
	if ( szBuf[0] != '.' || szBuf[1] != 'p' ) {
		fprintf( stderr, "\nillegal clauses count in pla: %d.pla", (unsigned long)son );
		goto MINI_PLA_READ_FAIL_LABEL;
	}

	cCntSon = (int)( strtod( &szBuf[3], &szEnd ) );
	if ( cCntSon == 0 ) {
		fclose( fp );
		return TRUE;
	}

	// Set prefix string ( of each clause )
	szPrefix[0] = sonType;
	for ( i = 1; i < vCnt - vCntSon; i++ )
		szPrefix[i] = '-';
	szPrefix[i] = '\0';

	// Go through clauses until end of file flag reached
	i           = 0;
	while ( 1 ) {
		fgets( szBuf, MINI_BUFSIZE_L, fp );
		if ( szBuf[0] == '.' && szBuf[1] == 'e' )
			break;
		if ( feof( fp ) ) {
			fprintf( stderr, "\npremature end of pla: %d.pla", (unsigned long)son );
			goto MINI_PLA_READ_FAIL_LABEL;
		}
		cuddStringAddCharString( str, szPrefix, str->length );
		cuddStringAddCharString( str, szBuf, str->length );
		i++;
	}
	// Check whether all clauses are red
	if ( i != cCntSon ) {
		fprintf( stderr, "\npla clauses count not fit: %d.pla", (unsigned long)son );
		goto MINI_PLA_READ_FAIL_LABEL;
	}
	*cCnt += cCntSon;

	// Close file
	fclose( fp );
	return TRUE;

MINI_PLA_READ_FAIL_LABEL:

	fclose( fp );
	return FALSE;

}

//
// Write result PLA to file
//

int cuddDdMinimizationWritePla(
    const DdNode * node,
	const int      vCnt,
	const int      cCnt,
	DdString *     str )
{
	FILE *			fp;		// Output file stream
	DdSubstring *	actual;
	int				remlen;
	char            szBuf[MINI_BUFSIZE_S];

	// Open file
	sprintf( szBuf, "%d.pla", (unsigned long)(node) );
	if ( fopen_s( &fp, szBuf, "w" ) ) {
		fprintf( stderr, "\nunable to open pla for write: %s", szBuf ); 
		goto MINI_PLA_WRITE_FAIL_LABEL;
	}

	// Write pla header
	sprintf( szBuf, ".i %d\n.o 1\n.p %d\n", vCnt, cCnt );
	if ( !fwrite( szBuf, strlen(szBuf), 1, fp ) ) {
		fprintf( stderr, "\nunable to write pla header: %d.pla", (unsigned long)(node) );
		goto MINI_PLA_WRITE_FAIL_LABEL;
	}
	// Write clauses to file and close file
	actual = str->first;
	remlen = str->length;
	while ( remlen > MINI_SUBSTRING_LEN ) {
		if ( !fwrite( actual->data, MINI_SUBSTRING_LEN, 1, fp ) ) {
			fprintf( stderr, "\nunable to write clause to pla: %d.pla", (unsigned long)(node) );
			goto MINI_PLA_WRITE_FAIL_LABEL;
		}
		actual  = actual->next;
		remlen -= MINI_SUBSTRING_LEN;
	}
	if ( !fwrite( actual->data, remlen, 1, fp ) && remlen != 0 ) {
		fprintf( stderr, "\nunable to write clause to pla: %d.pla", (unsigned long)(node) );
		goto MINI_PLA_WRITE_FAIL_LABEL;
	}
	// Write end pla flag
	if ( !fwrite( ".e", 2, 1, fp ) ) {
		fprintf( stderr, "\nunable to write end flag to pla: %d.pla", (unsigned long)(node) );
		goto MINI_PLA_WRITE_FAIL_LABEL;
	}
	// Flush and close file
	fflush( fp );
	fclose( fp );
	return TRUE;

MINI_PLA_WRITE_FAIL_LABEL:

	fflush( fp );
	fclose( fp );
	return FALSE;
}


//
// Final session, joining all vector function PLA's to one multiple-output function PLA
//

int cuddDdMiniGroupJoin(
	DdNode **		   roots,
	const unsigned int inputs,
	const unsigned int outputs,
	const char *       output )
{
	DdNode *     node;
	int          f, i;
	int          vCnt, cCnt, rCnt;
	unsigned int size;
	char         val;
	char         szBuf[MINI_BUFSIZE_L];
	char         szPrefix[MINI_BUFSIZE_L];
	char         szSuffix[MINI_BUFSIZE_L];
	char *       szEnd;
	FILE *       fpOut, *fpIn;

	// Open output file for write
	if ( fopen_s( &fpOut, output, "w" ) ) {
		fprintf( stderr, "\nunable to open pla for write: %s", output );
		return FALSE;
	}

	// Write PLA header
	size = inputs + outputs + 2;
	sprintf( szBuf, ".i %d\n.o %d\n", inputs, outputs );
	if ( !fwrite( szBuf, strlen(szBuf), 1, fpOut ) ) {
		fprintf( stderr, "\nunable to write pla header: %s", output );
		fclose( fpOut );
		return FALSE;
	}
	// Set maximal clauses prefix
	for ( i = 0; i < inputs; i++ )
		szPrefix[i] = '-';
	// Set clauses suffix
	for ( i = 0; i < outputs; i++ )
		szSuffix[i] = '0';
	// Go through all functions of vector
	for ( f = 0; f < outputs; f++ ) 
	{
		node = roots[f];
		// Open PLA of f-th function
		sprintf( szBuf, "%d.pla", (unsigned long)node );
		if ( fopen_s( &fpIn, szBuf, "r" ) ) {
			fprintf( stderr, "\nunable to open pla for read: %s", szBuf ); 
			fclose( fpOut );
			return FALSE;
		}
		// Read number of input variables
		fgets( szBuf, MINI_BUFSIZE_L, fpIn );
		if ( szBuf[0] != '.' || szBuf[1] != 'i' ) {
			fprintf( stderr, "\nbad flag .i position in pla: %d.pla", (unsigned long)node );
			goto MINI_PLA_GROUP_FAIL_LABEL;
		}
		vCnt = (int)( strtod( &szBuf[3], &szEnd ) );
		if ( vCnt == 0 ) {
			fprintf( stderr, "\nillegal variable count in pla: %d.pla", (unsigned long)node );
			goto MINI_PLA_GROUP_FAIL_LABEL;
		}
		rCnt = inputs - vCnt;

		// Read number of output variables
		fgets( szBuf, MINI_BUFSIZE_L, fpIn );
		if ( szBuf[0] != '.' || szBuf[1] != 'o' ) {
			fprintf( stderr, "\nbad flag .o position in pla: %d.pla", (unsigned long)node );
			goto MINI_PLA_GROUP_FAIL_LABEL;
		}

		// Read number of clauses
		fgets( szBuf, MINI_BUFSIZE_L, fpIn );
		if ( szBuf[0] != '.' || szBuf[1] != 'p' ) {
			fprintf( stderr, "\nbad flag .p position in pla: %d.pla", (unsigned long)node );
			goto MINI_PLA_GROUP_FAIL_LABEL;
		}
		cCnt = (int)( strtod( &szBuf[3], &szEnd ) );
		if ( cCnt == 0 ) {
			fclose( fpIn );
			continue;
		}
		// Go through clauses until end of file flag reached
		i = 0;
		while ( 1 ) {
			fgets( szBuf, MINI_BUFSIZE_L, fpIn );
			if ( szBuf[0] == '.' && szBuf[1] == 'e' )
				break;
			if ( feof( fpIn ) ) {
				fprintf( stderr, "\npremature end of pla: %d.pla", (unsigned long)node );
				goto MINI_PLA_GROUP_FAIL_LABEL;
			}
			// Get clause value
			val  = szBuf[vCnt+1];
			// Set multiple-output clause
			memcpy( &szBuf[rCnt], szBuf, vCnt+1 );
			memcpy( szBuf, szPrefix, rCnt );
			memcpy( &szBuf[inputs+1], szSuffix, outputs ); 
			szBuf[f+inputs+1] = val;
			szBuf[size-1]   = '\n';
			// Write clause to output
			if ( !fwrite( szBuf, size, 1, fpOut )  ) {
				fprintf( stderr, "\nunable to write clause to pla: %d.pla", (unsigned long)node );
				goto MINI_PLA_GROUP_FAIL_LABEL;
			}
			i++;
		}
		// Check whether all clauses are red
		if ( i != cCnt ) {
			fprintf( stderr, "\npla clauses count not fit: %d.pla", (unsigned long)node );
			goto MINI_PLA_GROUP_FAIL_LABEL;
		}
		
		// Close input file and delete node's PLA
		fclose( fpIn );
	}
	if ( !fwrite( ".e", 2, 1, fpOut ) ) {
		fprintf( stderr, "\nunable to write end flag to pla: %d.pla", (unsigned long)(node) );
		goto MINI_PLA_GROUP_FAIL_LABEL;	
	}

	fflush( fpOut );
	fclose( fpOut );	
	return TRUE;

MINI_PLA_GROUP_FAIL_LABEL:

	fclose( fpIn );
	fflush( fpOut );
	fclose( fpOut );
	return FALSE;
}


//
// Main minimization routine
//

int Cudd_ddMinimization(
	DdManager *					dd,					// DD Manager
	DdNode **					roots,				// roots of minimized functions
	const unsigned int			inputs,				// input variables count
	const unsigned int			outputs,			// functions count
	const DdMinimizPlaCommand * command,			// Minimization command of PLAs 
	const char *                output )			// Output file of minimization result
{
	DdNode *		node, *son, *ddOne, *ddZero;	// Actual node, son of actual node, node ~ 1, node ~ 0
	DdString		strPla;							// Actual node PLA's
	int	            stackIdx, stackSize;			// Stack position, stack size
	int				idx, key, val;					// Variables of temporary usage
	int				i, vCnt, cCnt;					// Variables count, clauses count of builded minimized node PLA
	unsigned int	f;								// Variables of loops
	char			bCheck, bComplement;			// Check node minimization data flag, build negated function node flag
	char	 		szStr[MINI_BUFSIZE_L];			// Character buffer
	char			szNodeFile[MINI_BUFSIZE_XS];	// Filename charactre buffer
	DdMinimizationData *	data;					// Node minimization data
	DdMinimizStackEntry *	stack;					// Stack
	DdMinimizStackEntry		top;					// Actual top of stack
	// Time measure
	struct _timeb time1, time2;
	int           timer;

	// Check bad cases
	if ( roots == NULL || inputs == 0 || outputs == 0 )
		return FALSE;
	// Check long line of PLA bad cases
	if ( inputs + outputs + 10 > MINI_BUFSIZE_L )
		return FALSE;

	// Constant nodes
	ddOne     = DD_ONE(dd);
	ddZero    = Cudd_Not(ddOne);
	stackSize = inputs;
	stack     = malloc( sizeof(DdMinimizStackEntry) * stackSize );
	if ( stack == NULL ) {
		fprintf( stderr, "\nunable to allocate stack memory" );
		return FALSE;
	}
	if ( !cuddStringInit(&strPla) ) {
		fprintf( stderr, "\nunable to allocate string memory" );
		return FALSE;
	}
	_ftime( &time1 );
	// Initialize minimized function nodes
	if ( !cuddDdMinimizitionInit(dd, roots, inputs, outputs, stack) ) {
		fprintf( stderr, "\ninitialization error" );
		return FALSE;
	}
	_ftime( &time2 );
	timer = (int)( 1000 * (time2.time - time1.time) + (time2.millitm - time1.millitm) );
	printf( "\nNodes initialization in %d milliseconds !", timer );
	timer = 0;

	// Go through all functions of v-th array
	for ( f = 0; f < outputs; f++ ) 
	{
		// Check constant case
		if ( Cudd_IsConstant(roots[f])) {
			node          = roots[f];
			cCnt          = 0;
			strPla.length = 0;
			if ( node != ddZero ) {
				for ( i = 0; i < inputs; i++ )
					szStr[i] = '-';
				szStr[i++] = ' ';
				szStr[i++] = '1';
				szStr[i++] = '\n';
				szStr[i]   = '\0';
				if ( node != ddOne )
					szStr[i-2] = '-';
				cuddStringAddCharString( &strPla, szStr, strPla.length);
				cCnt++;
			}
			cuddDdMinimizationWritePla( node, inputs, cCnt, &strPla );
			continue;
		}
		// Set root of i-th function node as top, push it on stack
		top.node            = roots[f];
		top.son[MINI_L_IDX] = 
		top.son[MINI_R_IDX] = MINI_STACK_SON_NINIT;
		stackIdx            = 0;
		stack[stackIdx]     = top;
		bCheck              = TRUE;

		// Loop until given function minimized ( Depth first search via stack )
		do 
		{
			top         = stack[stackIdx];
			node        = top.node;
			bComplement = Cudd_IsComplement(node);
			// Should check table ?
			if ( bCheck ) {
				data = Cudd_Regular(node)->data;
				idx  = MINI_REGULAR_IDX + bComplement;
				// If node is multiple-referenced in minimized BDDarrays
				if ( data != NULL ) {
					// If node function minimized already, go back in depth first search
					if ( Mini_MinData_Existence(data->flags,idx) ) {
						stackIdx--;
						bCheck = FALSE;
						continue;
					}
				}
			}
			// Check direction of depth search
			if      ( Mini_StackGoL(top) ) {
				son = Cudd_NotCond( Mini_CuddLSon(node), bComplement );
				idx = MINI_L_IDX;
			}
			else if ( Mini_StackGoR(top) ) {
				son = Cudd_NotCond( Mini_CuddRSon(node), bComplement );
				idx = MINI_R_IDX;
			} 
			else { // Mini_StackGoB(top) == TRUE
				// Move back in recursion tree ( join 2 son's PLAs )
				strPla.length = 0; 
				cCnt          = 0;
				vCnt          = stackSize - Cudd_ReadPerm( dd, Cudd_Regular(node)->index );
				
				// LEFT SON

				key = Mini_StackLSon(top);
				// If left son is constant
				if ( Mini_StackConstSon(key) ) {
					// If son is not 0
					if ( key != MINI_STACK_SON_0 ) {
						szStr[0] = MINI_L_VAL;
						for ( i = 1; i < vCnt; i++ )
							szStr[i] = '-';
						szStr[i++] = ' ';
						szStr[i++] = '1';
						szStr[i++] = '\n';
						szStr[i]   = '\0';
						if ( key != MINI_STACK_SON_1 )
							szStr[i-2] = '~';
						cuddStringAddCharString( &strPla, szStr, strPla.length );
						cCnt++;
					}
				}
				else {
					// Left son ~ non-constant function ( stored in PLA file )
					son = Cudd_NotCond( Mini_CuddLSon(node), bComplement );
					// Read non-negated and negated function of son node
					cuddDdMinimizationReadPla( son, MINI_L_VAL, vCnt, &cCnt, &strPla );
					data = Cudd_Regular(son)->data;
					idx = MINI_REGULAR_IDX + Cudd_IsComplement(son); 
					// If son is referenced once or all references processed => son pla files can be deleted
					if ( data == NULL || ++data->refs[idx] >= data->refsCnt[idx] ) {
						sprintf( szNodeFile, "%d.pla", (unsigned long)son );
						remove( szNodeFile );
						// If negated son is all references processed too => we hould free son minimization data
						idx = 1-idx;
						if ( data != NULL && data->refs[idx] >= data->refsCnt[idx] ) {
							free( data );
							Cudd_Regular( son )->data = NULL;
						}
					}
				}

				// RIGHT SON

				key = Mini_StackRSon(top);
				if ( Mini_StackConstSon(key) ) {
					// If son is not 0
					if ( key != MINI_STACK_SON_0 ) {
						szStr[0] = MINI_R_VAL;
						for ( i = 1; i < vCnt; i++ )
							szStr[i] = '-';
						szStr[i++] = ' ';
						szStr[i++] = '1';
						szStr[i++] = '\n';
						szStr[i]   = '\0';
						if ( key != MINI_STACK_SON_1 )
							szStr[i-2] = '~';
						cuddStringAddCharString( &strPla, szStr, strPla.length );
						cCnt++;
					}
				}
				else {
					// Right son ~ non-constant function ( stored in PLA file )
					son = Cudd_NotCond( Mini_CuddRSon(node), bComplement );
					// Read non-negated and negated function of son node
					cuddDdMinimizationReadPla( son, MINI_R_VAL, vCnt, &cCnt, &strPla );
					data = Cudd_Regular(son)->data;
					idx = MINI_REGULAR_IDX + Cudd_IsComplement(son);
					// If son is referenced once or all references processed => son pla files can be deleted
					if ( data == NULL || ++data->refs[idx] >= data->refsCnt[idx] ) {
						sprintf( szNodeFile, "%d.pla", (unsigned long)son );
						remove( szNodeFile );
						// If negated son is all references processed too => we hould free son minimization data
						idx = 1-idx;
						if ( data != NULL && data->refs[idx] >= data->refsCnt[idx] ) {
							free( data );
							Cudd_Regular( son )->data = NULL;
						}
					}
				}

				// Build non-negated node PLA
				cuddDdMinimizationWritePla( node, vCnt, cCnt, &strPla );
				// If not trivial minimization case 
				if ( cCnt > 1 ) {
					sprintf( szStr, "%s %d.pla %s m%d.pla %s", 
						command->prefix, (unsigned long)(node), command->middle, (unsigned long)(node), command->suffix ); 
					
					// External minimization
					_ftime( &time1 );
					system( szStr );
					_ftime( &time2 );
					timer += (int)( 1000 * (time2.time - time1.time) + (time2.millitm - time1.millitm) );

					sprintf( szNodeFile, "%d.pla", (unsigned long)(node) );
					remove( szNodeFile );
					sprintf( szStr, "m%s", szNodeFile );
					rename( szStr, szNodeFile );
				}
				// Set flag that node PLA exists
				data = Cudd_Regular(node)->data;
				if ( data != NULL ) {
					idx         = MINI_REGULAR_IDX + bComplement;
					data->flags = Mini_MinData_Set_Existence(data->flags, idx, TRUE);
				}
				// Decrease stack top position, set don't check table flag
				stackIdx--;
				bCheck = FALSE;
				continue;
			}

			if ( Cudd_IsConstant(son) ) {
				// Son node ~ constant function
				if      ( son == ddOne )
					val = MINI_STACK_SON_1;
				else if ( son == ddZero )
					val = MINI_STACK_SON_0;
				else   // son == DD_X(dd)
					val = MINI_STACK_SON_X;
				
				stack[stackIdx].son[idx] = val;
				bCheck                   = FALSE;
				continue;
			}
			// Son node ~ non-constant function, go to depth
			stack[stackIdx].son[idx] = MINI_STACK_SON_NCONST;
			top.node                 = son;
			top.son[MINI_L_IDX]      = 
			top.son[MINI_R_IDX]      = MINI_STACK_SON_NINIT;
			stack[++stackIdx]        = top;
			bCheck                   = TRUE;
		} 
		while ( stackIdx >= 0 );
	}
	// Join PLAs to one PLA
	sprintf_s( szNodeFile, MINI_BUFSIZE_XS, "%s", output );
	if ( outputs > 1 ) {
		if ( !cuddDdMiniGroupJoin(roots, inputs, outputs, szNodeFile) ) {
			// Free structures
			cuddStringFree( &strPla );
			free( stack );
			return FALSE;
		}
		sprintf( szStr, "%s %s %s m%s %s", command->prefix, szNodeFile, command->middle, szNodeFile, command->suffix ); 
		// External minimization
		_ftime( &time1 );
		system( szStr );
		_ftime( &time2 );
		timer += (int)( 1000 * (time2.time - time1.time) + (time2.millitm - time1.millitm) );

		remove( szNodeFile );
		sprintf( szStr, "m%s", szNodeFile );
		rename( szStr, szNodeFile );
	}
	else {
		node = roots[0];
		sprintf( szStr, "%d.pla", (unsigned long)(node) );
		rename( szStr, szNodeFile );
	}
	printf( "\nExternal minimization takes %d milliseconds !", timer );

	// Free minimization data of vector functions, delete it's PLAs
	for ( f = 0; f < outputs; f++ ) {
		node = roots[f];
		data = Cudd_Regular(node)->data;
		if ( data != NULL ) {
			free(data);
			Cudd_Regular(node)->data = NULL;
		}
		sprintf( szNodeFile, "%d.pla", (unsigned long)(node) );
		remove( szNodeFile );
	}
	// Free structures
	cuddStringFree( &strPla );
	free( stack );
	return TRUE;
}

#endif