/**CFile**************************************************************** FileName [extraUtilPrime.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [extra] Synopsis [Function enumeration.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: extraUtilPrime.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $] ***********************************************************************/ #include #include #include #include #include "misc/vec/vec.h" #include "misc/vec/vecHsh.h" #include "bool/kit/kit.h" #include "misc/extra/extra.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_GenCountDump( Vec_Int_t * vPrimes, int nVars, char * pFileName ) { FILE * pFile; int i, k, Prime; pFile = fopen( pFileName, "wb" ); fprintf( pFile, "# %d prime numbers up to 2^%d generated by ABC on %s\n", Vec_IntSize(vPrimes), nVars, Extra_TimeStamp() ); fprintf( pFile, ".i %d\n", nVars ); fprintf( pFile, ".o %d\n", 1 ); fprintf( pFile, ".p %d\n", Vec_IntSize(vPrimes) ); Vec_IntForEachEntry( vPrimes, Prime, i ) for ( k = nVars-1; k >= 0; k-- ) fprintf( pFile, "%d%s", (Prime >> k)&1, k ? "" : " 1\n" ); fprintf( pFile, ".e\n\n" ); fclose( pFile ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_GenCountHits1( Vec_Bit_t * vMap, Vec_Int_t * vPrimes, int nVars ) { abctime clk = Abc_Clock(); int i, k, Prime, Count = 0; Vec_IntForEachEntry( vPrimes, Prime, i ) { for ( k = 0; k < nVars; k++ ) if ( !Vec_BitEntry(vMap, Prime ^ (1< cube + lit + lit) int Degree; // degree of 2 larger than log2(nCubes) int Mask; // table size (2^Degree) int nEnts; // number of entries }; struct Tab_Ent_t_ { int Table; int Cube; unsigned VarA : 16; unsigned VarB : 16; int Next; }; static inline int * Tab_ManCube( Tab_Man_t * p, int i ) { assert(i >= 0 && i < p->nCubes); return p->pCubes + i * (p->nVars + 1); } static inline Tab_Ent_t * Tab_ManEnt( Tab_Man_t * p, int i ) { assert(i >= -1 && i < p->nTable); return i >= 0 ? p->pTable + i : NULL; } static inline int Tab_ManValue( Tab_Man_t * p, int a ) { assert( a >= 0 && a < 256 ); return s_256Primes[a]; } static inline int Tab_ManFinal( Tab_Man_t * p, int a ) { return a & p->Mask; } static inline word Tab_ManHashValue( Tab_Man_t * p, int * pCube ) { word Value = 0; int i; for ( i = 1; i <= pCube[0]; i++ ) Value += Tab_ManValue( p, pCube[i] ); return Value; } static inline word Tab_ManHashValueWithoutVar( Tab_Man_t * p, int * pCube, int iVar ) { word Value = 0; int i; for ( i = 1; i <= pCube[0]; i++ ) if ( i != iVar ) Value += Tab_ManValue( p, pCube[i] ); return Value; } static inline unsigned Tab_ManHashValueCube( Tab_Man_t * p, int c, int iVar ) { if ( iVar == 0xFFFF ) return (unsigned)(p->pValues[c] % p->nTable); return (unsigned)((p->pValues[c] - Tab_ManValue(p, Tab_ManCube(p, c)[iVar+1])) % p->nTable); } static inline void Tab_ManPrintCube( Tab_Man_t * p, int c, int Var ) { int i, * pCube = Tab_ManCube( p, c ); for ( i = 1; i <= pCube[0]; i++ ) // if ( i == Var + 1 ) // printf( "-" ); // else printf( "%d", !Abc_LitIsCompl(pCube[i]) ); } static inline void Tab_ManHashAdd( Tab_Man_t * p, int Value, int Cube, int VarA, int VarB ) { Tab_Ent_t * pCell = p->pTable + p->nEnts; Tab_Ent_t * pBin = p->pTable + Value; /* printf( "Adding cube " ); Tab_ManPrintCube( p, Cube, VarA ); printf( " with var %d and value %d\n", VarA, Value ); */ if ( pBin->Table >= 0 ) pCell->Next = pBin->Table; pBin->Table = p->nEnts++; pCell->Cube = Cube; pCell->VarA = VarA; pCell->VarB = VarB; } static inline void Tab_ManPrintEntry( Tab_Man_t * p, int e ) { printf( "Entry %10d : ", e ); printf( "Cube %6d ", p->pTable[e].Cube ); printf( "Value %12u ", Tab_ManHashValueCube(p, p->pTable[e].Cube, p->pTable[e].VarA) % p->nTable ); Tab_ManPrintCube( p, p->pTable[e].Cube, p->pTable[e].VarA ); printf( " " ); if ( p->pTable[e].VarA != 0xFFFF ) printf( "%2d ", p->pTable[e].VarA ); else printf( " " ); if ( p->pTable[e].VarB != 0xFFFF ) printf( "%2d ", p->pTable[e].VarB ); else printf( " " ); printf( "\n" ); } static inline void Tab_ManHashCollectBin( Tab_Man_t * p, int Bin, Vec_Int_t * vBin ) { Tab_Ent_t * pEnt = p->pTable + Bin; Vec_IntClear( vBin ); for ( pEnt = Tab_ManEnt(p, pEnt->Table); pEnt; pEnt = Tab_ManEnt(p, pEnt->Next) ) { Vec_IntPush( vBin, pEnt - p->pTable ); //Tab_ManPrintEntry( p, pEnt - p->pTable ); } //printf( "\n" ); } #define Tab_ManForEachCube( p, pCube, c ) \ for ( c = 0; c < p->nCubes && (pCube = Tab_ManCube(p, c)); c++ ) \ if ( pCube[0] == -1 ) {} else #define Tab_ManForEachCubeReverse( p, pCube, c ) \ for ( c = p->nCubes - 1; c >= 0 && (pCube = Tab_ManCube(p, c)); c-- ) \ if ( pCube[0] == -1 ) {} else /**Function************************************************************* Synopsis [Manager manipulation.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Tab_Man_t * Tab_ManAlloc( int nVars, int nCubes ) { Tab_Man_t * p = ABC_CALLOC( Tab_Man_t, 1 ); p->nVars = nVars; p->nCubes = nCubes; p->Degree = Abc_Base2Log((p->nVars + 1) * p->nCubes + 1) + 3; p->Mask = (1 << p->Degree) - 1; //p->nEnts = 1; p->pCubes = ABC_CALLOC( int, p->nCubes * (p->nVars + 1) ); p->pValues = ABC_CALLOC( word, p->nCubes ); // p->pTable = ABC_CALLOC( Tab_Ent_t, (p->Mask + 1) ); printf( "Allocated %.2f MB for cube structure.\n", 4.0 * p->nCubes * (p->nVars + 2) / (1 << 20) ); return p; } void Tab_ManFree( Tab_Man_t * p ) { ABC_FREE( p->pCubes ); ABC_FREE( p->pValues ); ABC_FREE( p->pTable ); ABC_FREE( p ); } void Tab_ManStart( Tab_Man_t * p, Vec_Int_t * vCubes ) { int * pCube, Cube, c, v; p->nLits = 0; Tab_ManForEachCube( p, pCube, c ) { Cube = Vec_IntEntry( vCubes, c ); pCube[0] = p->nVars; for ( v = 0; v < p->nVars; v++ ) pCube[v+1] = Abc_Var2Lit( v, !((Cube >> v) & 1) ); p->pValues[c] = Tab_ManHashValue( p, pCube ); p->nLits += pCube[0]; } } /**Function************************************************************* Synopsis [Find a cube-free divisor of the two cubes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Tab_ManCubeFree( int * pCube1, int * pCube2, Vec_Int_t * vCubeFree ) { int * pBeg1 = pCube1 + 1; // skip variable ID int * pBeg2 = pCube2 + 1; // skip variable ID int * pEnd1 = pBeg1 + pCube1[0]; int * pEnd2 = pBeg2 + pCube2[0]; int Counter = 0, fAttr0 = 0, fAttr1 = 1; Vec_IntClear( vCubeFree ); while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) { if ( *pBeg1 == *pBeg2 ) pBeg1++, pBeg2++, Counter++; else if ( *pBeg1 < *pBeg2 ) Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); else { if ( Vec_IntSize(vCubeFree) == 0 ) fAttr0 = 1, fAttr1 = 0; Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); } } while ( pBeg1 < pEnd1 ) Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg1++, fAttr0) ); while ( pBeg2 < pEnd2 ) Vec_IntPush( vCubeFree, Abc_Var2Lit(*pBeg2++, fAttr1) ); if ( Vec_IntSize(vCubeFree) == 0 ) printf( "The SOP has duplicated cubes.\n" ); else if ( Vec_IntSize(vCubeFree) == 1 ) printf( "The SOP has contained cubes.\n" ); // else if ( Vec_IntSize(vCubeFree) == 2 && Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 0))) == Abc_Lit2Var(Abc_Lit2Var(Vec_IntEntry(vCubeFree, 1))) ) // printf( "The SOP has distance-1 cubes or it is not a prime cover. Please make sure the result verifies.\n" ); assert( !Abc_LitIsCompl(Vec_IntEntry(vCubeFree, 0)) ); return Counter; } int Tab_ManCheckEqual2( int * pCube1, int * pCube2, int Var1, int Var2 ) { int i1, i2; for ( i1 = i2 = 1; ; i1++, i2++ ) { if ( i1 == Var1 ) i1++; if ( i2 == Var2 ) i2++; if ( i1 > pCube1[0] || i2 > pCube2[0] ) return 0; if ( pCube1[i1] != pCube2[i2] ) return 0; if ( i1 == pCube1[0] && i2 == pCube2[0] ) return 1; } } int Tab_ManCheckEqual( int * pCube1, int * pCube2, int Var1, int Var2 ) { int Cube1[32], Cube2[32]; int i, k, nVars1, nVars2; assert( pCube1[0] <= 32 ); assert( pCube2[0] <= 32 ); for ( i = 1, k = 0; i <= pCube1[0]; i++ ) if ( i != Var1 ) Cube1[k++] = pCube1[i]; nVars1 = k; for ( i = 1, k = 0; i <= pCube2[0]; i++ ) if ( i != Var2 ) Cube2[k++] = pCube2[i]; nVars2 = k; if ( nVars1 != nVars2 ) return 0; for ( i = 0; i < nVars1; i++ ) if ( Cube1[i] != Cube2[i] ) return 0; return 1; } /**Function************************************************************* Synopsis [Collecting distance-1 pairs.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Tab_ManCountItems( Tab_Man_t * p, int Dist2, Vec_Int_t ** pvStarts ) { Vec_Int_t * vStarts = Vec_IntAlloc( p->nCubes ); int * pCube, c, Count = 0; Tab_ManForEachCube( p, pCube, c ) { Vec_IntPush( vStarts, Count ); Count += 1 + pCube[0]; if ( Dist2 ) Count += pCube[0] * pCube[0] / 2; } assert( Vec_IntSize(vStarts) == p->nCubes ); if ( pvStarts ) *pvStarts = vStarts; return Count; } Vec_Int_t * Tab_ManCollectDist1( Tab_Man_t * p, int Dist2 ) { Vec_Int_t * vStarts = NULL; // starting mark for each cube int nItems = Tab_ManCountItems( p, Dist2, &vStarts ); // item count int nBits = Abc_Base2Log( nItems ) + 6; // hash table size Vec_Bit_t * vPres = Vec_BitStart( 1 << nBits ); // hash table Vec_Bit_t * vMarks = Vec_BitStart( nItems ); // collisions Vec_Int_t * vUseful = Vec_IntAlloc( 1000 ); // useful pairs Vec_Int_t * vBin = Vec_IntAlloc( 100 ); Vec_Int_t * vCubeFree = Vec_IntAlloc( 100 ); word Value; unsigned Mask = (1 << nBits) - 1; int * pCube, c, a, b, nMarks = 0, nUseful, Entry1, Entry2; // iterate forward Tab_ManForEachCube( p, pCube, c ) { // cube if ( Vec_BitAddEntry(vPres, (int)p->pValues[c] & Mask) ) Vec_BitWriteEntry( vMarks, nMarks, 1 ); nMarks++; // dist1 for ( a = 1; a <= pCube[0]; a++, nMarks++ ) if ( Vec_BitAddEntry(vPres, (int)(p->pValues[c] - Tab_ManValue(p, pCube[a])) & Mask) ) Vec_BitWriteEntry( vMarks, nMarks, 1 ); // dist2 if ( Dist2 ) for ( a = 1; a <= pCube[0]; a++ ) { Value = p->pValues[c] - Tab_ManValue(p, pCube[a]); for ( b = a + 1; b <= pCube[0]; b++, nMarks++ ) if ( Vec_BitAddEntry(vPres, (int)(Value - Tab_ManValue(p, pCube[b])) & Mask) ) Vec_BitWriteEntry( vMarks, nMarks, 1 ); } } assert( nMarks == nItems ); Vec_BitReset( vPres ); // iterate backward nMarks--; Tab_ManForEachCubeReverse( p, pCube, c ) { Value = p->pValues[c]; // dist2 if ( Dist2 ) for ( a = pCube[0]; a >= 1; a-- ) { Value = p->pValues[c] - Tab_ManValue(p, pCube[a]); for ( b = pCube[0]; b >= a + 1; b--, nMarks-- ) if ( Vec_BitAddEntry(vPres, (int)(Value - Tab_ManValue(p, pCube[b])) & Mask) ) Vec_BitWriteEntry( vMarks, nMarks, 1 ); } // dist1 for ( a = pCube[0]; a >= 1; a--, nMarks-- ) if ( Vec_BitAddEntry(vPres, (int)(p->pValues[c] - Tab_ManValue(p, pCube[a])) & Mask) ) Vec_BitWriteEntry( vMarks, nMarks, 1 ); // cube if ( Vec_BitAddEntry(vPres, (int)p->pValues[c] & Mask) ) Vec_BitWriteEntry( vMarks, nMarks, 1 ); nMarks--; } nMarks++; assert( nMarks == 0 ); Vec_BitFree( vPres ); // count useful nUseful = Vec_BitCount( vMarks ); printf( "Items = %d. Bits = %d. Useful = %d. \n", nItems, nBits, nUseful ); // add to the hash table p->nTable = Abc_PrimeCudd(nUseful); p->pTable = ABC_FALLOC( Tab_Ent_t, p->nTable ); printf( "Table %d\n", p->nTable ); Tab_ManForEachCube( p, pCube, c ) { // cube if ( Vec_BitEntry(vMarks, nMarks++) ) Tab_ManHashAdd( p, (int)(p->pValues[c] % p->nTable), c, TAB_UNUSED, TAB_UNUSED ); // dist1 for ( a = 1; a <= pCube[0]; a++, nMarks++ ) if ( Vec_BitEntry(vMarks, nMarks) ) Tab_ManHashAdd( p, (int)((p->pValues[c] - Tab_ManValue(p, pCube[a])) % p->nTable), c, a-1, TAB_UNUSED ); // dist2 if ( Dist2 ) for ( a = 1; a <= pCube[0]; a++ ) { Value = p->pValues[c] - Tab_ManValue(p, pCube[a]); for ( b = a + 1; b <= pCube[0]; b++, nMarks++ ) if ( Vec_BitEntry(vMarks, nMarks) ) Tab_ManHashAdd( p, (int)((Value - Tab_ManValue(p, pCube[b])) % p->nTable), c, a-1, b-1 ); } } assert( nMarks == nItems ); // collect entries for ( c = 0; c < p->nTable; c++ ) { Tab_ManHashCollectBin( p, c, vBin ); //printf( "%d ", Vec_IntSize(vBin) ); //if ( c > 100 ) // break; Vec_IntForEachEntry( vBin, Entry1, a ) Vec_IntForEachEntryStart( vBin, Entry2, b, a + 1 ) { Tab_Ent_t * pEntA = Tab_ManEnt( p, Entry1 ); Tab_Ent_t * pEntB = Tab_ManEnt( p, Entry2 ); int * pCubeA = Tab_ManCube( p, pEntA->Cube ); int * pCubeB = Tab_ManCube( p, pEntB->Cube ); // int Base = Tab_ManCubeFree( pCubeA, pCubeB, vCubeFree ); // if ( Vec_IntSize(vCubeFree) == 2 ) if ( Tab_ManCheckEqual(pCubeA, pCubeB, pEntA->VarA+1, pEntB->VarA+1) ) { Vec_IntPushTwo( vUseful, pEntA->Cube, pEntB->Cube ); } } } //printf( "\n" ); ABC_FREE( p->pTable ); Vec_IntFree( vCubeFree ); Vec_IntFree( vBin ); Vec_BitFree( vMarks ); return vUseful; } /**Function************************************************************* Synopsis [Table decomposition.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Tab_DecomposeTest() { int nVars = 20;// no more than 13 abctime clk = Abc_Clock(); Vec_Int_t * vPairs; Vec_Int_t * vPrimes = Abc_GenPrimes( nVars ); Tab_Man_t * p = Tab_ManAlloc( nVars, Vec_IntSize(vPrimes) ); Tab_ManStart( p, vPrimes ); printf( "Created %d cubes dependent on %d variables.\n", p->nCubes, p->nVars ); vPairs = Tab_ManCollectDist1( p, 0 ); printf( "Collected %d pairs.\n", Vec_IntSize(vPairs)/2 ); Vec_IntFree( vPairs ); Tab_ManFree( p ); Vec_IntFree( vPrimes ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END