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/pla/plaFxch.c | 854 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 854 insertions(+) create mode 100644 src/base/pla/plaFxch.c (limited to 'src/base/pla/plaFxch.c') 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 + -- cgit v1.2.3