From 8160721240399c5f89881a8bc5e60f4adb8f2958 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 21 May 2014 22:11:44 +0900 Subject: Experiment with support minimization. --- abclib.dsp | 12 +++ src/base/abci/abc.c | 30 +++++- src/misc/extra/extraUtilSupp.c | 226 +++++++++++++++++++++++++++++++++++++++++ src/misc/extra/module.make | 1 + src/sat/bmc/bmcEco.c | 25 ++++- 5 files changed, 287 insertions(+), 7 deletions(-) create mode 100644 src/misc/extra/extraUtilSupp.c diff --git a/abclib.dsp b/abclib.dsp index 276631a7..1be7cd0c 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -1451,6 +1451,10 @@ SOURCE=.\src\sat\bmc\bmcCexTools.c # End Source File # Begin Source File +SOURCE=.\src\sat\bmc\bmcEco.c +# End Source File +# Begin Source File + SOURCE=.\src\sat\bmc\bmcFault.c # End Source File # Begin Source File @@ -2739,6 +2743,10 @@ SOURCE=.\src\misc\extra\extraUtilReader.c # End Source File # Begin Source File +SOURCE=.\src\misc\extra\extraUtilSupp.c +# End Source File +# Begin Source File + SOURCE=.\src\misc\extra\extraUtilTruth.c # End Source File # Begin Source File @@ -3791,6 +3799,10 @@ SOURCE=.\src\aig\gia\giaIso2.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaIso3.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaJf.c # End Source File # Begin Source File diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6b754f2d..db033d34 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -10317,18 +10317,19 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv ) ***********************************************************************/ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); +// Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); int nCutMax = 1; - int nLeafMax = 10; + int nLeafMax = 4; int nDivMax = 2; - int nDecMax = 3; + int nDecMax = 20; + int nNumOnes = 4; int fNewAlgo = 0; int fNewOrder = 0; int fVerbose = 0; int fVeryVerbose = 0; int c; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNaovwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNMaovwh" ) ) != EOF ) { switch ( c ) { @@ -10376,6 +10377,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nDecMax < 0 ) goto usage; break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nNumOnes = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nNumOnes < 0 ) + goto usage; + break; case 'a': fNewAlgo ^= 1; break; @@ -10464,6 +10476,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Abc_EnumerateFuncs( int nDecMax, int nDivMax, int fVerbose ); // Abc_EnumerateFuncs( nDecMax, nDivMax, fVerbose ); } + + if ( fNewAlgo ) + { + extern void Abc_SuppTest( int nOnes, int nVars, int fVerbose ); + Abc_SuppTest( nNumOnes, nDecMax, fVerbose ); + } + else { extern void Bmc_EcoMiterTest(); Bmc_EcoMiterTest(); @@ -10483,12 +10502,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) */ return 0; usage: - Abc_Print( -2, "usage: test [-CKDN] [-aovwh] \n" ); + Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] \n" ); Abc_Print( -2, "\t testbench for new procedures\n" ); Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax ); Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax ); Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax ); Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax ); + Abc_Print( -2, "\t-M num : the max number of ones in the vector [default = %d]\n", nNumOnes ); Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" ); Abc_Print( -2, "\t-o : toggle using new ordering [default = %s]\n", fNewOrder? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/misc/extra/extraUtilSupp.c b/src/misc/extra/extraUtilSupp.c new file mode 100644 index 00000000..4699b7ae --- /dev/null +++ b/src/misc/extra/extraUtilSupp.c @@ -0,0 +1,226 @@ +/**CFile**************************************************************** + + FileName [extraUtilSupp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [extra] + + Synopsis [Support minimization.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: extraUtilSupp.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include +#include +#include +#include +#include "misc/vec/vec.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Generate m-out-of-n vectors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_SuppCountOnes( unsigned i ) +{ + i = i - ((i >> 1) & 0x55555555); + i = (i & 0x33333333) + ((i >> 2) & 0x33333333); + i = ((i + (i >> 4)) & 0x0F0F0F0F); + return (i*(0x01010101))>>24; +} +Vec_Int_t * Abc_SuppGen( int m, int n ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 1000 ); + int i, Size = (1 << n); + for ( i = 0; i < Size; i++ ) + if ( Abc_SuppCountOnes(i) == m ) + Vec_IntPush( vRes, i ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Generate pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_SuppGenPairs( Vec_Int_t * p, int nBits ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 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; + for ( ; pEntry1 < pLimit; pEntry1++ ) + for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ ) + { + Value = *pEntry1 ^ *pEntry2; + if ( Abc_InfoHasBit(pMap, Value) ) + continue; + Abc_InfoXorBit( pMap, Value ); + Vec_IntPush( vRes, Value ); + } + ABC_FREE( pMap ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [Select variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_SuppPrintMask( unsigned 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 ) +{ + int i, k, b, Ent; + Vec_IntForEachEntry( 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 ) +{ + int k, Counts[32] = {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) ); +} +int Abc_SuppGenFindBest( Vec_Int_t * p, int nBits, int * pMerit ) +{ + int k, kBest = 0, Counts[32] = {0}; + Abc_SuppGenProfile( p, nBits, Counts ); + for ( k = 1; k < nBits; k++ ) + if ( Counts[kBest] < Counts[k] ) + kBest = k; + *pMerit = Counts[kBest]; + return kBest; +} +void Abc_SuppGenSelectVar( Vec_Int_t * p, int nBits, int iVar ) +{ + int * pEntry = Vec_IntArray(p); + int * pLimit = Vec_IntLimit(p); + for ( ; pEntry < pLimit; pEntry++ ) + if ( (*pEntry >> iVar) & 1 ) + *pEntry ^= (1 << nBits); +} +void Abc_SuppGenFilter( Vec_Int_t * p, int nBits ) +{ + int i, k = 0, Ent; + Vec_IntForEachEntry( p, Ent, i ) + if ( ((Ent >> nBits) & 1) == 0 ) + Vec_IntWriteEntry( p, k++, Ent ); + Vec_IntShrink( p, k ); +} +unsigned Abc_SuppFindOne( Vec_Int_t * p, int nBits ) +{ + unsigned uMask = 0; + int Prev = -1, This, Var; + while ( 1 ) + { + Var = Abc_SuppGenFindBest( p, nBits, &This ); + if ( Prev >= This ) + break; + Prev = This; + Abc_SuppGenSelectVar( p, nBits, Var ); + uMask |= (1 << Var); + } + return uMask; +} +int Abc_SuppMinimize( Vec_Int_t * p, int nBits, int fVerbose ) +{ + unsigned uMask; int i; + for ( i = 0; Vec_IntSize(p) > 0; i++ ) + { +// Abc_SuppPrintProfile( p, nBits ); + uMask = 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 ); +// printf( "\n" ); + } + return i; +} + +/**Function************************************************************* + + Synopsis [Create representation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_SuppTest( int nOnes, int nVars, int fVerbose ) +{ + int nVarsMin; + abctime clk = Abc_Clock(); + // create the problem + Vec_Int_t * vRes = Abc_SuppGen( nOnes, nVars ); + Vec_Int_t * vPairs = Abc_SuppGenPairs( vRes, nVars ); + printf( "M = %2d N = %2d : ", nOnes, nVars ); + printf( "K = %6d ", Vec_IntSize(vRes) ); + printf( "Total = %10d ", Vec_IntSize(vRes) * (Vec_IntSize(vRes) - 1) /2 ); + printf( "Distinct = %8d ", Vec_IntSize(vPairs) ); + Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk ); + // solve the problem + clk = Abc_Clock(); + nVarsMin = Abc_SuppMinimize( vPairs, nVars, fVerbose ); + printf( "Solution with %d variables found. ", nVarsMin ); + Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk ); + Vec_IntFree( vPairs ); + Vec_IntFree( vRes ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index 466d2279..1503cec1 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -17,5 +17,6 @@ SRC += src/misc/extra/extraBddAuto.c \ src/misc/extra/extraUtilPerm.c \ src/misc/extra/extraUtilProgress.c \ src/misc/extra/extraUtilReader.c \ + src/misc/extra/extraUtilSupp.c \ src/misc/extra/extraUtilTruth.c \ src/misc/extra/extraUtilUtil.c diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c index 5f0313f5..c4fc3ba8 100644 --- a/src/sat/bmc/bmcEco.c +++ b/src/sat/bmc/bmcEco.c @@ -264,12 +264,33 @@ int Bmc_EcoPatch( Gia_Man_t * p, int nIns, int nOuts ) ***********************************************************************/ void Bmc_EcoMiterTest() { + char * pFileGold = "eco_gold.aig"; + char * pFileOld = "eco_old.aig"; Vec_Int_t * vFans; + FILE * pFile; Gia_Man_t * pMiter; Gia_Obj_t * pObj; - Gia_Man_t * pGold = Gia_AigerRead( "eco_gold.aig", 0, 0 ); - Gia_Man_t * pOld = Gia_AigerRead( "eco_old.aig", 0, 0 ); + Gia_Man_t * pGold; + Gia_Man_t * pOld; int i, RetValue; + // check that the files exist + pFile = fopen( pFileGold, "r" ); + if ( pFile == NULL ) + { + printf( "File \"%s\" does not exist.\n", pFileGold ); + return; + } + fclose( pFile ); + pFile = fopen( pFileOld, "r" ); + if ( pFile == NULL ) + { + printf( "File \"%s\" does not exist.\n", pFileOld ); + return; + } + fclose( pFile ); + // read files + pGold = Gia_AigerRead( pFileGold, 0, 0 ); + pOld = Gia_AigerRead( pFileOld, 0, 0 ); // create ECO miter vFans = Vec_IntAlloc( Gia_ManCiNum(pOld) ); Gia_ManForEachCi( pOld, pObj, i ) -- cgit v1.2.3