diff options
| -rw-r--r-- | src/misc/extra/extraUtilSupp.c | 58 |
1 files changed, 53 insertions, 5 deletions
diff --git a/src/misc/extra/extraUtilSupp.c b/src/misc/extra/extraUtilSupp.c index 52cd435b..1623bd01 100644 --- a/src/misc/extra/extraUtilSupp.c +++ b/src/misc/extra/extraUtilSupp.c @@ -64,6 +64,51 @@ Vec_Int_t * Abc_SuppGen( int m, int n ) /**Function************************************************************* + Synopsis [Perform verification.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_SuppVerify( Vec_Int_t * p, unsigned * 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 ) + { + EntryNew = 0; + for ( v = 0; v < nVarsMin; v++ ) + { + Value = 0; + for ( k = 0; k < nVars; k++ ) + if ( ((pMatrix[v] >> k) & 1) && ((Entry >> k) & 1) ) + Value ^= 1; + if ( Value ) + EntryNew |= (1 << v); + } + Vec_IntPush( pNew, EntryNew ); + } + // check that they are disjoint + pLimit = Vec_IntLimit(pNew); + pEntry1 = Vec_IntArray(pNew); + for ( ; pEntry1 < pLimit; pEntry1++ ) + for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ ) + if ( *pEntry1 == *pEntry2 ) + Counter++; + if ( Counter ) + printf( "The total of %d pairs fail verification.\n", Counter ); + else + printf( "Verification successful.\n" ); + Vec_IntFree( pNew ); +} + +/**Function************************************************************* + Synopsis [Generate pairs.] Description [] @@ -181,20 +226,20 @@ unsigned Abc_SuppFindOne( Vec_Int_t * p, int nBits ) } return uMask; } -int Abc_SuppMinimize( Vec_Int_t * p, int nBits, int fVerbose ) +int Abc_SuppMinimize( unsigned * pMatrix, Vec_Int_t * p, int nBits, int fVerbose ) { - unsigned uMask; int i; + int i; for ( i = 0; Vec_IntSize(p) > 0; i++ ) { // Abc_SuppPrintProfile( p, nBits ); - uMask = Abc_SuppFindOne( p, nBits ); + pMatrix[i] = Abc_SuppFindOne( p, nBits ); Abc_SuppGenFilter( p, nBits ); if ( !fVerbose ) continue; // print stats printf( "%2d : ", i ); printf( "%6d ", Vec_IntSize(p) ); - Abc_SuppPrintMask( uMask, nBits ); + Abc_SuppPrintMask( pMatrix[i], nBits ); // printf( "\n" ); } return i; @@ -214,10 +259,12 @@ int Abc_SuppMinimize( Vec_Int_t * p, int nBits, int fVerbose ) void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fVerbose ) { int nVarsMin; + unsigned Matrix[100]; 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 ); + 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) ); @@ -225,9 +272,10 @@ void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fVerbose ) Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk ); // solve the problem clk = Abc_Clock(); - nVarsMin = Abc_SuppMinimize( vPairs, nVars, fVerbose ); + nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose ); printf( "Solution with %d variables found. ", nVarsMin ); Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk ); + Abc_SuppVerify( vRes, Matrix, nVars, nVarsMin ); Vec_IntFree( vPairs ); Vec_IntFree( vRes ); } |