From bfa48cef2aab9e21f0fe9bd24a0bcfd7ce464686 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 May 2014 01:12:00 +0900 Subject: Experiment with support minimization. --- src/base/abci/abc.c | 7 + src/misc/extra/extraUtilSupp.c | 499 ++++++++++++++++++++++++++++++++++++----- 2 files changed, 449 insertions(+), 57 deletions(-) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 83fd0933..bdf57e55 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -6330,6 +6330,7 @@ usage: int Abc_CommandVarMin( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose ); + extern void Abc_SuppReadMinTest( char * pFileName ); int nOnes = 4; int nVars = 20; int fUseSimple = 0; @@ -6378,6 +6379,12 @@ int Abc_CommandVarMin( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } + // get the file name + if ( argc == globalUtilOptind + 1 ) + { + Abc_SuppReadMinTest( argv[globalUtilOptind] ); + return 0; + } Abc_SuppTest( nOnes, nVars, fUseSimple, fCheck, fVerbose ); return 0; diff --git a/src/misc/extra/extraUtilSupp.c b/src/misc/extra/extraUtilSupp.c index 44895c58..3cb0296e 100644 --- a/src/misc/extra/extraUtilSupp.c +++ b/src/misc/extra/extraUtilSupp.c @@ -23,6 +23,7 @@ #include #include #include "misc/vec/vec.h" +#include "misc/vec/vecWec.h" ABC_NAMESPACE_IMPL_START @@ -30,10 +31,156 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); + + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Counts the number of unique entries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Vec_IntUniqueHashKeyDebug( unsigned char * pStr, int nChars, int TableMask ) +{ + static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319}; + unsigned Key = 0; int c; + for ( c = 0; c < nChars; c++ ) + { + Key += (unsigned)pStr[c] * s_BigPrimes[c & 3]; + printf( "%d : ", c ); + printf( "%3d ", pStr[c] ); + printf( "%12u ", Key ); + printf( "%12u ", Key&TableMask ); + printf( "\n" ); + } + return Key; +} +void Vec_IntUniqueProfile( Vec_Int_t * vData, int * pTable, int * pNexts, int TableMask, int nIntSize ) +{ + int i, Key, Counter; + for ( i = 0; i <= TableMask; i++ ) + { + Counter = 0; + for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] ) + Counter++; + if ( Counter < 7 ) + continue; + printf( "%d\n", Counter ); + for ( Key = pTable[i]; Key != -1; Key = pNexts[Key] ) + { + Extra_PrintBinary( stdout, Vec_IntEntryP(vData, Key*nIntSize), 40 ), printf( "\n" ); +// Vec_IntUniqueHashKeyDebug( (unsigned char *)Vec_IntEntryP(vData, Key*nIntSize), 4*nIntSize, TableMask ); + } + } + printf( "\n" ); +} + + +static inline unsigned Vec_IntUniqueHashKey2( unsigned char * pStr, int nChars ) +{ + static unsigned s_BigPrimes[4] = {12582917, 25165843, 50331653, 100663319}; + unsigned Key = 0; int c; + for ( c = 0; c < nChars; c++ ) + Key += (unsigned)pStr[c] * s_BigPrimes[c & 3]; + return Key; +} + +static inline unsigned Vec_IntUniqueHashKey( unsigned char * pStr, int nChars ) +{ + static unsigned s_BigPrimes[16] = + { + 0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55, + 0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055 + }; + static unsigned s_BigPrimes2[16] = + { + 0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035, + 0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10 + }; + unsigned Key = 0; int c; + for ( c = 0; c < nChars; c++ ) + Key += s_BigPrimes2[(2*c)&15] * s_BigPrimes[(unsigned)pStr[c] & 15] + + s_BigPrimes2[(2*c+1)&15] * s_BigPrimes[(unsigned)pStr[c] >> 4]; + return Key; +} +static inline int * Vec_IntUniqueLookup( Vec_Int_t * vData, int i, int nIntSize, int * pNexts, int * pStart ) +{ + int * pData = Vec_IntEntryP( vData, i*nIntSize ); + for ( ; *pStart != -1; pStart = pNexts + *pStart ) + if ( !memcmp( pData, Vec_IntEntryP(vData, *pStart*nIntSize), sizeof(int) * nIntSize ) ) + return pStart; + return pStart; +} +static inline int Vec_IntUniqueCount( Vec_Int_t * vData, int nIntSize, Vec_Int_t ** pvMap ) +{ + int nEntries = Vec_IntSize(vData) / nIntSize; + int TableMask = (1 << Abc_Base2Log(nEntries)) - 1; + int * pTable = ABC_FALLOC( int, TableMask+1 ); + int * pNexts = ABC_FALLOC( int, TableMask+1 ); + int * pClass = ABC_ALLOC( int, nEntries ); + int i, Key, * pEnt, nUnique = 0; + assert( nEntries * nIntSize == Vec_IntSize(vData) ); + for ( i = 0; i < nEntries; i++ ) + { + pEnt = Vec_IntEntryP( vData, i*nIntSize ); + Key = TableMask & Vec_IntUniqueHashKey( (unsigned char *)pEnt, 4*nIntSize ); + pEnt = Vec_IntUniqueLookup( vData, i, nIntSize, pNexts, pTable+Key ); + if ( *pEnt == -1 ) + *pEnt = i, nUnique++; + pClass[i] = *pEnt; + } +// Vec_IntUniqueProfile( vData, pTable, pNexts, TableMask, nIntSize ); + ABC_FREE( pTable ); + ABC_FREE( pNexts ); + if ( pvMap ) + *pvMap = Vec_IntAllocArray( pClass, nEntries ); + else + ABC_FREE( pClass ); + return nUnique; +} +static inline Vec_Int_t * Vec_IntUniqifyHash( Vec_Int_t * vData, int nIntSize ) +{ + Vec_Int_t * vMap, * vUnique; + int i, Ent, nUnique = Vec_IntUniqueCount( vData, nIntSize, &vMap ); + vUnique = Vec_IntAlloc( nUnique * nIntSize ); + Vec_IntForEachEntry( vMap, Ent, i ) + { + if ( Ent < i ) continue; + assert( Ent == i ); + Vec_IntPushArray( vUnique, Vec_IntEntryP(vData, i*nIntSize), nIntSize ); + } + assert( Vec_IntSize(vUnique) == nUnique * nIntSize ); + Vec_IntFree( vMap ); + return vUnique; +} +static inline Vec_Wrd_t * Vec_WrdUniqifyHash( Vec_Wrd_t * vData, int nWordSize ) +{ + Vec_Int_t * vResInt; + Vec_Int_t * vDataInt = (Vec_Int_t *)vData; + vDataInt->nSize *= 2; + vDataInt->nCap *= 2; + vResInt = Vec_IntUniqifyHash( vDataInt, 2 * nWordSize ); + vDataInt->nSize /= 2; + vDataInt->nCap /= 2; + vResInt->nSize /= 2; + vResInt->nCap /= 2; + return (Vec_Wrd_t *)vResInt; +} +static inline word * Vec_WrdLimit( Vec_Wrd_t * p ) +{ + return p->pArray + p->nSize; +} + + /**Function************************************************************* Synopsis [Generate m-out-of-n vectors.] @@ -52,13 +199,13 @@ static inline int Abc_SuppCountOnes( unsigned i ) i = ((i + (i >> 4)) & 0x0F0F0F0F); return (i*(0x01010101))>>24; } -Vec_Int_t * Abc_SuppGen( int m, int n ) +Vec_Wrd_t * Abc_SuppGen( int m, int n ) { - Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 ); int i, Size = (1 << n); for ( i = 0; i < Size; i++ ) if ( Abc_SuppCountOnes(i) == m ) - Vec_IntPush( vRes, i ); + Vec_WrdPush( vRes, i ); return vRes; } @@ -73,13 +220,14 @@ Vec_Int_t * Abc_SuppGen( int m, int n ) SeeAlso [] ***********************************************************************/ -void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin ) +void Abc_SuppVerify( Vec_Wrd_t * p, word * pMatrix, int nVars, int nVarsMin ) { - Vec_Int_t * pNew; - int * pLimit, * pEntry1, * pEntry2; - int i, k, v, Entry, EntryNew, Value, Counter = 0; - pNew = Vec_IntAlloc( Vec_IntSize(p) ); - Vec_IntForEachEntry( p, Entry, i ) + Vec_Wrd_t * pNew; + word * pLimit, * pEntry1, * pEntry2; + word Entry, EntryNew; + int i, k, v, Value, Counter = 0; + pNew = Vec_WrdAlloc( Vec_WrdSize(p) ); + Vec_WrdForEachEntry( p, Entry, i ) { EntryNew = 0; for ( v = 0; v < nVarsMin; v++ ) @@ -89,13 +237,13 @@ void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin if ( ((pMatrix[v] >> k) & 1) && ((Entry >> k) & 1) ) Value ^= 1; if ( Value ) - EntryNew |= (1 << v); + EntryNew |= (((word)1) << v); } - Vec_IntPush( pNew, EntryNew ); + Vec_WrdPush( pNew, EntryNew ); } // check that they are disjoint - pLimit = Vec_IntLimit(pNew); - pEntry1 = Vec_IntArray(pNew); + pLimit = Vec_WrdLimit(pNew); + pEntry1 = Vec_WrdArray(pNew); for ( ; pEntry1 < pLimit; pEntry1++ ) for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ ) if ( *pEntry1 == *pEntry2 ) @@ -104,7 +252,7 @@ void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin printf( "The total of %d pairs fail verification.\n", Counter ); else printf( "Verification successful.\n" ); - Vec_IntFree( pNew ); + Vec_WrdFree( pNew ); } /**Function************************************************************* @@ -118,28 +266,28 @@ void Abc_SuppVerify( Vec_Int_t * p, unsigned * pMatrix, int nVars, int nVarsMin SeeAlso [] ***********************************************************************/ -Vec_Int_t * Abc_SuppGenPairs( Vec_Int_t * p, int nBits ) +Vec_Wrd_t * Abc_SuppGenPairs( Vec_Wrd_t * p, int nBits ) { - Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 ); unsigned * pMap = ABC_CALLOC( unsigned, 1 << Abc_MaxInt(0,nBits-5) ); - int * pLimit = Vec_IntLimit(p); - int * pEntry1 = Vec_IntArray(p); - int * pEntry2, Value; + word * pLimit = Vec_WrdLimit(p); + word * pEntry1 = Vec_WrdArray(p); + word * pEntry2, Value; for ( ; pEntry1 < pLimit; pEntry1++ ) for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ ) { Value = *pEntry1 ^ *pEntry2; - if ( Abc_InfoHasBit(pMap, Value) ) + if ( Abc_InfoHasBit(pMap, (int)Value) ) continue; - Abc_InfoXorBit( pMap, Value ); - Vec_IntPush( vRes, Value ); + Abc_InfoXorBit( pMap, (int)Value ); + Vec_WrdPush( vRes, Value ); } ABC_FREE( pMap ); return vRes; } -Vec_Int_t * Abc_SuppGenPairs2( int nOnes, int nBits ) +Vec_Wrd_t * Abc_SuppGenPairs2( int nOnes, int nBits ) { - Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 ); int i, k, Size = (1 << nBits), Value; for ( i = 0; i < Size; i++ ) { @@ -148,7 +296,7 @@ Vec_Int_t * Abc_SuppGenPairs2( int nOnes, int nBits ) if ( Value == 2*k ) break; if ( k <= nOnes ) - Vec_IntPush( vRes, i ); + Vec_WrdPush( vRes, i ); } return vRes; } @@ -164,30 +312,31 @@ Vec_Int_t * Abc_SuppGenPairs2( int nOnes, int nBits ) SeeAlso [] ***********************************************************************/ -void Abc_SuppPrintMask( unsigned uMask, int nBits ) +void Abc_SuppPrintMask( word uMask, int nBits ) { int i; for ( i = 0; i < nBits; i++ ) printf( "%d", (uMask >> i) & 1 ); printf( "\n" ); } -void Abc_SuppGenProfile( Vec_Int_t * p, int nBits, int * pCounts ) +void Abc_SuppGenProfile( Vec_Wrd_t * p, int nBits, int * pCounts ) { - int i, k, b, Ent; - Vec_IntForEachEntry( p, Ent, i ) + word Ent; + int i, k, b; + Vec_WrdForEachEntry( p, Ent, i ) for ( b = ((Ent >> nBits) & 1), k = 0; k < nBits; k++ ) pCounts[k] += ((Ent >> k) & 1) ^ b; } -void Abc_SuppPrintProfile( Vec_Int_t * p, int nBits ) +void Abc_SuppPrintProfile( Vec_Wrd_t * p, int nBits ) { - int k, Counts[32] = {0}; + int k, Counts[64] = {0}; Abc_SuppGenProfile( p, nBits, Counts ); for ( k = 0; k < nBits; k++ ) - printf( "%2d : %6d %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_IntSize(p) ); + printf( "%2d : %6d %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_WrdSize(p) ); } -int Abc_SuppGenFindBest( Vec_Int_t * p, int nBits, int * pMerit ) +int Abc_SuppGenFindBest( Vec_Wrd_t * p, int nBits, int * pMerit ) { - int k, kBest = 0, Counts[32] = {0}; + int k, kBest = 0, Counts[64] = {0}; Abc_SuppGenProfile( p, nBits, Counts ); for ( k = 1; k < nBits; k++ ) if ( Counts[kBest] < Counts[k] ) @@ -195,25 +344,26 @@ int Abc_SuppGenFindBest( Vec_Int_t * p, int nBits, int * pMerit ) *pMerit = Counts[kBest]; return kBest; } -void Abc_SuppGenSelectVar( Vec_Int_t * p, int nBits, int iVar ) +void Abc_SuppGenSelectVar( Vec_Wrd_t * p, int nBits, int iVar ) { - int * pEntry = Vec_IntArray(p); - int * pLimit = Vec_IntLimit(p); + word * pEntry = Vec_WrdArray(p); + word * pLimit = Vec_WrdLimit(p); for ( ; pEntry < pLimit; pEntry++ ) if ( (*pEntry >> iVar) & 1 ) - *pEntry ^= (1 << nBits); + *pEntry ^= (((word)1) << nBits); } -void Abc_SuppGenFilter( Vec_Int_t * p, int nBits ) +void Abc_SuppGenFilter( Vec_Wrd_t * p, int nBits ) { - int i, k = 0, Ent; - Vec_IntForEachEntry( p, Ent, i ) + word Ent; + int i, k = 0; + Vec_WrdForEachEntry( p, Ent, i ) if ( ((Ent >> nBits) & 1) == 0 ) - Vec_IntWriteEntry( p, k++, Ent ); - Vec_IntShrink( p, k ); + Vec_WrdWriteEntry( p, k++, Ent ); + Vec_WrdShrink( p, k ); } -unsigned Abc_SuppFindOne( Vec_Int_t * p, int nBits ) +word Abc_SuppFindOne( Vec_Wrd_t * p, int nBits ) { - unsigned uMask = 0; + word uMask = 0; int Prev = -1, This, Var; while ( 1 ) { @@ -222,14 +372,14 @@ unsigned Abc_SuppFindOne( Vec_Int_t * p, int nBits ) break; Prev = This; Abc_SuppGenSelectVar( p, nBits, Var ); - uMask |= (1 << Var); + uMask |= (((word)1) << Var); } return uMask; } -int Abc_SuppMinimize( unsigned * pMatrix, Vec_Int_t * p, int nBits, int fVerbose ) +int Abc_SuppMinimize( word * pMatrix, Vec_Wrd_t * p, int nBits, int fVerbose ) { int i; - for ( i = 0; Vec_IntSize(p) > 0; i++ ) + for ( i = 0; Vec_WrdSize(p) > 0; i++ ) { // Abc_SuppPrintProfile( p, nBits ); pMatrix[i] = Abc_SuppFindOne( p, nBits ); @@ -238,7 +388,7 @@ int Abc_SuppMinimize( unsigned * pMatrix, Vec_Int_t * p, int nBits, int fVerbose continue; // print stats printf( "%2d : ", i ); - printf( "%6d ", Vec_IntSize(p) ); + printf( "%6d ", Vec_WrdSize(p) ); Abc_SuppPrintMask( pMatrix[i], nBits ); // printf( "\n" ); } @@ -259,16 +409,16 @@ int Abc_SuppMinimize( unsigned * pMatrix, Vec_Int_t * p, int nBits, int fVerbose void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose ) { int nVarsMin; - unsigned Matrix[100]; + word Matrix[64]; abctime clk = Abc_Clock(); // create the problem - Vec_Int_t * vRes = Abc_SuppGen( nOnes, nVars ); - Vec_Int_t * vPairs = fUseSimple ? Abc_SuppGenPairs2( nOnes, nVars ) : Abc_SuppGenPairs( vRes, nVars ); + Vec_Wrd_t * vRes = Abc_SuppGen( nOnes, nVars ); + Vec_Wrd_t * vPairs = fUseSimple ? Abc_SuppGenPairs2( nOnes, nVars ) : Abc_SuppGenPairs( vRes, nVars ); assert( nVars < 100 ); printf( "M = %2d N = %2d : ", nOnes, nVars ); - printf( "K = %6d ", Vec_IntSize(vRes) ); - printf( "Total = %12.0f ", 0.5 * Vec_IntSize(vRes) * (Vec_IntSize(vRes) - 1) ); - printf( "Distinct = %8d ", Vec_IntSize(vPairs) ); + printf( "K = %6d ", Vec_WrdSize(vRes) ); + printf( "Total = %12.0f ", 0.5 * Vec_WrdSize(vRes) * (Vec_WrdSize(vRes) - 1) ); + printf( "Distinct = %8d ", Vec_WrdSize(vPairs) ); Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk ); // solve the problem clk = Abc_Clock(); @@ -277,8 +427,243 @@ void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbos Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk ); if ( fCheck ) Abc_SuppVerify( vRes, Matrix, nVars, nVarsMin ); - Vec_IntFree( vPairs ); - Vec_IntFree( vRes ); + Vec_WrdFree( vPairs ); + Vec_WrdFree( vRes ); +} + + +/**Function************************************************************* + + Synopsis [Reads the input part of the cubes specified in MIN format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Abc_SuppReadMin( char * pFileName, int * pnVars ) +{ + extern char * Extra_FileReadContents( char * pFileName ); + Vec_Wrd_t * vRes; word uCube; + int nCubes = 0, nVars = -1, iVar; + char * pCur, * pToken, * pStart = "INPUT F-COVER"; + char * pStr = Extra_FileReadContents( pFileName ); + if ( pStr == NULL ) + { printf( "Cannot open input file (%s).\n", pFileName ); return NULL; } + pCur = strstr( pStr, pStart ); + if ( pCur == NULL ) + { printf( "Cannot find beginning of cube cover (%s).\n", pStart ); return NULL; } + pToken = strtok( pCur + strlen(pStart), " \t\r\n," ); + nCubes = atoi( pToken ); + if ( nCubes < 1 || nCubes > 1000000 ) + { printf( "The number of cubes in not in the range [1; 1000000].\n" ); return NULL; } + vRes = Vec_WrdAlloc( 1000 ); + uCube = 0; iVar = 0; + while ( (pToken = strtok(NULL, " \t\r\n,")) != NULL ) + { + if ( strlen(pToken) > 2 ) + { + if ( !strncmp(pToken, "INPUT", strlen("INPUT")) ) + break; + if ( iVar > 64 ) + { printf( "The number of inputs (%d) is too high.\n", iVar ); Vec_WrdFree(vRes); return NULL; } + if ( nVars == -1 ) + nVars = iVar; + else if ( nVars != iVar ) + { printf( "The number of inputs (%d) does not match declaration (%d).\n", nVars, iVar ); Vec_WrdFree(vRes); return NULL; } + Vec_WrdPush( vRes, uCube ); + uCube = 0; iVar = 0; + continue; + } + if ( pToken[1] == '0' && pToken[0] == '1' ) // value 1 + uCube |= (((word)1) << iVar); + else if ( pToken[1] != '1' || pToken[0] != '0' ) // value 0 + { printf( "Strange literal representation (%s) of cube %d.\n", pToken, nCubes ); Vec_WrdFree(vRes); return NULL; } + iVar++; + } + ABC_FREE( pStr ); + if ( Vec_WrdSize(vRes) != nCubes ) + { printf( "The number of cubes (%d) does not match declaration (%d).\n", Vec_WrdSize(vRes), nCubes ); Vec_WrdFree(vRes); return NULL; } + else + printf( "Successfully parsed function with %d inputs and %d cubes.\n", nVars, nCubes ); + *pnVars = nVars; + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Wrd_t * Abc_SuppDiffMatrix( Vec_Wrd_t * vCubes ) +{ + abctime clk = Abc_Clock(); + word * pEnt2, * pEnt = Vec_WrdArray( vCubes ); + word * pLimit = Vec_WrdLimit( vCubes ); + Vec_Wrd_t * vRes, * vPairs = Vec_WrdAlloc( Vec_WrdSize(vCubes) * (Vec_WrdSize(vCubes) - 1) / 2 ); + word * pStore = Vec_WrdArray( vPairs ); + for ( ; pEnt < pLimit; pEnt++ ) + for ( pEnt2 = pEnt+1; pEnt2 < pLimit; pEnt2++ ) + *pStore++ = *pEnt ^ *pEnt2; + vPairs->nSize = Vec_WrdCap(vPairs); + assert( pStore == Vec_WrdLimit(vPairs) ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); +// vRes = Vec_WrdUniqifyHash( vPairs, 1 ); + vRes = Vec_WrdDup( vPairs ); + printf( "Successfully generated diff matrix with %10d rows (%6.2f %%). ", + Vec_WrdSize(vRes), 100.0 * Vec_WrdSize(vRes) / Vec_WrdSize(vPairs) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Vec_WrdFree( vPairs ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Solve difference matrix.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_SuppCountOnes64( word i ) +{ + i = i - ((i >> 1) & 0x5555555555555555); + i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333); + i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F); + return (i*(0x0101010101010101))>>56; +} +int Abc_SuppFindVar( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars ) +{ + int v, vBest = -1, dBest; + for ( v = 0; v < nVars; v++ ) + { + if ( Vec_WecLevelSize(pS, v) ) + continue; + if ( vBest == -1 || dBest > Vec_WecLevelSize(pD, v) ) + vBest = v, dBest = Vec_WecLevelSize(pD, v); + } + return vBest; +} +void Abc_SuppRemove( Vec_Wrd_t * p, int * pCounts, Vec_Wec_t * pS, Vec_Wec_t * pD, int iVar, int nVars ) +{ + word Entry; int i, v; + assert( Vec_WecLevelSize(pS, iVar) == 0 ); + Vec_IntClear( Vec_WecEntry(pD, iVar) ); + Vec_WrdForEachEntry( p, Entry, i ) + { + if ( ((Entry >> iVar) & 1) == 0 ) + continue; + pCounts[i]--; + if ( pCounts[i] == 1 ) + { + for ( v = 0; v < nVars; v++ ) + if ( (Entry >> v) & 1 ) + { + Vec_IntRemove( Vec_WecEntry(pD, v), i ); + Vec_WecPush( pS, v, i ); + } + } + else if ( pCounts[i] == 2 ) + { + for ( v = 0; v < nVars; v++ ) + if ( (Entry >> v) & 1 ) + Vec_WecPush( pD, v, i ); + } + } +} +void Abc_SuppProfile( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars ) +{ + int v; + for ( v = 0; v < nVars; v++ ) + printf( "%2d : S = %3d D = %3d\n", v, Vec_WecLevelSize(pS, v), Vec_WecLevelSize(pD, v) ); +} +int Abc_SuppSolve( Vec_Wrd_t * p, int nVars ) +{ + abctime clk = Abc_Clock(); + Vec_Wrd_t * pNew = Vec_WrdDup( p ); + Vec_Wec_t * vSingles = Vec_WecStart( 64 ); + Vec_Wec_t * vDoubles = Vec_WecStart( 64 ); + word Entry; int i, v, iVar, nVarsNew = nVars; + int * pCounts = ABC_ALLOC( int, Vec_WrdSize(p) ); + Vec_WrdForEachEntry( p, Entry, i ) + { + pCounts[i] = Abc_SuppCountOnes64( Entry ); + if ( pCounts[i] == 1 ) + { + for ( v = 0; v < nVars; v++ ) + if ( (Entry >> v) & 1 ) + Vec_WecPush( vSingles, v, i ); + } + else if ( pCounts[i] == 2 ) + { + for ( v = 0; v < nVars; v++ ) + if ( (Entry >> v) & 1 ) + Vec_WecPush( vDoubles, v, i ); + } + } + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); +// Abc_SuppProfile( vSingles, vDoubles, nVars ); + // find variable in 0 singles and the smallest doubles + while ( 1 ) + { + iVar = Abc_SuppFindVar( vSingles, vDoubles, nVars ); + if ( iVar == -1 ) + break; +// printf( "Selected variable %d.\n", iVar ); + Abc_SuppRemove( pNew, pCounts, vSingles, vDoubles, iVar, nVars ); +// Abc_SuppProfile( vSingles, vDoubles, nVars ); + nVarsNew--; + } +// printf( "Result = %d (out of %d)\n", nVarsNew, nVars ); + Vec_WecFree( vSingles ); + Vec_WecFree( vDoubles ); + Vec_WrdFree( pNew ); + ABC_FREE( pCounts ); + return nVarsNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_SuppReadMinTest( char * pFileName ) +{ + int fVerbose = 0; + abctime clk = Abc_Clock(); + word Matrix[64]; + int nVars, nVarsMin; + Vec_Wrd_t * vPairs, * vCubes; + vCubes = Abc_SuppReadMin( pFileName, &nVars ); + if ( vCubes == NULL ) + return; + vPairs = Abc_SuppDiffMatrix( vCubes ); + Vec_WrdFreeP( &vCubes ); + // solve the problem + clk = Abc_Clock(); +// nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose ); + nVarsMin = Abc_SuppSolve( vPairs, nVars ); + printf( "Solution with %d variables found. ", nVarsMin ); + Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk ); + + Vec_WrdFreeP( &vPairs ); } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3