Commit ffea3a2c by Alan Mishchenko

Improvements to technology mapping.

parent 9291ab9f
...@@ -233,11 +233,13 @@ struct If_Man_t_ ...@@ -233,11 +233,13 @@ struct If_Man_t_
int nCutsCountAll; int nCutsCountAll;
int nCutsUselessAll; int nCutsUselessAll;
int nCuts5, nCuts5a; int nCuts5, nCuts5a;
If_DsdMan_t * pIfDsdMan;
Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
If_DsdMan_t * pIfDsdMan; // DSD manager
Vec_Int_t * vTtDsds; // mapping of truth table into DSD Vec_Int_t * vTtDsds; // mapping of truth table into DSD
Vec_Str_t * vTtPerms; // mapping of truth table into permutations Vec_Str_t * vTtPerms; // mapping of truth table into permutations
Hash_IntMan_t * vPairHash; // hashing pairs of truth tables Hash_IntMan_t * vPairHash; // hashing pairs of truth tables
Vec_Int_t * vPairRes; // resulting truth table
Vec_Str_t * vPairPerms; // resulting permutation
int nBestCutSmall[2]; int nBestCutSmall[2];
int nCountNonDec[2]; int nCountNonDec[2];
Vec_Int_t * vCutData; // cut data storage Vec_Int_t * vCutData; // cut data storage
...@@ -389,6 +391,7 @@ static inline int * If_CutLeaves( If_Cut_t * pCut ) { r ...@@ -389,6 +391,7 @@ static inline int * If_CutLeaves( If_Cut_t * pCut ) { r
static inline unsigned If_CutSuppMask( If_Cut_t * pCut ) { return (~(unsigned)0) >> (32-pCut->nLeaves); } static inline unsigned If_CutSuppMask( If_Cut_t * pCut ) { return (~(unsigned)0) >> (32-pCut->nLeaves); }
static inline int If_CutTruthWords( int nVarsMax ) { return nVarsMax <= 5 ? 2 : (1 << (nVarsMax - 5)); } static inline int If_CutTruthWords( int nVarsMax ) { return nVarsMax <= 5 ? 2 : (1 << (nVarsMax - 5)); }
static inline int If_CutPermWords( int nVarsMax ) { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); } static inline int If_CutPermWords( int nVarsMax ) { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
static inline int If_CutLeafBit( If_Cut_t * pCut, int i ) { return (pCut->iCutDsd >> i) & 1; }
static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj ) { return &pObj->CutBest; } static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj ) { return &pObj->CutBest; }
static inline unsigned If_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId % 31)); } static inline unsigned If_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId % 31)); }
......
...@@ -215,7 +215,6 @@ int If_CutMergeOrdered_( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t ...@@ -215,7 +215,6 @@ int If_CutMergeOrdered_( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t
p->pPerm[0][i] = p->pPerm[1][i] = p->pPerm[2][i] = i; p->pPerm[0][i] = p->pPerm[1][i] = p->pPerm[2][i] = i;
pC->pLeaves[i] = pC0->pLeaves[i]; pC->pLeaves[i] = pC0->pLeaves[i];
} }
p->nShared = nLimit;
pC->nLeaves = nLimit; pC->nLeaves = nLimit;
pC->uSign = pC0->uSign | pC1->uSign; pC->uSign = pC0->uSign | pC1->uSign;
p->uSharedMask = Abc_InfoMask( nLimit ); p->uSharedMask = Abc_InfoMask( nLimit );
...@@ -259,7 +258,6 @@ FlushCut0: ...@@ -259,7 +258,6 @@ FlushCut0:
p->pPerm[0][i] = c; p->pPerm[0][i] = c;
pC->pLeaves[c++] = pC0->pLeaves[i++]; pC->pLeaves[c++] = pC0->pLeaves[i++];
} }
p->nShared = s;
pC->nLeaves = c; pC->nLeaves = c;
pC->uSign = pC0->uSign | pC1->uSign; pC->uSign = pC0->uSign | pC1->uSign;
assert( c > 0 ); assert( c > 0 );
...@@ -272,7 +270,6 @@ FlushCut1: ...@@ -272,7 +270,6 @@ FlushCut1:
p->pPerm[1][k] = c; p->pPerm[1][k] = c;
pC->pLeaves[c++] = pC1->pLeaves[k++]; pC->pLeaves[c++] = pC1->pLeaves[k++];
} }
p->nShared = s;
pC->nLeaves = c; pC->nLeaves = c;
pC->uSign = pC0->uSign | pC1->uSign; pC->uSign = pC0->uSign | pC1->uSign;
assert( c > 0 ); assert( c > 0 );
...@@ -312,7 +309,7 @@ int If_CutMergeOrdered( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * ...@@ -312,7 +309,7 @@ int If_CutMergeOrdered( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t *
} }
// compare two cuts with different numbers // compare two cuts with different numbers
i = k = c = s = 0; p->nShared = 0; i = k = c = s = 0;
if ( nSizeC0 == 0 ) goto FlushCut1; if ( nSizeC0 == 0 ) goto FlushCut1;
if ( nSizeC1 == 0 ) goto FlushCut0; if ( nSizeC1 == 0 ) goto FlushCut0;
while ( 1 ) while ( 1 )
...@@ -330,7 +327,7 @@ int If_CutMergeOrdered( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * ...@@ -330,7 +327,7 @@ int If_CutMergeOrdered( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t *
} }
else else
{ {
pC->pLeaves[c++] = pC0->pLeaves[i++]; k++; p->nShared++; pC->pLeaves[c++] = pC0->pLeaves[i++]; k++;
if ( i == nSizeC0 ) goto FlushCut1; if ( i == nSizeC0 ) goto FlushCut1;
if ( k == nSizeC1 ) goto FlushCut0; if ( k == nSizeC1 ) goto FlushCut0;
} }
...@@ -374,7 +371,7 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pC ...@@ -374,7 +371,7 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pC
int * pC = pCut->pLeaves; int * pC = pCut->pLeaves;
int i, k, c; int i, k, c;
// compare two cuts with different numbers // compare two cuts with different numbers
c = nSize0; p->nShared = 0; c = nSize0;
for ( i = 0; i < nSize1; i++ ) for ( i = 0; i < nSize1; i++ )
{ {
for ( k = 0; k < nSize0; k++ ) for ( k = 0; k < nSize0; k++ )
...@@ -383,7 +380,6 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pC ...@@ -383,7 +380,6 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pCut0, If_Cut_t * pCut1, If_Cut_t * pC
if ( k < nSize0 ) if ( k < nSize0 )
{ {
p->pPerm[1][i] = k; p->pPerm[1][i] = k;
p->nShared++;
continue; continue;
} }
if ( c == nLutSize ) if ( c == nLutSize )
......
...@@ -102,7 +102,10 @@ If_Man_t * If_ManStart( If_Par_t * pPars ) ...@@ -102,7 +102,10 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
if ( pPars->fUseTtPerm ) if ( pPars->fUseTtPerm )
{ {
p->vPairHash = Hash_IntManStart( 10000 ); p->vPairHash = Hash_IntManStart( 10000 );
p->vTtPerms = Vec_StrAlloc( 10000 ); p->vPairPerms = Vec_StrAlloc( 10000 );
Vec_StrFill( p->vPairPerms, p->pPars->nLutSize, 0 );
p->vPairRes = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vPairRes, -1 );
} }
// create the constant node // create the constant node
p->pConst1 = If_ManSetupObj( p ); p->pConst1 = If_ManSetupObj( p );
...@@ -196,6 +199,8 @@ void If_ManStop( If_Man_t * p ) ...@@ -196,6 +199,8 @@ void If_ManStop( If_Man_t * p )
Vec_IntFreeP( &p->vTtDsds ); Vec_IntFreeP( &p->vTtDsds );
Vec_StrFreeP( &p->vTtPerms ); Vec_StrFreeP( &p->vTtPerms );
Vec_IntFreeP( &p->vCutData ); Vec_IntFreeP( &p->vCutData );
Vec_IntFreeP( &p->vPairRes );
Vec_StrFreeP( &p->vPairPerms );
if ( p->vPairHash ) if ( p->vPairHash )
Hash_IntManStop( p->vPairHash ); Hash_IntManStop( p->vPairHash );
for ( i = 6; i <= p->pPars->nLutSize; i++ ) for ( i = 6; i <= p->pPars->nLutSize; i++ )
......
...@@ -83,50 +83,6 @@ float If_CutDelaySpecial( If_Man_t * p, If_Cut_t * pCut, int fCarry ) ...@@ -83,50 +83,6 @@ float If_CutDelaySpecial( If_Man_t * p, If_Cut_t * pCut, int fCarry )
/**Function************************************************************* /**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int * If_CutPerm0( If_Cut_t * pCut, If_Cut_t * pCut0 )
{
static int pPerm[IF_MAX_LUTSIZE];
int i, k;
for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
{
if ( k == (int)pCut0->nLeaves )
break;
if ( pCut->pLeaves[i] < pCut0->pLeaves[k] )
continue;
assert( pCut->pLeaves[i] == pCut0->pLeaves[k] );
pPerm[k++] = i;
}
return pPerm;
}
static inline int * If_CutPerm1( If_Cut_t * pCut, If_Cut_t * pCut1 )
{
static int pPerm[IF_MAX_LUTSIZE];
int i, k;
for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
{
if ( k == (int)pCut1->nLeaves )
break;
if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
continue;
assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
pPerm[k++] = i;
}
return pPerm;
}
/**Function*************************************************************
Synopsis [Finds the best cut for the given node.] Synopsis [Finds the best cut for the given node.]
Description [Mapping modes: delay (0), area flow (1), area (2).] Description [Mapping modes: delay (0), area flow (1), area (2).]
...@@ -140,6 +96,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -140,6 +96,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
{ {
If_Set_t * pCutSet; If_Set_t * pCutSet;
If_Cut_t * pCut0, * pCut1, * pCut; If_Cut_t * pCut0, * pCut1, * pCut;
If_Cut_t * pCut0R, * pCut1R;
int fFunc0R, fFunc1R;
int i, k, v, fChange; int i, k, v, fChange;
assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 ); assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 ); assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
...@@ -196,15 +154,29 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -196,15 +154,29 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// make sure K-feasible cut exists // make sure K-feasible cut exists
if ( If_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->pPars->nLutSize ) if ( If_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->pPars->nLutSize )
continue; continue;
pCut0R = pCut0;
pCut1R = pCut1;
fFunc0R = pCut0->iCutFunc ^ pCut0->fCompl ^ pObj->fCompl0;
fFunc1R = pCut1->iCutFunc ^ pCut1->fCompl ^ pObj->fCompl1;
if ( !p->pPars->fUseTtPerm || pCut0->nLeaves > pCut1->nLeaves || (pCut0->nLeaves == pCut1->nLeaves && fFunc0R > fFunc1R) )
{
}
else
{
ABC_SWAP( If_Cut_t *, pCut0R, pCut1R );
ABC_SWAP( int, fFunc0R, fFunc1R );
}
// merge the cuts // merge the cuts
if ( p->pPars->fUseTtPerm ) if ( p->pPars->fUseTtPerm )
{ {
if ( !If_CutMerge( p, pCut0, pCut1, pCut ) ) if ( !If_CutMerge( p, pCut0R, pCut1R, pCut ) )
continue; continue;
} }
else else
{ {
if ( !If_CutMergeOrdered( p, pCut0, pCut1, pCut ) ) if ( !If_CutMergeOrdered( p, pCut0R, pCut1R, pCut ) )
continue; continue;
} }
if ( pObj->fSpec && pCut->nLeaves == (unsigned)p->pPars->nLutSize ) if ( pObj->fSpec && pCut->nLeaves == (unsigned)p->pPars->nLutSize )
...@@ -218,13 +190,13 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -218,13 +190,13 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
pCut->fCompl = 0; pCut->fCompl = 0;
pCut->iCutFunc = -1; pCut->iCutFunc = -1;
pCut->iCutDsd = -1; pCut->iCutDsd = -1;
if ( p->pPars->fTruth )//&& !p->pPars->fUseTtPerm ) if ( p->pPars->fTruth )
{ {
// abctime clk = Abc_Clock(); // abctime clk = Abc_Clock();
if ( p->pPars->fUseTtPerm ) if ( p->pPars->fUseTtPerm )
fChange = If_CutComputeTruthPerm( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 ); fChange = If_CutComputeTruthPerm( p, pCut, pCut0R, pCut1R, fFunc0R, fFunc1R );
else else
fChange = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 ); fChange = If_CutComputeTruth( p, pCut, pCut0R, pCut1R, pObj->fCompl0, pObj->fCompl1 );
if ( !p->pPars->fSkipCutFilter && fChange && If_CutFilter( pCutSet, pCut ) ) if ( !p->pPars->fSkipCutFilter && fChange && If_CutFilter( pCutSet, pCut ) )
continue; continue;
// p->timeTruth += Abc_Clock() - clk; // p->timeTruth += Abc_Clock() - clk;
...@@ -251,7 +223,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep ...@@ -251,7 +223,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
for ( v = 0; v < (int)pCut->nLeaves; v++ ) for ( v = 0; v < (int)pCut->nLeaves; v++ )
pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v ); pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
} }
If_ManCacheRecord( p, pCut0->iCutDsd, pCut1->iCutDsd, p->nShared, pCut->iCutDsd ); If_ManCacheRecord( p, pCut0R->iCutDsd, pCut1R->iCutDsd, p->nShared, pCut->iCutDsd );
} }
// run user functions // run user functions
pCut->fUseless = 0; pCut->fUseless = 0;
......
...@@ -146,22 +146,22 @@ int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_ ...@@ -146,22 +146,22 @@ int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 ) int If_CutComputeTruthPerm_int( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int iCutFunc0, int iCutFunc1 )
{ {
int fVerbose = 0; int fVerbose = 0;
int pPerm[IF_MAX_LUTSIZE]; int pPerm[IF_MAX_LUTSIZE];
char pCanonPerm[IF_MAX_LUTSIZE]; char pCanonPerm[IF_MAX_LUTSIZE];
int v, Place, fCompl, truthId, nLeavesNew, uCanonPhase, RetValue = 0; int v, Place, fCompl, truthId, nLeavesNew, uCanonPhase, RetValue = 0;
int nWords = Abc_TtWordNum( pCut->nLeaves ); int nWords = Abc_TtWordNum( pCut->nLeaves );
word * pTruth0s = Vec_MemReadEntry( p->vTtMem[pCut0->nLeaves], Abc_Lit2Var(pCut0->iCutFunc) ); word * pTruth0s = Vec_MemReadEntry( p->vTtMem[pCut0->nLeaves], Abc_Lit2Var(iCutFunc0) );
word * pTruth1s = Vec_MemReadEntry( p->vTtMem[pCut1->nLeaves], Abc_Lit2Var(pCut1->iCutFunc) ); word * pTruth1s = Vec_MemReadEntry( p->vTtMem[pCut1->nLeaves], Abc_Lit2Var(iCutFunc1) );
word * pTruth0 = (word *)p->puTemp[0]; word * pTruth0 = (word *)p->puTemp[0];
word * pTruth1 = (word *)p->puTemp[1]; word * pTruth1 = (word *)p->puTemp[1];
word * pTruth = (word *)p->puTemp[2]; word * pTruth = (word *)p->puTemp[2];
assert( pCut0->iCutDsd >= 0 ); assert( pCut0->iCutDsd >= 0 );
assert( pCut1->iCutDsd >= 0 ); assert( pCut1->iCutDsd >= 0 );
Abc_TtCopy( pTruth0, pTruth0s, nWords, fCompl0 ^ pCut0->fCompl ^ Abc_LitIsCompl(pCut0->iCutFunc) ); Abc_TtCopy( pTruth0, pTruth0s, nWords, Abc_LitIsCompl(iCutFunc0) );
Abc_TtCopy( pTruth1, pTruth1s, nWords, fCompl1 ^ pCut1->fCompl ^ Abc_LitIsCompl(pCut1->iCutFunc) ); Abc_TtCopy( pTruth1, pTruth1s, nWords, Abc_LitIsCompl(iCutFunc1) );
Abc_TtStretch6( pTruth0, pCut0->nLeaves, pCut->nLeaves ); Abc_TtStretch6( pTruth0, pCut0->nLeaves, pCut->nLeaves );
Abc_TtStretch6( pTruth1, pCut1->nLeaves, pCut->nLeaves ); Abc_TtStretch6( pTruth1, pCut1->nLeaves, pCut->nLeaves );
...@@ -172,11 +172,11 @@ if ( fVerbose ) ...@@ -172,11 +172,11 @@ if ( fVerbose )
} }
// create literals // create literals
for ( v = 0; v < (int)pCut0->nLeaves; v++ ) for ( v = 0; v < (int)pCut0->nLeaves; v++ )
pCut->pLeaves[v] = Abc_Var2Lit( pCut0->pLeaves[v], ((pCut0->iCutDsd >> v) & 1) ); pCut->pLeaves[v] = Abc_Var2Lit( pCut0->pLeaves[v], If_CutLeafBit(pCut0, v) );
for ( v = 0; v < (int)pCut1->nLeaves; v++ ) for ( v = 0; v < (int)pCut1->nLeaves; v++ )
if ( p->pPerm[1][v] >= (int)pCut0->nLeaves ) if ( p->pPerm[1][v] >= (int)pCut0->nLeaves )
pCut->pLeaves[p->pPerm[1][v]] = Abc_Var2Lit( pCut1->pLeaves[v], ((pCut1->iCutDsd >> v) & 1) ); pCut->pLeaves[p->pPerm[1][v]] = Abc_Var2Lit( pCut1->pLeaves[v], If_CutLeafBit(pCut1, v) );
else if ( ((pCut0->iCutDsd >> p->pPerm[1][v]) & 1) != ((pCut1->iCutDsd >> v) & 1) ) else if ( If_CutLeafBit(pCut0, p->pPerm[1][v]) != If_CutLeafBit(pCut1, v) )
Abc_TtFlip( pTruth1, nWords, v ); Abc_TtFlip( pTruth1, nWords, v );
// permute variables // permute variables
for ( v = (int)pCut1->nLeaves; v < (int)pCut->nLeaves; v++ ) for ( v = (int)pCut1->nLeaves; v < (int)pCut->nLeaves; v++ )
...@@ -243,6 +243,69 @@ if ( fVerbose ) ...@@ -243,6 +243,69 @@ if ( fVerbose )
return RetValue; return RetValue;
} }
int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int iCutFunc0, int iCutFunc1 )
{
int i, k, Num, nEntriesOld, RetValue;
// if ( pCut0->nLeaves + pCut1->nLeaves > pCut->nLeaves || iCutFunc0 < 2 || iCutFunc1 < 2 )
return If_CutComputeTruthPerm_int( p, pCut, pCut0, pCut1, iCutFunc0, iCutFunc1 );
assert( pCut0->nLeaves + pCut1->nLeaves == pCut->nLeaves );
nEntriesOld = Hash_IntManEntryNum(p->vPairHash);
Num = Hash_Int2ManInsert( p->vPairHash, (iCutFunc0 << 5)|pCut0->nLeaves, (iCutFunc1 << 5)|pCut1->nLeaves, -1 );
assert( Num > 0 );
if ( nEntriesOld == Hash_IntManEntryNum(p->vPairHash) )
{
int v, pPerm[IF_MAX_LUTSIZE];
char * pCanonPerm = Vec_StrEntryP( p->vPairPerms, Num * pCut->nLimit );
pCut->iCutFunc = Vec_IntEntry( p->vPairRes, Num );
// move complements from the fanin cuts
for ( v = 0; v < (int)pCut->nLeaves; v++ )
if ( v < (int)pCut0->nLeaves )
{
assert( pCut->pLeaves[v] == pCut0->pLeaves[v] );
pCut->pLeaves[v] = Abc_Var2Lit( pCut->pLeaves[v], If_CutLeafBit(pCut0, v) );
}
else
{
assert( pCut->pLeaves[v] == pCut1->pLeaves[v-(int)pCut0->nLeaves] );
pCut->pLeaves[v] = Abc_Var2Lit( pCut->pLeaves[v], If_CutLeafBit(pCut1, v-(int)pCut0->nLeaves) );
}
// reorder the cut
for ( v = 0; v < (int)pCut->nLeaves; v++ )
{
assert( pCanonPerm[v] >= 0 );
pPerm[v] = Abc_LitNotCond( pCut->pLeaves[Abc_Lit2Var((int)pCanonPerm[v])], Abc_LitIsCompl((int)pCanonPerm[v]) );
}
// generate the result
pCut->iCutDsd = 0;
for ( v = 0; v < (int)pCut->nLeaves; v++ )
{
pCut->pLeaves[v] = Abc_Lit2Var(pPerm[v]);
if ( Abc_LitIsCompl(pPerm[v]) )
pCut->iCutDsd |= (1 << v);
}
// printf( "Found: %d(%d) %d(%d) -> %d(%d)\n", iCutFunc0, pCut0->nLeaves, iCutFunc1, pCut0->nLeaves, pCut->iCutFunc, pCut->nLeaves );
return 0;
}
RetValue = If_CutComputeTruthPerm_int( p, pCut, pCut0, pCut1, iCutFunc0, iCutFunc1 );
assert( RetValue == 0 );
// printf( "Added: %d(%d) %d(%d) -> %d(%d)\n", iCutFunc0, pCut0->nLeaves, iCutFunc1, pCut0->nLeaves, pCut->iCutFunc, pCut->nLeaves );
// save the result
assert( Num == Vec_IntSize(p->vPairRes) );
Vec_IntPush( p->vPairRes, pCut->iCutFunc );
// save the permutation
assert( Num * (int)pCut->nLimit == Vec_StrSize(p->vPairPerms) );
for ( i = 0; i < (int)pCut0->nLeaves; i++ )
for ( k = 0; k < (int)pCut->nLeaves; k++ )
if ( pCut0->pLeaves[i] == pCut->pLeaves[k] )
{ Vec_StrPush( p->vPairPerms, (char)Abc_Var2Lit(k, If_CutLeafBit(pCut0, i) != If_CutLeafBit(pCut, k)) ); break; }
for ( i = 0; i < (int)pCut1->nLeaves; i++ )
for ( k = 0; k < (int)pCut->nLeaves; k++ )
if ( pCut1->pLeaves[i] == pCut->pLeaves[k] )
{ Vec_StrPush( p->vPairPerms, (char)Abc_Var2Lit(k, If_CutLeafBit(pCut1, i) != If_CutLeafBit(pCut, k)) ); break; }
for ( i = (int)pCut0->nLeaves + (int)pCut1->nLeaves; i < (int)pCut->nLimit; i++ )
Vec_StrPush( p->vPairPerms, (char)-1 );
return 0;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment