+void Gia_ManReadMiniAigNames( char * pFileName, Gia_Man_t * pGia )

+{

+ char * filename3 = Abc_UtilStrsavTwo( pFileName, ".ilo" );

+ FILE * pFile = fopen( filename3, "rb" );

+ if ( pFile )

+ {

+ char Buffer[5000], * pName; int i, iLines = 0;

+ Vec_Ptr_t * vTemp = Vec_PtrAlloc( Gia_ManRegNum(pGia) );

+ assert( pGia->vNamesIn == NULL );

+ pGia->vNamesIn = Vec_PtrAlloc( Gia_ManCiNum(pGia) );

+ assert( pGia->vNamesOut == NULL );

+ pGia->vNamesOut = Vec_PtrAlloc( Gia_ManCoNum(pGia) );

+ while ( fgets(Buffer, 5000, pFile) )

+ {

+ if ( Buffer[strlen(Buffer)-1] == '\n' )

+ Buffer[strlen(Buffer)-1] = 0;

+ if ( iLines < Gia_ManPiNum(pGia) )

+ Vec_PtrPush( pGia->vNamesIn, Abc_UtilStrsav(Buffer) );

+ else if ( iLines < Gia_ManCiNum(pGia) )

+ Vec_PtrPush( vTemp, Abc_UtilStrsav(Buffer) );

+ else

+ Vec_PtrPush( pGia->vNamesOut, Abc_UtilStrsav(Buffer) );

+ iLines++;

+ }

+ Vec_PtrForEachEntry( char *, vTemp, pName, i )

+ {

+ Vec_PtrPush( pGia->vNamesIn, Abc_UtilStrsav(pName) );

+ Vec_PtrPush( pGia->vNamesOut, Abc_UtilStrsavTwo(pName, "_in") );

+ }

+ Vec_PtrFreeFree( vTemp );

+ fclose( pFile );

+ printf( "Read ILO names into file \"%s\".\n", filename3 );

+ }

+ ABC_FREE( filename3 );

+}

+ Gia_Man_t * pTemp, * pGia = Gia_ManFromMiniAig( p, NULL, fGiaSimple );

+ Gia_ManReadMiniAigNames( pFileName, pGia );

+ if ( !Gia_ManIsNormalized(pGia) )

+ {

+ pGia = Gia_ManDupNormalize( pTemp = pGia, 0 );

+ ABC_SWAP( Vec_Ptr_t *, pTemp->vNamesIn, pGia->vNamesIn );

+ ABC_SWAP( Vec_Ptr_t *, pTemp->vNamesOut, pGia->vNamesOut );

+ Gia_ManStop( pTemp );

+ }

+#ifndef _VERIFIC_DATABASE_H_

+#endif

+ assert( p->pArray[2*Id] == MINI_AIG_NULL || p->pArray[2*Id] < 2*Id );

+ assert( p->pArray[2*Id+1] == MINI_AIG_NULL || p->pArray[2*Id+1] < 2*Id );

+ printf( "MiniAIG stats: PI = %d PO = %d FF = %d AND = %d\n", Mini_AigPiNum(p), Mini_AigPoNum(p), Mini_AigRegNum(p), Mini_AigAndNum(p) );

+ if ( Lit0 < Lit1 )

+ Mini_AigPush( p, Lit0, Lit1 );

+ else

+ Mini_AigPush( p, Lit1, Lit0 );

+static int Mini_AigXorSpecial( Mini_Aig_t * p, int Lit0, int Lit1 )

+{

+ int Lit = p->nSize;

+ assert( Lit0 >= 0 && Lit0 < Lit );

+ assert( Lit1 >= 0 && Lit1 < Lit );

+ if ( Lit0 > Lit1 )

+ Mini_AigPush( p, Lit0, Lit1 );

+ else

+ Mini_AigPush( p, Lit1, Lit0 );

+ return Lit;

+}

+static int Mini_AigAndMulti( Mini_Aig_t * p, int * pLits, int nLits )

+{

+ int i;

+ assert( nLits > 0 );

+ while ( nLits > 1 )

+ {

+ for ( i = 0; i < nLits/2; i++ )

+ pLits[i] = Mini_AigAnd(p, pLits[2*i], pLits[2*i+1]);

+ if ( nLits & 1 )

+ pLits[i++] = pLits[nLits-1];

+ nLits = i;

+ }

+ return pLits[0];

+}

+static int Mini_AigMuxMulti( Mini_Aig_t * p, int * pCtrl, int * pData, int nData )

+{

+ int Res0, Res1;

+ assert( nData > 0 );

+ if ( nData == 1 )

+ return pData[0];

+ assert( nData % 2 == 0 );

+ Res0 = Mini_AigMuxMulti( p, pCtrl+1, pData, nData/2 );

+ Res1 = Mini_AigMuxMulti( p, pCtrl+1, pData+nData/2, nData/2 );

+ return Mini_AigMux( p, pCtrl[0], Res1, Res0 );

+}

+ char * pObjIsPi = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) );

+ if ( pFile == NULL ) { printf( "Cannot open output file %s\n", pFileName ); MINI_AIG_FREE( pObjIsPi ); return; }

+ //fprintf( pFile, "// This MiniAIG dump was produced by ABC on %s\n\n", Extra_TimeStamp() );

+ pObjIsPi[i] = 1;

+ fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", pObjIsPi[iFaninLit0 >> 1] ? 'i':'n', iFaninLit0 >> 1 );

+ fprintf( pFile, "%s%c%d", (iFaninLit1 & 1) ? "~":"", pObjIsPi[iFaninLit1 >> 1] ? 'i':'n', iFaninLit1 >> 1 );

+ fprintf( pFile, "%s%c%d", (iFaninLit0 & 1) ? "~":"", pObjIsPi[iFaninLit0 >> 1] ? 'i':'n', iFaninLit0 >> 1 );

+ MINI_AIG_FREE( pObjIsPi );

+// checks if MiniAIG is normalized (first inputs, then internal nodes, then outputs)

+static int Mini_AigIsNormalized( Mini_Aig_t * p )

+{

+ int nCiNum = Mini_AigPiNum(p);

+ int nCoNum = Mini_AigPoNum(p);

+ int i, nOffset = 1;

+ for ( i = 0; i < nCiNum; i++ )

+ if ( !Mini_AigNodeIsPi( p, nOffset+i ) )

+ return 0;

+ nOffset = Mini_AigNodeNum(p) - nCoNum;

+ for ( i = 0; i < nCoNum; i++ )

+ if ( !Mini_AigNodeIsPo( p, nOffset+i ) )

+ return 0;

+ return 1;

+}

+

+

+////////////////////////////////////////////////////////////////////////

+/// MiniAIG reading from / write into AIGER ///

+////////////////////////////////////////////////////////////////////////

+

+static unsigned Mini_AigerReadUnsigned( FILE * pFile )

+{

+ unsigned x = 0, i = 0;

+ unsigned char ch;

+ while ((ch = fgetc(pFile)) & 0x80)

+ x |= (ch & 0x7f) << (7 * i++);

+ return x | (ch << (7 * i));

+}

+static void Mini_AigerWriteUnsigned( FILE * pFile, unsigned x )

+{

+ unsigned char ch;

+ while (x & ~0x7f)

+ {

+ ch = (x & 0x7f) | 0x80;

+ fputc( ch, pFile );

+ x >>= 7;

+ }

+ ch = x;

+ fputc( ch, pFile );

+}

+static int * Mini_AigerReadInt( char * pFileName, int * pnObjs, int * pnIns, int * pnLatches, int * pnOuts, int * pnAnds )

+{

+ int i, Temp, nTotal, nObjs, nIns, nLatches, nOuts, nAnds, * pObjs;

+ FILE * pFile = fopen( pFileName, "rb" );

+ if ( pFile == NULL )

+ {

+ fprintf( stdout, "Mini_AigerRead(): Cannot open the output file \"%s\".\n", pFileName );

+ return NULL;

+ }

+ if ( fgetc(pFile) != 'a' || fgetc(pFile) != 'i' || fgetc(pFile) != 'g' )

+ {

+ fprintf( stdout, "Mini_AigerRead(): Can only read binary AIGER.\n" );

+ fclose( pFile );

+ return NULL;

+ }

+ if ( fscanf(pFile, "%d %d %d %d %d", &nTotal, &nIns, &nLatches, &nOuts, &nAnds) != 5 )

+ {

+ fprintf( stdout, "Mini_AigerRead(): Cannot read the header line.\n" );

+ fclose( pFile );

+ return NULL;

+ }

+ if ( nTotal != nIns + nLatches + nAnds )

+ {

+ fprintf( stdout, "The number of objects does not match.\n" );

+ fclose( pFile );

+ return NULL;

+ }

+ nObjs = 1 + nIns + 2*nLatches + nOuts + nAnds;

+ pObjs = MINI_AIG_CALLOC( int, nObjs * 2 );

+ for ( i = 0; i <= nIns + nLatches; i++ )

+ pObjs[2*i] = pObjs[2*i+1] = MINI_AIG_NULL;

+ // read flop input literals

+ for ( i = 0; i < nLatches; i++ )

+ {

+ while ( fgetc(pFile) != '\n' );

+ fscanf( pFile, "%d", &Temp );

+ pObjs[2*(nObjs-nLatches+i)+0] = Temp;

+ pObjs[2*(nObjs-nLatches+i)+1] = MINI_AIG_NULL;

+ }

+ // read output literals

+ for ( i = 0; i < nOuts; i++ )

+ {

+ while ( fgetc(pFile) != '\n' );

+ fscanf( pFile, "%d", &Temp );

+ pObjs[2*(nObjs-nOuts-nLatches+i)+0] = Temp;

+ pObjs[2*(nObjs-nOuts-nLatches+i)+1] = MINI_AIG_NULL;

+ }

+ // read the binary part

+ while ( fgetc(pFile) != '\n' );

+ for ( i = 0; i < nAnds; i++ )

+ {

+ int uLit = 2*(1+nIns+nLatches+i);

+ int uLit1 = uLit - Mini_AigerReadUnsigned( pFile );

+ int uLit0 = uLit1 - Mini_AigerReadUnsigned( pFile );

+ pObjs[uLit+0] = uLit0;

+ pObjs[uLit+1] = uLit1;

+ }

+ fclose( pFile );

+ if ( pnObjs ) *pnObjs = nObjs;

+ if ( pnIns ) *pnIns = nIns;

+ if ( pnLatches ) *pnLatches = nLatches;

+ if ( pnOuts ) *pnOuts = nOuts;

+ if ( pnAnds ) *pnAnds = nAnds;

+ return pObjs;

+}

+static Mini_Aig_t * Mini_AigerRead( char * pFileName, int fVerbose )

+{

+ Mini_Aig_t * p;

+ int nObjs, nIns, nLatches, nOuts, nAnds, * pObjs = Mini_AigerReadInt( pFileName, &nObjs, &nIns, &nLatches, &nOuts, &nAnds );

+ if ( pObjs == NULL )

+ return NULL;

+ p = MINI_AIG_CALLOC( Mini_Aig_t, 1 );

+ p->nCap = 2*nObjs;

+ p->nSize = 2*nObjs;

+ p->nRegs = nLatches;

+ p->pArray = pObjs;

+ if ( fVerbose )

+ printf( "Loaded MiniAIG from the AIGER file \"%s\".\n", pFileName );

+ return p;

+}

+

+static void Mini_AigerWriteInt( char * pFileName, int * pObjs, int nObjs, int nIns, int nLatches, int nOuts, int nAnds )

+{

+ FILE * pFile = fopen( pFileName, "wb" ); int i;

+ if ( pFile == NULL )

+ {

+ fprintf( stdout, "Mini_AigerWrite(): Cannot open the output file \"%s\".\n", pFileName );

+ return;

+ }

+ fprintf( pFile, "aig %d %d %d %d %d\n", nIns + nLatches + nAnds, nIns, nLatches, nOuts, nAnds );

+ for ( i = 0; i < nLatches; i++ )

+ fprintf( pFile, "%d\n", pObjs[2*(nObjs-nLatches+i)+0] );

+ for ( i = 0; i < nOuts; i++ )

+ fprintf( pFile, "%d\n", pObjs[2*(nObjs-nOuts-nLatches+i)+0] );

+ for ( i = 0; i < nAnds; i++ )

+ {

+ int uLit = 2*(1+nIns+nLatches+i);

+ int uLit0 = pObjs[uLit+0];

+ int uLit1 = pObjs[uLit+1];

+ Mini_AigerWriteUnsigned( pFile, uLit - uLit1 );

+ Mini_AigerWriteUnsigned( pFile, uLit1 - uLit0 );

+ }

+ fprintf( pFile, "c\n" );

+ fclose( pFile );

+}

+static void Mini_AigerWrite( char * pFileName, Mini_Aig_t * p, int fVerbose )

+{

+ int i, nIns = 0, nOuts = 0, nAnds = 0;

+ assert( Mini_AigIsNormalized(p) );

+ for ( i = 1; i < Mini_AigNodeNum(p); i++ )

+ {

+ if ( Mini_AigNodeIsPi(p, i) )

+ nIns++;

+ else if ( Mini_AigNodeIsPo(p, i) )

+ nOuts++;

+ else

+ nAnds++;

+ }

+ Mini_AigerWriteInt( pFileName, p->pArray, p->nSize/2, nIns - p->nRegs, p->nRegs, nOuts - p->nRegs, nAnds );

+ if ( fVerbose )

+ printf( "Written MiniAIG into the AIGER file \"%s\".\n", pFileName );

+}

+static void Mini_AigerTest( char * pFileNameIn, char * pFileNameOut )

+{

+ Mini_Aig_t * p = Mini_AigerRead( pFileNameIn, 1 );

+ if ( p == NULL )

+ return;

+ printf( "Finished reading input file \"%s\".\n", pFileNameIn );

+ Mini_AigerWrite( pFileNameOut, p, 1 );

+ printf( "Finished writing output file \"%s\".\n", pFileNameOut );

+ Mini_AigStop( p );

+}

+

+/*

+int main( int argc, char ** argv )

+{

+ if ( argc != 3 )

+ return 0;

+ Mini_AigerTest( argv[1], argv[2] );

+ return 1;

+}

+*/

+

+#ifndef _VERIFIC_DATABASE_H_

+#endif