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

  FileName    [cuddLoadPla.c]

  PackageName [cudd]

  Synopsis    [Loading functions for loading bool. functions in PLA file 
  to BDDs.]

  Description [External procedures included in this module:
		<ul>
		<li> Cudd_plaLoad()
		</ul>
	Internal procedures included in this module:
		<ul>
		<li> cuddPlaFileLoad()
		<li> cuddPlaFreeData()
		</ul>]

  Author      [Ondrej Kolos, modified by Pavel Cerny]

  Copyright   [Copyright (c) 2007-2008, CTU 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 CTU FEL 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"

/**Function********************************************************************

  Synopsis    [Loads boolean function in PLA file format to BDDs.]
  
  Description [Main routine loads boolean function in PLA format 
  in stored in file to internal PlaData structure and then builds 
  BDDs from this structure. In case of incompletely specified function
  is this function loaded to 2 BDDs.]

  SideEffects [None]

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

#define CUDD_PLA_LOAD_0        0
#define CUDD_PLA_LOAD_1        1
#define CUDD_PLA_LOAD_X        2
#define CUDD_PLA_LOAD_N        3

#define CUDD_PLA_LOAD_TYPE_F   0
#define CUDD_PLA_LOAD_TYPE_R   1
#define CUDD_PLA_LOAD_TYPE_FD  2
#define CUDD_PLA_LOAD_TYPE_FR  3
#define CUDD_PLA_LOAD_TYPE_DR  4
#define CUDD_PLA_LOAD_TYPE_FDR 5


struct BddArray * Cudd_plaLoad(
	DdManager * ddMgr, 
	FILE *      fp,
	const int * specVec1,
	const int * specVec2 )
{
	struct PlaData  * data;
	struct BddArray * rval;
	struct PlaArray	* temp;
	DdNode **         terms, **vec[3];
	DdNode *          f, *f0, *f1, * fX, *var,* tmp, *tmp2, *incomp;
	int               i, j, val;
	char              bSingleton;
	char              plaType;
	
	// break if null file pointer
	if ( !fp ) {
  		fprintf( stderr, "\nno file to load." );
		return NULL;
    }
	// set singelton/pair BDDvector(-s) flag
	bSingleton = ( specVec2[0] == specVec2[1] && specVec2[1] == specVec2[2] ) ? TRUE : FALSE;
	// load function from file to internal form, break if not succeed
	data = cuddPlaFileLoad( fp );
	if ( !data ) {
		fprintf( stderr,"\nerror during loading file to internal form." );
		return NULL;
	}
	// memory alocation
	terms                = ( DdNode** )malloc( sizeof( DdNode* ) * data->terms );
	vec[CUDD_PLA_LOAD_0] = ( DdNode** )malloc( sizeof( DdNode* ) * data->outputs );
	vec[CUDD_PLA_LOAD_1] = ( DdNode** )malloc( sizeof( DdNode* ) * data->outputs );
	vec[CUDD_PLA_LOAD_X] = ( DdNode** )malloc( sizeof( DdNode* ) * data->outputs );
	rval                 = ( BddArray* )malloc( sizeof( struct BddArray ) );
	rval->roots          = ( DdNode** )malloc( sizeof( DdNode* ) * data->outputs );
	rval->roots2         = bSingleton == FALSE ? ( DdNode** ) malloc( sizeof( DdNode* ) * data->outputs ) : NULL;
	// break if allocation failed
	if ( !terms || !vec[CUDD_PLA_LOAD_0] || !vec[CUDD_PLA_LOAD_1] || !vec[CUDD_PLA_LOAD_X] || 
		 !rval || !rval->roots || ( bSingleton == FALSE && !rval->roots2 ) ) {
		fprintf( stderr,"\ncan't allocate memory." );
		cuddPlaFreeData( data, 0 );
		if ( terms )
			free( terms );
		if ( vec[CUDD_PLA_LOAD_0] )
			free( vec[CUDD_PLA_LOAD_0] );
		if ( vec[CUDD_PLA_LOAD_1] )
			free( vec[CUDD_PLA_LOAD_1] );
		if ( vec[CUDD_PLA_LOAD_X] )
			free( vec[CUDD_PLA_LOAD_X] );
		if ( rval->roots )
			free( rval->roots );
		if ( rval->roots2 )
			free( rval->roots2 );
		if ( rval )
			free( rval );
		return NULL;
	}
	rval->inames  = data->inames;
	rval->onames  = data->onames;
	rval->outputs = data->outputs;
	rval->inputs  = data->inputs;
	plaType       = data->plaType;

	// build terms ( temporary )
	temp = data->iplaArray;
	for ( i = 0; i < data->terms && temp; i++ )
	{
		f = Cudd_ReadOne( ddMgr );
		Cudd_Ref( f );
		// go through term variables and build term incrementaly
		for ( j = data->inputs - 1; j >= 0; j-- )
		{
			// If x_j = X
			val = temp->line[j];
			if ( val == CUDD_PLA_LOAD_X )
				continue;
			var = Cudd_bddIthVar( ddMgr, j );
			// If x_j = 1 
			if ( val == CUDD_PLA_LOAD_0 )
				var = Cudd_Not( var );
			tmp = Cudd_bddAnd( ddMgr, var, f );
			Cudd_Ref( tmp );
			Cudd_RecursiveDeref( ddMgr, f );
			f   = tmp;
		}
		// set bdd root of term
		terms[i] = f;
		// get next term
		temp = temp->next;
	}
	// Building of output functions
	//
	// If PLA TYPE ~ .type f, take into account only terms t, where val(t) = 1.
	// If PLA TYPE ~ .type r, take into account only terms t, where val(t) = 0.
	// If PLA TYPE ~ .type fr, take into account only terms t, where val(t) = 1 or val(t) = 0.
	// If PLA TYPE ~ .type fd, take into account only terms t, where val(t) = 1 or val(t) = X.
	// If PLA TYPE ~ .type dr, take into account only terms t, where val(t) = X or val(t) = 0.
	// If PLA TYPE ~ .type fdr, take into account all terms t, where val(t) = 1 or val(t) = 0 or val(t) = X.
	//
	// In last two PLA TYPES for every t with val(t) = 1 and val(t) = X is val(t) = X privileged. So we cannot 
	// build diagrams directly, because in direct creation ( go trough all terms t and sum all t with give value 
	// possibly ) is for t with val(t) = 1 and val(t) = X value val(t) = 1 privileged. Instead of we build two 
	// completely specified diagrams D1 where (0,1,X) -> (0,1,1), D2 where (0,1,X) -> (0,1,0). If D3 = !(!D1 + D2), 
	// then D = D3 + X.D2 corresponds to PLA function and satisfies precedence X before 1.
	//
	// So for cohesive implementation, we build for every PLA TYPE completely specified diagrams f0 where 
	// (0,1,X) -> (1,0,0), f1 where (0,1,X) -> (0,0,1) and fX where (0,1,X) -> (0,0,1), then from them we 
	// build result functions. 
	for ( i = 0; i < data->outputs; i++ )
	{
		tmp  = NULL;
		f0   = NULL;
		f1   = NULL;
		fX   = NULL;
		temp = data->oplaArray;
		// go through all term outputs

		// PLA TYPE ~ .type f
		if ( plaType == CUDD_PLA_LOAD_TYPE_F )
		{
			for ( j = 0; j < data->terms && temp; j++ ) 
			{
				val = temp->line[i];
				if ( val == CUDD_PLA_LOAD_1 ) {
					// If f1 already initialized
					if ( f1 ) {
						tmp = Cudd_bddOr( ddMgr, f1, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, f1 );
						f1   = tmp;
					}
					else {
						f1 = terms[j];
						Cudd_Ref( f1 );
					}
				}
				temp = temp->next;
			}
			if ( !f1 ) {
				// f1 ~ const 0
				f1 = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( f1 );
			}
			// OFF-set is complement of ON set
			f0 = Cudd_Not( f1 );
			Cudd_Ref( f0 );
			// DC-set is empty
			fX = Cudd_Not( Cudd_ReadOne( ddMgr ) );
			Cudd_Ref( fX );
		}
		// PLA TYPE ~ .type r
		if ( plaType == CUDD_PLA_LOAD_TYPE_R )
		{
			for ( j = 0; j < data->terms && temp; j++ ) 
			{
				val = temp->line[i];
				if ( val == CUDD_PLA_LOAD_0 ) {
					// If f1 already initialized
					if ( f0 ) {
						tmp = Cudd_bddOr( ddMgr, f0, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, f0 );
						f0   = tmp;
					}
					else {
						f0 = terms[j];
						Cudd_Ref( f0 );
					}
				}
				temp = temp->next;
			}
			if ( !f0 ) {
				// f1 ~ const 0
				f0 = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( f0 );
			}
			// ON-set is complement of ON set
			f1 = Cudd_Not( f0 );
			Cudd_Ref( f1 );
			// DC-set is empty
			fX = Cudd_Not( Cudd_ReadOne( ddMgr ) );
			Cudd_Ref( fX );
		}
		// PLA TYPE ~ .type fd or PLA TYPE ~ .type fdr
		else if ( plaType == CUDD_PLA_LOAD_TYPE_FD || plaType == CUDD_PLA_LOAD_TYPE_FDR ) {
			for ( j = 0; j < data->terms && temp; j++ ) 
			{
				val = temp->line[i];
				if      ( val == CUDD_PLA_LOAD_1 || val == CUDD_PLA_LOAD_X ) {
					// If f0 already initialized
					if ( f0 ) {
						tmp = Cudd_bddOr( ddMgr, f0, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, f0 );
						f0   = tmp;
					}
					else {
						f0 = terms[j];
						Cudd_Ref( f0 );
					}
				}
				if ( val == CUDD_PLA_LOAD_X ) {
					// If fX already initialized
					if ( fX ) {
						tmp = Cudd_bddOr( ddMgr, fX, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, fX );
						fX   = tmp;
					}
					else {
						fX = terms[j];
						Cudd_Ref( fX );
					}
				}
				temp = temp->next;
			}
			if ( !f0 ) {
				// f0 ~ const 0
				f0 = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( f0 );
			}
			if ( !fX ) {
				// fX ~ const 0
				fX = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( fX );
			}
			// we make from (0,1,X) -> (0,1,1) negation (0,1,X) -> (1,0,0) ~ OFF-set
			f0 = Cudd_Not( f0 );
			// ON-set is complement of OFF-set and DC-set union
			f1 = Cudd_Not( Cudd_bddOr( ddMgr, f0, fX ) );
			Cudd_Ref( f1 );
		}
		// PLA TYPE ~ .type fr
		else if ( plaType == CUDD_PLA_LOAD_TYPE_FR ) {
			for ( j = 0; j < data->terms && temp; j++ ) 
			{
				val = temp->line[i];
				if      ( val == CUDD_PLA_LOAD_1 ) {
					// If f1 already initialized
					if ( f1 ) {
						tmp = Cudd_bddOr( ddMgr, f1, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, f1 );
						f1   = tmp;
					}
					else {
						f1 = terms[j];
						Cudd_Ref( f1 );
					}
				}
				else if ( val == CUDD_PLA_LOAD_0 ) {
					// If f0 already initialized
					if ( f0 ) {
						tmp = Cudd_bddOr( ddMgr, f0, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, f0 );
						f0   = tmp;
					}
					else {
						f0 = terms[j];
						Cudd_Ref( f0 );
					}
				}
				temp = temp->next;
			}
			if ( !f1 ) {
				// f1 ~ const 0
				f1 = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( f1 );
			}
			if ( !f0 ) {
				// f0 ~ const 0
				f0 = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( f0 );
			}
			// DC-set is complement of ON-set and OFF-set union
			fX = Cudd_Not( Cudd_bddOr( ddMgr, f1, f0 ) );
			Cudd_Ref( fX );
		}
		// PLA TYPE ~ .type dr
		else if ( plaType == CUDD_PLA_LOAD_TYPE_DR ) {
			for ( j = 0; j < data->terms && temp; j++ ) 
			{
				val = temp->line[i];
				if      ( val == CUDD_PLA_LOAD_0 || val == CUDD_PLA_LOAD_X ) {
					// If f1 already initialized
					if ( f1 ) {
						tmp = Cudd_bddOr( ddMgr, f1, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, f1 );
						f1   = tmp;
					}
					else {
						f1 = terms[j];
						Cudd_Ref( f1 );
					}
				}
				if ( val == CUDD_PLA_LOAD_X ) {
					// If fX already initialized
					if ( fX ) {
						tmp = Cudd_bddOr( ddMgr, fX, terms[j] );
						Cudd_Ref( tmp );
						Cudd_RecursiveDeref( ddMgr, fX );
						fX   = tmp;
					}
					else {
						fX = terms[j];
						Cudd_Ref( fX );
					}
				}
				temp = temp->next;
			}
			if ( !f1 ) {
				// f1 ~ const 0
				f1 = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( f1 );
			}
			if ( !fX ) {
				// fX ~ const 0
				fX = Cudd_Not( Cudd_ReadOne( ddMgr ) );
				Cudd_Ref( fX );
			}
			// we make from (0,1,X) -> (1,1,0) negation (0,1,X) -> (0,0,1) ~ ON-set
			f1 = Cudd_Not( f1 );
			// ON-set is complement of OFF-set and DC-set union
			f0 = Cudd_Not( Cudd_bddOr( ddMgr, f1, fX ) );
			Cudd_Ref( f1 );
		}
		// store OFF-set, ON-set and DC-set
		vec[CUDD_PLA_LOAD_0][i] = f0;
		vec[CUDD_PLA_LOAD_1][i] = f1;
		vec[CUDD_PLA_LOAD_X][i] = fX;
	}

	// final step: build roots
	for ( i = 0; i < data->outputs; i++ ) {
		f = Cudd_Not( Cudd_ReadOne( ddMgr ) );
		Cudd_Ref( f );
		// build first root
		for ( j = 0; j < 3; j++ ) {
			if      ( specVec1[j] == CUDD_PLA_LOAD_1 ) {
				tmp = Cudd_bddOrIncomp( ddMgr, f, vec[j][i] );
				Cudd_Ref( tmp );
				Cudd_RecursiveDeref( ddMgr, f );
				f   = tmp;
			}
			else if ( specVec1[j] == CUDD_PLA_LOAD_X ) {
				incomp = Cudd_ReadIncomplete( ddMgr );
				Cudd_Ref( incomp );
				tmp  = Cudd_bddAndIncomp( ddMgr, incomp, vec[j][i] );
				Cudd_Ref( tmp );
				Cudd_Deref( incomp );
				tmp2 = Cudd_bddOrIncomp( ddMgr, f, tmp );
				Cudd_Ref( tmp2 );
				Cudd_RecursiveDeref( ddMgr, tmp );
				Cudd_RecursiveDeref( ddMgr, f );
				f = tmp2;
			}
		}
		// set first root
		rval->roots[i] = f;
		// if not singleton, build second root
		if ( bSingleton == FALSE ) {
			f = Cudd_Not( Cudd_ReadOne( ddMgr ) );
			Cudd_Ref( f );
			for ( j = 0; j < 3; j++ ) {
				if      ( specVec2[j] == CUDD_PLA_LOAD_1 ) {
					tmp = Cudd_bddOrIncomp( ddMgr, f, vec[j][i] );
					Cudd_Ref( tmp );
					Cudd_RecursiveDeref( ddMgr, f );
					f   = tmp;
				}
				else if ( specVec2[j] == CUDD_PLA_LOAD_X ) {
					incomp = Cudd_ReadIncomplete( ddMgr );
					Cudd_Ref( incomp );
					tmp  = Cudd_bddAndIncomp( ddMgr, incomp, vec[j][i] );
					Cudd_Ref( tmp );
					Cudd_Deref( incomp );
					tmp2 = Cudd_bddOrIncomp( ddMgr, f, tmp );
					Cudd_Ref( tmp2 );
					Cudd_RecursiveDeref( ddMgr, tmp );
					Cudd_RecursiveDeref( ddMgr, f );
					f = tmp2;
				}
			}
			// set second root
			rval->roots2[i] = f;
		}
	}

	// temporary terms and vectors dereference
	for ( i = 0; i < data->terms; i++ )
		Cudd_RecursiveDeref( ddMgr, terms[i] );
	for ( i = 0; i < data->outputs; i++ ) {
		Cudd_RecursiveDeref( ddMgr, vec[CUDD_PLA_LOAD_0][i] );
		Cudd_RecursiveDeref( ddMgr, vec[CUDD_PLA_LOAD_1][i] );
		Cudd_RecursiveDeref( ddMgr, vec[CUDD_PLA_LOAD_X][i] );
	}
	// free memory
	free( terms );
	free( vec[CUDD_PLA_LOAD_0] );
	free( vec[CUDD_PLA_LOAD_1] );
	free( vec[CUDD_PLA_LOAD_X] );
	// free structure data
	cuddPlaFreeData( data, 1 );
	return rval;

} /* end of Cudd_plaLoad */


/**Function********************************************************************

  Synopsis    [Loads boolean function from PLA file to internal PlaData 
  structure.]
  
  Description [Routine is used in main Cudd_plaLoad routine.]

  SideEffects [None]

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

struct PlaData * cuddPlaFileLoad( FILE * fp )
{
	char        		buf;
	char        		namebuf[40];
	int         		i;
	unsigned int        term;
	struct PlaData *    data;
	struct PlaArray *   itemp,*otemp;
	
	// memory allocation
	data = ( PlaData * )malloc( sizeof( struct PlaData ) );
	// break if unable to allocate mem.
	if ( !data ) {
		fprintf( stderr, "\ncan't allocate memory.");
		return NULL;
	}
	data->iplaArray = NULL;
	data->oplaArray = NULL;
	data->inputs    = 0;
	data->outputs   = 0;
	data->inames    = 0;
	data->onames    = 0;
	data->terms     = 0;
	data->plaType   = CUDD_PLA_LOAD_TYPE_FD;
	term            = 0;
	itemp           = NULL;
	otemp           = NULL;

	// loop while end of file not reached
	while ( !feof( fp ) )
	{
		// get next characters from file until "normal" character loaded
		do {
			buf = fgetc( fp );
		}
		while ( buf == ' ' || buf == '\n' || buf == '.' || buf== '\t' );
		// switch character
		switch ( buf )
		{
			// input variables count flag
			case 'i':
				buf = fgetc( fp );		//rozpoznavani klicovych slov
				switch ( buf )
				{
					case 'l': 
						buf = fgetc( fp );
						if ( buf == 'b' ) {
							if ( data->inputs == 0 ) {
								fprintf( stderr, "\nnumber of inputs missing." );
								cuddPlaFreeData(data,0);
								return NULL;
							}
							else {
								data->inames = ( char** )malloc( sizeof( char* )*data->inputs );
								if ( !data->inames ) {
									fprintf( stderr, "\ncan't allocate memory." );
									cuddPlaFreeData( data, 0 );
									return NULL;
								}
								for ( i = 0; i < data->inputs; i++ )
								{
									fscanf( fp, "%s", &namebuf );
									data->inames[i] = ( char* )malloc( sizeof( char )*strlen( namebuf ) );
									if ( !data->inames[i] ) {
										fprintf( stderr,"\ncan't allocate memory." );
										cuddPlaFreeData( data, 0 );
										return NULL;
									}
									strcpy( data->inames[i], namebuf );
								}
							}
						}
						else {
							fprintf( stderr, "\nunknown identifier.\n" );
							cuddPlaFreeData( data, 0 );
							return NULL;
						}
						break;
					case ' ': 
						fscanf( fp, "%d", &data->inputs );
						break;
					default: 
						fprintf( stderr, "\nunknown identifier.\n" );
						cuddPlaFreeData( data, 0 );
						return NULL;
				}
				break;
			// oputput variables count flag
			case 'o': 
				buf = fgetc( fp );
				switch ( buf )
				{
					case 'b': 
						if ( data->outputs == 0 ) {
							fprintf( stderr, "\nnumber of outputs missing.\n" );
							cuddPlaFreeData( data, 0 );
							return NULL;
						}
						else {
							data->onames = ( char** )malloc( sizeof( char* )*data->outputs );
							if ( !data->onames ) {
            					fprintf( stderr, "\ncan't allocate memory." );
								cuddPlaFreeData( data, 0 );
								return NULL;
							}
							for ( i = 0; i < data->outputs; i++ )
							{
								fscanf( fp, "%s", &namebuf );
								data->onames[i] = ( char* )malloc( sizeof( char )*strlen( namebuf ) );
								if( !data->onames[i] ) {
									fprintf( stderr, "\ncan't allocate memory." );
									cuddPlaFreeData( data, 0 );
									return NULL;
							    }
								strcpy( data->onames[i], namebuf );
							}
						}
						break;
					case ' ': 
						fscanf( fp, "%d", &data->outputs );
						break;
					default: 
						fprintf( stderr, "\nunknown identifier.\n" );
						cuddPlaFreeData( data, 0 );
						return NULL;
				}
				break;
			// terms area
			case 'p':
				fscanf( fp, "%d", &data->terms );
				break;
			case '-':          // nahravani matice hodnot vstupu a vystupu
			case '0':
			case '1': 
				if ( data->inputs == 0 || data->outputs == 0 ) {
					fprintf( stderr, "\nnumer of inputs or outputs missing.\n" );
					cuddPlaFreeData( data, 0 );
					return NULL;
				}                        
				if ( !data->iplaArray ) {
					data->iplaArray = ( PlaArray* )malloc( sizeof ( struct PlaArray ) );
					if ( !data->iplaArray ) {
 						fprintf( stderr, "\ncan't allocate memory." );
						cuddPlaFreeData( data, 0 );
						return NULL;
					}
					itemp       = data->iplaArray;
					itemp->next = NULL;
				}
				else {                      
					itemp->next = ( PlaArray* )malloc( sizeof( struct PlaArray ) );
					if ( !itemp->next ) {
 						fprintf( stderr, "\ncan't allocate memory." );
						cuddPlaFreeData( data, 0 );
						return NULL;
					}
					itemp       = itemp->next;
					itemp->next = NULL;
				}
				itemp->line = ( char* )malloc( sizeof( char )*data->inputs );
				if ( !itemp->line ) {
					fprintf( stderr, "\ncan't allocate memory." );
					cuddPlaFreeData( data, 0 );
					return NULL;
				}
				for ( i = 0; i < data->inputs; i++ )
				{
					while( buf == ' ' || buf == '\n' || buf == '\t' )
						buf = fgetc( fp );
					if      ( buf == '0' )
						itemp->line[i] = CUDD_PLA_LOAD_0;	
					else if ( buf == '1' )
						itemp->line[i] = CUDD_PLA_LOAD_1;
					else if ( buf == '-' )
						itemp->line[i] = CUDD_PLA_LOAD_X;
					else {
						fprintf( stderr, "\nexpected '1', '0' or '-' in term %d.", term + 1 );
						cuddPlaFreeData( data, 0 );
						return NULL;
					}
					buf = fgetc( fp );
				}
				if ( buf != ' ' && buf != '\n' && buf != '\t' ) {
					fprintf( stderr, "\nerror in term %d.", term );
					cuddPlaFreeData( data, 0 );
					return NULL;
				}
				if ( !data->oplaArray ) {
					data->oplaArray = ( PlaArray* )malloc( sizeof ( struct PlaArray ) );
					if( !data->oplaArray ) {
						fprintf( stderr, "\ncan't allocate memory." );
						cuddPlaFreeData( data, 0 );
						return NULL;
					}
					otemp       = data->oplaArray;
					otemp->next = NULL;
				}
				else {
					otemp->next = ( PlaArray* )malloc( sizeof( struct PlaArray ) );
					if( !otemp->next ) {
						fprintf( stderr, "\ncan't allocate memory." );
						cuddPlaFreeData( data, 0 );
						return NULL;
					}
					otemp       = otemp->next;
					otemp->next = NULL;
				}
				otemp->line = ( char* )malloc( sizeof( char )*data->outputs );
				if ( !otemp->line ) {
					fprintf( stderr,"\ncan't allocate memory." );
					cuddPlaFreeData( data, 0 );
					return NULL;
				}
				for ( i = 0; i < data->outputs; i++ )
				{
					buf = fgetc( fp );
					while ( buf == ' ' || buf == '\n'|| buf == '\t' )
						buf = fgetc(fp);
					if      ( buf == '0' )
						otemp->line[i] = CUDD_PLA_LOAD_0;	
					else if ( buf == '1' )
						otemp->line[i] = CUDD_PLA_LOAD_1;
					else if ( buf == '-' )
						otemp->line[i] = CUDD_PLA_LOAD_X;
					else if ( buf == '~' )
						otemp->line[i] = CUDD_PLA_LOAD_N;
					else {
						fprintf( stderr, "\nexpected '1', '0', '-' or '~' in term %d.", term );
						cuddPlaFreeData( data, 0 );
						return NULL;
					}
				}
				term++;
				break;
			// end pla file flag
			case 'e': 
				break;
			case EOF: 
				break;
			default:
				// last possibility: .type
				if ( buf == 't' ) {
					buf = fgetc( fp );
					if ( buf == 'y' ) {
						buf = fgetc( fp );
						if ( buf == 'p' ) {
							buf = fgetc( fp );
							if ( buf == 'e' ) {
								// skip value
								fscanf(fp, "%s", &namebuf[0]);
								if      ( !strcmp("f", &namebuf[0]) )
									data->plaType = CUDD_PLA_LOAD_TYPE_F;
								else if ( !strcmp("r", &namebuf[0]) )
									data->plaType = CUDD_PLA_LOAD_TYPE_R;
								else if ( !strcmp("fd", &namebuf[0]) )
									data->plaType = CUDD_PLA_LOAD_TYPE_FD;
								else if ( !strcmp("fr", &namebuf[0]) )
									data->plaType = CUDD_PLA_LOAD_TYPE_FR;
								else if ( !strcmp("dr", &namebuf[0]) )
									data->plaType = CUDD_PLA_LOAD_TYPE_DR;
								else if ( !strcmp("fdr", &namebuf[0]) )
									data->plaType = CUDD_PLA_LOAD_TYPE_FDR;
								else {
									fprintf( stderr, "\nunknown pla type.\n" );
									cuddPlaFreeData( data, 0 );
									return NULL;
								}
								break;
							}
						}
					}
				}
				fprintf( stderr, "\nunexpected symbol at start of a line.\n" );
				cuddPlaFreeData( data, 0 );
				return NULL;
		}
	}
	// check whether whole matrix was loaded
	if ( data->iplaArray && data->oplaArray ) {
		if ( data->terms && data->terms != term )
			fprintf( stderr, "\nwarning: found %d terms instead %d.\n", term, data->terms );
		data->terms = term;
		return data;
	}
	else {
		fprintf( stderr, "\nunknown error in reading file\n" );
		cuddPlaFreeData( data, 0 );
		return NULL;
	}
}

/**Function********************************************************************

  Synopsis    [Free internal structure of PLA file.]
  
  Description [Frees memory allocated to PlaData structure for storing 
  function.]

  SideEffects [None]

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

void cuddPlaFreeData( 
	struct PlaData * data, 
	int              type )
{
	int 			  i;
	struct PlaArray	* temp, * temp2;
	
	// if nonempty iplaArray (input vectors array), free it
	if ( data->iplaArray && data->inputs > 0 ) {
		for ( temp = data->iplaArray; temp; temp = temp2 )
		{
			free( temp->line );
			temp2 = temp->next;
			free( temp );
		}
	}
	else
		fprintf( stderr, "\nwarning: not freeing iplaArray memory.\n" );
	
	// if nonempty oplaArray (output vectors array), free it
	if ( data->oplaArray && data->outputs > 0 ) {
		for ( temp = data->oplaArray; temp; temp = temp2 )
		{
			free( temp->line );
			temp2 = temp->next;
			free( temp );
		}
	}
	else
		fprintf( stderr, "\nwarning: not freeing oplaArray memory.\n" );

	// if nonempty inames (input variable names array), free it
	if ( data->inames && !type )
		for ( i = 0; i < data->inputs; i++ )
			free( data->inames[i] );

	// if nonempty onames (output variable names array), free it
	if ( data->onames && !type )
		for ( i = 0; i < data->outputs; i++ )
			free( data->onames[i] );

	// free Data structure
	free( data );

} /** end of cuddPlaFreeData */