From efdd26f86d3dbbde1626fe6a84304bc700b97479 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 23 Mar 2015 18:40:38 +0700 Subject: Scalable SOP manipulation package. --- src/base/abci/abcFx.c | 6 +- src/base/pla/module.make | 2 + src/base/pla/pla.h | 54 ++- src/base/pla/plaCom.c | 25 +- src/base/pla/plaFxch.c | 854 +++++++++++++++++++++++++++++++++++++++++++++++ src/base/pla/plaHash.c | 144 +++++++- src/base/pla/plaMan.c | 60 +++- src/base/pla/plaSimple.c | 339 +++++++++++++++++++ src/base/pla/plaWrite.c | 2 +- src/misc/vec/vecBit.h | 2 +- src/misc/vec/vecFlt.h | 12 + src/misc/vec/vecInt.h | 47 +++ src/misc/vec/vecWrd.h | 19 ++ 13 files changed, 1524 insertions(+), 42 deletions(-) create mode 100644 src/base/pla/plaFxch.c create mode 100644 src/base/pla/plaSimple.c (limited to 'src') diff --git a/src/base/abci/abcFx.c b/src/base/abci/abcFx.c index 1be25f52..de7125bc 100644 --- a/src/base/abci/abcFx.c +++ b/src/base/abci/abcFx.c @@ -1091,12 +1091,12 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning ) if ( Vec_IntSize(vDiv) == 2 || fCompl ) { Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 1) ); - Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) ); + Vec_IntPush( vLitN, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID } else { Vec_IntPush( vCube, Abc_Var2Lit(iVarNew, 0) ); - Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); + Vec_IntPush( vLitP, Vec_WecLevelId(p->vCubes, vCube) ); // MAKE SURE vCube IS SORTED BY ID } p->nLits -= Vec_IntSize(vDiv) + Vec_IntSize(vCube2) - 2; // remove second cube @@ -1106,6 +1106,8 @@ void Fx_ManUpdate( Fx_Man_t * p, int iDiv, int * fWarning ) assert( k == Vec_IntSize(p->vCubesD) / 2 ); Vec_IntShrink( p->vCubesD, k ); Vec_IntSort( p->vCubesD, 0 ); + //Vec_IntSort( vLitN, 0 ); + //Vec_IntSort( vLitP, 0 ); // add cost of single-cube divisors Fx_ManForEachCubeVec( p->vCubesS, p->vCubes, vCube, i ) diff --git a/src/base/pla/module.make b/src/base/pla/module.make index ab883fef..b34d30d0 100644 --- a/src/base/pla/module.make +++ b/src/base/pla/module.make @@ -1,6 +1,8 @@ SRC += src/base/pla/plaCom.c \ src/base/pla/plaHash.c \ + src/base/pla/plaFxch.c \ src/base/pla/plaMan.c \ src/base/pla/plaMerge.c \ + src/base/pla/plaSimple.c \ src/base/pla/plaRead.c \ src/base/pla/plaWrite.c diff --git a/src/base/pla/pla.h b/src/base/pla/pla.h index bf81f16d..2806df2f 100644 --- a/src/base/pla/pla.h +++ b/src/base/pla/pla.h @@ -74,20 +74,33 @@ struct Pla_Man_t_ Vec_Int_t vHashes; // hash values Vec_Wrd_t vInBits; // input bits Vec_Wrd_t vOutBits; // output bits - Vec_Wec_t vLits; // cubes as interger arrays - Vec_Wec_t vOccurs; // occurent counters for the literals + Vec_Wec_t vCubeLits; // cubes as interger arrays + Vec_Wec_t vOccurs; // occurence counters for the literals + Vec_Int_t vDivs; // divisor definitions }; +static inline char * Pla_ManName( Pla_Man_t * p ) { return p->pName; } static inline int Pla_ManInNum( Pla_Man_t * p ) { return p->nIns; } static inline int Pla_ManOutNum( Pla_Man_t * p ) { return p->nOuts; } static inline int Pla_ManCubeNum( Pla_Man_t * p ) { return Vec_IntSize( &p->vCubes ); } +static inline int Pla_ManDivNum( Pla_Man_t * p ) { return Vec_IntSize( &p->vDivs ); } static inline word * Pla_CubeIn( Pla_Man_t * p, int i ) { return Vec_WrdEntryP(&p->vInBits, i * p->nInWords); } static inline word * Pla_CubeOut( Pla_Man_t * p, int i ) { return Vec_WrdEntryP(&p->vOutBits, i * p->nOutWords); } -static inline int Pla_CubeGetLit( word * p, int k ) { return (int)(p[k>>5] >> ((k<<1) & 63)) & 3; } -static inline void Pla_CubeSetLit( word * p, int k, Pla_Lit_t d ) { p[k>>5] |= (((word)d)<<((k<<1) & 63)); } -static inline void Pla_CubeXorLit( word * p, int k, Pla_Lit_t d ) { p[k>>5] ^= (((word)d)<<((k<<1) & 63)); } +static inline int Pla_CubeNum( int hCube ) { return hCube >> 8; } +static inline int Pla_CubeLit( int hCube ) { return hCube & 0xFF; } +static inline int Pla_CubeHandle( int iCube, int iLit ) { assert( !(iCube >> 24) && !(iLit >> 8) ); return iCube << 8 | iLit; } + +// read/write/flip i-th bit of a bit string table +static inline int Pla_TtGetBit( word * p, int i ) { return (int)(p[i>>6] >> (i & 63)) & 1; } +static inline void Pla_TtSetBit( word * p, int i ) { p[i>>6] |= (((word)1)<<(i & 63)); } +static inline void Pla_TtXorBit( word * p, int i ) { p[i>>6] ^= (((word)1)<<(i & 63)); } + +// read/write/flip i-th literal in a cube +static inline int Pla_CubeGetLit( word * p, int i ) { return (int)(p[i>>5] >> ((i<<1) & 63)) & 3; } +static inline void Pla_CubeSetLit( word * p, int i, Pla_Lit_t d ) { p[i>>5] |= (((word)d)<<((i<<1) & 63)); } +static inline void Pla_CubeXorLit( word * p, int i, Pla_Lit_t d ) { p[i>>5] ^= (((word)d)<<((i<<1) & 63)); } //////////////////////////////////////////////////////////////////////// @@ -170,6 +183,23 @@ static inline int Pla_CubesAreConsensus( word * p, word * q, int nWords, int * p } return fFound; } +static inline int Pla_TtCountOnesOne( word x ) +{ + x = x - ((x >> 1) & ABC_CONST(0x5555555555555555)); + x = (x & ABC_CONST(0x3333333333333333)) + ((x >> 2) & ABC_CONST(0x3333333333333333)); + x = (x + (x >> 4)) & ABC_CONST(0x0F0F0F0F0F0F0F0F); + x = x + (x >> 8); + x = x + (x >> 16); + x = x + (x >> 32); + return (int)(x & 0xFF); +} +static inline int Pla_TtCountOnes( word * p, int nWords ) +{ + int i, Count = 0; + for ( i = 0; i < nWords; i++ ) + Count += Pla_TtCountOnesOne( p[i] ); + return Count; +} /**Function************************************************************* @@ -202,8 +232,9 @@ static inline void Pla_ManFree( Pla_Man_t * p ) Vec_IntErase( &p->vHashes ); Vec_WrdErase( &p->vInBits ); Vec_WrdErase( &p->vOutBits ); - Vec_WecErase( &p->vLits ); + Vec_WecErase( &p->vCubeLits ); Vec_WecErase( &p->vOccurs ); + Vec_IntErase( &p->vDivs ); ABC_FREE( p->pName ); ABC_FREE( p->pSpec ); ABC_FREE( p ); @@ -226,26 +257,33 @@ static inline int Pla_ManLitOutNum( Pla_Man_t * p ) } static inline void Pla_ManPrintStats( Pla_Man_t * p, int fVerbose ) { - printf( "%-16s : ", p->pName ); + printf( "%-16s : ", Pla_ManName(p) ); printf( "In =%4d ", Pla_ManInNum(p) ); printf( "Out =%4d ", Pla_ManOutNum(p) ); printf( "Cube =%8d ", Pla_ManCubeNum(p) ); printf( "LitIn =%8d ", Pla_ManLitInNum(p) ); printf( "LitOut =%8d ", Pla_ManLitOutNum(p) ); + printf( "Div =%6d ", Pla_ManDivNum(p) ); printf( "\n" ); } +/*=== plaFxch.c ========================================================*/ +extern int Pla_ManPerformFxch( Pla_Man_t * p ); /*=== plaHash.c ========================================================*/ extern int Pla_ManHashDist1NumTest( Pla_Man_t * p ); +extern void Pla_ManComputeDist1Test( Pla_Man_t * p ); /*=== plaMan.c ========================================================*/ -extern Pla_Man_t * Pla_ManPrimeDetector( int nVars ); +extern Vec_Bit_t * Pla_ManPrimesTable( int nVars ); +extern Pla_Man_t * Pla_ManPrimesDetector( int nVars ); extern Pla_Man_t * Pla_ManGenerate( int nIns, int nOuts, int nCubes, int fVerbose ); extern void Pla_ManConvertFromBits( Pla_Man_t * p ); extern void Pla_ManConvertToBits( Pla_Man_t * p ); extern int Pla_ManDist1NumTest( Pla_Man_t * p ); /*=== plaMerge.c ========================================================*/ extern int Pla_ManDist1Merge( Pla_Man_t * p ); +/*=== plaSimple.c ========================================================*/ +extern int Pla_ManFxPerformSimple( int nVars ); /*=== plaRead.c ========================================================*/ extern Pla_Man_t * Pla_ReadPla( char * pFileName ); /*=== plaWrite.c ========================================================*/ diff --git a/src/base/pla/plaCom.c b/src/base/pla/plaCom.c index 5ccfe98b..6d2d4b62 100644 --- a/src/base/pla/plaCom.c +++ b/src/base/pla/plaCom.c @@ -359,7 +359,7 @@ int Abc_CommandGen( Abc_Frame_t * pAbc, int argc, char ** argv ) } } if ( fPrimes ) - p = Pla_ManPrimeDetector( nInputs ); + p = Pla_ManPrimesDetector( nInputs ); else { Gia_ManRandom( 1 ); @@ -444,12 +444,23 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { Pla_Man_t * p = Pla_AbcGetMan(pAbc); - int c, fVerbose = 0; + int c, nVars = 4, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF ) { switch ( c ) { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -459,18 +470,22 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } +/* if ( p == NULL ) { Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" ); return 0; } - Pla_ManHashDist1NumTest( p ); +*/ + //Pla_ManFxPerformSimple( nVars ); //Pla_ManConvertFromBits( p ); //Pla_ManConvertToBits( p ); + Pla_ManPerformFxch( p ); return 0; usage: - Abc_Print( -2, "usage: |test [-vh]\n" ); + Abc_Print( -2, "usage: |test [-N num] [-vh]\n" ); Abc_Print( -2, "\t experiments with SOPs\n" ); + Abc_Print( -2, "\t-N num : the number of variables [default = %d]\n", nVars ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/pla/plaFxch.c b/src/base/pla/plaFxch.c new file mode 100644 index 00000000..fd06b9a5 --- /dev/null +++ b/src/base/pla/plaFxch.c @@ -0,0 +1,854 @@ +/**CFile**************************************************************** + + FileName [plaFxch.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SOP manager.] + + Synopsis [Scalable SOP transformations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - March 18, 2015.] + + Revision [$Id: plaFxch.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pla.h" +#include "misc/vec/vecHash.h" +#include "misc/vec/vecQue.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Fxch_Obj_t_ Fxch_Obj_t; +struct Fxch_Obj_t_ +{ + unsigned Table : 30; + unsigned MarkN : 1; + unsigned MarkP : 1; + int Next; + int Prev; + int Cube; +}; + +typedef struct Fxch_Man_t_ Fxch_Man_t; +struct Fxch_Man_t_ +{ + // user's data + Vec_Wec_t vCubes; // cube -> lit + // internal data + Vec_Wec_t vLits; // lit -> cube + Vec_Int_t vRands; // random numbers for each literal + Vec_Int_t vCubeLinks; // first link for each cube + Fxch_Obj_t * pBins; // hash table (lits -> cube + lit) + Hash_IntMan_t * vHash; // divisor hash table + Vec_Que_t * vPrio; // priority queue for divisors by weight + Vec_Flt_t vWeights; // divisor weights + Vec_Wec_t vPairs; // cube pairs for each div + Vec_Wrd_t vDivs; // extracted divisors + // temporary data + Vec_Int_t vCubesS; // cube pairs for single + Vec_Int_t vCubesD; // cube pairs for double + Vec_Int_t vCube1; // first cube + Vec_Int_t vCube2; // second cube + // statistics + abctime timeStart; // starting time + int SizeMask; // hash table mask + int nVars; // original problem variables + int nLits; // the number of SOP literals + int nCompls; // the number of complements + int nPairsS; // number of lit pairs + int nPairsD; // number of cube pairs +}; + +#define Fxch_ManForEachCubeVec( vVec, vCubes, vCube, i ) \ + for ( i = 0; (i < Vec_IntSize(vVec)) && ((vCube) = Vec_WecEntry(vCubes, Vec_IntEntry(vVec, i))); i++ ) + +static inline Vec_Int_t * Fxch_ManCube( Fxch_Man_t * p, int hCube ) { return Vec_WecEntry(&p->vCubes, Pla_CubeNum(hCube)); } + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Writes the current state of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_ManWriteBlif( char * pFileName, Vec_Wec_t * vCubes, Vec_Wrd_t * vDivs ) +{ + // find the number of original variables + int nVarsInit = Vec_WrdCountZero(vDivs); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + else + { + char * pLits = "-01?"; + Vec_Str_t * vStr; + Vec_Int_t * vCube; + int i, k, Lit; + word Div; + // comment + fprintf( pFile, "# BLIF file written via PLA package in ABC on " ); + fprintf( pFile, "%s", Extra_TimeStamp() ); + fprintf( pFile, "\n\n" ); + // header + fprintf( pFile, ".model %s\n", pFileName ); + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nVarsInit; i++ ) + fprintf( pFile, " i%d", i ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".outputs o" ); + fprintf( pFile, "\n" ); + // SOP header + fprintf( pFile, ".names" ); + for ( i = 0; i < Vec_WrdSize(vDivs); i++ ) + fprintf( pFile, " i%d", i ); + fprintf( pFile, " o\n" ); + // SOP cubes + vStr = Vec_StrStart( Vec_WrdSize(vDivs) + 1 ); + Vec_WecForEachLevel( vCubes, vCube, i ) + { + if ( !Vec_IntSize(vCube) ) + continue; + for ( k = 0; k < Vec_WrdSize(vDivs); k++ ) + Vec_StrWriteEntry( vStr, k, '-' ); + Vec_IntForEachEntry( vCube, Lit, k ) + Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') ); + fprintf( pFile, "%s 1\n", Vec_StrArray(vStr) ); + } + Vec_StrFree( vStr ); + // divisors + Vec_WrdForEachEntryStart( vDivs, Div, i, nVarsInit ) + { + int pLits[2] = { (int)(Div & 0xFFFFFFFF), (int)(Div >> 32) }; + fprintf( pFile, ".names" ); + fprintf( pFile, " i%d", Abc_Lit2Var(pLits[0]) ); + fprintf( pFile, " i%d", Abc_Lit2Var(pLits[1]) ); + fprintf( pFile, " i%d\n", i ); + fprintf( pFile, "%d%d 1\n", !Abc_LitIsCompl(pLits[0]), !Abc_LitIsCompl(pLits[1]) ); + } + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + printf( "Written BLIF file \"%s\".\n", pFileName ); + } +} + +/**Function************************************************************* + + Synopsis [Starting the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Fxch_Man_t * Fxch_ManStart( Vec_Wec_t * vCubes, Vec_Wec_t * vLits ) +{ + Vec_Int_t * vCube; int i, LogSize; + Fxch_Man_t * p = ABC_CALLOC( Fxch_Man_t, 1 ); + p->vCubes = *vCubes; + p->vLits = *vLits; + p->nVars = Vec_WecSize(vLits)/2; + p->nLits = 0; + // random numbers + Gia_ManRandom( 1 ); + Vec_IntGrow( &p->vRands, 2*p->nVars ); + for ( i = 0; i < 2*p->nVars; i++ ) + Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF ); // assert( LogSize <= 26 ); + // create cube links + Vec_IntGrow( &p->vCubeLinks, Vec_WecSize(&p->vCubes) ); + Vec_WecForEachLevel( vCubes, vCube, i ) + { + Vec_IntPush( &p->vCubeLinks, p->nLits+1 ); + p->nLits += Vec_IntSize(vCube); + } + assert( Vec_IntSize(&p->vCubeLinks) == Vec_WecSize(&p->vCubes) ); + // create table + LogSize = Abc_Base2Log( p->nLits+1 ); + assert( LogSize <= 26 ); + p->SizeMask = (1 << LogSize) - 1; + p->pBins = ABC_CALLOC( Fxch_Obj_t, p->SizeMask + 1 ); + assert( p->nLits+1 < p->SizeMask+1 ); + // divisor weights and cube pairs + Vec_FltGrow( &p->vWeights, 1000 ); + Vec_FltPush( &p->vWeights, -1 ); + Vec_WecGrow( &p->vPairs, 1000 ); + Vec_WecPushLevel( &p->vPairs ); + // prepare divisors + Vec_WrdGrow( &p->vDivs, p->nVars + 1000 ); + Vec_WrdFill( &p->vDivs, p->nVars, 0 ); + return p; +} +void Fxch_ManStop( Fxch_Man_t * p ) +{ + Vec_WecErase( &p->vCubes ); + Vec_WecErase( &p->vLits ); + Vec_IntErase( &p->vRands ); + Vec_IntErase( &p->vCubeLinks ); + Hash_IntManStop( p->vHash ); + Vec_QueFree( p->vPrio ); + Vec_FltErase( &p->vWeights ); + Vec_WecErase( &p->vPairs ); + Vec_WrdErase( &p->vDivs ); + Vec_IntErase( &p->vCubesS ); + Vec_IntErase( &p->vCubesD ); + Vec_IntErase( &p->vCube1 ); + Vec_IntErase( &p->vCube2 ); + ABC_FREE( p->pBins ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Fxch_TabCompare( Fxch_Man_t * p, int hCube1, int hCube2 ) +{ + Vec_Int_t * vCube1 = Fxch_ManCube( p, hCube1 ); + Vec_Int_t * vCube2 = Fxch_ManCube( p, hCube2 ); + if ( !Vec_IntSize(vCube1) || !Vec_IntSize(vCube2) || Vec_IntSize(vCube1) != Vec_IntSize(vCube2) ) + return 0; + Vec_IntClear( &p->vCube1 ); + Vec_IntClear( &p->vCube2 ); + Vec_IntAppendSkip( &p->vCube1, vCube1, Pla_CubeLit(hCube1) ); + Vec_IntAppendSkip( &p->vCube2, vCube2, Pla_CubeLit(hCube2) ); + return Vec_IntEqual( &p->vCube1, &p->vCube2 ); +} +static inline void Fxch_CompressCubes( Fxch_Man_t * p, Vec_Int_t * vLit2Cube ) +{ + int i, hCube, k = 0; + Vec_IntForEachEntry( vLit2Cube, hCube, i ) + if ( Vec_IntSize(Vec_WecEntry(&p->vCubes, hCube)) > 0 ) + Vec_IntWriteEntry( vLit2Cube, k++, hCube ); + Vec_IntShrink( vLit2Cube, k ); +} +static inline int Fxch_CollectSingles( Vec_Int_t * vArr1, Vec_Int_t * vArr2, Vec_Int_t * vArr ) +{ + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + int * pBeg1New = vArr1->pArray; + int * pBeg2New = vArr2->pArray; + Vec_IntClear( vArr ); + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( Pla_CubeNum(*pBeg1) == Pla_CubeNum(*pBeg2) ) + Vec_IntPushTwo( vArr, *pBeg1, *pBeg2 ), pBeg1++, pBeg2++; + else if ( *pBeg1 < *pBeg2 ) + *pBeg1New++ = *pBeg1++; + else + *pBeg2New++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pBeg1New++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *pBeg2New++ = *pBeg2++; + Vec_IntShrink( vArr1, pBeg1New - vArr1->pArray ); + Vec_IntShrink( vArr2, pBeg2New - vArr2->pArray ); + return Vec_IntSize(vArr); +} +static inline void Fxch_CollectDoubles( Fxch_Man_t * p, Vec_Int_t * vPairs, Vec_Int_t * vRes, int Lit0, int Lit1 ) +{ + int i, hCube1, hCube2; + Vec_IntClear( vRes ); + Vec_IntForEachEntryDouble( vPairs, hCube1, hCube2, i ) + if ( Fxch_TabCompare(p, hCube1, hCube2) && + Vec_IntEntry(Fxch_ManCube(p, hCube1), Pla_CubeLit(hCube1)) == Lit0 && + Vec_IntEntry(Fxch_ManCube(p, hCube2), Pla_CubeLit(hCube2)) == Lit1 ) + Vec_IntPushTwo( vRes, hCube1, hCube2 ); + Vec_IntClear( vPairs ); + // order pairs in the increasing order of the first cube + //Vec_IntSortPairs( vRes ); +} +static inline void Fxch_CompressLiterals2( Vec_Int_t * p, int iInd1, int iInd2 ) +{ + int i, Lit, k = 0; + assert( iInd1 >= 0 && iInd1 < Vec_IntSize(p) ); + if ( iInd2 != -1 ) + assert( iInd1 >= 0 && iInd1 < Vec_IntSize(p) ); + Vec_IntForEachEntry( p, Lit, i ) + if ( i != iInd1 && i != iInd2 ) + Vec_IntWriteEntry( p, k++, Lit ); + Vec_IntShrink( p, k ); +} +static inline void Fxch_CompressLiterals( Vec_Int_t * p, int iLit1, int iLit2 ) +{ + int i, Lit, k = 0; + Vec_IntForEachEntry( p, Lit, i ) + if ( Lit != iLit1 && Lit != iLit2 ) + Vec_IntWriteEntry( p, k++, Lit ); + assert( Vec_IntSize(p) == k + 2 ); + Vec_IntShrink( p, k ); +} +static inline void Fxch_FilterCubes( Fxch_Man_t * p, Vec_Int_t * vCubesS, int Lit0, int Lit1 ) +{ + Vec_Int_t * vCube; + int i, k, Lit, iCube, n = 0; + int fFound0, fFound1; + Vec_IntForEachEntry( vCubesS, iCube, i ) + { + vCube = Vec_WecEntry( &p->vCubes, iCube ); + fFound0 = fFound1 = 0; + Vec_IntForEachEntry( vCube, Lit, k ) + { + if ( Lit == Lit0 ) + fFound0 = 1; + else if ( Lit == Lit1 ) + fFound1 = 1; + } + if ( fFound0 && fFound1 ) + Vec_IntWriteEntry( vCubesS, n++, Pla_CubeHandle(iCube, 255) ); + } + Vec_IntShrink( vCubesS, n ); +} + + +/**Function************************************************************* + + Synopsis [Divisor addition removal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fxch_DivisorAdd( Fxch_Man_t * p, int Lit0, int Lit1, int Weight ) +{ + int iDiv; + assert( Lit0 != Lit1 ); + if ( Lit0 < Lit1 ) + iDiv = Hash_Int2ManInsert( p->vHash, Lit0, Lit1, 0 ); + else + iDiv = Hash_Int2ManInsert( p->vHash, Lit1, Lit0, 0 ); + if ( iDiv == Vec_FltSize(&p->vWeights) ) + { + Vec_FltPush( &p->vWeights, -2 ); + Vec_WecPushLevel( &p->vPairs ); + assert( Vec_FltSize(&p->vWeights) == Vec_WecSize(&p->vPairs) ); + } + Vec_FltAddToEntry( &p->vWeights, iDiv, Weight ); + if ( p->vPrio ) + { + if ( Vec_QueIsMember(p->vPrio, iDiv) ) + Vec_QueUpdate( p->vPrio, iDiv ); + else + Vec_QuePush( p->vPrio, iDiv ); + //assert( iDiv < Vec_QueSize(p->vPrio) ); + } + return iDiv; +} +void Fxch_DivisorRemove( Fxch_Man_t * p, int Lit0, int Lit1, int Weight ) +{ + int iDiv; + assert( Lit0 != Lit1 ); + if ( Lit0 < Lit1 ) + iDiv = *Hash_Int2ManLookup( p->vHash, Lit0, Lit1 ); + else + iDiv = *Hash_Int2ManLookup( p->vHash, Lit1, Lit0 ); + assert( iDiv > 0 && iDiv < Vec_FltSize(&p->vWeights) ); + Vec_FltAddToEntry( &p->vWeights, iDiv, -Weight ); + if ( Vec_QueIsMember(p->vPrio, iDiv) ) + Vec_QueUpdate( p->vPrio, iDiv ); +} + +/**Function************************************************************* + + Synopsis [Starting the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Fxch_Obj_t * Fxch_TabBin( Fxch_Man_t * p, int Value ) { return p->pBins + (Value & p->SizeMask); } +static inline Fxch_Obj_t * Fxch_TabEntry( Fxch_Man_t * p, int i ) { return i ? p->pBins + i : NULL; } +static inline int Fxch_TabEntryId( Fxch_Man_t * p, Fxch_Obj_t * pEnt ) { assert(pEnt > p->pBins); return pEnt - p->pBins; } + +static inline void Fxch_TabMarkPair( Fxch_Man_t * p, int i, int j ) +{ + Fxch_Obj_t * pI = Fxch_TabEntry(p, i); + Fxch_Obj_t * pJ = Fxch_TabEntry(p, j); + assert( pI->Next == j ); + assert( pJ->Prev == i ); + assert( pI->MarkN == 0 ); + assert( pI->MarkP == 0 ); + assert( pJ->MarkN == 0 ); + assert( pJ->MarkP == 0 ); + pI->MarkN = 1; + pJ->MarkP = 1; +} +static inline void Fxch_TabUnmarkPair( Fxch_Man_t * p, int i, int j ) +{ + Fxch_Obj_t * pI = Fxch_TabEntry(p, i); + Fxch_Obj_t * pJ = Fxch_TabEntry(p, j); + assert( pI->Next == j ); + assert( pJ->Prev == i ); + assert( pI->MarkN == 1 ); + assert( pI->MarkP == 0 ); + assert( pJ->MarkN == 0 ); + assert( pJ->MarkP == 1 ); + pI->MarkN = 0; + pJ->MarkP = 0; +} +static inline void Fxch_TabInsertLink( Fxch_Man_t * p, int i, int j, int fSkipCheck ) +{ + Fxch_Obj_t * pI = Fxch_TabEntry(p, i); + Fxch_Obj_t * pN = Fxch_TabEntry(p, pI->Next); + Fxch_Obj_t * pJ = Fxch_TabEntry(p, j); + //assert( pJ->Cube != 0 ); + assert( pN->Prev == i ); + assert( fSkipCheck || pI->MarkN == 0 ); + assert( fSkipCheck || pN->MarkP == 0 ); + assert( fSkipCheck || pJ->MarkN == 0 ); + assert( fSkipCheck || pJ->MarkP == 0 ); + pJ->Next = pI->Next; pI->Next = j; + pJ->Prev = i; pN->Prev = j; +} +static inline void Fxch_TabExtractLink( Fxch_Man_t * p, int i, int j ) +{ + Fxch_Obj_t * pI = Fxch_TabEntry(p, i); + Fxch_Obj_t * pJ = Fxch_TabEntry(p, j); + Fxch_Obj_t * pN = Fxch_TabEntry(p, pJ->Next); + //assert( pJ->Cube != 0 ); + assert( pI->Next == j ); + assert( pJ->Prev == i ); + assert( pN->Prev == j ); + assert( pI->MarkN == 0 ); + assert( pJ->MarkP == 0 ); + assert( pJ->MarkN == 0 ); + assert( pN->MarkP == 0 ); + pI->Next = pJ->Next; pJ->Next = 0; + pN->Prev = pJ->Prev; pJ->Prev = 0; +} +static inline void Fxch_TabInsert( Fxch_Man_t * p, int iLink, int Value, int hCube ) +{ + int iEnt, iDiv, Lit0, Lit1, fStart = 1; + Fxch_Obj_t * pEnt; + Fxch_Obj_t * pBin = Fxch_TabBin( p, Value ); + Fxch_Obj_t * pCell = Fxch_TabEntry( p, iLink ); + assert( pCell->MarkN == 0 ); + assert( pCell->MarkP == 0 ); + assert( pCell->Cube == 0 ); + pCell->Cube = hCube; + if ( pBin->Table == 0 ) + { + pBin->Table = pCell->Next = pCell->Prev = iLink; + return; + } + // find equal cubes + for ( iEnt = pBin->Table; iEnt != (int)pBin->Table || fStart; iEnt = pEnt->Next, fStart = 0 ) + { + pEnt = Fxch_TabBin( p, iEnt ); + if ( pEnt->MarkN || pEnt->MarkP || !Fxch_TabCompare(p, pEnt->Cube, hCube) ) + continue; + Fxch_TabInsertLink( p, iEnt, iLink, 0 ); + Fxch_TabMarkPair( p, iEnt, iLink ); + // get literals + Lit0 = Vec_IntEntry( Fxch_ManCube(p, hCube), Pla_CubeLit(hCube) ); + Lit1 = Vec_IntEntry( Fxch_ManCube(p, pEnt->Cube), Pla_CubeLit(pEnt->Cube) ); + // increment divisor weight + iDiv = Fxch_DivisorAdd( p, Abc_LitNot(Lit0), Abc_LitNot(Lit1), Vec_IntSize(Fxch_ManCube(p, hCube)) ); + // add divisor pair + assert( iDiv < Vec_WecSize(&p->vPairs) ); + if ( Lit0 < Lit1 ) + { + Vec_WecPush( &p->vPairs, iDiv, hCube ); + Vec_WecPush( &p->vPairs, iDiv, pEnt->Cube ); + } + else + { + Vec_WecPush( &p->vPairs, iDiv, pEnt->Cube ); + Vec_WecPush( &p->vPairs, iDiv, hCube ); + } + p->nPairsD++; + return; + } + assert( iEnt == (int)pBin->Table ); + pEnt = Fxch_TabBin( p, iEnt ); + Fxch_TabInsertLink( p, pEnt->Prev, iLink, 1 ); +} +static inline void Fxch_TabExtract( Fxch_Man_t * p, int iLink, int Value, int hCube ) +{ + int Lit0, Lit1; + Fxch_Obj_t * pPair = NULL; + Fxch_Obj_t * pBin = Fxch_TabBin( p, Value ); + Fxch_Obj_t * pLink = Fxch_TabEntry( p, iLink ); + assert( pLink->Cube == hCube ); + if ( pLink->MarkN ) + { + pPair = Fxch_TabEntry( p, pLink->Next ); + Fxch_TabUnmarkPair( p, iLink, pLink->Next ); + } + else if ( pLink->MarkP ) + { + pPair = Fxch_TabEntry( p, pLink->Prev ); + Fxch_TabUnmarkPair( p, pLink->Prev, iLink ); + } + if ( (int)pBin->Table == iLink ) + pBin->Table = pLink->Next != iLink ? pLink->Next : 0; + if ( pLink->Next == iLink ) + { + assert( pLink->Prev == iLink ); + pLink->Next = pLink->Prev = 0; + } + else + Fxch_TabExtractLink( p, pLink->Prev, iLink ); + pLink->Cube = 0; + if ( pPair == NULL ) + return; + assert( Fxch_TabCompare(p, pPair->Cube, hCube) ); + // get literals + Lit0 = Vec_IntEntry( Fxch_ManCube(p, hCube), Pla_CubeLit(hCube) ); + Lit1 = Vec_IntEntry( Fxch_ManCube(p, pPair->Cube), Pla_CubeLit(pPair->Cube) ); + // decrement divisor weight + Fxch_DivisorRemove( p, Abc_LitNot(Lit0), Abc_LitNot(Lit1), Vec_IntSize(Fxch_ManCube(p, hCube)) ); + p->nPairsD--; +} + +/**Function************************************************************* + + Synopsis [Starting the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Fxch_TabSingleDivisors( Fxch_Man_t * p, int iCube, int fAdd ) +{ + Vec_Int_t * vCube = Vec_WecEntry( &p->vCubes, iCube ); + int i, k, Lit, Lit2; + if ( Vec_IntSize(vCube) < 2 ) + return 0; + Vec_IntForEachEntry( vCube, Lit, i ) + Vec_IntForEachEntryStart( vCube, Lit2, k, i+1 ) + { + assert( Lit < Lit2 ); + if ( fAdd ) + Fxch_DivisorAdd( p, Lit, Lit2, 1 ), p->nPairsS++; + else + Fxch_DivisorRemove( p, Lit, Lit2, 1 ), p->nPairsS--; + } + return Vec_IntSize(vCube) * (Vec_IntSize(vCube) - 1) / 2; +} +int Fxch_TabDoubleDivisors( Fxch_Man_t * p, int iCube, int fAdd ) +{ + Vec_Int_t * vCube = Vec_WecEntry( &p->vCubes, iCube ); + int iLinkFirst = Vec_IntEntry( &p->vCubeLinks, iCube ); + int k, Lit, Value = 0; + Vec_IntForEachEntry( vCube, Lit, k ) + Value += Vec_IntEntry(&p->vRands, Lit); + Vec_IntForEachEntry( vCube, Lit, k ) + { + Value -= Vec_IntEntry(&p->vRands, Lit); + if ( fAdd ) + Fxch_TabInsert( p, iLinkFirst + k, Value, Pla_CubeHandle(iCube, k) ); + else + Fxch_TabExtract( p, iLinkFirst + k, Value, Pla_CubeHandle(iCube, k) ); + Value += Vec_IntEntry(&p->vRands, Lit); + } + return 1; +} +void Fxch_ManCreateDivisors( Fxch_Man_t * p ) +{ + float Weight; int i; + // alloc hash table + assert( p->vHash == NULL ); + p->vHash = Hash_IntManStart( 1000 ); + // create single-cube two-literal divisors + for ( i = 0; i < Vec_WecSize(&p->vCubes); i++ ) + Fxch_TabSingleDivisors( p, i, 1 ); // add - no update + // create two-cube divisors + for ( i = 0; i < Vec_WecSize(&p->vCubes); i++ ) + Fxch_TabDoubleDivisors( p, i, 1 ); // add - no update + // create queue with all divisors + p->vPrio = Vec_QueAlloc( Vec_FltSize(&p->vWeights) ); + Vec_QueSetPriority( p->vPrio, Vec_FltArrayP(&p->vWeights) ); + Vec_FltForEachEntry( &p->vWeights, Weight, i ) + if ( Weight > 0.0 ) + Vec_QuePush( p->vPrio, i ); +} + + +/**Function************************************************************* + + Synopsis [Updates the data-structure when one divisor is selected.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fxch_ManUpdate( Fxch_Man_t * p, int iDiv ) +{ + Vec_Int_t * vCube1, * vCube2, * vLitP, * vLitN; + int nLitsNew = p->nLits - (int)Vec_FltEntry(&p->vWeights, iDiv); + int i, Lit0, Lit1, hCube1, hCube2, iVarNew; + //float Diff = Vec_FltEntry(&p->vWeights, iDiv) - (float)((int)Vec_FltEntry(&p->vWeights, iDiv)); + //assert( Diff > 0.0 && Diff < 1.0 ); + + // get the divisor and select pivot variables + Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF ); + Vec_IntPush( &p->vRands, Gia_ManRandom(0) & 0x3FFFFFF ); + Lit0 = Hash_IntObjData0( p->vHash, iDiv ); + Lit1 = Hash_IntObjData1( p->vHash, iDiv ); + assert( Lit0 >= 0 && Lit1 >= 0 && Lit0 < Lit1 ); + Vec_WrdPush( &p->vDivs, ((word)Lit1 << 32) | (word)Lit0 ); + + // if the input cover is not prime, it may happen that we are extracting divisor (x + !x) + // although it is not strictly correct, it seems to be fine to just skip such divisors +// if ( Abc_Lit2Var(Lit0) == Abc_Lit2Var(Lit1) && Vec_IntSize(Hsh_VecReadEntry(p->vHash, iDiv)) == 2 ) +// return; + + // collect single-cube-divisor cubes + vLitP = Vec_WecEntry(&p->vLits, Lit0); + vLitN = Vec_WecEntry(&p->vLits, Lit1); + Fxch_CompressCubes( p, vLitP ); + Fxch_CompressCubes( p, vLitN ); +// Fxch_CollectSingles( vLitP, vLitN, &p->vCubesS ); +// assert( Vec_IntSize(&p->vCubesS) % 2 == 0 ); + Vec_IntTwoRemoveCommon( vLitP, vLitN, &p->vCubesS ); + Fxch_FilterCubes( p, &p->vCubesS, Lit0, Lit1 ); + + // collect double-cube-divisor cube pairs + Fxch_CollectDoubles( p, Vec_WecEntry(&p->vPairs, iDiv), &p->vCubesD, Abc_LitNot(Lit0), Abc_LitNot(Lit1) ); + assert( Vec_IntSize(&p->vCubesD) % 2 == 0 ); + Vec_IntUniqifyPairs( &p->vCubesD ); + assert( Vec_IntSize(&p->vCubesD) % 2 == 0 ); + + // subtract cost of single-cube divisors +// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i ) + Vec_IntForEachEntry( &p->vCubesS, hCube1, i ) + Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 ); // remove - update + Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i ) + Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 0 ), // remove - update + Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube2), 0 ); // remove - update + + // subtract cost of double-cube divisors +// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i ) + Vec_IntForEachEntry( &p->vCubesS, hCube1, i ) + { + //printf( "%d ", Pla_CubeNum(hCube1) ); + Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 ); // remove - update + } + //printf( "\n" ); + + Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i ) + { + //printf( "%d ", Pla_CubeNum(hCube1) ); + //printf( "%d ", Pla_CubeNum(hCube2) ); + Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 0 ), // remove - update + Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube2), 0 ); // remove - update + } + //printf( "\n" ); + + // create new literals + p->nLits += 2; + iVarNew = Vec_WecSize( &p->vLits ) / 2; + vLitP = Vec_WecPushLevel( &p->vLits ); + vLitN = Vec_WecPushLevel( &p->vLits ); + vLitP = Vec_WecEntry( &p->vLits, Vec_WecSize(&p->vLits) - 2 ); + // update single-cube divisor cubes +// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i ) + Vec_IntForEachEntry( &p->vCubesS, hCube1, i ) + { +// int Lit0s, Lit1s; + vCube1 = Fxch_ManCube( p, hCube1 ); +// Lit0s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)); +// Lit1s = Vec_IntEntry(vCube1, Pla_CubeLit(hCube2)); +// assert( Pla_CubeNum(hCube1) == Pla_CubeNum(hCube2) ); +// assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Lit0 ); +// assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube2)) == Lit1 ); + Fxch_CompressLiterals( vCube1, Lit0, Lit1 ); +// Vec_IntPush( vLitP, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) ); + Vec_IntPush( vLitP, Pla_CubeNum(hCube1) ); + Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 0) ); + + //if ( Pla_CubeNum(hCube1) == 3 ) + // printf( "VecSize = %d\n", Vec_IntSize(vCube1) ); + + p->nLits--; + } + // update double-cube divisor cube pairs + Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i ) + { + vCube1 = Fxch_ManCube( p, hCube1 ); + vCube2 = Fxch_ManCube( p, hCube2 ); + assert( Vec_IntEntry(vCube1, Pla_CubeLit(hCube1)) == Abc_LitNot(Lit0) ); + assert( Vec_IntEntry(vCube2, Pla_CubeLit(hCube2)) == Abc_LitNot(Lit1) ); + Fxch_CompressLiterals2( vCube1, Pla_CubeLit(hCube1), -1 ); +// Vec_IntPush( vLitN, Pla_CubeHandle(Pla_CubeNum(hCube1), Vec_IntSize(vCube1)) ); + Vec_IntPush( vLitN, Pla_CubeNum(hCube1) ); + Vec_IntPush( vCube1, Abc_Var2Lit(iVarNew, 1) ); + p->nLits -= Vec_IntSize(vCube2); + + //if ( Pla_CubeNum(hCube1) == 3 ) + // printf( "VecSize = %d\n", Vec_IntSize(vCube1) ); + + // remove second cube + Vec_IntClear( vCube2 ); + } + Vec_IntSort( vLitN, 0 ); + Vec_IntSort( vLitP, 0 ); + + // add cost of single-cube divisors +// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i ) + Vec_IntForEachEntry( &p->vCubesS, hCube1, i ) + Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update + Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i ) + Fxch_TabSingleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update + + // add cost of double-cube divisors +// Vec_IntForEachEntryDouble( &p->vCubesS, hCube1, hCube2, i ) + Vec_IntForEachEntry( &p->vCubesS, hCube1, i ) + Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update + Vec_IntForEachEntryDouble( &p->vCubesD, hCube1, hCube2, i ) + Fxch_TabDoubleDivisors( p, Pla_CubeNum(hCube1), 1 ); // add - update + + // check predicted improvement: (new SOP lits == old SOP lits - divisor weight) + //assert( p->nLits == nLitsNew ); +} + +/**Function************************************************************* + + Synopsis [Implements the improved fast_extract algorithm.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Fxch_PrintStats( Fxch_Man_t * p, abctime clk ) +{ + printf( "Num =%6d ", Vec_WrdSize(&p->vDivs) - p->nVars ); + printf( "Cubes =%8d ", Vec_WecSizeUsed(&p->vCubes) ); + printf( "Lits =%8d ", p->nLits ); + printf( "Divs =%8d ", Hash_IntManEntryNum(p->vHash) ); + printf( "Divs+ =%8d ", Vec_QueSize(p->vPrio) ); + printf( "PairS =%6d ", p->nPairsS ); + printf( "PairD =%6d ", p->nPairsD ); + Abc_PrintTime( 1, "Time", clk ); +// printf( "\n" ); +} +static inline void Fxch_PrintDivOne( Fxch_Man_t * p, int iDiv ) +{ + int i; + int Lit0 = Hash_IntObjData0( p->vHash, iDiv ); + int Lit1 = Hash_IntObjData1( p->vHash, iDiv ); + assert( Lit0 >= 0 && Lit1 >= 0 && Lit0 < Lit1 ); + printf( "Div %4d : ", iDiv ); + printf( "Weight %12.5f ", Vec_FltEntry(&p->vWeights, iDiv) ); + printf( "Pairs = %5d ", Vec_IntSize(Vec_WecEntry(&p->vPairs, iDiv))/2 ); + for ( i = 0; i < Vec_WrdSize(&p->vDivs); i++ ) + { + if ( i == Abc_Lit2Var(Lit0) ) + printf( "%d", !Abc_LitIsCompl(Lit0) ); + else if ( i == Abc_Lit2Var(Lit1) ) + printf( "%d", !Abc_LitIsCompl(Lit1) ); + else + printf( "-" ); + } + printf( "\n" ); +} +static void Fxch_PrintDivisors( Fxch_Man_t * p ) +{ + int iDiv; + for ( iDiv = 1; iDiv < Vec_FltSize(&p->vWeights); iDiv++ ) + Fxch_PrintDivOne( p, iDiv ); + printf( "\n" ); +} + +int Fxch_ManFastExtract( Fxch_Man_t * p, int fVerbose, int fVeryVerbose ) +{ + int nNewNodesMax = ABC_INFINITY; + abctime clk = Abc_Clock(); + int i, iDiv; + Fxch_ManCreateDivisors( p ); +// Fxch_PrintDivisors( p ); + if ( fVerbose ) + Fxch_PrintStats( p, Abc_Clock() - clk ); + p->timeStart = Abc_Clock(); + for ( i = 0; i < nNewNodesMax && Vec_QueTopPriority(p->vPrio) > 0.0; i++ ) + { + iDiv = Vec_QuePop(p->vPrio); + //if ( fVerbose ) + // Fxch_PrintStats( p, Abc_Clock() - clk ); + if ( fVeryVerbose ) + Fxch_PrintDivOne( p, iDiv ); + Fxch_ManUpdate( p, iDiv ); + } + if ( fVerbose ) + Fxch_PrintStats( p, Abc_Clock() - clk ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Implements the improved fast_extract algorithm.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pla_ManPerformFxch( Pla_Man_t * p ) +{ + char pFileName[1000]; + Fxch_Man_t * pFxch; + Pla_ManConvertFromBits( p ); + pFxch = Fxch_ManStart( &p->vCubeLits, &p->vOccurs ); + Vec_WecZero( &p->vCubeLits ); + Vec_WecZero( &p->vOccurs ); + Fxch_ManFastExtract( pFxch, 1, 0 ); + sprintf( pFileName, "%s.blif", Pla_ManName(p) ); + //Fxch_ManWriteBlif( pFileName, &pFxch->vCubes, &pFxch->vDivs ); + Fxch_ManStop( pFxch ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/pla/plaHash.c b/src/base/pla/plaHash.c index d05bd9c9..b51ba4c1 100644 --- a/src/base/pla/plaHash.c +++ b/src/base/pla/plaHash.c @@ -63,7 +63,7 @@ static unsigned s_PlaHashValues[PLA_HASH_VALUE_NUM] = 0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d }; -static inline int Pla_HashValue( int i ) { assert( i >= 0 && i < PLA_HASH_VALUE_NUM ); return s_PlaHashValues[i] & 0xFFFFFF; } +static inline int Pla_HashValue( int i ) { assert( i >= 0 && i < PLA_HASH_VALUE_NUM ); return s_PlaHashValues[i] & 0x3FFFFFF; } #define PLA_LIT_UNUSED 0xFFFF @@ -107,7 +107,7 @@ static inline Tab_Obj_t * Tab_ManEntry( Tab_Man_t * p, int i ) { return i ? p static inline Tab_Man_t * Tab_ManAlloc( int LogSize, Pla_Man_t * pMan ) { Tab_Man_t * p = ABC_CALLOC( Tab_Man_t, 1 ); - assert( LogSize >= 4 && LogSize <= 24 ); + assert( LogSize >= 4 && LogSize <= 26 ); p->SizeMask = (1 << LogSize) - 1; p->pBins = ABC_CALLOC( Tab_Obj_t, p->SizeMask + 1 ); p->nBins = 1; @@ -119,11 +119,12 @@ static inline void Tab_ManFree( Tab_Man_t * p ) ABC_FREE( p->pBins ); ABC_FREE( p ); } -static inline void Tab_ManHashInsert( Tab_Man_t * p, int Value, int iCube ) +static inline void Tab_ManHashInsert( Tab_Man_t * p, int Value, int iCube, int iVar ) { Tab_Obj_t * pBin = Tab_ManBin( p, Value ); Tab_Obj_t * pCell = p->pBins + p->nBins; pCell->Cube = iCube; + pCell->VarA = iVar; pCell->Next = pBin->Table; pBin->Table = p->nBins++; } @@ -131,10 +132,17 @@ static inline int Tab_ManHashLookup( Tab_Man_t * p, int Value, Vec_Int_t * vCube { Tab_Obj_t * pEnt, * pBin = Tab_ManBin( p, Value ); for ( pEnt = Tab_ManEntry(p, pBin->Table); pEnt; pEnt = Tab_ManEntry(p, pEnt->Next) ) - if ( Vec_IntEqual( Vec_WecEntry(&p->pMan->vLits, pEnt->Cube), vCube ) ) + if ( Vec_IntEqual( Vec_WecEntry(&p->pMan->vCubeLits, pEnt->Cube), vCube ) ) return 1; return 0; } +static inline void Tab_ManHashCollect( Tab_Man_t * p, int iBin, Vec_Int_t * vEntries ) +{ + Tab_Obj_t * pEnt, * pBin = Tab_ManBin( p, iBin ); + Vec_IntClear( vEntries ); + for ( pEnt = Tab_ManEntry(p, pBin->Table); pEnt; pEnt = Tab_ManEntry(p, pEnt->Next) ) + Vec_IntPushTwo( vEntries, pEnt->Cube, pEnt->VarA ); +} /**Function************************************************************* @@ -160,11 +168,11 @@ void Pla_ManHashCubes( Pla_Man_t * p, Tab_Man_t * pTab ) Vec_Int_t * vCube; int i, Value; Vec_IntClear( &p->vHashes ); Vec_IntGrow( &p->vHashes, Pla_ManCubeNum(p) ); - Vec_WecForEachLevel( &p->vLits, vCube, i ) + Vec_WecForEachLevel( &p->vCubeLits, vCube, i ) { Value = Pla_CubeHashValue(vCube); Vec_IntPush( &p->vHashes, Value ); - Tab_ManHashInsert( pTab, Value, i ); + Tab_ManHashInsert( pTab, Value, i, PLA_LIT_UNUSED ); } } int Pla_ManHashDistance1( Pla_Man_t * p ) @@ -174,11 +182,11 @@ int Pla_ManHashDistance1( Pla_Man_t * p ) Vec_Int_t * vCubeCopy = Vec_IntAlloc( p->nIns ); int nBits = Abc_Base2Log( Pla_ManCubeNum(p) ) + 2; int i, k, Lit, Value, ValueCopy, Count = 0; - assert( nBits <= 24 ); + assert( nBits <= 26 ); pTab = Tab_ManAlloc( nBits, p ); Pla_ManConvertFromBits( p ); Pla_ManHashCubes( p, pTab ); - Vec_WecForEachLevel( &p->vLits, vCube, i ) + Vec_WecForEachLevel( &p->vCubeLits, vCube, i ) { Vec_IntClear( vCubeCopy ); Vec_IntAppend( vCubeCopy, vCube ); @@ -210,6 +218,126 @@ int Pla_ManHashDist1NumTest( Pla_Man_t * p ) return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pla_PrintCube( Vec_Int_t * vLits, int nVars, int iVar ) +{ + int v, Lit; + Vec_Str_t * vStr = Vec_StrStart( nVars + 1 ); + Vec_StrFill( vStr, nVars, '-' ); + Vec_IntForEachEntry( vLits, Lit, v ) + Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') ); + fprintf( stdout, "%s %d\n", Vec_StrArray(vStr), iVar ); + Vec_StrFree( vStr ); +} +void Pla_ManHashCubes2( Pla_Man_t * p, Tab_Man_t * pTab ) +{ + Vec_Int_t * vCube; + int i, v, Lit, Value; + Vec_WecForEachLevel( &p->vCubeLits, vCube, i ) + { + Value = Pla_CubeHashValue(vCube); + Vec_IntForEachEntry( vCube, Lit, v ) + { + Value -= Pla_HashValue(Lit); + Tab_ManHashInsert( pTab, Value, i, v ); + Value += Pla_HashValue(Lit); + } + } +} +void Vec_IntCopySkip( Vec_Int_t * vCube, int iVar, Vec_Int_t * vRes ) +{ + int i; + Vec_IntClear( vRes ); + for ( i = 0; i < Vec_IntSize(vCube); i++ ) + if ( i != iVar ) + Vec_IntPush( vRes, Vec_IntEntry(vCube, i) ); +} +Vec_Int_t * Pla_ManComputeDistance1Int( Pla_Man_t * p ) +{ + Tab_Man_t * pTab; + Vec_Int_t * vCube1, * vCube2; + Vec_Int_t * vTemp1 = Vec_IntAlloc( 100 ); + Vec_Int_t * vTemp2 = Vec_IntAlloc( 100 ); + Vec_Int_t * vPairs = Vec_IntAlloc( 1000 ); + Vec_Int_t * vCounts = Vec_IntStart( Vec_WecSize(&p->vCubeLits) ); + Vec_Int_t * vEntries = Vec_IntAlloc( p->nIns ); + int nBits = Abc_Base2Log( Vec_WecSizeSize(&p->vCubeLits) ) + 2; + int v, i, k, Count = 0; + int iCube1, iCube2, iVar1, iVar2; + assert( nBits <= 26 ); + pTab = Tab_ManAlloc( nBits, p ); + //Pla_ManConvertFromBits( p ); + Pla_ManHashCubes2( p, pTab ); + // iterate through the hash bins + for ( v = 0; v <= pTab->SizeMask; v++ ) + { + Tab_ManHashCollect( pTab, v, vEntries ); + for ( i = 0; i < Vec_IntSize(vEntries)/2; i++ ) + for ( k = i+1; k < Vec_IntSize(vEntries)/2; k++ ) + { + iCube1 = Vec_IntEntry(vEntries, 2*i); + iCube2 = Vec_IntEntry(vEntries, 2*k); + iVar1 = Vec_IntEntry(vEntries, 2*i+1); + iVar2 = Vec_IntEntry(vEntries, 2*k+1); + + vCube1 = Vec_WecEntry(&p->vCubeLits, iCube1); + vCube2 = Vec_WecEntry(&p->vCubeLits, iCube2); +/* + Pla_PrintCube( vCube1, p->nIns, iVar1 ); + Pla_PrintCube( vCube2, p->nIns, iVar2 ); + printf( "\n" ); +*/ + if ( Vec_IntSize(vCube1) != Vec_IntSize(vCube2) ) + continue; + Vec_IntCopySkip( vCube1, iVar1, vTemp1 ); + Vec_IntCopySkip( vCube2, iVar2, vTemp2 ); + if ( !Vec_IntEqual( vTemp1, vTemp2 ) ) + continue; + + printf( "%d %d ", iCube1, iCube2 ); + + Vec_IntPushTwo( vPairs, iCube1, iVar1 ); + Vec_IntPushTwo( vPairs, iCube2, iVar2 ); + + Vec_IntAddToEntry( vCounts, iCube1, 1 ); + Vec_IntAddToEntry( vCounts, iCube2, 1 ); + } + } + Vec_IntPrint( vCounts ); + + Vec_IntFree( vCounts ); + Vec_IntFree( vTemp1 ); + Vec_IntFree( vTemp2 ); + Vec_IntFree( vEntries ); + Tab_ManFree( pTab ); + return vPairs; +} +Vec_Int_t * Pla_ManComputeDistance1( Pla_Man_t * p ) +{ + abctime clk = Abc_Clock(); + Vec_Int_t * vPairs = Pla_ManComputeDistance1Int( p ); + printf( "Found %d pairs among %d cubes using cube hashing. ", Vec_IntSize(vPairs)/4, Pla_ManCubeNum(p) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return vPairs; +} +void Pla_ManComputeDist1Test( Pla_Man_t * p ) +{ + Vec_Int_t * vPairs; + Pla_ManConvertFromBits( p ); + vPairs = Pla_ManComputeDistance1( p ); + Vec_IntFree( vPairs ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/pla/plaMan.c b/src/base/pla/plaMan.c index bc3cd8ad..23ea8368 100644 --- a/src/base/pla/plaMan.c +++ b/src/base/pla/plaMan.c @@ -41,19 +41,28 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Vec_Int_t * Pla_GenPrimes( int nVars ) +Vec_Bit_t * Pla_ManPrimesTable( int nVars ) { - int i, n, nBits = ( 1 << nVars ); - Vec_Bit_t * vMap = Vec_BitStart( nBits ); - Vec_Int_t * vPrimes = Vec_IntAlloc( 1000 ); - Vec_BitWriteEntry(vMap, 0, 1); - Vec_BitWriteEntry(vMap, 1, 1); + int i, n, nBits = 1 << nVars; + Vec_Bit_t * vMap = Vec_BitStartFull( Abc_MaxInt(64, nBits) ); + for ( i = nBits; i < 64; i++ ) + Vec_BitWriteEntry( vMap, i, 0 ); + Vec_BitShrink( vMap, nBits ); + Vec_BitWriteEntry( vMap, 0, 0 ); + Vec_BitWriteEntry( vMap, 1, 0 ); for ( n = 2; n < nBits; n++ ) - if ( !Vec_BitEntry(vMap, n) ) + if ( Vec_BitEntry(vMap, n) ) for ( i = 2*n; i < nBits; i += n ) - Vec_BitWriteEntry(vMap, i, 1); + Vec_BitWriteEntry( vMap, i, 0 ); + return vMap; +} +Vec_Int_t * Pla_GenPrimes( int nVars ) +{ + int n, nBits = ( 1 << nVars ); + Vec_Int_t * vPrimes = Vec_IntAlloc( 1000 ); + Vec_Bit_t * vMap = Pla_ManPrimesTable( nVars ); for ( n = 2; n < nBits; n++ ) - if ( !Vec_BitEntry(vMap, n) ) + if ( Vec_BitEntry(vMap, n) ) Vec_IntPush( vPrimes, n ); printf( "Primes up to 2^%d = %d\n", nVars, Vec_IntSize(vPrimes) ); // Abc_GenCountHits1( vMap, vPrimes, nVars ); @@ -75,7 +84,7 @@ Pla_Man_t * Pla_GenFromMinterms( char * pName, Vec_Int_t * vMints, int nVars ) Pla_CubeSetLit( pCube, 0, PLA_LIT_ONE ); return p; } -Pla_Man_t * Pla_ManPrimeDetector( int nVars ) +Pla_Man_t * Pla_ManPrimesDetector( int nVars ) { char pName[1000]; Pla_Man_t * p; @@ -117,10 +126,13 @@ Vec_Bit_t * Pla_GenRandom( int nVars, int nNums, int fNonZero ) } Pla_Man_t * Pla_ManGenerate( int nInputs, int nOutputs, int nCubes, int fVerbose ) { + Pla_Man_t * p; Vec_Bit_t * vBits; int i, k, Count; word * pCube; - Pla_Man_t * p = Pla_ManAlloc( "rand", nInputs, nOutputs, nCubes ); + char Buffer[1000]; + sprintf( Buffer, "%s_%d_%d_%d", "rand", nInputs, nOutputs, nCubes ); + p = Pla_ManAlloc( Buffer, nInputs, nOutputs, nCubes ); // generate nCube random input minterms vBits = Pla_GenRandom( nInputs, nCubes, 0 ); for ( i = Count = 0; i < Vec_BitSize(vBits); i++ ) @@ -167,26 +179,40 @@ Pla_Man_t * Pla_ManGenerate( int nInputs, int nOutputs, int nCubes, int fVerbose ***********************************************************************/ void Pla_ManConvertFromBits( Pla_Man_t * p ) { - word * pCube; int i, k, Lit; - Vec_WecClear( &p->vLits ); + Vec_Int_t * vCube; + word * pCube; int i, k, Lit, Count; + Vec_WecClear( &p->vCubeLits ); Vec_WecClear( &p->vOccurs ); - Vec_WecInit( &p->vLits, Pla_ManCubeNum(p) ); + Vec_WecInit( &p->vCubeLits, Pla_ManCubeNum(p) ); Vec_WecInit( &p->vOccurs, 2*Pla_ManInNum(p) ); Pla_ForEachCubeIn( p, pCube, i ) + { + vCube = Vec_WecEntry( &p->vCubeLits, i ); + + Count = 0; + Pla_CubeForEachLitIn( p, pCube, Lit, k ) + if ( Lit != PLA_LIT_DASH ) + Count++; + Vec_IntGrow( vCube, Count ); + + Count = 0; Pla_CubeForEachLitIn( p, pCube, Lit, k ) if ( Lit != PLA_LIT_DASH ) { Lit = Abc_Var2Lit( k, Lit == PLA_LIT_ZERO ); - Vec_WecPush( &p->vLits, i, Lit ); + Vec_WecPush( &p->vCubeLits, i, Lit ); +// Vec_WecPush( &p->vOccurs, Lit, Pla_CubeHandle(i, Count++) ); Vec_WecPush( &p->vOccurs, Lit, i ); } + assert( Vec_IntSize(vCube) == Vec_IntCap(vCube) ); + } } void Pla_ManConvertToBits( Pla_Man_t * p ) { Vec_Int_t * vCube; int i, k, Lit; - Vec_IntFillNatural( &p->vCubes, Vec_WecSize(&p->vLits) ); + Vec_IntFillNatural( &p->vCubes, Vec_WecSize(&p->vCubeLits) ); Vec_WrdFill( &p->vInBits, Pla_ManCubeNum(p) * p->nInWords, 0 ); - Vec_WecForEachLevel( &p->vLits, vCube, i ) + Vec_WecForEachLevel( &p->vCubeLits, vCube, i ) Vec_IntForEachEntry( vCube, Lit, k ) Pla_CubeSetLit( Pla_CubeIn(p, i), Abc_Lit2Var(Lit), Abc_LitIsCompl(Lit) ? PLA_LIT_ZERO : PLA_LIT_ONE ); } diff --git a/src/base/pla/plaSimple.c b/src/base/pla/plaSimple.c new file mode 100644 index 00000000..8fea5c1f --- /dev/null +++ b/src/base/pla/plaSimple.c @@ -0,0 +1,339 @@ +/**CFile**************************************************************** + + FileName [plaSimple.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SOP manager.] + + Synopsis [Scalable SOP transformations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - March 18, 2015.] + + Revision [$Id: plaSimple.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "pla.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Dump PLA manager into a BLIF file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Pla_ManDumpPla( Pla_Man_t * p, char * pFileName ) +{ + // find the number of original variables + int nVarsInit = Pla_ManDivNum(p) ? Vec_IntCountZero(&p->vDivs) : Pla_ManInNum(p); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + else + { + char * pLits = "-01?"; + Vec_Str_t * vStr; + Vec_Int_t * vCube; + int i, k, Lit; + // comment + fprintf( pFile, "# PLA file written via PLA package in ABC on " ); + fprintf( pFile, "%s", Extra_TimeStamp() ); + fprintf( pFile, "\n\n" ); + // header + fprintf( pFile, ".i %d\n", Pla_ManInNum(p) ); + fprintf( pFile, ".o %d\n", 1 ); + fprintf( pFile, ".p %d\n", Vec_WecSize(&p->vCubeLits) ); + // SOP + vStr = Vec_StrStart( Pla_ManInNum(p) + 1 ); + Vec_WecForEachLevel( &p->vCubeLits, vCube, i ) + { + if ( !Vec_IntSize(vCube) ) + continue; + for ( k = 0; k < Pla_ManInNum(p); k++ ) + Vec_StrWriteEntry( vStr, k, '-' ); + Vec_IntForEachEntry( vCube, Lit, k ) + Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') ); + fprintf( pFile, "%s 1\n", Vec_StrArray(vStr) ); + } + Vec_StrFree( vStr ); + fprintf( pFile, ".e\n\n" ); + fclose( pFile ); + printf( "Written file \"%s\".\n", pFileName ); + } +} +void Pla_ManDumpBlif( Pla_Man_t * p, char * pFileName ) +{ + // find the number of original variables + int nVarsInit = Pla_ManDivNum(p) ? Vec_IntCountZero(&p->vDivs) : Pla_ManInNum(p); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + else + { + char * pLits = "-01?"; + Vec_Str_t * vStr; + Vec_Int_t * vCube; + int i, k, Lit, Div; + // comment + fprintf( pFile, "# BLIF file written via PLA package in ABC on " ); + fprintf( pFile, "%s", Extra_TimeStamp() ); + fprintf( pFile, "\n\n" ); + // header + fprintf( pFile, ".model %s\n", Pla_ManName(p) ); + fprintf( pFile, ".inputs" ); + for ( i = 0; i < nVarsInit; i++ ) + fprintf( pFile, " i%d", i ); + fprintf( pFile, "\n" ); + fprintf( pFile, ".outputs o" ); + fprintf( pFile, "\n" ); + // SOP + fprintf( pFile, ".names" ); + for ( i = 0; i < Pla_ManInNum(p); i++ ) + fprintf( pFile, " i%d", i ); + fprintf( pFile, " o\n" ); + vStr = Vec_StrStart( Pla_ManInNum(p) + 1 ); + Vec_WecForEachLevel( &p->vCubeLits, vCube, i ) + { + for ( k = 0; k < Pla_ManInNum(p); k++ ) + Vec_StrWriteEntry( vStr, k, '-' ); + Vec_IntForEachEntry( vCube, Lit, k ) + Vec_StrWriteEntry( vStr, Abc_Lit2Var(Lit), (char)(Abc_LitIsCompl(Lit) ? '0' : '1') ); + fprintf( pFile, "%s 1\n", Vec_StrArray(vStr) ); + } + Vec_StrFree( vStr ); + // divisors + Vec_IntForEachEntryStart( &p->vDivs, Div, i, nVarsInit ) + { + int pLits[3] = { (Div >> 2) & 0x3FF, (Div >> 12) & 0x3FF, (Div >> 22) & 0x3FF }; + fprintf( pFile, ".names" ); + fprintf( pFile, " i%d", Abc_Lit2Var(pLits[0]) ); + fprintf( pFile, " i%d", Abc_Lit2Var(pLits[1]) ); + if ( (Div & 3) == 3 ) // MUX + fprintf( pFile, " i%d", Abc_Lit2Var(pLits[2]) ); + fprintf( pFile, " i%d\n", i ); + if ( (Div & 3) == 1 ) // AND + fprintf( pFile, "%d%d 1\n", !Abc_LitIsCompl(pLits[0]), !Abc_LitIsCompl(pLits[1]) ); + else if ( (Div & 3) == 2 ) // XOR + { + assert( !Abc_LitIsCompl(pLits[0]) ); + assert( !Abc_LitIsCompl(pLits[1]) ); + fprintf( pFile, "10 1\n01 1\n" ); + } + else if ( (Div & 3) == 3 ) // MUX + { + assert( !Abc_LitIsCompl(pLits[1]) ); + assert( !Abc_LitIsCompl(pLits[2]) ); + fprintf( pFile, "%d-0 1\n-11 1\n", !Abc_LitIsCompl(pLits[0]) ); + } + else assert( 0 ); + } + fprintf( pFile, ".end\n\n" ); + fclose( pFile ); + printf( "Written file \"%s\".\n", pFileName ); + } +} + +/**Function************************************************************* + + Synopsis [Transforms truth table into an SOP manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Pla_ManExpendDirNum( word * pOn, int nBits, int iMint, int * pVars ) +{ + int v, nVars = 0; + for ( v = 0; v < nBits; v++ ) + if ( Pla_TtGetBit(pOn, iMint ^ (1 << v)) ) + pVars[nVars++] = v; + return nVars; +} +void Pla_PrintBinary( word * pT, int nBits ) +{ + int v; + for ( v = 0; v < nBits; v++ ) + printf( "%d", Pla_TtGetBit(pT, v) ); + printf( "\n" ); +} +Vec_Wrd_t * Pla_ManFxMinimize( word * pOn, int nVars ) +{ + int i, v, iMint, iVar, nMints = (1 << nVars); + int nWords = Abc_Bit6WordNum( nMints ); + Vec_Wrd_t * vCubes = Vec_WrdAlloc( 1000 ); + word * pDc = ABC_CALLOC( word, nWords ); + int Count[32] = {0}; + int Cubes[32] = {0}; + Vec_Int_t * vStore = Vec_IntAlloc( 1000 ); + + // count the number of expansion directions + for ( i = 0; i < nMints; i++ ) + if ( Pla_TtGetBit(pOn, i) && !Pla_TtGetBit(pDc, i) ) + { + int pDirs[32], nDirs = Pla_ManExpendDirNum(pOn, nVars, i, pDirs); + Count[nDirs]++; + if ( nDirs == 0 ) + { + Pla_TtSetBit(pDc, i); + Cubes[0]++; + // save + Vec_IntPushTwo( vStore, i, -1 ); + continue; + } + if ( nDirs == 1 ) + { + //Pla_PrintBinary( (word *)&i, nVars ); + //printf( " %d \n", pDirs[0] ); + + Pla_TtSetBit(pDc, i); + Pla_TtSetBit(pDc, i ^ (1 << pDirs[0])); + Cubes[1]++; + // save + Vec_IntPushTwo( vStore, i, pDirs[0] ); + continue; + } + if ( nDirs == 2 && Pla_TtGetBit(pOn, i ^ (1 << pDirs[0]) ^ (1 << pDirs[1])) ) + { + assert( 0 ); + Pla_TtSetBit(pDc, i); + Pla_TtSetBit(pDc, i ^ (1 << pDirs[0])); + Pla_TtSetBit(pDc, i ^ (1 << pDirs[1])); + Pla_TtSetBit(pDc, i ^ (1 << pDirs[0]) ^ (1 << pDirs[1])); + Cubes[2]++; + continue; + } + } + + // go through the remaining cubes + for ( i = 0; i < nMints; i++ ) + if ( Pla_TtGetBit(pOn, i) && !Pla_TtGetBit(pDc, i) ) + { + int pDirs[32], nDirs = Pla_ManExpendDirNum(pOn, nVars, i, pDirs); + // find direction, which is not taken + for ( v = 0; v < nDirs; v++ ) + if ( Pla_TtGetBit(pOn, i ^ (1 << pDirs[v])) && !Pla_TtGetBit(pDc, i ^ (1 << pDirs[v])) ) + break; + // if there is no open directions, use any one + if ( v == nDirs ) + v = 0; + // mark this one + Pla_TtSetBit(pDc, i); + Pla_TtSetBit(pDc, i ^ (1 << pDirs[v])); + Cubes[10]++; + // save + Vec_IntPushTwo( vStore, i, pDirs[v] ); + continue; + } + + printf( "\n" ); + printf( "Truth = %d. ", Pla_TtCountOnes(pOn, nWords) ); + printf( "Cover = %d. ", Pla_TtCountOnes(pDc, nWords) ); + printf( "\n" ); + + printf( "Count: " ); + for ( i = 0; i < 16; i++ ) + if ( Count[i] ) + printf( "%d=%d ", i, Count[i] ); + printf( "\n" ); + + printf( "Cubes: " ); + for ( i = 0; i < 16; i++ ) + if ( Cubes[i] ) + printf( "%d=%d ", i, Cubes[i] ); + printf( "\n" ); + +/* + // extract cubes one at a time + for ( i = 0; i < nMints; i++ ) + if ( Pla_TtGetBit(pOn, i) ) + { + word Cube = 0; + for ( v = 0; v < nVars; v++ ) + if ( (i >> v) & 1 ) + Pla_CubeSetLit( &Cube, v, PLA_LIT_ONE ); + else + Pla_CubeSetLit( &Cube, v, PLA_LIT_ZERO ); + Vec_WrdPush( vCubes, Cube ); + } +*/ + Vec_IntForEachEntryDouble( vStore, iMint, iVar, i ) + { + word Cube = 0; + for ( v = 0; v < nVars; v++ ) + { + if ( v == iVar ) + continue; + if ( (iMint >> v) & 1 ) + Pla_CubeSetLit( &Cube, v, PLA_LIT_ONE ); + else + Pla_CubeSetLit( &Cube, v, PLA_LIT_ZERO ); + } + Vec_WrdPush( vCubes, Cube ); + } + Vec_IntFree( vStore ); + + // collect the minterms + ABC_FREE( pDc ); + return vCubes; +} +Pla_Man_t * Pla_ManFxPrepare( int nVars ) +{ + Pla_Man_t * p; char Buffer[1000]; + Vec_Bit_t * vFunc = Pla_ManPrimesTable( nVars ); + Vec_Wrd_t * vSop = Pla_ManFxMinimize( (word *)Vec_BitArray(vFunc), nVars ); + word Cube, * pCube = &Cube; int i, k, Lit; + sprintf( Buffer, "primes%02d", nVars ); + p = Pla_ManAlloc( Buffer, nVars, 1, Vec_WrdSize(vSop) ); + Vec_WecInit( &p->vCubeLits, Pla_ManCubeNum(p) ); + Vec_WecInit( &p->vOccurs, 2*Pla_ManInNum(p) ); + Vec_WrdForEachEntry( vSop, Cube, i ) + Pla_CubeForEachLit( nVars, pCube, Lit, k ) + if ( Lit != PLA_LIT_DASH ) + { + Lit = Abc_Var2Lit( k, Lit == PLA_LIT_ZERO ); + Vec_WecPush( &p->vCubeLits, i, Lit ); + Vec_WecPush( &p->vOccurs, Lit, i ); + } + Vec_BitFree( vFunc ); + Vec_WrdFree( vSop ); + return p; +} +int Pla_ManFxPerformSimple( int nVars ) +{ + char Buffer[100]; + Pla_Man_t * p = Pla_ManFxPrepare( nVars ); + sprintf( Buffer, "primesmin%02d.pla", nVars ); + Pla_ManDumpPla( p, Buffer ); + Pla_ManFree( p ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/pla/plaWrite.c b/src/base/pla/plaWrite.c index ed301e87..48f429a4 100644 --- a/src/base/pla/plaWrite.c +++ b/src/base/pla/plaWrite.c @@ -49,7 +49,7 @@ Vec_Str_t * Pla_WritePlaInt( Pla_Man_t * p ) int i, k, Lit; // write comments Vec_StrPrintStr( vOut, "# SOP \"" ); - Vec_StrPrintStr( vOut, p->pName ); + Vec_StrPrintStr( vOut, Pla_ManName(p) ); Vec_StrPrintStr( vOut, "\" written via PLA package in ABC on " ); Vec_StrPrintStr( vOut, Extra_TimeStamp() ); Vec_StrPrintStr( vOut, "\n\n" ); diff --git a/src/misc/vec/vecBit.h b/src/misc/vec/vecBit.h index cb89e982..543a1258 100644 --- a/src/misc/vec/vecBit.h +++ b/src/misc/vec/vecBit.h @@ -124,7 +124,7 @@ static inline Vec_Bit_t * Vec_BitStartFull( int nSize ) { Vec_Bit_t * p; nSize = (nSize >> 5) + ((nSize & 31) > 0); - p = Vec_BitAlloc( nSize ); + p = Vec_BitAlloc( nSize * 32 ); p->nSize = nSize * 32; memset( p->pArray, 0xff, sizeof(int) * nSize ); return p; diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h index 482973f7..9988deae 100644 --- a/src/misc/vec/vecFlt.h +++ b/src/misc/vec/vecFlt.h @@ -225,6 +225,18 @@ static inline Vec_Flt_t * Vec_FltDupArray( Vec_Flt_t * pVec ) SeeAlso [] ***********************************************************************/ +static inline void Vec_FltZero( Vec_Flt_t * p ) +{ + p->pArray = NULL; + p->nSize = 0; + p->nCap = 0; +} +static inline void Vec_FltErase( Vec_Flt_t * p ) +{ + ABC_FREE( p->pArray ); + p->nSize = 0; + p->nCap = 0; +} static inline void Vec_FltFree( Vec_Flt_t * p ) { ABC_FREE( p->pArray ); diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 6d3ea8f6..e18b4616 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1338,6 +1338,16 @@ static inline void Vec_IntSort( Vec_Int_t * p, int fReverse ) qsort( (void *)p->pArray, p->nSize, sizeof(int), (int (*)(const void *, const void *)) Vec_IntSortCompare1 ); } +static inline void Vec_IntSortPairs( Vec_Int_t * p, int fReverse ) +{ + assert( Vec_IntSize(p) % 2 == 0 ); + if ( fReverse ) + qsort( (void *)p->pArray, p->nSize/2, 2*sizeof(int), + (int (*)(const void *, const void *)) Vec_IntSortCompare2 ); + else + qsort( (void *)p->pArray, p->nSize/2, 2*sizeof(int), + (int (*)(const void *, const void *)) Vec_IntSortCompare1 ); +} /**Function************************************************************* @@ -1392,6 +1402,36 @@ static inline int Vec_IntCountUnique( Vec_Int_t * p ) return Count; } +/**Function************************************************************* + + Synopsis [Counts the number of unique pairs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_IntUniqifyPairs( Vec_Int_t * p ) +{ + int i, k, RetValue; + assert( p->nSize % 2 == 0 ); + if ( p->nSize < 4 ) + return 0; + Vec_IntSortPairs( p, 0 ); + for ( i = k = 1; i < p->nSize/2; i++ ) + if ( p->pArray[2*i] != p->pArray[2*(i-1)] || p->pArray[2*i+1] != p->pArray[2*(i-1)+1] ) + { + p->pArray[2*k] = p->pArray[2*i]; + p->pArray[2*k+1] = p->pArray[2*i+1]; + k++; + } + RetValue = p->nSize/2 - k; + p->nSize = 2*k; + return RetValue; +} + /**Function************************************************************* Synopsis [Counts the number of unique entries.] @@ -1891,6 +1931,13 @@ static inline void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 ) Vec_IntForEachEntry( vVec2, Entry, i ) Vec_IntPush( vVec1, Entry ); } +static inline void Vec_IntAppendSkip( Vec_Int_t * vVec1, Vec_Int_t * vVec2, int iVar ) +{ + int Entry, i; + Vec_IntForEachEntry( vVec2, Entry, i ) + if ( i != iVar ) + Vec_IntPush( vVec1, Entry ); +} ABC_NAMESPACE_HEADER_END diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index 5227fec5..d286baf3 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -959,6 +959,25 @@ static inline word Vec_WrdSum( Vec_Wrd_t * p ) return Counter; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Vec_WrdCountZero( Vec_Wrd_t * p ) +{ + int i, Counter = 0; + for ( i = 0; i < p->nSize; i++ ) + Counter += (p->pArray[i] == 0); + return Counter; +} + /**Function************************************************************* Synopsis [Checks if two vectors are equal.] -- cgit v1.2.3