From d51f798956a9f9fbdd1fc4eeecc483e511b1c3d3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 3 May 2020 10:32:30 -0700 Subject: Experimental resubstitution. --- src/aig/gia/gia.h | 1 + src/aig/gia/giaResub.c | 695 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaSimBase.c | 8 +- src/aig/gia/giaUtil.c | 88 ++++++ src/base/abci/abc.c | 100 +++++++ src/base/acb/acbFunc.c | 4 +- src/base/acb/acbUtil.c | 4 + src/misc/util/utilTruth.h | 146 ++++++++++ src/misc/vec/vecInt.h | 8 + 9 files changed, 1049 insertions(+), 5 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index ae9835ee..45291702 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1704,6 +1704,7 @@ extern int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, i extern int Gia_ManCountPisWithFanout( Gia_Man_t * p ); extern int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p ); extern void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p ); +extern Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c index b8c0e294..4dd8951f 100644 --- a/src/aig/gia/giaResub.c +++ b/src/aig/gia/giaResub.c @@ -22,6 +22,7 @@ #include "misc/vec/vecWec.h" #include "misc/vec/vecQue.h" #include "misc/vec/vecHsh.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -271,6 +272,214 @@ Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); } + + + +/**Function************************************************************* + + Synopsis [Resubstitution data-structure.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +typedef struct Gia_ResbMan_t_ Gia_ResbMan_t; +struct Gia_ResbMan_t_ +{ + int nWords; + Vec_Ptr_t * vDivs; + Vec_Int_t * vGates; + Vec_Int_t * vUnateLits[2]; + Vec_Int_t * vNotUnateVars[2]; + Vec_Int_t * vUnatePairs[2]; + Vec_Int_t * vBinateVars; + Vec_Int_t * vUnateLitsW[2]; + Vec_Int_t * vUnatePairsW[2]; + word * pDivA; + word * pDivB; +}; +Gia_ResbMan_t * Gia_ResbAlloc( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates ) +{ + 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 ); + p->vNotUnateVars[1] = Vec_IntAlloc( 100 ); + p->vUnatePairs[0] = Vec_IntAlloc( 100 ); + p->vUnatePairs[1] = Vec_IntAlloc( 100 ); + p->vUnateLitsW[0] = Vec_IntAlloc( 100 ); + p->vUnateLitsW[1] = Vec_IntAlloc( 100 ); + p->vUnatePairsW[0] = Vec_IntAlloc( 100 ); + p->vUnatePairsW[1] = Vec_IntAlloc( 100 ); + p->vBinateVars = Vec_IntAlloc( 100 ); + p->pDivA = ABC_CALLOC( word, nWords ); + p->pDivB = ABC_CALLOC( word, nWords ); + return p; +} +void Gia_ResbReset( Gia_ResbMan_t * p ) +{ + Vec_IntClear( p->vUnateLits[0] ); + Vec_IntClear( p->vUnateLits[1] ); + Vec_IntClear( p->vNotUnateVars[0] ); + Vec_IntClear( p->vNotUnateVars[1] ); + Vec_IntClear( p->vUnatePairs[0] ); + Vec_IntClear( p->vUnatePairs[1] ); + Vec_IntClear( p->vUnateLitsW[0] ); + Vec_IntClear( p->vUnateLitsW[1] ); + Vec_IntClear( p->vUnatePairsW[0] ); + Vec_IntClear( p->vUnatePairsW[1] ); + Vec_IntClear( p->vBinateVars ); +} +void Gia_ResbFree( Gia_ResbMan_t * p ) +{ + Vec_IntFree( p->vUnateLits[0] ); + Vec_IntFree( p->vUnateLits[1] ); + Vec_IntFree( p->vNotUnateVars[0] ); + Vec_IntFree( p->vNotUnateVars[1] ); + Vec_IntFree( p->vUnatePairs[0] ); + Vec_IntFree( p->vUnatePairs[1] ); + Vec_IntFree( p->vUnateLitsW[0] ); + Vec_IntFree( p->vUnateLitsW[1] ); + Vec_IntFree( p->vUnatePairsW[0] ); + Vec_IntFree( p->vUnatePairsW[1] ); + Vec_IntFree( p->vBinateVars ); + ABC_FREE( p->pDivA ); + ABC_FREE( p->pDivB ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Verify resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManResubVerify( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vGates, int iTopLit ) +{ + int i, iLit0, iLit1, RetValue, nDivs = Vec_PtrSize(vDivs); + word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); + word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); + word * pDivRes; + Vec_Wrd_t * vSims = NULL; + if ( iTopLit <= -1 ) + return -1; + if ( iTopLit == 0 ) + return Abc_TtIsConst0( pOnSet, nWords ); + if ( iTopLit == 1 ) + return Abc_TtIsConst0( pOffSet, nWords ); + if ( Abc_Lit2Var(iTopLit) < nDivs ) + { + assert( Vec_IntSize(vGates) == 0 ); + pDivRes = (word *)Vec_PtrEntry( 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 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); + if ( iVar0 < iVar1 ) + Abc_TtAndCompl( pDiv, pDiv0, Abc_LitIsCompl(iLit0), pDiv1, Abc_LitIsCompl(iLit1), nWords ); + else if ( iVar0 > iVar1 ) + { + assert( !Abc_LitIsCompl(iLit0) ); + assert( !Abc_LitIsCompl(iLit1) ); + Abc_TtXor( pDiv, pDiv0, pDiv1, nWords, 0 ); + } + else assert( 0 ); + } + pDivRes = Vec_WrdEntryP( vSims, nWords*(Vec_IntSize(vGates)/2-1) ); + } + if ( Abc_LitIsCompl(iTopLit) ) + RetValue = !Abc_TtIntersectOne(pOnSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 1, nWords); + else + RetValue = !Abc_TtIntersectOne(pOffSet, 0, pDivRes, 0, nWords) && !Abc_TtIntersectOne(pOnSet, 0, pDivRes, 1, nWords); + Vec_WrdFreeP( &vSims ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Construct AIG manager from gates.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManGetVar( Gia_Man_t * pNew, Vec_Int_t * vUsed, int iVar ) +{ + if ( Vec_IntEntry(vUsed, iVar) == -1 ) + 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 ) +{ + int i, iLit0, iLit1, iLitRes; + Gia_Man_t * pNew = Gia_ManStart( 100 ); + pNew->pName = Abc_UtilStrsav( "resub" ); + assert( iTopLit >= 0 ); + if ( iTopLit == 0 || iTopLit == 1 ) + iLitRes = 0; + else if ( Abc_Lit2Var(iTopLit) < nVars ) + { + assert( Vec_IntSize(vGates) == 0 ); + 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( 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); + if ( iVar0 < iVar1 ) + iLitRes = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); + else if ( iVar0 > iVar1 ) + { + assert( !Abc_LitIsCompl(iLit0) ); + assert( !Abc_LitIsCompl(iLit1) ); + iLitRes = Gia_ManAppendXor( pNew, Abc_LitNotCond(iRes0, Abc_LitIsCompl(iLit0)), Abc_LitNotCond(iRes1, Abc_LitIsCompl(iLit1)) ); + } + else assert( 0 ); + Vec_IntPush( vCopy, iLitRes ); + } + assert( Vec_IntSize(vCopy) == Vec_IntSize(vGates)/2 ); + iLitRes = Vec_IntEntry( vCopy, Vec_IntSize(vGates)/2-1 ); + Vec_IntFree( vUsed ); + Vec_IntFree( vCopy ); + } + Gia_ManAppendCo( pNew, Abc_LitNotCond(iLitRes, Abc_LitIsCompl(iTopLit)) ); + return pNew; +} + + /**Function************************************************************* Synopsis [Perform resubstitution.] @@ -282,6 +491,492 @@ Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart ); SeeAlso [] ***********************************************************************/ +static inline int Gia_ManFindFirstCommonLit( Vec_Int_t * vArr1, Vec_Int_t * vArr2 ) +{ + int * pBeg1 = vArr1->pArray; + int * pBeg2 = vArr2->pArray; + int * pEnd1 = vArr1->pArray + vArr1->nSize; + int * pEnd2 = vArr2->pArray + vArr2->nSize; + int * pStart1 = vArr1->pArray; + int * pStart2 = vArr2->pArray; + int nRemoved = 0; + while ( pBeg1 < pEnd1 && pBeg2 < pEnd2 ) + { + if ( Abc_Lit2Var(*pBeg1) == Abc_Lit2Var(*pBeg2) ) + { + if ( *pBeg1 != *pBeg2 ) + return *pBeg1; + else + pBeg1++, pBeg2++; + nRemoved++; + } + else if ( *pBeg1 < *pBeg2 ) + *pStart1++ = *pBeg1++; + else + *pStart2++ = *pBeg2++; + } + while ( pBeg1 < pEnd1 ) + *pStart1++ = *pBeg1++; + while ( pBeg2 < pEnd2 ) + *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) ); + return -1; +} + +void Gia_ManFindOneUnateInt( word * pOffSet, word * pOnSet, 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 ) ) + Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 0) ); + else if ( !Abc_TtIntersectOne( pOffSet, 0, pDiv, 1, nWords ) ) + Vec_IntPush( vUnateLits, Abc_Var2Lit(i, 1) ); + else + Vec_IntPush( vNotUnateVars, i ); +} +int Gia_ManFindOneUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vNotUnateVars[2] ) +{ + 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 ); + } + return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] ); +} + +static inline int Gia_ManDivCover( word * pOffSet, word * pOnSet, 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 ); +} +int Gia_ManFindTwoUnateInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits ) +{ + int i, k, iDiv0, iDiv1; + Vec_IntForEachEntry( vUnateLits, iDiv1, i ) + Vec_IntForEachEntryStop( vUnateLits, iDiv0, k, i ) + { + 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); + } + return -1; +} +int Gia_ManFindTwoUnate( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2] ) +{ + 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] ); + if ( iLit >= 0 ) + return Abc_LitNotCond(iLit, !n); + ABC_SWAP( word *, pOffSet, pOnSet ); + } + return -1; +} + +void Gia_ManFindXorInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits ) +{ + 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) ); + 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) ); + } +} +int Gia_ManFindXor( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] ) +{ + 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 ); + } + return Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] ); +} + +void Gia_ManFindUnatePairsInt( word * pOffSet, word * pOnSet, Vec_Int_t * vBinate, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits ) +{ + int n, 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); + 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, pDiv0, n&1, pDiv1, n>>1, nWords ) ) + Vec_IntPush( vUnateLits, Abc_Var2Lit((iLit0 << 16) | iLit1, 0) ); + } + } +} +void Gia_ManFindUnatePairs( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vBinateVars, Vec_Int_t * vUnateLits[2] ) +{ + 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 ); + } + RetValue = Gia_ManFindFirstCommonLit( vUnateLits[0], vUnateLits[1] ); + 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 ) +{ + 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); + } + return -1; +} +int Gia_ManFindAndGate( 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 ); + } + return -1; +} + +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 fCompB = 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( 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); + } + } + return -1; +} +int Gia_ManFindGateGate( 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; + } + return -1; +} + +void Gia_ManComputeLitWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits, Vec_Int_t * vUnateLitsW ) +{ + int i, iLit; + Vec_IntClear( vUnateLitsW ); + 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)) ); + } +} +void Gia_ManComputeLitWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnateLits[2], Vec_Int_t * vUnateLitsW[2] ) +{ + word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); + word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); + int n; + 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 ); + } + 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++ ) + { + printf( "%5d : ", i ); + printf( "Obj = %5d ", Vec_IntEntry(vUnateLits[n], pPerm[i]) ); + printf( "Cost = %5d\n", Vec_IntEntry(vUnateLitsW[n], pPerm[i]) ); + } + ABC_FREE( pPerm ); + } +} + +void Gia_ManComputePairWeightsInt( word * pOffSet, word * pOnSet, Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs, Vec_Int_t * vUnatePairsW ) +{ + int i, iPair; + 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; + word * pDiv0 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit0) ); + word * pDiv1 = (word *)Vec_PtrEntry( vDivs, Abc_Lit2Var(iLit1) ); + if ( iLit0 < iLit1 ) + { + assert( !fCompl ); + 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) ); + } + 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) ); + } + } +} +void Gia_ManComputePairWeights( Vec_Ptr_t * vDivs, int nWords, Vec_Int_t * vUnatePairs[2], Vec_Int_t * vUnatePairsW[2] ) +{ + word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); + word * pOnSet = (word *)Vec_PtrEntry( vDivs, 1 ); + int n; + for ( n = 0; n < 2; n++ ) + { + Gia_ManComputePairWeightsInt( pOffSet, pOnSet, vDivs, nWords, vUnatePairs[n], vUnatePairsW[n] ); + ABC_SWAP( word *, pOffSet, pOnSet ); + } + 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++ ) + { + printf( "%5d : ", i ); + printf( "Obj = %5d ", Vec_IntEntry(vUnatePairs[n], pPerm[i]) ); + printf( "Cost = %5d\n", Vec_IntEntry(vUnatePairsW[n], pPerm[i]) ); + } + ABC_FREE( pPerm ); + } +} + + +/**Function************************************************************* + + Synopsis [Perform resubstitution.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManResubInt2( Vec_Ptr_t * vDivs, int nWords, int NodeLimit, int ChoiceType, Vec_Int_t * vGates ) +{ + 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 + { + printf( "Creating %s (%d).\n", Abc_LitIsCompl(iResLit) ? "inverter" : "buffer", Abc_Lit2Var(iResLit) ); + return iResLit; + } + iResLit = Gia_ManFindTwoUnate( p->vDivs, p->nWords, p->vUnateLits ); + if ( iResLit >= 0 ) // and + { + int fCompl = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) >> 16; + int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF; + Vec_IntPushTwo( p->vGates, iDiv0, iDiv1 ); + printf( "Creating one AND-gate.\n" ); + return Abc_Var2Lit( nDivs + Vec_IntSize(p->vGates)/2-1, fCompl ); + } + 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 ); + } + iResLit = Gia_ManFindXor( p->vDivs, p->nWords, p->vBinateVars, p->vUnatePairs ); + if ( iResLit >= 0 ) // xor + { + int fCompl = Abc_LitIsCompl(iResLit); + int iDiv0 = Abc_Lit2Var(iResLit) >> 16; + int iDiv1 = Abc_Lit2Var(iResLit) & 0xFFFF; + 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" ); + return -1; + } +*/ + Gia_ManComputeLitWeights( p->vDivs, p->nWords, p->vUnateLits, p->vUnateLitsW ); + Gia_ManComputePairWeights( p->vDivs, p->nWords, p->vUnatePairs, p->vUnatePairsW ); + return -1; +} + +/**Function************************************************************* + + Synopsis [Top level.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCheckResub( Vec_Ptr_t * vDivs, int nWords ) +{ + int i, Set[10] = { 2, 189, 2127, 2125, 177, 178 }; + word * pOffSet = (word *)Vec_PtrEntry( vDivs, 0 ); + word * pOnSet = (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 ) + continue; + for ( v = 0; v < 6; v++ ) + if ( Abc_TtGetBit((word *)Vec_PtrEntry(vDivs, Set[v]), i) ) + Mint |= 1 << v; + if ( Vec_IntEntry(vValue, Mint) == -1 ) + Vec_IntWriteEntry(vValue, Mint, Value); + else if ( Vec_IntEntry(vValue, Mint) != Value ) + printf( "Mismatch in pattern %d\n", i ); + } + printf( "Finished verifying resub.\n" ); + Vec_IntFree( vValue ); +} +Vec_Ptr_t * Gia_ManDeriveDivs( Vec_Wrd_t * vSims, int nWords ) +{ + int i, nDivs = Vec_WrdSize(vSims)/nWords; + Vec_Ptr_t * vDivs = Vec_PtrAlloc( nDivs ); + for ( i = 0; i < nDivs; i++ ) + 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 fVerbose, int fVeryVerbose ) +{ + return NULL; +} +Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose ) +{ + extern Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName, int * pnWords ); + int iTopLit, nWords = 0; + Gia_Man_t * pMan = NULL; + Vec_Wrd_t * vSims = Gia_ManSimPatRead( pFileName, &nWords ); + Vec_Ptr_t * vDivs = vSims ? Gia_ManDeriveDivs( vSims, nWords ) : NULL; + Vec_Int_t * vGates = vDivs ? Vec_IntAlloc( 100 ) : NULL; + Gia_ResbMan_t * p = vDivs ? Gia_ResbAlloc( vDivs, nWords, vGates ) : NULL; + if ( p == NULL ) + return NULL; + assert( Vec_PtrSize(vDivs) < (1<<15) ); + printf( "OFF = %5d (%6.2f %%) ", Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 0), nWords), 100.0*Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 0), nWords)/(64*nWords) ); + printf( "ON = %5d (%6.2f %%)\n", Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 1), nWords), 100.0*Abc_TtCountOnesVec(Vec_PtrEntry(vDivs, 1), nWords)/(64*nWords) ); + if ( Vec_PtrSize(vDivs) > 4000 ) + { + printf( "Reducing all divs from %d to 4000.\n", Vec_PtrSize(vDivs) ); + Vec_PtrShrink( vDivs, 4000 ); + } + Gia_ResbReset( p ); +// Gia_ManCheckResub( vDivs, nWords ); + iTopLit = Gia_ManResubInt( p ); + if ( iTopLit >= 0 ) + { + printf( "Verification %s.\n", Gia_ManResubVerify( vDivs, nWords, vGates, iTopLit ) ? "succeeded" : "FAILED" ); + pMan = Gia_ManConstructFromGates( Vec_PtrSize(vDivs), vGates, iTopLit ); + } + else + printf( "Decomposition did not succeed.\n" ); + Gia_ResbFree( p ); + Vec_IntFree( vGates ); + Vec_PtrFree( vDivs ); + Vec_WrdFree( vSims ); + return pMan; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index c53c1db8..f9539faf 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -343,7 +343,7 @@ void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) for ( i = 0; i < nNodes; i++ ) Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords ); fclose( pFile ); - printf( "Written %d words of simulation data into file \"%s\".\n", nWords, pFileName ); + 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 ) { @@ -358,7 +358,7 @@ int Gia_ManSimPatReadOne( char c ) assert( Digit >= 0 && Digit < 16 ); return Digit; } -Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName ) +Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName, int * pnWords ) { Vec_Wrd_t * vSimsIn = NULL; int c, nWords = -1, nChars = 0; word Num = 0; @@ -384,7 +384,9 @@ Vec_Wrd_t * Gia_ManSimPatRead( char * pFileName ) } assert( Vec_WrdSize(vSimsIn) % nWords == 0 ); fclose( pFile ); - printf( "Read %d words of simulation data.\n", nWords ); + printf( "Read %d words of simulation data for %d objects.\n", nWords, Vec_WrdSize(vSimsIn)/nWords ); + if ( pnWords ) + *pnWords = nWords; return vSimsIn; } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index d0ec969f..5ee20e6a 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -2290,6 +2290,94 @@ Gia_Man_t * Gia_ManDupWithMuxPos( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [Collect distance info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManRingAdd( Gia_Man_t * p, int iObj, Vec_Int_t * vRes, Vec_Int_t * vDists, int Dist ) +{ + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return; + Gia_ObjSetTravIdCurrentId(p, iObj); + Vec_IntWriteEntry( vDists, iObj, Dist ); + Vec_IntPush( vRes, iObj ); +} +void Gia_ManCollectRing( Gia_Man_t * p, Vec_Int_t * vStart, Vec_Int_t * vRes, Vec_Int_t * vDists ) +{ + int i, k, iObj, iFan; + Vec_IntForEachEntry( vStart, iObj, i ) + { + int Weight = Vec_IntEntry( vDists, iObj ); + Gia_Obj_t * pObj = Gia_ManObj(p, iObj); + assert( Weight > 0 ); + if ( Gia_ObjIsAnd(pObj) ) + { + Gia_ManRingAdd( p, Gia_ObjFaninId0(pObj, iObj), vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ObjFanin0(pObj)) ); + Gia_ManRingAdd( p, Gia_ObjFaninId1(pObj, iObj), vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ObjFanin1(pObj)) ); + } + Gia_ObjForEachFanoutStaticId( p, iObj, iFan, k ) + Gia_ManRingAdd( p, iFan, vRes, vDists, Weight + 1*!Gia_ObjIsBuf(Gia_ManObj(p, iFan)) ); + } +} +Vec_Int_t * Gia_ManComputeDistanceInt( Gia_Man_t * p, int iTarg, Vec_Int_t * vObjs, int fVerbose ) +{ + int i, iObj; + Vec_Int_t * vDists, * vStart, * vNexts; + vStart = Vec_IntAlloc( 100 ); + vNexts = Vec_IntAlloc( 100 ); + vDists = Vec_IntStart( Gia_ManObjNum(p) ); + Gia_ManIncrementTravId( p ); + if ( vObjs ) + { + Vec_IntForEachEntry( vObjs, iObj, i ) + { + Gia_ObjSetTravIdCurrentId(p, iObj); + Vec_IntWriteEntry( vDists, iObj, 1 ); + Vec_IntPush( vStart, iObj ); + } + } + else + { + Gia_ObjSetTravIdCurrentId(p, iTarg); + Vec_IntWriteEntry( vDists, iTarg, 1 ); + Vec_IntPush( vStart, iTarg ); + } + for ( i = 0; ; i++ ) + { + if ( fVerbose ) + printf( "Ring %2d : %6d\n", i, Vec_IntSize(vDists)-Vec_IntCountZero(vDists) ); + Gia_ManCollectRing( p, vStart, vNexts, vDists ); + if ( Vec_IntSize(vNexts) == 0 ) + break; + Vec_IntClear( vStart ); + ABC_SWAP( Vec_Int_t, *vStart, *vNexts ); + } + Vec_IntFree( vStart ); + Vec_IntFree( vNexts ); + return vDists; +} +Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose ) +{ + Vec_Int_t * vDists; + if ( p->vFanoutNums ) + vDists = Gia_ManComputeDistanceInt( p, iObj, vObjs, fVerbose ); + else + { + Gia_ManStaticFanoutStart( p ); + vDists = Gia_ManComputeDistanceInt( p, iObj, vObjs, fVerbose ); + Gia_ManStaticFanoutStop( p ); + } + return vDists; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 85053e18..70ef45ca 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -437,6 +437,7 @@ static int Abc_CommandAbc9Shrink ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Fx ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Balance ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BalanceLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Resub ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Syn2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Syn3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Syn4 ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1156,6 +1157,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&fx", Abc_CommandAbc9Fx, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&b", Abc_CommandAbc9Balance, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&blut", Abc_CommandAbc9BalanceLut, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&resub", Abc_CommandAbc9Resub, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&syn2", Abc_CommandAbc9Syn2, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&syn3", Abc_CommandAbc9Syn3, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&syn4", Abc_CommandAbc9Syn4, 0 ); @@ -34769,6 +34771,104 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Resub( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManResub1( char * pFileName, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose ); + extern Gia_Man_t * Gia_ManResub2( Gia_Man_t * pGia, int nNodes, int nSupp, int nDivs, int fVerbose, int fVeryVerbose ); + Gia_Man_t * pTemp; + int nNodes = 0; + int nSupp = 0; + int nDivs = 0; + int c, fVerbose = 0; + int fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NSDvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( 1, "Command line switch \"-N\" should be followed by a floating point number.\n" ); + return 0; + } + nNodes = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nNodes < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( 1, "Command line switch \"-S\" should be followed by a floating point number.\n" ); + return 0; + } + nSupp = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSupp < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( 1, "Command line switch \"-D\" should be followed by a floating point number.\n" ); + return 0; + } + nDivs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nDivs < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc == globalUtilOptind + 1 ) + { + pTemp = Gia_ManResub1( argv[globalUtilOptind], nNodes, nSupp, nDivs, fVerbose, fVeryVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Resub(): There is no AIG.\n" ); + return 1; + } + pTemp = Gia_ManResub2( pAbc->pGia, nNodes, nSupp, nDivs, fVerbose, fVeryVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &resub [-NSD num] [-vwh]\n" ); + Abc_Print( -2, "\t performs AIG resubstitution\n" ); + Abc_Print( -2, "\t-N num : the limit on added nodes (num >= 0) [default = %d]\n", nNodes ); + Abc_Print( -2, "\t-S num : the limit on support size (num > 0) [default = %d]\n", nSupp ); + Abc_Print( -2, "\t-D num : the limit on divisor count (num > 0) [default = %d]\n", nDivs ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggles printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index 8f72a00f..485a5e4e 100644 --- a/src/base/acb/acbFunc.c +++ b/src/base/acb/acbFunc.c @@ -1541,7 +1541,7 @@ char * Acb_EnumerateSatAssigns( sat_solver * pSat, int PivotVar, int FreeVar, Ve { if ( iMint == 1000 ) { - //if ( Vec_IntSize(vDivVars) == 0 ) + if ( Vec_IntSize(vDivVars) == 0 ) { printf( "Assuming constant 0 function.\n" ); Vec_StrClear( vTempSop ); @@ -2511,7 +2511,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4] abctime clk = Abc_Clock(); int nTargets = Vec_IntSize(&pNtkF->vTargets); - int TimeOut = fCisOnly ? 0 : 60; // 60 seconds + int TimeOut = fCisOnly ? 0 : 120; // 60 seconds int RetValue = 1; // compute various sets of nodes diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c index 2243541b..8a51bd3e 100644 --- a/src/base/acb/acbUtil.c +++ b/src/base/acb/acbUtil.c @@ -671,6 +671,8 @@ int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer int nTargets = Vec_IntSize(&pNtkF->vTargets); Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF, fUseBuf, fUseXors, &pNtkF->vTargets, 0 ); Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG, 0, 0, NULL, nTargets ); + pGiaF->pSpec = Abc_UtilStrsav( pNtkF->pDesign->pSpec ); + pGiaG->pSpec = Abc_UtilStrsav( pNtkG->pDesign->pSpec ); assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) ); assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) ); *ppGiaF = pGiaF; @@ -784,6 +786,8 @@ int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer Gia_Man_t * pGiaG = Abc_NtkToGia2( pNtkG, 0 ); assert( Abc_NtkCiNum(pNtkF) == Abc_NtkCiNum(pNtkG) ); assert( Abc_NtkCoNum(pNtkF) == Abc_NtkCoNum(pNtkG) ); + pGiaF->pSpec = Abc_UtilStrsav( pNtkF->pSpec ); + pGiaG->pSpec = Abc_UtilStrsav( pNtkG->pSpec ); *ppGiaF = pGiaF; *ppGiaG = pGiaG; *pvNodes = Abc_NtkCollectCopies( pNtkF, pGiaF, pvNodesR, pvPolar ); diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index e0ee1720..425ec27d 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -365,6 +365,141 @@ static inline int Abc_TtIntersect( word * pIn1, word * pIn2, int nWords, int fCo } return 0; } +static inline int Abc_TtIntersectOne( word * pOut, int fComp, word * pIn, int fComp0, int nWords ) +{ + int w; + if ( fComp0 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn[w] & pOut[w] ) + return 1; + } + } + else + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( pIn[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pIn[w] & pOut[w] ) + return 1; + } + } + return 0; +} +static inline int Abc_TtIntersectTwo( word * pOut, int fComp, word * pIn0, int fComp0, word * pIn1, int fComp1, int nWords ) +{ + int w; + if ( fComp0 && fComp1 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & ~pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & ~pIn1[w] & pOut[w] ) + return 1; + } + } + else if ( fComp0 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~pIn0[w] & pIn1[w] & pOut[w] ) + return 1; + } + } + else if ( fComp1 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & ~pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & ~pIn1[w] & pOut[w] ) + return 1; + } + } + else + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & pIn1[w] & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( pIn0[w] & pIn1[w] & pOut[w] ) + return 1; + } + } + return 0; +} +static inline int Abc_TtIntersectXor( word * pOut, int fComp, word * pIn0, word * pIn1, int fComp01, int nWords ) +{ + int w; + if ( fComp01 ) + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( ~(pIn0[w] ^ pIn1[w]) & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( ~(pIn0[w] ^ pIn1[w]) & pOut[w] ) + return 1; + } + } + else + { + if ( fComp ) + { + for ( w = 0; w < nWords; w++ ) + if ( (pIn0[w] ^ pIn1[w]) & ~pOut[w] ) + return 1; + } + else + { + for ( w = 0; w < nWords; w++ ) + if ( (pIn0[w] ^ pIn1[w]) & pOut[w] ) + return 1; + } + } + return 0; +} static inline int Abc_TtEqual( word * pIn1, word * pIn2, int nWords ) { int w; @@ -1869,6 +2004,17 @@ static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords ) Count += Abc_TtCountOnes( x[w] ^ y[w] ); return Count; } +static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords ) +{ + int w, Count = 0; + if ( fCompl ) + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ ~y[w]) ); + else + for ( w = 0; w < nWords; w++ ) + Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ y[w]) ); + return Count; +} static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nWords ) { int w, Count = 0; diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 514ce455..7125593b 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -1397,6 +1397,14 @@ static inline void Vec_IntSortMulti( Vec_Int_t * p, int nMulti, int fReverse ) qsort( (void *)p->pArray, (size_t)(p->nSize/nMulti), nMulti*sizeof(int), (int (*)(const void *, const void *)) Vec_IntSortCompare1 ); } +static inline int Vec_IntIsSorted( Vec_Int_t * p, int fReverse ) +{ + int i; + for ( i = 1; i < p->nSize; i++ ) + if ( fReverse ? (p->pArray[i-1] < p->pArray[i]) : (p->pArray[i-1] > p->pArray[i]) ) + return 0; + return 1; +} /**Function************************************************************* -- cgit v1.2.3