From 372eb7bdefbb3da989746ea1abbab6dc10a19dd8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 7 May 2020 20:06:39 -0700 Subject: Experimental resubstitution. --- src/aig/gia/giaResub.c | 675 ++++++++++++++++++++++++++++++++----------------- 1 file changed, 442 insertions(+), 233 deletions(-) (limited to 'src/aig') diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c index 092603ed..7b57db15 100644 --- a/src/aig/gia/giaResub.c +++ b/src/aig/gia/giaResub.c @@ -26,7 +26,6 @@ ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -290,6 +289,7 @@ typedef struct Gia_ResbMan_t_ Gia_ResbMan_t; struct Gia_ResbMan_t_ { int nWords; + int fVerbose; Vec_Ptr_t * vDivs; Vec_Int_t * vGates; Vec_Int_t * vUnateLits[2]; @@ -298,15 +298,15 @@ struct Gia_ResbMan_t_ Vec_Int_t * vBinateVars; Vec_Int_t * vUnateLitsW[2]; Vec_Int_t * vUnatePairsW[2]; + word * pSets[2]; word * pDivA; word * pDivB; + Vec_Wrd_t * vSims; }; -Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates ) +Gia_ResbMan_t * Gia_ResbAlloc( int nWords ) { Gia_ResbMan_t * p = ABC_CALLOC( Gia_ResbMan_t, 1 ); p->nWords = nWords; - p->vDivs = vDivs; - p->vGates = vGates; p->vUnateLits[0] = Vec_IntAlloc( 100 ); p->vUnateLits[1] = Vec_IntAlloc( 100 ); p->vNotUnateVars[0] = Vec_IntAlloc( 100 ); @@ -318,12 +318,22 @@ Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates p->vUnatePairsW[0] = Vec_IntAlloc( 100 ); p->vUnatePairsW[1] = Vec_IntAlloc( 100 ); p->vBinateVars = Vec_IntAlloc( 100 ); + p->pSets[0] = ABC_CALLOC( word, nWords ); + p->pSets[1] = ABC_CALLOC( word, nWords ); p->pDivA = ABC_CALLOC( word, nWords ); p->pDivB = ABC_CALLOC( word, nWords ); + p->vSims = Vec_WrdAlloc( 100 ); return p; } -void Gia_ResbReset( Gia_ResbMan_t * p ) +void Gia_ResbInit( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int fVerbose ) { + assert( p->nWords == nWords ); + p->fVerbose = fVerbose; + Abc_TtCopy( p->pSets[0], (word *)Vec_PtrEntry(vDivs, 0), nWords, 0 ); + Abc_TtCopy( p->pSets[1], (word *)Vec_PtrEntry(vDivs, 1), nWords, 0 ); + p->vDivs = vDivs; + p->vGates = vGates; + Vec_IntClear( p->vGates ); Vec_IntClear( p->vUnateLits[0] ); Vec_IntClear( p->vUnateLits[1] ); Vec_IntClear( p->vNotUnateVars[0] ); @@ -349,11 +359,69 @@ void Gia_ResbFree( Gia_ResbMan_t * p ) Vec_IntFree( p->vUnatePairsW[0] ); Vec_IntFree( p->vUnatePairsW[1] ); Vec_IntFree( p->vBinateVars ); + Vec_WrdFree( p->vSims ); + ABC_FREE( p->pSets[0] ); + ABC_FREE( p->pSets[1] ); ABC_FREE( p->pDivA ); ABC_FREE( p->pDivB ); ABC_FREE( p ); } +/**Function************************************************************* + + Synopsis [Print resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManResubPrintNode( Vec_Int_t * vRes, int nVars, int Node, int fCompl ) +{ + extern void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ); + int iLit0 = Vec_IntEntry( vRes, 2*Node + 0 ); + int iLit1 = Vec_IntEntry( vRes, 2*Node + 1 ); + assert( iLit0 != iLit1 ); + if ( iLit0 > iLit1 && Abc_LitIsCompl(fCompl) ) // xor + { + printf( "~" ); + fCompl = 0; + } + printf( "(" ); + Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit0, fCompl) ); + printf( " %c ", iLit0 > iLit1 ? '^' : (fCompl ? '|' : '&') ); + Gia_ManResubPrintLit( vRes, nVars, Abc_LitNotCond(iLit1, fCompl) ); + printf( ")" ); +} +void Gia_ManResubPrintLit( Vec_Int_t * vRes, int nVars, int iLit ) +{ + if ( Abc_Lit2Var(iLit) < nVars ) + { + if ( nVars < 26 ) + printf( "%s%c", Abc_LitIsCompl(iLit) ? "~":"", 'a' + Abc_Lit2Var(iLit)-2 ); + else + printf( "%si%d", Abc_LitIsCompl(iLit) ? "~":"", Abc_Lit2Var(iLit)-2 ); + } + else + Gia_ManResubPrintNode( vRes, nVars, Abc_Lit2Var(iLit) - nVars, Abc_LitIsCompl(iLit) ); +} +int Gia_ManResubPrint( Vec_Int_t * vRes, int nVars ) +{ + int iTopLit; + if ( Vec_IntSize(vRes) == 0 ) + return printf( "none" ); + assert( Vec_IntSize(vRes) % 2 == 1 ); + iTopLit = Vec_IntEntryLast(vRes); + if ( iTopLit == 0 ) + return printf( "const0" ); + if ( iTopLit == 1 ) + return printf( "const1" ); + Gia_ManResubPrintLit( vRes, nVars, iTopLit ); + return 0; +} + /**Function************************************************************* Synopsis [Verify resubstitution.] @@ -365,54 +433,54 @@ void Gia_ResbFree( Gia_ResbMan_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_ManResubVerify( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int iTopLit ) +int Gia_ManResubVerify( Gia_ResbMan_t * p ) { - int i, iLit0, iLit1, RetValue, nDivs = Vec_PtrSize(vDivs); - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); + int nVars = Vec_PtrSize(p->vDivs); + int iTopLit, RetValue; word * pDivRes; - Vec_Wrd_t * vSims = NULL; - if ( iTopLit <= -1 ) + if ( Vec_IntSize(p->vGates) == 0 ) return -1; + iTopLit = Vec_IntEntryLast(p->vGates); + assert( iTopLit >= 0 ); if ( iTopLit == 0 ) - return Abc_TtIsConst0( pOnSet, nWords ); + return Abc_TtIsConst0( p->pSets[1], p->nWords ); if ( iTopLit == 1 ) - return Abc_TtIsConst0( pOffSet, nWords ); - if ( Abc_Lit2Var(iTopLit) < nDivs ) + return Abc_TtIsConst0( p->pSets[0], p->nWords ); + if ( Abc_Lit2Var(iTopLit) < nVars ) { - assert( Vec_IntSize(vGates) == 0 ); - pDivRes = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iTopLit) ); + assert( Vec_IntSize(p->vGates) == 1 ); + pDivRes = (word *)Vec_PtrEntry( p->vDivs, Abc_Lit2Var(iTopLit) ); } else { - assert( Vec_IntSize(vGates) > 0 ); - assert( Vec_IntSize(vGates) % 2 == 0 ); - assert( Abc_Lit2Var(iTopLit)-nDivs == Vec_IntSize(vGates)/2-1 ); - vSims = Vec_WrdStart( nWords * Vec_IntSize(vGates)/2 ); - Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i ) + int i, iLit0, iLit1; + assert( Vec_IntSize(p->vGates) > 1 ); + assert( Vec_IntSize(p->vGates) % 2 == 1 ); + assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(p->vGates)/2-1 ); + Vec_WrdFill( p->vSims, p->nWords * Vec_IntSize(p->vGates)/2, 0 ); + Vec_IntForEachEntryDouble( p->vGates, iLit0, iLit1, i ) { int iVar0 = Abc_Lit2Var(iLit0); int iVar1 = Abc_Lit2Var(iLit1); - word * pDiv0 = iVar0 < nDivs ? (word *)Vec_PtrEntry(vDivs, iVar0) : Vec_WrdEntryP(vSims, nWords*(nDivs - iVar0)); - word * pDiv1 = iVar1 < nDivs ? (word *)Vec_PtrEntry(vDivs, iVar1) : Vec_WrdEntryP(vSims, nWords*(nDivs - iVar1)); - word * pDiv = Vec_WrdEntryP(vSims, nWords*i/2); + word * pDiv0 = iVar0 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar0) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar0 - nVars)); + word * pDiv1 = iVar1 < nVars ? (word *)Vec_PtrEntry(p->vDivs, iVar1) : Vec_WrdEntryP(p->vSims, p->nWords*(iVar1 - nVars)); + word * pDiv = Vec_WrdEntryP(p->vSims, p->nWords*i/2); if ( iVar0 < iVar1 ) - Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ); + Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), p->nWords ); else if ( iVar0 > iVar1 ) { assert( !Abc_LitIsCompl(iLit0) ); assert( !Abc_LitIsCompl(iLit1) ); - Abc_TtXor( pDiv, pDiv0, pDiv1, nWords, 0 ); + Abc_TtXor( pDiv, pDiv0, pDiv1, p->nWords, 0 ); } else assert( 0 ); } - pDivRes = Vec_WrdEntryP( vSims, nWords*(Vec_IntSize(vGates)/2-1) ); + pDivRes = Vec_WrdEntryP( p->vSims, p->nWords*(Vec_IntSize(p->vGates)/2-1) ); } if ( Abc_LitIsCompl(iTopLit) ) - RetValue = !Abc_TtIntersectOne(pOnSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 1, nWords); + RetValue = !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 1, p->nWords); else - RetValue = !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOnSet, 0, pDivRes, 1, nWords); - Vec_WrdFreeP( &vSims ); + RetValue = !Abc_TtIntersectOne(p->pSets[0], 0, pDivRes, 0, p->nWords) && !Abc_TtIntersectOne(p->pSets[1], 0, pDivRes, 1, p->nWords); return RetValue; } @@ -433,32 +501,36 @@ int Gia_ManGetVar( Gia_Man_t * pNew, Vec_Int_t * vUsed, int iVar ) Vec_IntWriteEntry( vUsed, iVar, Gia_ManAppendCi(pNew) ); return Vec_IntEntry(vUsed, iVar); } -Gia_Man_t * Gia_ManConstructFromGates( int nVars, Vec_Int_t * vGates, int iTopLit ) +Gia_Man_t * Gia_ManConstructFromGates( Vec_Int_t * vGates, int nVars ) { - int i, iLit0, iLit1, iLitRes; - Gia_Man_t * pNew = Gia_ManStart( 100 ); + int i, iLit0, iLit1, iTopLit, iLitRes; + Gia_Man_t * pNew; + if ( Vec_IntSize(vGates) == 0 ) + return NULL; + assert( Vec_IntSize(vGates) % 2 == 1 ); + pNew = Gia_ManStart( 100 ); pNew->pName = Abc_UtilStrsav( "resub" ); - assert( iTopLit >= 0 ); + iTopLit = Vec_IntEntryLast( vGates ); if ( iTopLit == 0 || iTopLit == 1 ) iLitRes = 0; else if ( Abc_Lit2Var(iTopLit) < nVars ) { - assert( Vec_IntSize(vGates) == 0 ); + assert( Vec_IntSize(vGates) == 1 ); iLitRes = Gia_ManAppendCi(pNew); } else { Vec_Int_t * vUsed = Vec_IntStartFull( nVars ); Vec_Int_t * vCopy = Vec_IntAlloc( Vec_IntSize(vGates)/2 ); - assert( Vec_IntSize(vGates) > 0 ); - assert( Vec_IntSize(vGates) % 2 == 0 ); + assert( Vec_IntSize(vGates) > 1 ); + assert( Vec_IntSize(vGates) % 2 == 1 ); assert( Abc_Lit2Var(iTopLit)-nVars == Vec_IntSize(vGates)/2-1 ); Vec_IntForEachEntryDouble( vGates, iLit0, iLit1, i ) { int iVar0 = Abc_Lit2Var(iLit0); int iVar1 = Abc_Lit2Var(iLit1); - int iRes0 = iVar0 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar0) : Vec_IntEntry(vCopy, nVars - iVar0); - int iRes1 = iVar1 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar1) : Vec_IntEntry(vCopy, nVars - iVar1); + int iRes0 = iVar0 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar0) : Vec_IntEntry(vCopy, iVar0 - nVars); + int iRes1 = iVar1 < nVars ? Gia_ManGetVar(pNew, vUsed, iVar1) : Vec_IntEntry(vCopy, iVar1 - nVars); if ( iVar0 < iVar1 ) iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); else if ( iVar0 > iVar1 ) @@ -491,7 +563,7 @@ Gia_Man_t * Gia_ManConstructFromGates( int nVars, Vec_Int_t * vGates, int iTopLi SeeAlso [] ***********************************************************************/ -static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) +static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2, int fVerbose ) { int * pBeg1 = vArr1->pArray; int * pBeg2 = vArr2->pArray; @@ -521,7 +593,7 @@ 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 ); - 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; } @@ -538,20 +610,17 @@ void Gia_ManFindOneUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, i else Vec_IntPush( vNotUnateVars, i ); } -int Gia_ManFindOneUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2] ) +int Gia_ManFindOneUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2], int fVerbose ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); int n; for ( n = 0; n < 2; n++ ) { Vec_IntClear( vUnateLits[n] ); Vec_IntClear( vNotUnateVars[n] ); - Gia_ManFindOneUnateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vNotUnateVars[n] ); - ABC_SWAP( word *, pOffSet, pOnSet ); - printf( "Found %d %d-unate divs.\n", Vec_IntSize(vUnateLits[n]), 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 ); } - return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] ); + 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 ) @@ -568,61 +637,54 @@ int Gia_ManFindTwoUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, in { word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); - if ( Gia_ManDivCover(pOffSet, pOnSet, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords) ) - return Abc_Var2Lit((Abc_LitNot(iDiv0) << 16) | Abc_LitNot(iDiv1), 0); + 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); } return -1; } -int Gia_ManFindTwoUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2] ) +int Gia_ManFindTwoUnate( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], int fVerbose ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); int n, iLit; for ( n = 0; n < 2; n++ ) { - printf( "Trying %d pairs of %d-unate divs.\n", Vec_IntSize(vUnateLits[n])*(Vec_IntSize(vUnateLits[n])-1)/2, n ); - iLit = Gia_ManFindTwoUnateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[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] ); if ( iLit >= 0 ) - return Abc_LitNotCond(iLit, !n); - ABC_SWAP( word *, pOffSet, pOnSet ); + 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 * vUnateLits ) +void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) { int i, k, iDiv0, iDiv1; - Vec_IntClear( vUnateLits ); Vec_IntForEachEntry( vBinate, iDiv1, i ) Vec_IntForEachEntryStop( vBinate, iDiv0, k, i ) { word * pDiv0 = (word *)Vec_PtrEntry(vDivs, iDiv0); word * pDiv1 = (word *)Vec_PtrEntry(vDivs, iDiv1); if ( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 0, nWords ) ) - Vec_IntPush( vUnateLits, Abc_Var2Lit((Abc_Var2Lit(iDiv1, 0) << 16) | Abc_Var2Lit(iDiv0, 0), 0) ); + 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 ) ) - Vec_IntPush( vUnateLits, Abc_Var2Lit((Abc_Var2Lit(iDiv1, 0) << 16) | Abc_Var2Lit(iDiv0, 0), 1) ); + Vec_IntPush( vUnatePairs, Abc_Var2Lit((Abc_Var2Lit(iDiv0, 0) << 15) | Abc_Var2Lit(iDiv1, 0), 1) ); } } -int Gia_ManFindXor( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] ) +int Gia_ManFindXor( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); int n; for ( n = 0; n < 2; n++ ) { - Vec_IntClear( vUnateLits[n] ); - Gia_ManFindXorInt( pOffSet, pOnSet, vBinateVars, vDivs, nWords, vUnateLits[n] ); - ABC_SWAP( word *, pOffSet, pOnSet ); - printf( "Found %d %d-unate XOR divs.\n", Vec_IntSize(vUnateLits[n]), 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 ); } - return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] ); + 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 * vUnateLits ) +void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs ) { int n, i, k, iDiv0, iDiv1; - Vec_IntClear( vUnateLits ); Vec_IntForEachEntry( vBinate, iDiv1, i ) Vec_IntForEachEntryStop( vBinate, iDiv0, k, i ) { @@ -632,56 +694,67 @@ void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinat { int iLit0 = Abc_Var2Lit( iDiv0, n&1 ); int iLit1 = Abc_Var2Lit( iDiv1, n>>1 ); - if ( !Abc_TtIntersectTwo( pOffSet, 0, pDiv0, n&1, pDiv1, n>>1, nWords ) ) - Vec_IntPush( vUnateLits, Abc_Var2Lit((iLit0 << 16) | iLit1, 0) ); + if ( !Abc_TtIntersectTwo( pOffSet, 0, pDiv1, n>>1, pDiv0, n&1, nWords ) ) + Vec_IntPush( vUnatePairs, Abc_Var2Lit((iLit1 << 15) | iLit0, 0) ); } } } -void Gia_ManFindUnatePairs( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] ) +void Gia_ManFindUnatePairs( word * pSets[2], Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnatePairs[2], int fVerbose ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); int n, RetValue; for ( n = 0; n < 2; n++ ) { - int nBefore = Vec_IntSize(vUnateLits[n]); - Gia_ManFindUnatePairsInt( pOffSet, pOnSet, vBinateVars, vDivs, nWords, vUnateLits[n] ); - ABC_SWAP( word *, pOffSet, pOnSet ); - printf( "Found %d %d-unate pair divs.\n", Vec_IntSize(vUnateLits[n])-nBefore, 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 ); } - RetValue = Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] ); + RetValue = Gia_ManFindFirstCommonLit( vUnatePairs[0], vUnatePairs[1], fVerbose ); assert( RetValue == -1 ); } -int Gia_ManFindAndGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnatePairs, word * pDivTemp ) +void Gia_ManDeriveDivPair( int iDiv, Vec_Ptr_t * vDivs, int nWords, word * pRes ) +{ + int fComp = Abc_LitIsCompl(iDiv); + int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iDiv) >> 15; + word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); + word * pDiv1 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv1)); + if ( iDiv0 < iDiv1 ) + { + assert( !fComp ); + Abc_TtAndCompl( pRes, pDiv0, Abc_LitIsCompl(iDiv0), pDiv1, Abc_LitIsCompl(iDiv1), nWords ); + } + else + { + assert( !Abc_LitIsCompl(iDiv0) ); + assert( !Abc_LitIsCompl(iDiv1) ); + 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 i, k, iDiv0, iDiv1; - Vec_IntForEachEntry( vUnateLits, iDiv0, i ) - Vec_IntForEachEntry( vUnatePairs, iDiv1, k ) - { - int fCompl = Abc_LitIsCompl(iDiv1); - int iDiv10 = Abc_Lit2Var(iDiv1) >> 16; - int iDiv11 = Abc_Lit2Var(iDiv1) & 0xFFF; - word * pDiv0 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv0)); - word * pDiv10 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv10)); - word * pDiv11 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv11)); - Abc_TtAndCompl( pDivTemp, pDiv10, Abc_LitIsCompl(iDiv10), pDiv11, Abc_LitIsCompl(iDiv11), nWords ); - if ( Gia_ManDivCover(pOnSet, pOffSet, pDiv0, Abc_LitIsCompl(iDiv0), pDivTemp, fCompl, nWords) ) - return Abc_Var2Lit((Abc_LitNot(iDiv0) << 16) | Abc_Var2Lit(k, 1), 0); + 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 ) + { + 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); } return -1; } -int Gia_ManFindAndGate( 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], word * pDivTemp ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); int n, iLit; for ( n = 0; n < 2; n++ ) { - iLit = Gia_ManFindAndGateInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vUnatePairs[n], pDivTemp ); - if ( iLit > 0 ) - return Abc_LitNotCond( iLit, !n ); - ABC_SWAP( word *, pOffSet, pOnSet ); + iLit = Gia_ManFindDivGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnatePairs[n], pDivTemp ); + if ( iLit >= 0 ) + return Abc_LitNotCond( iLit, n ); } return -1; } @@ -689,39 +762,29 @@ int Gia_ManFindAndGate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2] int Gia_ManFindGateGateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, word * pDivTempA, word * pDivTempB ) { int i, k, iDiv0, iDiv1; - Vec_IntForEachEntry( vUnatePairs, iDiv0, i ) - { - int fCompA = Abc_LitIsCompl(iDiv0); - int iDiv00 = Abc_Lit2Var(iDiv0 >> 16); - int iDiv01 = Abc_Lit2Var(iDiv0 & 0xFFF); - word * pDiv00 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv00)); - word * pDiv01 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv01)); - Abc_TtAndCompl( pDivTempA, pDiv00, Abc_LitIsCompl(iDiv00), pDiv01, Abc_LitIsCompl(iDiv01), nWords ); - Vec_IntForEachEntryStop( vUnatePairs, iDiv1, k, i ) + int Limit2 = Abc_MinInt( Vec_IntSize(vUnatePairs), 1000 ); + Vec_IntForEachEntryStop( vUnatePairs, iDiv1, i, Limit2 ) + { + int fCompB = Abc_LitIsCompl(iDiv1); + Gia_ManDeriveDivPair( iDiv1, vDivs, nWords, pDivTempB ); + Vec_IntForEachEntryStop( vUnatePairs, iDiv0, k, i ) { - int fCompB = Abc_LitIsCompl(iDiv1); - int iDiv10 = Abc_Lit2Var(iDiv1 >> 16); - int iDiv11 = Abc_Lit2Var(iDiv1 & 0xFFF); - word * pDiv10 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv10)); - word * pDiv11 = (word *)Vec_PtrEntry(vDivs, Abc_Lit2Var(iDiv11)); - Abc_TtAndCompl( pDivTempB, pDiv10, Abc_LitIsCompl(iDiv10), pDiv11, Abc_LitIsCompl(iDiv11), nWords ); - if ( Gia_ManDivCover(pOnSet, pOffSet, pDivTempA, fCompA, pDivTempB, fCompB, nWords) ) - return Abc_Var2Lit((iDiv1 << 16) | iDiv0, 0); + int fCompA = Abc_LitIsCompl(iDiv0); + Gia_ManDeriveDivPair( iDiv0, vDivs, nWords, pDivTempA ); + if ( Gia_ManDivCover(pOffSet, pOnSet, pDivTempA, fCompA, pDivTempB, fCompB, nWords) ) + return Abc_Var2Lit((Abc_Var2Lit(i, 1) << 15) | Abc_Var2Lit(k, 1), 1); } } return -1; } -int Gia_ManFindGateGate( 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], word * pDivTempA, word * pDivTempB ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); int n, iLit; for ( n = 0; n < 2; n++ ) { - iLit = Gia_ManFindGateGateInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], pDivTempA, pDivTempB ); - ABC_SWAP( word *, pOffSet, pOnSet ); - if ( iLit > 0 ) - return iLit; + iLit = Gia_ManFindGateGateInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], pDivTempA, pDivTempB ); + if ( iLit >= 0 ) + return Abc_LitNotCond( iLit, n ); } return -1; } @@ -734,33 +797,36 @@ void Gia_ManComputeLitWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDi { 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)) ); + Vec_IntPush( vUnateLitsW, -Abc_TtCountOnesVecMask(pDiv, pOnSet, nWords, Abc_LitIsCompl(iLit)) ); } } -void Gia_ManComputeLitWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2] ) +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 ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); - int n; + int n, TopNum = 5; + TopW[0] = TopW[1] = 0; for ( n = 0; n < 2; n++ ) - { - Vec_IntClear( vUnateLitsW[n] ); - Gia_ManComputeLitWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnateLits[n], vUnateLitsW[n] ); - ABC_SWAP( word *, pOffSet, pOnSet ); - } + Gia_ManComputeLitWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnateLits[n], vUnateLitsW[n] ); for ( n = 0; n < 2; n++ ) - { - int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnateLitsW[n]), Vec_IntSize(vUnateLitsW[n]) ); - Abc_ReverseOrder( pPerm, Vec_IntSize(vUnateLitsW[n]) ); - printf( "Top 10 %d-unate:\n", n ); - for ( i = 0; i < 10 && i < Vec_IntSize(vUnateLits[n]); i++ ) + if ( Vec_IntSize(vUnateLitsW[n]) ) { - printf( "%5d : ", i ); - printf( "Obj = %5d ", Vec_IntEntry(vUnateLits[n], pPerm[i]) ); - printf( "Cost = %5d\n", Vec_IntEntry(vUnateLitsW[n], pPerm[i]) ); + 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 ); } - ABC_FREE( pPerm ); - } } void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW ) @@ -769,50 +835,59 @@ void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vD Vec_IntClear( vUnatePairsW ); Vec_IntForEachEntry( vUnatePairs, iPair, i ) { - int fCompl = Abc_LitIsCompl(iPair); - int Pair = Abc_Lit2Var(iPair); - int iLit0 = Pair >> 16; - int iLit1 = Pair & 0xFFFF; + int fComp = Abc_LitIsCompl(iPair); + int iLit0 = Abc_Lit2Var(iPair) & 0x7FFF; + int iLit1 = Abc_Lit2Var(iPair) >> 15; word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) ); word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) ); if ( iLit0 < iLit1 ) { - assert( !fCompl ); + 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) ); + Vec_IntPush( vUnatePairsW, -Abc_TtCountOnesVecMask2(pDiv0, pDiv1, Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1), pOnSet, nWords) ); } else { assert( !Abc_LitIsCompl(iLit0) ); assert( !Abc_LitIsCompl(iLit1) ); - assert( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, 0, nWords ) ); - Vec_IntPush( vUnatePairsW, Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fCompl, pOnSet, nWords) ); + assert( !Abc_TtIntersectXor( pOffSet, 0, pDiv0, pDiv1, fComp, nWords ) ); + Vec_IntPush( vUnatePairsW, -Abc_TtCountOnesVecXorMask(pDiv0, pDiv1, fComp, pOnSet, nWords) ); } } } -void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2] ) +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 ) { - word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); - word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); - int n; + int n, TopNum = 5; + TopW[0] = TopW[1] = 0; for ( n = 0; n < 2; n++ ) - { - Gia_ManComputePairWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] ); - ABC_SWAP( word *, pOffSet, pOnSet ); - } + Gia_ManComputePairWeightsInt( pSets[n], pSets[!n], vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] ); for ( n = 0; n < 2; n++ ) - { - int i, * pPerm = Abc_MergeSortCost( Vec_IntArray(vUnatePairsW[n]), Vec_IntSize(vUnatePairsW[n]) ); - Abc_ReverseOrder( pPerm, Vec_IntSize(vUnatePairsW[n]) ); - printf( "Top 10 %d-unate:\n", n ); - for ( i = 0; i < 10 && i < Vec_IntSize(vUnatePairs[n]); i++ ) + if ( Vec_IntSize(vUnatePairsW[n]) ) { - printf( "%5d : ", i ); - printf( "Obj = %5d ", Vec_IntEntry(vUnatePairs[n], pPerm[i]) ); - printf( "Cost = %5d\n", Vec_IntEntry(vUnatePairsW[n], pPerm[i]) ); + 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 ); } - ABC_FREE( pPerm ); - } } @@ -827,28 +902,32 @@ void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnat SeeAlso [] ***********************************************************************/ -int Gia_ManResubInt2( Vec_Ptr_t * vDivs, int nWords, int NodeLimit, int ChoiceType, Vec_Int_t * vGates ) +int Gia_ManResubPerformInt( Gia_ResbMan_t * p ) { - return 0; -} -int Gia_ManResubInt( Gia_ResbMan_t * p ) -{ - int nDivs = Vec_PtrSize(p->vDivs); - int iResLit = Gia_ManFindOneUnate( p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars ); - if ( iResLit >= 0 ) // buffer + int TopOneW[2], TopTwoW[2], Max, iResLit, nVars = Vec_PtrSize(p->vDivs); + if ( p->fVerbose ) { - printf( "Creating %s (%d).\n", Abc_LitIsCompl(iResLit) ? "inverter" : "buffer", Abc_Lit2Var(iResLit) ); - return iResLit; + 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) ); } - iResLit = Gia_ManFindTwoUnate( p->vDivs, p->nWords, p->vUnateLits ); + if ( Abc_TtIsConst0( p->pSets[1], p->nWords ) ) + return 0; + if ( Abc_TtIsConst0( p->pSets[0], p->nWords ) ) + return 1; + iResLit = Gia_ManFindOneUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->vNotUnateVars, p->fVerbose ); + if ( iResLit >= 0 ) // buffer + return iResLit; + iResLit = Gia_ManFindTwoUnate( p->pSets, p->vDivs, p->nWords, p->vUnateLits, p->fVerbose ); if ( iResLit >= 0 ) // and { - int fCompl = Abc_LitIsCompl(iResLit); - int iDiv0 = Abc_Lit2Var(iResLit) >> 16; - int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF; + int iNode = nVars + Vec_IntSize(p->vGates)/2; + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; + assert( iDiv0 < iDiv1 ); Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); - printf( "Creating one AND-gate.\n" ); - return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl ); + return Abc_Var2Lit( iNode, fComp ); } Vec_IntTwoFindCommon( p->vNotUnateVars[0], p->vNotUnateVars[1], p->vBinateVars ); if ( Vec_IntSize(p->vBinateVars) > 1000 ) @@ -856,43 +935,181 @@ int Gia_ManResubInt( Gia_ResbMan_t * p ) printf( "Reducing binate divs from %d to 1000.\n", Vec_IntSize(p->vBinateVars) ); Vec_IntShrink( p->vBinateVars, 1000 ); } - iResLit = Gia_ManFindXor( p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs ); + iResLit = Gia_ManFindXor( p->pSets, p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs, p->fVerbose ); if ( iResLit >= 0 ) // xor { - int fCompl = Abc_LitIsCompl(iResLit); - int iDiv0 = Abc_Lit2Var(iResLit) >> 16; - int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF; + int iNode = nVars + Vec_IntSize(p->vGates)/2; + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; assert( !Abc_LitIsCompl(iDiv0) ); assert( !Abc_LitIsCompl(iDiv1) ); - Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); // xor - printf( "Creating one XOR-gate.\n" ); - return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl ); - } - Gia_ManFindUnatePairs( p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs ); -/* - iResLit = Gia_ManFindAndGate( p->vDivs, p->nWords, p->vUnateLits, p->vUnatePairs, p->pDivA ); - if ( iResLit >= 0 ) // and-gate - { - int New = nDivs + Vec_IntSize(p->vGates)/2; - int fCompl = Abc_LitIsCompl(iResLit); - int iDiv0 = Abc_Lit2Var(iResLit) >> 16; - int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF; - Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv1), Abc_LitNot(iDiv0) ); - Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv0), New ); - printf( "Creating one two gates.\n" ); - return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, 1 ); - } - iResLit = Gia_ManFindGateGate( p->vDivs, p->nWords, p->vUnatePairs, p->pDivA, p->pDivB ); - if ( iResLit >= 0 ) // and-(gate,gate) - { - printf( "Creating one three gates.\n" ); + assert( iDiv0 > iDiv1 ); + Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); + return Abc_Var2Lit( iNode, fComp ); + } + 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 ); + if ( iResLit >= 0 ) // and(div,pair) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // div + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair + + int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); + int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); + int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; + int iDiv11 = Abc_Lit2Var(Div1) >> 15; + + Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); + Vec_IntPushTwo( p->vGates, iDiv0, Abc_Var2Lit(iNode, fComp1) ); + return Abc_Var2Lit( iNode+1, fComp ); + } + iResLit = Gia_ManFindGateGate( p->pSets, p->vDivs, p->nWords, p->vUnatePairs, p->pDivA, p->pDivB ); + if ( iResLit >= 0 ) // and(pair,pair) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + + int fComp = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) & 0x7FFF; // pair + int iDiv1 = Abc_Lit2Var(iResLit) >> 15; // pair + + int Div0 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv0) ); + int fComp0 = Abc_LitIsCompl(Div0) ^ Abc_LitIsCompl(iDiv0); + int iDiv00 = Abc_Lit2Var(Div0) & 0x7FFF; + int iDiv01 = Abc_Lit2Var(Div0) >> 15; + + int Div1 = Vec_IntEntry( p->vUnatePairs[!fComp], Abc_Lit2Var(iDiv1) ); + int fComp1 = Abc_LitIsCompl(Div1) ^ Abc_LitIsCompl(iDiv1); + int iDiv10 = Abc_Lit2Var(Div1) & 0x7FFF; + int iDiv11 = Abc_Lit2Var(Div1) >> 15; + + Vec_IntPushTwo( p->vGates, iDiv00, iDiv01 ); + Vec_IntPushTwo( p->vGates, iDiv10, iDiv11 ); + Vec_IntPushTwo( p->vGates, Abc_Var2Lit(iNode, fComp0), Abc_Var2Lit(iNode+1, fComp1) ); + return Abc_Var2Lit( iNode+2, fComp ); + } + 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 ); + //Max = Abc_MaxInt( Abc_MaxInt(TopOneW[0], TopOneW[1]), Abc_MaxInt(TopTwoW[0], TopTwoW[1]) ); + Max = Abc_MaxInt(TopOneW[0], TopOneW[1]); + if ( Max == 0 ) + return -1; + if ( Max == TopOneW[0] || Max == TopOneW[1] ) + { + int fUseOr = Max == TopOneW[0]; + int iDiv = Vec_IntEntry( p->vUnateLits[!fUseOr], 0 ); + 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 ); + iResLit = Gia_ManResubPerformInt( p ); + if ( iResLit >= 0 ) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + Vec_IntPushTwo( p->vGates, Abc_LitNot(iDiv), Abc_LitNotCond(iResLit, fUseOr) ); + return Abc_Var2Lit( iNode, fUseOr ); + } + } + if ( Max == TopTwoW[0] || Max == TopTwoW[1] ) + { + int fUseOr = Max == TopTwoW[0]; + int iDiv = Vec_IntEntry( p->vUnatePairs[!fUseOr], 0 ); + 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 ); + iResLit = Gia_ManResubPerformInt( p ); + if ( iResLit >= 0 ) + { + int iNode = nVars + Vec_IntSize(p->vGates)/2; + int iDiv0 = Abc_Lit2Var(iDiv) & 0x7FFF; + int iDiv1 = Abc_Lit2Var(iDiv) >> 15; + Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); + Vec_IntPushTwo( p->vGates, Abc_LitNotCond(iResLit, fUseOr), Abc_Var2Lit(iNode, !fComp) ); + return Abc_Var2Lit( iNode+1, fUseOr ); + } } -*/ - Gia_ManComputeLitWeights( p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW ); - Gia_ManComputePairWeights( p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW ); return -1; } +void Gia_ManResubPerform( Gia_ResbMan_t * p, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vRes, int fVerbose ) +{ + int Res; + Vec_IntClear( vRes ); + Gia_ResbInit( p, vDivs, nWords, vRes, fVerbose ); + Res = Gia_ManResubPerformInt( p ); + if ( Res == -1 ) + { + printf( "\n" ); + return; + } + Vec_IntPush( vRes, Res ); + Gia_ManResubPrint( vRes, Vec_PtrSize(vDivs) ); + printf( " Verification %s.\n", Gia_ManResubVerify(p) ? "succeeded" : "FAILED *******************************" ); +} +void Gia_ManResubTest3() +{ + int nVars = 3; + Gia_ResbMan_t * p = Gia_ResbAlloc( 1 ); + word Divs[6] = { 0, 0, + ABC_CONST(0xAAAAAAAAAAAAAAAA), + ABC_CONST(0xCCCCCCCCCCCCCCCC), + ABC_CONST(0xF0F0F0F0F0F0F0F0), + ABC_CONST(0xFF00FF00FF00FF00) + }; + Vec_Ptr_t * vDivs = Vec_PtrAlloc( 6 ); + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + int i; + for ( i = 0; i < 6; i++ ) + Vec_PtrPush( vDivs, Divs+i ); + for ( i = 0; i < (1<<(1< 4000 ) - { - printf( "Reducing all divs from %d to 4000.\n", Vec_PtrSize(vDivs) ); - Vec_PtrShrink( vDivs, 4000 ); - } - Gia_ResbReset( p ); + Gia_ResbMan_t * p = Gia_ResbAlloc( nWords ); // Gia_ManCheckResub( vDivs, nWords ); - iTopLit = Gia_ManResubInt( p ); - if ( iTopLit >= 0 ) + if ( Vec_PtrSize(vDivs) >= (1<<14) ) { - printf( "Verification %s.\n", Gia_ManResubVerify( vDivs, nWords, vGates, iTopLit ) ? "succeeded" : "FAILED" ); - pMan = Gia_ManConstructFromGates( Vec_PtrSize(vDivs), vGates, iTopLit ); + printf( "Reducing all divs from %d to %d.\n", Vec_PtrSize(vDivs), (1<<14)-1 ); + Vec_PtrShrink( vDivs, (1<<14)-1 ); } + assert( Vec_PtrSize(vDivs) < (1<<14) ); + Gia_ManResubPerform( p, vDivs, nWords, vGates, 1 ); + if ( Vec_IntSize(vGates) ) + pMan = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) ); else printf( "Decomposition did not succeed.\n" ); Gia_ResbFree( p ); -- cgit v1.2.3