From 0ae0744e73b978593a054e8bf80c35723c9f4b03 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 15 May 2020 22:11:10 -0700 Subject: Experimental resubstitution. --- src/aig/gia/gia.h | 4 +- src/aig/gia/giaResub.c | 534 ++++++++++++++++++++++++++++++++--------------- src/aig/gia/giaSimBase.c | 83 -------- src/aig/gia/giaUtil.c | 23 +- 4 files changed, 386 insertions(+), 258 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 4e10cbe6..2458b152 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1558,8 +1558,7 @@ extern void Gia_ManIncrSimSet( Gia_Man_t * p, Vec_Int_t * vObjLit extern int Gia_ManIncrSimCheckOver( Gia_Man_t * p, int iLit0, int iLit1 ); extern int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, int iLit1 ); /*=== giaSimBase.c ============================================================*/ -extern Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName, int * pnWords ); -extern void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ); +extern Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * p ); /*=== giaSpeedup.c ============================================================*/ extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); @@ -1685,6 +1684,7 @@ extern int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** extern Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE ); extern int Gia_ObjRecognizeMuxLits( Gia_Man_t * p, Gia_Obj_t * pNode, int * iLitT, int * iLitE ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); +extern int Gia_NodeMffcSizeMark( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp ); extern int Gia_ManHasDangling( Gia_Man_t * p ); extern int Gia_ManMarkDangling( Gia_Man_t * p ); diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c index 66f27310..a32d0094 100644 --- a/src/aig/gia/giaResub.c +++ b/src/aig/gia/giaResub.c @@ -290,10 +290,12 @@ struct Gia_ResbMan_t_ { int nWords; int nLimit; - int nChoice; + int nDivsMax; + int iChoice; int fUseXor; int fDebug; int fVerbose; + int fVeryVerbose; Vec_Ptr_t * vDivs; Vec_Int_t * vGates; Vec_Int_t * vUnateLits[2]; @@ -302,6 +304,7 @@ struct Gia_ResbMan_t_ Vec_Int_t * vBinateVars; Vec_Int_t * vUnateLitsW[2]; Vec_Int_t * vUnatePairsW[2]; + Vec_Wec_t * vSorter; word * pSets[2]; word * pDivA; word * pDivB; @@ -321,6 +324,7 @@ Gia_ResbMan_t * Gia_ResbAlloc( int nWords ) p->vUnateLitsW[1] = Vec_IntAlloc( 100 ); p->vUnatePairsW[0] = Vec_IntAlloc( 100 ); p->vUnatePairsW[1] = Vec_IntAlloc( 100 ); + p->vSorter = Vec_WecAlloc( nWords*64 ); p->vBinateVars = Vec_IntAlloc( 100 ); p->vGates = Vec_IntAlloc( 100 ); p->vDivs = Vec_PtrAlloc( 100 ); @@ -331,14 +335,16 @@ Gia_ResbMan_t * Gia_ResbAlloc( int nWords ) p->vSims = Vec_WrdAlloc( 100 ); return p; } -void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nChoice, int fUseXor, int fDebug, int fVerbose ) +void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int fVeryVerbose ) { assert( p->nWords == nWords ); - p->nLimit = nLimit; - p->nChoice = nChoice; - p->fUseXor = fUseXor; - p->fDebug = fDebug; - p->fVerbose = fVerbose; + p->nLimit = nLimit; + p->nDivsMax = nDivsMax; + p->iChoice = iChoice; + p->fUseXor = fUseXor; + p->fDebug = fDebug; + p->fVerbose = fVerbose; + p->fVeryVerbose = fVeryVerbose; Abc_TtCopy( p->pSets[0], (word *)Vec_PtrEntry(vDivs, 0), nWords, 0 ); Abc_TtCopy( p->pSets[1], (word *)Vec_PtrEntry(vDivs, 1), nWords, 0 ); Vec_PtrClear( p->vDivs ); @@ -372,6 +378,7 @@ void Gia_ResbFree( Gia_ResbMan_t * p ) Vec_IntFree( p->vGates ); Vec_WrdFree( p->vSims ); Vec_PtrFree( p->vDivs ); + Vec_WecFree( p->vSorter ); ABC_FREE( p->pSets[0] ); ABC_FREE( p->pSets[1] ); ABC_FREE( p->pDivA ); @@ -727,19 +734,19 @@ static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr *pStart2++ = *pBeg2++; Vec_IntShrink( vArr1, pStart1 - vArr1->pArray ); Vec_IntShrink( vArr2, pStart2 - vArr2->pArray ); - if ( fVerbose ) printf( "Removed %d duplicated entries. Array1 = %d. Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) ); + //if ( fVerbose ) printf( "Removed %d duplicated entries. Array1 = %d. Array2 = %d.\n", nRemoved, Vec_IntSize(vArr1), Vec_IntSize(vArr2) ); return -1; } -void Gia_ManFindOneUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vNotUnateVars ) +void Gia_ManFindOneUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vNotUnateVars ) { word * pDiv; int i; Vec_IntClear( vUnateLits ); Vec_IntClear( vNotUnateVars ); Vec_PtrForEachEntryStart( word *, vDivs, pDiv, i, 2 ) - if ( !Abc_TtIntersectOne( pOffSet, 0, pDiv, 0, nWords ) ) + if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 0, nWords ) ) Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 0) ); - else if ( !Abc_TtIntersectOne( pOffSet, 0, pDiv, 1, nWords ) ) + else if ( !Abc_TtIntersectOne( pOff, 0, pDiv, 1, nWords ) ) Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 1) ); else Vec_IntPush( vNotUnateVars, i ); @@ -747,86 +754,107 @@ void Gia_ManFindOneUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, i int Gia_ManFindOneUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2], int fVerbose ) { int n; + if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { Gia_ManFindOneUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vNotUnateVars[n] ); - if ( fVerbose ) printf( "Found %d %d-unate divs.\n", Vec_IntSize(vUnateLits[n]), n ); + if ( fVerbose ) printf( "U%d =%4d ", n, Vec_IntSize(vUnateLits[n]) ); } return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1], fVerbose ); } -static inline int Gia_ManDivCover( word * pOffSet, word * pOnSet, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords ) +static inline int Gia_ManDivCover( word * pOff, word * pOn, word * pDivA, int ComplA, word * pDivB, int ComplB, int nWords ) { - //assert( !Abc_TtIntersectOne(pOffSet, 0, pDivA, ComplA, nWords) ); - //assert( !Abc_TtIntersectOne(pOffSet, 0, pDivB, ComplB, nWords) ); - return !Abc_TtIntersectTwo( pOnSet, 0, pDivA, !ComplA, pDivB, !ComplB, nWords ); + //assert( !Abc_TtIntersectOne(pOff, 0, pDivA, ComplA, nWords) ); + //assert( !Abc_TtIntersectOne(pOff, 0, pDivB, ComplB, nWords) ); + return !Abc_TtIntersectTwo( pOn, 0, pDivA, !ComplA, pDivB, !ComplB, nWords ); } -int Gia_ManFindTwoUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits ) +int Gia_ManFindTwoUnateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, int * pnPairs ) { - int i, k, iDiv0, iDiv1; - Vec_IntForEachEntry( vUnateLits, iDiv1, i ) - Vec_IntForEachEntryStop( vUnateLits, iDiv0, k, i ) + int i, k, iDiv0_, iDiv1_, Cover0, Cover1; + int nTotal = Abc_TtCountOnesVec( pOn, nWords ); + (*pnPairs) = 0; + Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0_, Cover0, i ) { - word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); - word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); - if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv1, Abc_LitIsCompl(iDiv1), pDiv0, Abc_LitIsCompl(iDiv0), nWords) ) - return Abc_Var2Lit((Abc_LitNot(iDiv1) << 15) | Abc_LitNot(iDiv0), 1); + if ( 2*Cover0 < nTotal ) + break; + Vec_IntForEachEntryTwoStart( vUnateLits, vUnateLitsW, iDiv1_, Cover1, k, i+1 ) + { + int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); + int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); + word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); + word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); + if ( Cover0 + Cover1 < nTotal ) + break; + (*pnPairs)++; + if ( Gia_ManDivCover(pOff, pOn, pDiv1, Abc_LitIsCompl(iDiv1), pDiv0, Abc_LitIsCompl(iDiv0), nWords) ) + return Abc_Var2Lit((Abc_LitNot(iDiv1) << 15) | Abc_LitNot(iDiv0), 1); + } } return -1; } -int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], int fVerbose ) +int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], int fVerbose ) { - int n, iLit; + int n, iLit, nPairs; + if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { - int nPairs = Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2; - if ( fVerbose ) printf( "Trying %d pairs of %d-unate divs.\n", nPairs, n ); - iLit = Gia_ManFindTwoUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n] ); + //int nPairsAll = Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2; + iLit = Gia_ManFindTwoUnateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], &nPairs ); + if ( fVerbose ) printf( "UU%d =%5d ", n, nPairs ); if ( iLit >= 0 ) return Abc_LitNotCond(iLit, n); } return -1; } -void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) +void Gia_ManFindXorInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) { - int i, k, iDiv0, iDiv1; - Vec_IntForEachEntry( vBinate, iDiv1, i ) - Vec_IntForEachEntryStop( vBinate, iDiv0, k, i ) + int i, k, iDiv0_, iDiv1_; + int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); + Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) + Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) { + int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); + int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); - if ( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 0, nWords ) ) + if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 0, nWords ) ) Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 0) ); - else if ( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 1, nWords ) ) + else if ( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, 1, nWords ) ) Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 1) ); } } int Gia_ManFindXor( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) { int n; + if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { Vec_IntClear( vUnatePairs[n] ); Gia_ManFindXorInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); - if ( fVerbose ) printf( "Found %d %d-unate XOR divs.\n", Vec_IntSize(vUnatePairs[n]), n ); + if ( fVerbose ) printf( "UX%d =%5d ", n, Vec_IntSize(vUnatePairs[n]) ); } return Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); } -void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) +void Gia_ManFindUnatePairsInt( word * pOff, word * pOn, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) { - int n, i, k, iDiv0, iDiv1; - Vec_IntForEachEntry( vBinate, iDiv1, i ) - Vec_IntForEachEntryStop( vBinate, iDiv0, k, i ) + int n, i, k, iDiv0_, iDiv1_; + int Limit2 = Vec_IntSize(vBinate);//Abc_MinInt( Vec_IntSize(vBinate), 100 ); + Vec_IntForEachEntryStop( vBinate, iDiv1_, i, Limit2 ) + Vec_IntForEachEntryStop( vBinate, iDiv0_, k, i ) { + int iDiv0 = Abc_MinInt( iDiv0_, iDiv1_ ); + int iDiv1 = Abc_MaxInt( iDiv0_, iDiv1_ ); word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); for ( n = 0; n < 4; n++ ) { int iLit0 = Abc_Var2Lit( iDiv0, n&1 ); int iLit1 = Abc_Var2Lit( iDiv1, n>>1 ); - if ( !Abc_TtIntersectTwo( pOffSet, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) + //if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) + if ( !Abc_TtIntersectTwo( pOff, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) && Abc_TtIntersectTwo( pOn, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) Vec_IntPush( vUnatePairs, Abc_Var2Lit((iLit1 << 15) | iLit0, 0) ); } } @@ -834,11 +862,12 @@ void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinat void Gia_ManFindUnatePairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) { int n, RetValue; + if ( fVerbose ) printf( " " ); for ( n = 0; n < 2; n++ ) { int nBefore = Vec_IntSize(vUnatePairs[n]); Gia_ManFindUnatePairsInt( pSets[n], pSets[!n], vBinateVars, vDivs, nWords, vUnatePairs[n] ); - if ( fVerbose ) printf( "Found %d %d-unate pair divs.\n", Vec_IntSize(vUnatePairs[n])-nBefore, n ); + if ( fVerbose ) printf( "UP%d =%5d ", n, Vec_IntSize(vUnatePairs[n])-nBefore ); } RetValue = Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); assert( RetValue == -1 ); @@ -863,108 +892,107 @@ void Gia_ManDeriveDivPair( int iDiv, Vec_Ptr_t * vDivs, int nWords, word * pRes Abc_TtXor( pRes, pDiv0, pDiv1, nWords, 0 ); } } -int Gia_ManFindDivGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, word * pDivTemp ) +int Gia_ManFindDivGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnateLitsW, Vec_Int_t * vUnatePairsW, word * pDivTemp ) { - int i, k, iDiv0, iDiv1; - int Limit1 = Abc_MinInt( Vec_IntSize(vUnateLits), 1000 ); - int Limit2 = Abc_MinInt( Vec_IntSize(vUnatePairs), 1000 ); - Vec_IntForEachEntryStop( vUnateLits, iDiv0, i, Limit1 ) - Vec_IntForEachEntryStop( vUnatePairs, iDiv1, k, Limit2 ) + int i, k, iDiv0, iDiv1, Cover0, Cover1; + int nTotal = Abc_TtCountOnesVec( pOn, nWords ); + Vec_IntForEachEntryTwo( vUnateLits, vUnateLitsW, iDiv0, Cover0, i ) { word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); - int fComp1 = Abc_LitIsCompl(iDiv1); - Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTemp ); - if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fComp1, nWords) ) - return Abc_Var2Lit((Abc_Var2Lit(k, 1) << 15) | Abc_LitNot(iDiv0), 1); + if ( 2*Cover0 < nTotal ) + break; + Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv1, Cover1, k ) + { + int fComp1 = Abc_LitIsCompl(iDiv1); + if ( Cover0 + Cover1 < nTotal ) + break; + Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTemp ); + if ( Gia_ManDivCover(pOff, pOn, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fComp1, nWords) ) + return Abc_Var2Lit((Abc_Var2Lit(k, 1) << 15) | Abc_LitNot(iDiv0), 1); + } } return -1; } -int Gia_ManFindDivGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], word * pDivTemp ) +int Gia_ManFindDivGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnateLitsW[2], Vec_Int_t * vUnatePairsW[2], word * pDivTemp ) { int n, iLit; for ( n = 0; n < 2; n++ ) { - iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], pDivTemp ); + iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], vUnateLitsW[n], vUnatePairsW[n], pDivTemp ); if ( iLit >= 0 ) return Abc_LitNotCond( iLit, n ); } return -1; } -int Gia_ManFindGateGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, word * pDivTempA, word * pDivTempB ) +int Gia_ManFindGateGateInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, word * pDivTempA, word * pDivTempB ) { - int i, k, iDiv0, iDiv1; - int Limit2 = Abc_MinInt( Vec_IntSize(vUnatePairs), 1000 ); - Vec_IntForEachEntryStop( vUnatePairs, iDiv1, i, Limit2 ) + int i, k, iDiv0, iDiv1, Cover0, Cover1; + int nTotal = Abc_TtCountOnesVec( pOn, nWords ); + Vec_IntForEachEntryTwo( vUnatePairs, vUnatePairsW, iDiv0, Cover0, k ) { - int fCompB = Abc_LitIsCompl(iDiv1); - Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB ); - Vec_IntForEachEntryStop( vUnatePairs, iDiv0, k, i ) + int fCompA = Abc_LitIsCompl(iDiv0); + if ( 2*Cover0 < nTotal ) + break; + Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA ); + Vec_IntForEachEntryTwoStart( vUnatePairs, vUnatePairsW, iDiv1, Cover1, i, k+1 ) { - int fCompA = Abc_LitIsCompl(iDiv0); - Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA ); - if ( Gia_ManDivCover(pOffSet, pOnSet, pDivTempA, fCompA, pDivTempB, fCompB, nWords) ) + int fCompB = Abc_LitIsCompl(iDiv1); + if ( Cover0 + Cover1 < nTotal ) + break; + Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB ); + if ( Gia_ManDivCover(pOff, pOn, pDivTempA, fCompA, pDivTempB, fCompB, nWords) ) return Abc_Var2Lit((Abc_Var2Lit(i, 1) << 15) | Abc_Var2Lit(k, 1), 1); } } return -1; } -int Gia_ManFindGateGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], word * pDivTempA, word * pDivTempB ) +int Gia_ManFindGateGate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2], word * pDivTempA, word * pDivTempB ) { int n, iLit; for ( n = 0; n < 2; n++ ) { - iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], pDivTempA, pDivTempB ); + iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n], pDivTempA, pDivTempB ); if ( iLit >= 0 ) return Abc_LitNotCond( iLit, n ); } return -1; } -void Gia_ManComputeLitWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW ) +void Gia_ManSortUnatesInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW, Vec_Wec_t * vSorter ) { - int i, iLit; - Vec_IntClear( vUnateLitsW ); + int i, k, iLit; + Vec_Int_t * vLevel; + Vec_WecInit( vSorter, nWords*64 ); Vec_IntForEachEntry( vUnateLits, iLit, i ) { - word * pDiv = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit) ); - //assert( !Abc_TtIntersectOne( pOffSet, 0, pDiv, Abc_LitIsCompl(iLit), nWords ) ); - Vec_IntPush( vUnateLitsW, -Abc_TtCountOnesVecMask(pDiv, pOnSet, nWords, Abc_LitIsCompl(iLit)) ); + word * pDiv = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iLit)); + //assert( !Abc_TtIntersectOne( pOff, 0, pDiv, Abc_LitIsCompl(iLit), nWords ) ); + Vec_WecPush( vSorter, Abc_TtCountOnesVecMask(pDiv, pOn, nWords, Abc_LitIsCompl(iLit)), iLit ); } + Vec_IntClear( vUnateLits ); + Vec_IntClear( vUnateLitsW ); + Vec_WecForEachLevelReverse( vSorter, vLevel, k ) + Vec_IntForEachEntry( vLevel, iLit, i ) + { + Vec_IntPush( vUnateLits, iLit ); + Vec_IntPush( vUnateLitsW, k ); + } + //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); + Vec_WecClear( vSorter ); } -void Gia_ManComputeLitWeights( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], int TopW[2], int fVerbose ) +void Gia_ManSortUnates( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) { - int n, TopNum = 5; - TopW[0] = TopW[1] = 0; - for ( n = 0; n < 2; n++ ) - Gia_ManComputeLitWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n] ); + int n; for ( n = 0; n < 2; n++ ) - if ( Vec_IntSize(vUnateLitsW[n]) ) - { - int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnateLitsW[n]), Vec_IntSize(vUnateLitsW[n]) ); - TopW[n] = -Vec_IntEntry(vUnateLitsW[n], pPerm[0]); - if ( fVerbose ) - { - printf( "Top %d %d-unate divs:\n", TopNum, n ); - for ( i = 0; i < TopNum && i < Vec_IntSize(vUnateLits[n]); i++ ) - { - printf( "%5d : ", i ); - printf( "Lit = %5d ", Vec_IntEntry(vUnateLits[n], pPerm[i]) ); - printf( "Cost = %5d\n", -Vec_IntEntry(vUnateLitsW[n], pPerm[i]) ); - } - } - for ( i = 0; i < Vec_IntSize(vUnateLits[n]); i++ ) - pPerm[i] = Vec_IntEntry(vUnateLits[n], pPerm[i]); - for ( i = 0; i < Vec_IntSize(vUnateLits[n]); i++ ) - vUnateLits[n]->pArray[i] = pPerm[i]; - ABC_FREE( pPerm ); - } + Gia_ManSortUnatesInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); } -void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW ) +void Gia_ManSortPairsInt( word * pOff, word * pOn, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW, Vec_Wec_t * vSorter ) { - int i, iPair; - Vec_IntClear( vUnatePairsW ); + int i, k, iPair; + Vec_Int_t * vLevel; + Vec_WecInit( vSorter, nWords*64 ); Vec_IntForEachEntry( vUnatePairs, iPair, i ) { int fComp = Abc_LitIsCompl(iPair); @@ -975,53 +1003,70 @@ void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vD if ( iLit0 < iLit1 ) { assert( !fComp ); - //assert( !Abc_TtIntersectTwo( pOffSet, 0, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ) ); - Vec_IntPush( vUnatePairsW, -Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOnSet, nWords) ); + //assert( !Abc_TtIntersectTwo( pOff, 0, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ) ); + Vec_WecPush( vSorter, Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOn, nWords), iPair ); } else { assert( !Abc_LitIsCompl(iLit0) ); assert( !Abc_LitIsCompl(iLit1) ); - //assert( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, fComp, nWords ) ); - Vec_IntPush( vUnatePairsW, -Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOnSet, nWords) ); + //assert( !Abc_TtIntersectXor( pOff, 0, pDiv0, pDiv1, fComp, nWords ) ); + Vec_WecPush( vSorter, Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOn, nWords), iPair ); } } + Vec_IntClear( vUnatePairs ); + Vec_IntClear( vUnatePairsW ); + Vec_WecForEachLevelReverse( vSorter, vLevel, k ) + Vec_IntForEachEntry( vLevel, iPair, i ) + { + Vec_IntPush( vUnatePairs, iPair ); + Vec_IntPush( vUnatePairsW, k ); + } + //Vec_IntPrint( Vec_WecEntry(vSorter, 0) ); + Vec_WecClear( vSorter ); + } -void Gia_ManComputePairWeights( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2], int TopW[2], int fVerbose ) +void Gia_ManSortPairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2], Vec_Wec_t * vSorter ) { - int n, TopNum = 5; - TopW[0] = TopW[1] = 0; - for ( n = 0; n < 2; n++ ) - Gia_ManComputePairWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] ); + int n; for ( n = 0; n < 2; n++ ) - if ( Vec_IntSize(vUnatePairsW[n]) ) + Gia_ManSortPairsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n], vSorter ); +} + +void Gia_ManSortBinate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Wec_t * vSorter ) +{ + Vec_Int_t * vLevel; + int nMints[2] = { Abc_TtCountOnesVec(pSets[0], nWords), Abc_TtCountOnesVec(pSets[1], nWords) }; + word * pBig = nMints[0] > nMints[1] ? pSets[0] : pSets[1]; + word * pSmo = nMints[0] > nMints[1] ? pSets[1] : pSets[0]; + int Big = Abc_MaxInt( nMints[0], nMints[1] ); + int Smo = Abc_MinInt( nMints[0], nMints[1] ); + int i, k, iDiv, Gain; + + Vec_WecInit( vSorter, nWords*64 ); + Vec_IntForEachEntry( vBinateVars, iDiv, i ) + { + word * pDiv = (word *)Vec_PtrEntry( vDivs, iDiv ); + int nInter[2] = { Abc_TtCountOnesVecMask(pBig, pDiv, nWords, 0), Abc_TtCountOnesVecMask(pSmo, pDiv, nWords, 0) }; + if ( nInter[0] < Big/2 ) // complement the divisor { - int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnatePairsW[n]), Vec_IntSize(vUnatePairsW[n]) ); - TopW[n] = -Vec_IntEntry(vUnatePairsW[n], pPerm[0]); - if ( fVerbose ) - { - printf( "Top %d %d-unate pairs:\n", TopNum, n ); - for ( i = 0; i < TopNum && i < Vec_IntSize(vUnatePairs[n]); i++ ) - { - int Pair = Vec_IntEntry(vUnatePairs[n], pPerm[i]); - int Div0 = Abc_Lit2Var(Pair) & 0x7FFF; - int Div1 = Abc_Lit2Var(Pair) >> 15; - printf( "%5d : ", i ); - printf( "Compl = %5d ", Abc_LitIsCompl(Pair) ); - printf( "Type = %s ", Div0 < Div1 ? "and" : "xor" ); - printf( "Div0 = %5d ", Div0 ); - printf( "Div1 = %5d ", Div1 ); - printf( "Cost = %5d\n", -Vec_IntEntry(vUnatePairsW[n], pPerm[i]) ); - } - } - for ( i = 0; i < Vec_IntSize(vUnatePairs[n]); i++ ) - pPerm[i] = Vec_IntEntry(vUnatePairs[n], pPerm[i]); - for ( i = 0; i < Vec_IntSize(vUnatePairs[n]); i++ ) - vUnatePairs[n]->pArray[i] = pPerm[i]; - ABC_FREE( pPerm ); + nInter[0] = Big - nInter[0]; + nInter[1] = Smo - nInter[1]; } -} + assert( nInter[0] >= Big/2 ); + Gain = Abc_MaxInt( 0, nInter[0] - Big/2 + Smo/2 - nInter[1] ); + Vec_WecPush( vSorter, Gain, iDiv ); + } + Vec_IntClear( vBinateVars ); + Vec_WecForEachLevelReverse( vSorter, vLevel, k ) + Vec_IntForEachEntry( vLevel, iDiv, i ) + Vec_IntPush( vBinateVars, iDiv ); + Vec_WecClear( vSorter ); + + if ( Vec_IntSize(vBinateVars) > 2000 ) + Vec_IntShrink( vBinateVars, 2000 ); +} /**Function************************************************************* @@ -1039,9 +1084,11 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) int TopOneW[2] = {0}, TopTwoW[2] = {0}, Max1, Max2, iResLit, nVars = Vec_PtrSize(p->vDivs); if ( p->fVerbose ) { - printf( "\nCalling decomposition for ISF: " ); - printf( "OFF = %5d (%6.2f %%) ", Abc_TtCountOnesVec(p->pSets[0], p->nWords), 100.0*Abc_TtCountOnesVec(p->pSets[0], p->nWords)/(64*p->nWords) ); - printf( "ON = %5d (%6.2f %%)\n", Abc_TtCountOnesVec(p->pSets[1], p->nWords), 100.0*Abc_TtCountOnesVec(p->pSets[1], p->nWords)/(64*p->nWords) ); + int nMints[2] = { Abc_TtCountOnesVec(p->pSets[0], p->nWords), Abc_TtCountOnesVec(p->pSets[1], p->nWords) }; + printf( " " ); + printf( "ISF: " ); + printf( "0=%5d (%5.2f %%) ", nMints[0], 100.0*nMints[0]/(64*p->nWords) ); + printf( "1=%5d (%5.2f %%) ", nMints[1], 100.0*nMints[1]/(64*p->nWords) ); } if ( Abc_TtIsConst0( p->pSets[1], p->nWords ) ) return 0; @@ -1052,7 +1099,8 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) return iResLit; if ( nLimit == 0 ) return -1; - iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->fVerbose ); + Gia_ManSortUnates( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->vSorter ); + iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, p->fVerbose ); if ( iResLit >= 0 ) // and { int iNode = nVars + Vec_IntSize(p->vGates)/2; @@ -1064,11 +1112,10 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) return Abc_Var2Lit( iNode, fComp ); } Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars ); - if ( Vec_IntSize(p->vBinateVars) > 1000 ) - { - printf( "Reducing binate divs from %d to 1000.\n", Vec_IntSize(p->vBinateVars) ); - Vec_IntShrink( p->vBinateVars, 1000 ); - } + if ( Vec_IntSize(p->vBinateVars) > p->nDivsMax ) + Vec_IntShrink( p->vBinateVars, p->nDivsMax ); + if ( p->fVerbose ) printf( " B = %3d", Vec_IntSize(p->vBinateVars) ); + //Gia_ManSortBinate( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vSorter ); if ( p->fUseXor ) { iResLit = Gia_ManFindXor( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); @@ -1088,7 +1135,8 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) if ( nLimit == 1 ) return -1; Gia_ManFindUnatePairs( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); - iResLit = Gia_ManFindDivGate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->pDivA ); + Gia_ManSortPairs( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->vSorter ); + iResLit = Gia_ManFindDivGate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->vUnateLitsW, p->vUnatePairsW, p->pDivA ); if ( iResLit >= 0 ) // and(div,pair) { int iNode = nVars + Vec_IntSize(p->vGates)/2; @@ -1108,7 +1156,7 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) } if ( nLimit == 2 ) return -1; - iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->pDivA, p->pDivB ); + iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, p->pDivA, p->pDivB ); if ( iResLit >= 0 ) // and(pair,pair) { int iNode = nVars + Vec_IntSize(p->vGates)/2; @@ -1136,8 +1184,13 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) return -1; if ( Vec_IntSize(p->vUnateLits[0]) + Vec_IntSize(p->vUnateLits[1]) + Vec_IntSize(p->vUnatePairs[0]) + Vec_IntSize(p->vUnatePairs[1]) == 0 ) return -1; - Gia_ManComputeLitWeights( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW, TopOneW, p->fVerbose ); - Gia_ManComputePairWeights( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW, TopTwoW, p->fVerbose ); + + TopOneW[0] = Vec_IntSize(p->vUnateLitsW[0]) ? Vec_IntEntry(p->vUnateLitsW[0], 0) : 0; + TopOneW[1] = Vec_IntSize(p->vUnateLitsW[1]) ? Vec_IntEntry(p->vUnateLitsW[1], 0) : 0; + + TopTwoW[0] = Vec_IntSize(p->vUnatePairsW[0]) ? Vec_IntEntry(p->vUnatePairsW[0], 0) : 0; + TopTwoW[1] = Vec_IntSize(p->vUnatePairsW[1]) ? Vec_IntEntry(p->vUnatePairsW[1], 0) : 0; + Max1 = Abc_MaxInt(TopOneW[0], TopOneW[1]); Max2 = Abc_MaxInt(TopTwoW[0], TopTwoW[1]); if ( Abc_MaxInt(Max1, Max2) == 0 ) @@ -1151,6 +1204,8 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) int fComp = Abc_LitIsCompl(iDiv); word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n" ); iResLit = Gia_ManResubPerform_rec( p, nLimit-1 ); if ( iResLit >= 0 ) { @@ -1169,6 +1224,8 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) int fComp = Abc_LitIsCompl(iDiv); Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n " ); iResLit = Gia_ManResubPerform_rec( p, nLimit-2 ); if ( iResLit >= 0 ) { @@ -1191,6 +1248,8 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) int fComp = Abc_LitIsCompl(iDiv); Gia_ManDeriveDivPair( iDiv, p->vDivs, p->nWords, p->pDivA ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], p->pDivA, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n" ); iResLit = Gia_ManResubPerform_rec( p, nLimit-2 ); if ( iResLit >= 0 ) { @@ -1212,6 +1271,8 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) int fComp = Abc_LitIsCompl(iDiv); word * pDiv = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iDiv) ); Abc_TtAndSharp( p->pSets[fUseOr], p->pSets[fUseOr], pDiv, p->nWords, !fComp ); + if ( p->fVerbose ) + printf( "\n " ); iResLit = Gia_ManResubPerform_rec( p, nLimit-1 ); if ( iResLit >= 0 ) { @@ -1224,21 +1285,24 @@ int Gia_ManResubPerform_rec( Gia_ResbMan_t * p, int nLimit ) } return -1; } -void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nChoice, int fUseXor, int fDebug, int fVerbose ) +void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose ) { int Res; - Gia_ResbInit( p, vDivs, nWords, nLimit, nChoice, fUseXor, fDebug, fVerbose ); + Gia_ResbInit( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose, fVerbose ); Res = Gia_ManResubPerform_rec( p, nLimit ); - if ( Res >= 0 ) - Vec_IntPush( p->vGates, Res ); + if ( Res >= 0 ) Vec_IntPush( p->vGates, Res ); + if ( fVerbose ) + printf( "\n" ); } -Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc ) +Vec_Int_t * Gia_ManResubOne( Vec_Ptr_t * vDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, word * pFunc ) { Vec_Int_t * vRes; Gia_ResbMan_t * p = Gia_ResbAlloc( nWords ); - Gia_ManResubPerform( p, vDivs, nWords, nLimit, nChoice, fUseXor, fDebug, 0 ); + Gia_ManResubPerform( p, vDivs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose ); if ( fVerbose ) Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); + if ( fVerbose ) + printf( "\n" ); if ( !Gia_ManResubVerify(p, pFunc) ) { Gia_ManResubPrint( p->vGates, Vec_PtrSize(vDivs) ); @@ -1275,15 +1339,20 @@ void Abc_ResubPrepareManager( int nWords ) s_pResbMan = Gia_ResbAlloc( nWords ); } -int Abc_ResubComputeFunction( void ** ppDivs, int nDivs, int nWords, int nLimit, int nChoice, int fUseXor, int fDebug, int fVerbose, int ** ppArray ) +int Abc_ResubComputeFunction( void ** ppDivs, int nDivs, int nWords, int nLimit, int nDivsMax, int iChoice, int fUseXor, int fDebug, int fVerbose, int ** ppArray ) { Vec_Ptr_t Divs = { nDivs, nDivs, ppDivs }; assert( s_pResbMan != NULL ); // first call Abc_ResubPrepareManager() - Gia_ManResubPerform( s_pResbMan, &Divs, nWords, nLimit, nChoice, fUseXor, fDebug, 0 ); + Gia_ManResubPerform( s_pResbMan, &Divs, nWords, nLimit, nDivsMax, iChoice, fUseXor, fDebug, fVerbose==2 ); if ( fVerbose ) { - Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); - printf( "\n" ); + int nGates = Vec_IntSize(s_pResbMan->vGates)/2; + if ( nGates ) + { + printf( " Gain = %2d Gates = %2d __________ F = ", nLimit+1-nGates, nGates ); + Gia_ManResubPrint( s_pResbMan->vGates, nDivs ); + printf( "\n" ); + } } if ( fDebug ) { @@ -1308,7 +1377,7 @@ void Abc_ResubDumpProblem( char * pFileName, void ** ppDivs, int nDivs, int nWor for ( d = 0; d < nDivs; d++ ) for ( w = 0; w < nWords; w++ ) Vec_WrdPush( vSims, pDivs[d][w] ); - Gia_ManSimPatWrite( pFileName, vSims, nWords ); + Vec_WrdDumpHex( pFileName, vSims, nWords, 1 ); Vec_WrdFree( vSims ); } @@ -1355,7 +1424,7 @@ void Gia_ManResubTest3() printf( " " ); //Abc_ResubDumpProblem( "temp.resub", (void **)Vec_PtrArray(vDivs), Vec_PtrSize(vDivs), 1 ); - ArraySize = Abc_ResubComputeFunction( (void **)Vec_PtrArray(vDivs), Vec_PtrSize(vDivs), 1, 4, 0, 0, 1, fVerbose, &pArray ); + ArraySize = Abc_ResubComputeFunction( (void **)Vec_PtrArray(vDivs), Vec_PtrSize(vDivs), 1, 4, 50, 0, 0, 1, fVerbose, &pArray ); if ( !fVerbose ) printf( "\n" ); @@ -1394,7 +1463,7 @@ void Gia_ManResubTest3_() printf( " " ); Dau_DsdPrintFromTruth2( &Truth, 6 ); printf( " " ); - Gia_ManResubPerform( p, vDivs, 1, 100, 0, 1, 1, 0 ); + Gia_ManResubPerform( p, vDivs, 1, 100, 0, 50, 1, 1, 0 ); } Gia_ResbFree( p ); Vec_IntFree( vRes ); @@ -1416,14 +1485,14 @@ void Gia_ManCheckResub( Vec_Ptr_t * vDivs, int nWords ) { //int i, nVars = 6, pVarSet[10] = { 2, 189, 2127, 2125, 177, 178 }; int i, nVars = 3, pVarSet[10] = { 2, 3, 4 }; - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); + word * pOff = (word *)Vec_PtrEntry( vDivs, 0 ); + word * pOn = (word *)Vec_PtrEntry( vDivs, 1 ); Vec_Int_t * vValue = Vec_IntStartFull( 1 << 6 ); printf( "Verifying resub:\n" ); for ( i = 0; i < 64*nWords; i++ ) { - int v, Mint = 0, Value = Abc_TtGetBit(pOnSet, i); - if ( !Abc_TtGetBit(pOffSet, i) && !Value ) + int v, Mint = 0, Value = Abc_TtGetBit(pOn, i); + if ( !Abc_TtGetBit(pOff, i) && !Value ) continue; for ( v = 0; v < nVars; v++ ) if ( Abc_TtGetBit((word *)Vec_PtrEntry(vDivs, pVarSet[v]), i) ) @@ -1444,15 +1513,15 @@ Vec_Ptr_t * Gia_ManDeriveDivs( Vec_Wrd_t * vSims, int nWords ) Vec_PtrPush( vDivs, Vec_WrdEntryP(vSims, nWords*i) ); return vDivs; } -Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int nChoice, int fUseXor, int fVerbose, int fVeryVerbose ) +Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int iChoice, int fUseXor, int fVerbose, int fVeryVerbose ) { return NULL; } -Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int nChoice, int fUseXor, int fVerbose, int fVeryVerbose ) +Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int iChoice, int fUseXor, int fVerbose, int fVeryVerbose ) { int nWords = 0; Gia_Man_t * pMan = NULL; - Vec_Wrd_t * vSims = Gia_ManSimPatRead( pFileName, &nWords ); + Vec_Wrd_t * vSims = Vec_WrdReadHex( pFileName, &nWords, 1 ); Vec_Ptr_t * vDivs = vSims ? Gia_ManDeriveDivs( vSims, nWords ) : NULL; Gia_ResbMan_t * p = Gia_ResbAlloc( nWords ); //Gia_ManCheckResub( vDivs, nWords ); @@ -1462,7 +1531,7 @@ Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, i Vec_PtrShrink( vDivs, (1<<14)-1 ); } assert( Vec_PtrSize(vDivs) < (1<<14) ); - Gia_ManResubPerform( p, vDivs, nWords, 100, nChoice, fUseXor, 1, 1 ); + Gia_ManResubPerform( p, vDivs, nWords, 100, 50, iChoice, fUseXor, 1, 1 ); if ( Vec_IntSize(p->vGates) ) { Vec_Wec_t * vGates = Vec_WecStart(1); @@ -1478,6 +1547,135 @@ Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, i return pMan; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManUnivTfo_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes, Vec_Int_t * vPos ) +{ + int i, iFan, Count = 1; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + if ( vNodes && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) + Vec_IntPush( vNodes, iObj ); + if ( vPos && Gia_ObjIsCo(Gia_ManObj(p, iObj)) ) + Vec_IntPush( vPos, iObj ); + Gia_ObjForEachFanoutStaticId( p, iObj, iFan, i ) + Count += Gia_ManUnivTfo_rec( p, iFan, vNodes, vPos ); + return Count; +} +int Gia_ManUnivTfo( Gia_Man_t * p, int * pObjs, int nObjs, Vec_Int_t ** pvNodes, Vec_Int_t ** pvPos ) +{ + int i, Count = 0; + if ( pvNodes ) + { + if ( *pvNodes ) + Vec_IntClear( *pvNodes ); + else + *pvNodes = Vec_IntAlloc( 100 ); + } + if ( pvPos ) + { + if ( *pvPos ) + Vec_IntClear( *pvPos ); + else + *pvPos = Vec_IntAlloc( 100 ); + } + Gia_ManIncrementTravId( p ); + for ( i = 0; i < nObjs; i++ ) + Count += Gia_ManUnivTfo_rec( p, pObjs[i], pvNodes ? *pvNodes : NULL, pvPos ? *pvPos : NULL ); + if ( pvNodes ) + Vec_IntSort( *pvNodes, 0 ); + if ( pvPos ) + Vec_IntSort( *pvPos, 0 ); + return Count; +} + +/**Function************************************************************* + + Synopsis [Tuning resub.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManTryResub( Gia_Man_t * p ) +{ + int nLimit = 20; + int nDivsMax = 200; + int iChoice = 0; + int fUseXor = 1; + int fDebug = 1; + int fVerbose = 0; + abctime clk, clkResub = 0, clkStart = Abc_Clock(); + Vec_Ptr_t * vvSims = Vec_PtrAlloc( 100 ); + Vec_Wrd_t * vSims; + word * pSets[2], * pFunc; + Gia_Obj_t * pObj, * pObj2; + int i, i2, nWords, nNonDec = 0, nTotal = 0; + assert( Gia_ManCiNum(p) < 16 ); + Vec_WrdFreeP( &p->vSimsPi ); + p->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) ); + nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p); + //Vec_WrdPrintHex( p->vSimsPi, nWords ); + pSets[0] = ABC_CALLOC( word, nWords ); + pSets[1] = ABC_CALLOC( word, nWords ); + vSims = Gia_ManSimPatSim( p ); + Gia_ManLevelNum(p); + Gia_ManCreateRefs(p); + Abc_ResubPrepareManager( nWords ); + Gia_ManStaticFanoutStart( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + Vec_Int_t vGates; + int * pArray, nArray, nTfo, iObj = Gia_ObjId(p, pObj); + int Level = Gia_ObjLevel(p, pObj); + int nMffc = Gia_NodeMffcSizeMark(p, pObj); + pFunc = Vec_WrdEntryP( vSims, nWords*iObj ); + Abc_TtCopy( pSets[0], pFunc, nWords, 1 ); + Abc_TtCopy( pSets[1], pFunc, nWords, 0 ); + Vec_PtrClear( vvSims ); + Vec_PtrPushTwo( vvSims, pSets[0], pSets[1] ); + nTfo = Gia_ManUnivTfo( p, &iObj, 1, NULL, NULL ); + Gia_ManForEachCi( p, pObj2, i2 ) + Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); + Gia_ManForEachAnd( p, pObj2, i2 ) + if ( !Gia_ObjIsTravIdCurrent(p, pObj2) && !Gia_ObjIsTravIdPrevious(p, pObj2) && Gia_ObjLevel(p, pObj2) <= Level ) + Vec_PtrPush( vvSims, Vec_WrdEntryP(vSims, nWords*Gia_ObjId(p, pObj2)) ); + if ( fVerbose ) + printf( "%3d : Lev = %2d Mffc = %2d Divs = %3d Tfo = %3d\n", iObj, Level, nMffc, Vec_PtrSize(vvSims)-2, nTfo ); + clk = Abc_Clock(); + nArray = Abc_ResubComputeFunction( (void **)Vec_PtrArray(vvSims), Vec_PtrSize(vvSims), nWords, Abc_MinInt(nMffc-1, nLimit), nDivsMax, iChoice, fUseXor, fDebug, fVerbose, &pArray ); + clkResub += Abc_Clock() - clk; + vGates.nSize = vGates.nCap = nArray; + vGates.pArray = pArray; + assert( nMffc > Vec_IntSize(&vGates)/2 ); + if ( Vec_IntSize(&vGates) > 0 ) + nTotal += nMffc - Vec_IntSize(&vGates)/2; + nNonDec += Vec_IntSize(&vGates) == 0; + } + printf( "Total nodes = %5d. Non-realizable = %5d. Gain = %6d. ", Gia_ManAndNum(p), nNonDec, nTotal ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); + Abc_PrintTime( 1, "Pure resub time", clkResub ); + Abc_ResubPrepareManager( 0 ); + Gia_ManStaticFanoutStop( p ); + Vec_PtrFree( vvSims ); + Vec_WrdFree( vSims ); + ABC_FREE( pSets[0] ); + ABC_FREE( pSets[1] ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index f9539faf..00581de8 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -306,89 +306,6 @@ Gia_Man_t * Gia_ManSimPatGenMiter( Gia_Man_t * p, Vec_Wrd_t * vSims ) } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManSimPatWriteOne( FILE * pFile, word * pSim, int nWords ) -{ - int k, Digit, nDigits = nWords*16; - for ( k = 0; k < nDigits; k++ ) - { - Digit = (int)((pSim[k/16] >> ((k%16) * 4)) & 15); - if ( Digit < 10 ) - fprintf( pFile, "%d", Digit ); - else - fprintf( pFile, "%c", 'A' + Digit-10 ); - } - fprintf( pFile, "\n" ); -} -void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) -{ - int i, nNodes = Vec_WrdSize(vSimsIn) / nWords; - FILE * pFile = fopen( pFileName, "wb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\" for writing.\n", pFileName ); - return; - } - assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); - for ( i = 0; i < nNodes; i++ ) - Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords ); - fclose( pFile ); - printf( "Written %d words of simulation data for %d objects into file \"%s\".\n", nWords, Vec_WrdSize(vSimsIn)/nWords, pFileName ); -} -int Gia_ManSimPatReadOne( char c ) -{ - int Digit = 0; - if ( c >= '0' && c <= '9' ) - Digit = c - '0'; - else if ( c >= 'A' && c <= 'F' ) - Digit = c - 'A' + 10; - else if ( c >= 'a' && c <= 'f' ) - Digit = c - 'a' + 10; - else assert( 0 ); - assert( Digit >= 0 && Digit < 16 ); - return Digit; -} -Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName, int * pnWords ) -{ - Vec_Wrd_t * vSimsIn = NULL; - int c, nWords = -1, nChars = 0; word Num = 0; - FILE * pFile = fopen( pFileName, "rb" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\" for reading.\n", pFileName ); - return NULL; - } - vSimsIn = Vec_WrdAlloc( 1000 ); - while ( (c = fgetc(pFile)) != EOF ) - { - if ( c == '\n' && nWords == -1 ) - nWords = Vec_WrdSize(vSimsIn); - if ( c == '\n' || c == '\r' || c == '\t' || c == ' ' ) - continue; - Num |= (word)Gia_ManSimPatReadOne((char)c) << (nChars * 4); - if ( ++nChars < 16 ) - continue; - Vec_WrdPush( vSimsIn, Num ); - nChars = 0; - Num = 0; - } - assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); - fclose( pFile ); - printf( "Read %d words of simulation data for %d objects.\n", nWords, Vec_WrdSize(vSimsIn)/nWords ); - if ( pnWords ) - *pnWords = nWords; - return vSimsIn; -} /**Function************************************************************* diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 5ee20e6a..007faeca 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -1101,19 +1101,20 @@ int Gia_NodeDeref_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode ) +int Gia_NodeRef_rec( Gia_Man_t * p, Gia_Obj_t * pNode, int fMark ) { Gia_Obj_t * pFanin; int Counter = 0; if ( Gia_ObjIsCi(pNode) ) return 0; assert( Gia_ObjIsAnd(pNode) ); + if ( fMark ) Gia_ObjSetTravIdCurrent(p, pNode); pFanin = Gia_ObjFanin0(pNode); if ( Gia_ObjRefInc(p, pFanin) == 0 ) - Counter += Gia_NodeRef_rec( p, pFanin ); + Counter += Gia_NodeRef_rec( p, pFanin, fMark ); pFanin = Gia_ObjFanin1(pNode); if ( Gia_ObjRefInc(p, pFanin) == 0 ) - Counter += Gia_NodeRef_rec( p, pFanin ); + Counter += Gia_NodeRef_rec( p, pFanin, fMark ); return Counter + 1; } @@ -1152,7 +1153,19 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ) assert( !Gia_IsComplement(pNode) ); assert( Gia_ObjIsCand(pNode) ); ConeSize1 = Gia_NodeDeref_rec( p, pNode ); - ConeSize2 = Gia_NodeRef_rec( p, pNode ); + ConeSize2 = Gia_NodeRef_rec( p, pNode, 0 ); + assert( ConeSize1 == ConeSize2 ); + assert( ConeSize1 >= 0 ); + return ConeSize1; +} +int Gia_NodeMffcSizeMark( Gia_Man_t * p, Gia_Obj_t * pNode ) +{ + int ConeSize1, ConeSize2; + assert( !Gia_IsComplement(pNode) ); + assert( Gia_ObjIsCand(pNode) ); + ConeSize1 = Gia_NodeDeref_rec( p, pNode ); + Gia_ManIncrementTravId( p ); + ConeSize2 = Gia_NodeRef_rec( p, pNode, 1 ); assert( ConeSize1 == ConeSize2 ); assert( ConeSize1 >= 0 ); return ConeSize1; @@ -1193,7 +1206,7 @@ int Gia_NodeMffcSizeSupp( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Int_t * vSupp ) ConeSize1 = Gia_NodeDeref_rec( p, pNode ); Gia_NodeCollect_rec( p, Gia_ObjFanin0(pNode), vSupp ); Gia_NodeCollect_rec( p, Gia_ObjFanin1(pNode), vSupp ); - ConeSize2 = Gia_NodeRef_rec( p, pNode ); + ConeSize2 = Gia_NodeRef_rec( p, pNode, 0 ); assert( ConeSize1 == ConeSize2 ); assert( ConeSize1 >= 0 ); return ConeSize1; -- cgit v1.2.3