From c497acde5db6fcc4b7f272c04c65dbcaad7d02a0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 8 Sep 2018 08:30:11 +0300 Subject: Expriments with functions. --- src/opt/dau/dauNpn.c | 228 ++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 188 insertions(+), 40 deletions(-) (limited to 'src/opt') diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c index 7850a9a1..23b1df69 100644 --- a/src/opt/dau/dauNpn.c +++ b/src/opt/dau/dauNpn.c @@ -386,6 +386,45 @@ void Dau_NetworkEnumTest() +/**Function************************************************************* + + Synopsis [Count the number of symmetric pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dau_CountSymms( word t, int nVars ) +{ + word Cof0, Cof1; + int i, j, nPairs = 0; + for ( i = 0; i < nVars; i++ ) + for ( j = 0; j < i; j++ ) + nPairs += Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1); + return nPairs; +} +int Dau_CountCompl1( word t, int v, int nVars ) +{ + word tNew = Abc_Tt6Flip(t, v); + int k; + if ( tNew == ~t ) + return 1; + for ( k = 0; k < nVars; k++ ) if ( k != v ) + if ( tNew == Abc_Tt6Flip(t, k) ) + return 1; + return 0; +} +int Dau_CountCompl( word t, int nVars ) +{ + int i, nPairs = 0; + for ( i = 0; i < nVars; i++ ) + nPairs += Dau_CountCompl1(t, i, nVars); + return nPairs; +} + /**Function************************************************************* Synopsis [Performs exact canonicization of semi-canonical classes.] @@ -449,6 +488,83 @@ void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int fflush(stdout); } +/**Function************************************************************* + + Synopsis [Saving hash tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dau_TablesSave( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Mem_t * vTtMemA, Vec_Int_t * vNodSup, Vec_Int_t * vMapping ) +{ + FILE * pFile; + char FileName[100]; + int i, nWords = Abc_TtWordNum(nInputs); + // functions + sprintf( FileName, "fun%d%d.ttd", nInputs, nVars ); + pFile = fopen( FileName, "wb" ); + for ( i = 0; i < Vec_MemEntryNum(vTtMemA); i++ ) + fwrite( Vec_MemReadEntry(vTtMemA, i), 8, nWords, pFile ); + fwrite( Vec_IntArray(vMapping), 4, Vec_IntSize(vMapping), pFile ); + fclose( pFile ); + // NPN classes + sprintf( FileName, "npn%d%d.ttd", nInputs, nVars ); + pFile = fopen( FileName, "wb" ); + for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ ) + fwrite( Vec_MemReadEntry(vTtMem, i), 8, nWords, pFile ); + fwrite( Vec_IntArray(vNodSup), 4, Vec_IntSize(vNodSup), pFile ); + fclose( pFile ); + printf( "Dumped files with %10d functions and %10d classes.\n", Vec_IntSize(vMapping), Vec_IntSize(vNodSup) ); +} +void Dau_TablesLoad( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Mem_t * vTtMemA, Vec_Int_t * vNodSup, Vec_Int_t * vMapping ) +{ + char FileName1[100], FileName2[100]; + int i, FileSize1, FileSize2, nWords = Abc_TtWordNum(nInputs); + // functions + sprintf( FileName1, "fun%d%d.ttd", nInputs, nVars ); + FileSize1 = Extra_FileSize( FileName1 ); + if ( FileSize1 ) + { + word uTruth; + FILE * pFile = fopen( FileName1, "rb" ); + int nEntries = FileSize1 / 12; + assert( FileSize1 % 12 == 0 ); + for ( i = 0; i < nEntries; i++ ) + { + fread( &uTruth, 8, nWords, pFile ); + Vec_MemHashInsert( vTtMem, &uTruth ); + } + Vec_IntFill( vNodSup, nEntries, -1 ); + fread( Vec_IntArray(vNodSup), 4, Vec_IntSize(vNodSup), pFile ); + fclose( pFile ); + } + // classes + sprintf( FileName2, "npn%d%d.ttd", nInputs, nVars ); + FileSize2 = Extra_FileSize( FileName2 ); + if ( FileSize2 ) + { + word uTruth; + FILE * pFile = fopen( FileName2, "rb" ); + int nEntries = FileSize2 / 12; + assert( FileSize2 % 12 == 0 ); + for ( i = 0; i < nEntries; i++ ) + { + fread( &uTruth, 8, nWords, pFile ); + Vec_MemHashInsert( vTtMemA, &uTruth ); + } + Vec_IntFill( vMapping, nEntries, -1 ); + fread( Vec_IntArray(vMapping), 4, Vec_IntSize(vMapping), pFile ); + fclose( pFile ); + } + if ( FileSize1 ) + printf( "Loaded file \"%s\" with %10d functions and file \"%s\" with %10d classes.\n", + FileName1, FileSize1, FileName2, FileSize2 ); +} + /**Function************************************************************* Synopsis [Function enumeration.] @@ -480,21 +596,37 @@ int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int fflush(stdout); return nNew; } -int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup ) +int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Mem_t * vTtMemA, Vec_Int_t * vNodSup, Vec_Int_t * vMapping ) { - char Perm[16] = {0}; - int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs ); - unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 ); - int nEntries = Vec_MemEntryNum(vTtMem); - int Entry = Vec_MemHashInsert( vTtMem, pCur ); - if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new + int DumpDelta = 100000000; + int nEntries = Vec_MemEntryNum(vTtMemA); + Vec_MemHashInsert( vTtMemA, pCur ); + if ( nEntries == Vec_MemEntryNum(vTtMemA) ) // found in the table - not new return 0; - Phase = 0; - Entry = 0; - // this is a new class - Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew ); - assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) ); - return 1; + else // this is a new function + { + char Perm[16] = {0}; + int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs ); + unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 ); + int nEntries = Vec_MemEntryNum(vTtMem); + int Entry = Vec_MemHashInsert( vTtMem, pCur ); + Vec_IntPush( vMapping, Entry ); + assert( Vec_MemEntryNum(vTtMemA) == Vec_IntSize(vMapping) ); + if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new + { + if ( Vec_IntSize(vMapping) % DumpDelta == 0 ) + Dau_TablesSave( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping ); + return 0; + } + Phase = 0; + //printf( "%d ", Dau_CountCompl(pCur[0], nVarsNew) ); + // this is a new class + Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew ); + assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) ); + if ( Vec_IntSize(vMapping) % DumpDelta == 0 ) + Dau_TablesSave( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping ); + return 1; + } } void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ) { @@ -502,19 +634,31 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ) int nWords = Abc_TtWordNum(nInputs); word nSteps = 0; Abc_TtHieMan_t * pMan = Abc_TtHieManStart( nInputs, 5 ); Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 16 ); + Vec_Mem_t * vTtMemA = Vec_MemAlloc( nWords, 16 ); Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 ); + Vec_Int_t * vMapping = Vec_IntAlloc( 1 << 16 ); int v, g, k, m, n, Entry, nNew, iStart = 1, iStop = 2; word Truth[4] = {0}; assert( nVars >= 3 && nVars <= nInputs && nInputs <= 6 ); - Vec_MemHashAlloc( vTtMem, 1<<16 ); - // add constant 0 - Vec_MemHashInsert( vTtMem, Truth ); - Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0 - // add buffer/inverter - Abc_TtIthVar( Truth, 0, nInputs ); - Abc_TtNot( Truth, nWords ); - Vec_MemHashInsert( vTtMem, Truth ); - Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1 + Vec_MemHashAlloc( vTtMem, 1<<16 ); + Vec_MemHashAlloc( vTtMemA, 1<<16 ); + if ( 0 ) // load from file + Dau_TablesLoad( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping ); + else + { + // add constant 0 + Vec_MemHashInsert( vTtMem, Truth ); + Vec_MemHashInsert( vTtMemA, Truth ); + Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0 + Vec_IntPush( vMapping, 0 ); + // add buffer/inverter + Abc_TtIthVar( Truth, 0, nInputs ); + Abc_TtNot( Truth, nWords ); + Vec_MemHashInsert( vTtMem, Truth ); + Vec_MemHashInsert( vTtMemA, Truth ); + Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1 + Vec_IntPush( vMapping, 1 ); + } Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, nSteps, clk ); // numerate other functions based on how many nodes they have for ( n = 1; n < 32; n++ ) @@ -543,16 +687,16 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ) { tGate = s_Truths6[v] & s_Truths6[nSupp]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vTtMemA, vNodSup, vMapping ); tCur = (tGate & Cof0) | (~tGate & Cof1); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vTtMemA, vNodSup, vMapping ); } else { tGate = s_Truths6[v] ^ s_Truths6[nSupp]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vTtMemA, vNodSup, vMapping ); } } nSteps += 3; @@ -566,23 +710,23 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ) { tGate = s_Truths6[v] & s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tCur = (tGate & Cof0) | (~tGate & Cof1); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tGate = s_Truths6[v] & ~s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tCur = (tGate & Cof0) | (~tGate & Cof1); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); } else { tGate = s_Truths6[v] ^ s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); } nSteps += 5; } @@ -597,37 +741,37 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ) { tGate = s_Truths6[m] & s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tCur = (tGate & Cof0) | (~tGate & Cof1); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tGate = s_Truths6[m] & ~s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tCur = (tGate & Cof0) | (~tGate & Cof1); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tGate = ~s_Truths6[m] & s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tCur = (tGate & Cof0) | (~tGate & Cof1); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tGate = ~s_Truths6[m] & ~s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); tCur = (tGate & Cof0) | (~tGate & Cof1); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); } else { tGate = s_Truths6[m] ^ s_Truths6[k]; tCur = (tGate & Cof1) | (~tGate & Cof0); - Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup ); + Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping ); } nSteps += 9; } @@ -640,12 +784,16 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose ) if ( nNew == 0 ) break; } + Dau_TablesSave( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping ); Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); - //Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n ); + //Dau_ExactNpnPrint( vTtMem, vTtMemA, vNodSup, nVars, nInputs, n ); Abc_TtHieManStop( pMan ); Vec_MemHashFree( vTtMem ); + Vec_MemHashFree( vTtMemA ); Vec_MemFreeP( &vTtMem ); + Vec_MemFreeP( &vTtMemA ); Vec_IntFree( vNodSup ); + Vec_IntFree( vMapping ); fflush(stdout); } -- cgit v1.2.3