| /**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 |
| |
