diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/aig/gia/giaTruth.c | 152 | ||||
| -rw-r--r-- | src/aig/miniaig/miniaig.h | 58 | ||||
| -rw-r--r-- | src/base/abci/abcResub.c | 492 | ||||
| -rw-r--r-- | src/base/main/mainReal.c | 4 |
4 files changed, 580 insertions, 126 deletions
diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c index 2062f2ad..91c4fa24 100644 --- a/src/aig/gia/giaTruth.c +++ b/src/aig/gia/giaTruth.c @@ -83,7 +83,159 @@ word Gia_LutComputeTruth6Simple( Gia_Man_t * p, int iPo ) Gia_Obj_t * pObj = Gia_ManPo( p, iPo ); word Truth = Gia_LutComputeTruth6Simple_rec( p, Gia_ObjFaninId0p(p, pObj) ); return Gia_ObjFaninC0(pObj) ? ~Truth : Truth; +} + +word Gia_LutComputeTruth6Map_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vMap ) +{ + word Truth0, Truth1, Truth; + Gia_Obj_t * pObj = Gia_ManObj(p, iObj); + if ( Gia_ObjIsConst0(pObj) ) + return 0; + if ( Gia_ObjIsCi(pObj) ) + return s_Truths6[Vec_IntEntry(vMap, Gia_ObjCioId(pObj))]; + Truth0 = Gia_LutComputeTruth6Map_rec( p, Gia_ObjFaninId0(pObj, iObj), vMap ); + Truth1 = Gia_LutComputeTruth6Map_rec( p, Gia_ObjFaninId1(pObj, iObj), vMap ); + Truth0 = Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0; + Truth1 = Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1; + Truth = Gia_ObjIsXor(pObj) ? Truth0 ^ Truth1 : Truth0 & Truth1; + return Truth; +} +word Gia_LutComputeTruth6Map( Gia_Man_t * p, int iPo, Vec_Int_t * vMap ) +{ + Gia_Obj_t * pObj = Gia_ManPo( p, iPo ); + word Truth = Gia_LutComputeTruth6Map_rec( p, Gia_ObjFaninId0p(p, pObj), vMap ); + return Gia_ObjFaninC0(pObj) ? ~Truth : Truth; +} + +/**Function************************************************************* + + Synopsis [Generate MUX tree of the truth table.] + + Description [] + + SideEffects [] + SeeAlso [] + +***********************************************************************/ +static unsigned s_Truths5[5] = { + 0xAAAAAAAA, + 0xCCCCCCCC, + 0xF0F0F0F0, + 0xFF00FF00, + 0xFFFF0000, +}; +static inline int Abc_Tt5HasVar( unsigned t, int iVar ) +{ + return ((t << (1<<iVar)) & s_Truths5[iVar]) != (t & s_Truths5[iVar]); +} +static inline unsigned Abc_Tt5Cofactor0( unsigned t, int iVar ) +{ + assert( iVar >= 0 && iVar < 6 ); + return (t & ~s_Truths5[iVar]) | ((t & ~s_Truths5[iVar]) << (1<<iVar)); +} +static inline unsigned Abc_Tt5Cofactor1( unsigned t, int iVar ) +{ + assert( iVar >= 0 && iVar < 6 ); + return (t & s_Truths5[iVar]) | ((t & s_Truths5[iVar]) >> (1<<iVar)); +} +int Gia_Truth5ToGia( Gia_Man_t * p, int * pVarLits, int nVars, unsigned Truth, int fHash ) +{ + int Var, Lit0, Lit1; + if ( Truth == 0 ) + return 0; + if ( ~Truth == 0 ) + return 1; + assert( nVars > 0 ); + // find the topmost var + for ( Var = nVars-1; Var >= 0; Var-- ) + if ( Abc_Tt5HasVar( Truth, Var ) ) + break; + assert( Var >= 0 ); + // cofactor + Lit0 = Gia_Truth5ToGia( p, pVarLits, Var, Abc_Tt5Cofactor0(Truth, Var), fHash ); + Lit1 = Gia_Truth5ToGia( p, pVarLits, Var, Abc_Tt5Cofactor1(Truth, Var), fHash ); + if ( fHash ) + return Gia_ManHashMux( p, pVarLits[Var], Lit1, Lit0 ); + else + return Gia_ManAppendMux( p, pVarLits[Var], Lit1, Lit0 ); +} + +/**Function************************************************************* + + Synopsis [Generate MUX tree of the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_Truth6ToGia( Gia_Man_t * p, int * pVarLits, int nVars, word Truth, int fHash ) +{ + int Var, Lit0, Lit1; + if ( Truth == 0 ) + return 0; + if ( ~Truth == 0 ) + return 1; + assert( nVars > 0 ); + // find the topmost var + for ( Var = nVars-1; Var >= 0; Var-- ) + if ( Abc_Tt6HasVar( Truth, Var ) ) + break; + assert( Var >= 0 ); + // cofactor + Lit0 = Gia_Truth6ToGia( p, pVarLits, Var, Abc_Tt6Cofactor0(Truth, Var), fHash ); + Lit1 = Gia_Truth6ToGia( p, pVarLits, Var, Abc_Tt6Cofactor1(Truth, Var), fHash ); + if ( fHash ) + return Gia_ManHashMux( p, pVarLits[Var], Lit1, Lit0 ); + else + return Gia_ManAppendMux( p, pVarLits[Var], Lit1, Lit0 ); +} +void Gia_Truth6ToGiaTest( Gia_Man_t * p ) +{ + int Size = 5; + word Truth, TruthNew; + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManCiNum(p) ); + Vec_Int_t * vSupp = Vec_IntStart( 100 ); + int nCos = Gia_ManCoNum(p), Count = 0; + int i, k, Id, ObjId, iLitNew; + Gia_ManHashAlloc( p ); + Gia_ManForEachCoId( p, Id, i ) + { + Gia_ManCollectCis( p, &Id, 1, vSupp ); // ObjIds + if ( Vec_IntSize(vSupp) <= Size && i < nCos ) + { + int pVarLits[6]; + Vec_IntForEachEntry( vSupp, ObjId, k ) + { + int CioId = Gia_ObjCioId(Gia_ManObj(p, ObjId)); + Vec_IntWriteEntry( vMap, CioId, k ); + pVarLits[k] = Abc_Var2Lit( ObjId, 0 ); + } + Truth = Gia_LutComputeTruth6Map( p, i, vMap ); + if ( Size == 5 ) + iLitNew = Gia_Truth5ToGia( p, pVarLits, Vec_IntSize(vSupp), (unsigned)Truth, 1 ); + else + iLitNew = Gia_Truth6ToGia( p, pVarLits, Vec_IntSize(vSupp), Truth, 1 ); + Gia_ManAppendCo( p, iLitNew ); + TruthNew = Gia_LutComputeTruth6Map( p, Gia_ManCoNum(p)-1, vMap ); + Vec_IntForEachEntry( vSupp, ObjId, k ) + { + int CioId = Gia_ObjCioId(Gia_ManObj(p, ObjId)); + Vec_IntWriteEntry( vMap, CioId, -1 ); + } + if ( Truth != TruthNew ) + printf( "Error for output %d.\n", i ); + Count++; + //Dau_DsdPrintFromTruth( &Truth, Vec_IntSize(vSupp) ); + } + } + Gia_ManHashStop( p ); + printf( "Finished processing %d outputs.\n", Count ); + Vec_IntFree( vSupp ); + Vec_IntFree( vMap ); } /**Function************************************************************* diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h index 06769830..12061144 100644 --- a/src/aig/miniaig/miniaig.h +++ b/src/aig/miniaig/miniaig.h @@ -251,6 +251,64 @@ static int Mini_AigXor( Mini_Aig_t * p, int Lit0, int Lit1 ) return Mini_AigMux( p, Lit0, Mini_AigLitNot(Lit1), Lit1 ); } +static unsigned s_MiniTruths5[5] = { + 0xAAAAAAAA, + 0xCCCCCCCC, + 0xF0F0F0F0, + 0xFF00FF00, + 0xFFFF0000, +}; +static inline int Mini_AigTt5HasVar( unsigned t, int iVar ) +{ + return ((t << (1<<iVar)) & s_MiniTruths5[iVar]) != (t & s_MiniTruths5[iVar]); +} +static inline unsigned Mini_AigTt5Cofactor0( unsigned t, int iVar ) +{ + assert( iVar >= 0 && iVar < 6 ); + return (t & ~s_MiniTruths5[iVar]) | ((t & ~s_MiniTruths5[iVar]) << (1<<iVar)); +} +static inline unsigned Mini_AigTt5Cofactor1( unsigned t, int iVar ) +{ + assert( iVar >= 0 && iVar < 6 ); + return (t & s_MiniTruths5[iVar]) | ((t & s_MiniTruths5[iVar]) >> (1<<iVar)); +} +static inline int Mini_AigAndProp( Mini_Aig_t * p, int iLit0, int iLit1 ) +{ + if ( iLit0 < 2 ) + return iLit0 ? iLit1 : 0; + if ( iLit1 < 2 ) + return iLit1 ? iLit0 : 0; + if ( iLit0 == iLit1 ) + return iLit1; + if ( iLit0 == Mini_AigLitNot(iLit1) ) + return 0; + return Mini_AigAnd( p, iLit0, iLit1 ); +} +static inline int Mini_AigMuxProp( Mini_Aig_t * p, int iCtrl, int iData1, int iData0 ) +{ + int iTemp0 = Mini_AigAndProp( p, Mini_AigLitNot(iCtrl), iData0 ); + int iTemp1 = Mini_AigAndProp( p, iCtrl, iData1 ); + return Mini_AigLitNot( Mini_AigAndProp( p, Mini_AigLitNot(iTemp0), Mini_AigLitNot(iTemp1) ) ); +} +static inline int Mini_AigTruth( Mini_Aig_t * p, int * pVarLits, int nVars, unsigned Truth ) +{ + int Var, Lit0, Lit1; + if ( Truth == 0 ) + return 0; + if ( ~Truth == 0 ) + return 1; + assert( nVars > 0 ); + // find the topmost var + for ( Var = nVars-1; Var >= 0; Var-- ) + if ( Mini_AigTt5HasVar( Truth, Var ) ) + break; + assert( Var >= 0 ); + // cofactor + Lit0 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor0(Truth, Var) ); + Lit1 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor1(Truth, Var) ); + return Mini_AigMuxProp( p, pVarLits[Var], Lit1, Lit0 ); +} + // procedure to check the topological order during AIG construction static int Mini_AigCheck( Mini_Aig_t * p ) { diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 9323f9e7..b8934e23 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -650,14 +650,12 @@ Dec_Graph_t * Abc_ManResubQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, eNode0, eNode1; - assert( pObj0 != pObj1 ); - assert( !Abc_ObjIsComplement(pObj0) ); - assert( !Abc_ObjIsComplement(pObj1) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); pGraph = Dec_GraphCreate( 2 ); - Dec_GraphNode( pGraph, 0 )->pFunc = pObj0; - Dec_GraphNode( pGraph, 1 )->pFunc = pObj1; - eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase ); - eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase ); + Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); + Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) ); if ( fOrGate ) eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); else @@ -683,17 +681,16 @@ Dec_Graph_t * Abc_ManResubQuit21( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_ { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, eNode0, eNode1, eNode2; - assert( pObj0 != pObj1 ); - assert( !Abc_ObjIsComplement(pObj0) ); - assert( !Abc_ObjIsComplement(pObj1) ); - assert( !Abc_ObjIsComplement(pObj2) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) ); + assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) ); pGraph = Dec_GraphCreate( 3 ); - Dec_GraphNode( pGraph, 0 )->pFunc = pObj0; - Dec_GraphNode( pGraph, 1 )->pFunc = pObj1; - Dec_GraphNode( pGraph, 2 )->pFunc = pObj2; - eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase ); - eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase ); - eNode2 = Dec_EdgeCreate( 2, pObj2->fPhase ); + Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); + Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); + Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) ); + eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) ); + eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) ); if ( fOrGate ) { eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 ); @@ -725,15 +722,14 @@ Dec_Graph_t * Abc_ManResubQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, ePrev, eNode0, eNode1, eNode2; - assert( pObj0 != pObj1 ); - assert( pObj0 != pObj2 ); - assert( pObj1 != pObj2 ); - assert( !Abc_ObjIsComplement(pObj0) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) ); + assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) ); pGraph = Dec_GraphCreate( 3 ); Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2); - eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ); + eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) ); if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) { eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ); @@ -771,8 +767,8 @@ Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t { Dec_Graph_t * pGraph; Dec_Edge_t eRoot, ePrev0, ePrev1, eNode0, eNode1, eNode2, eNode3; - assert( pObj0 != pObj1 ); - assert( pObj2 != pObj3 ); + assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) ); + assert( Abc_ObjRegular(pObj2) != Abc_ObjRegular(pObj3) ); pGraph = Dec_GraphCreate( 4 ); Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0); Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1); @@ -840,6 +836,7 @@ Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t ***********************************************************************/ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) { + int fMoreDivs = 1; // bug fix by Siang-Yun Lee Abc_Obj_t * pObj; unsigned * puData, * puDataR; int i, w; @@ -863,6 +860,18 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs1UP, pObj ); continue; } + if ( fMoreDivs ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( ~puData[w] & ~puDataR[w] ) + if ( ~puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs1UP, Abc_ObjNot(pObj) ); + continue; + } + } // check negative containment for ( w = 0; w < p->nWords; w++ ) // if ( ~puData[w] & puDataR[w] ) @@ -873,6 +882,18 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs1UN, pObj ); continue; } + if ( fMoreDivs ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( puData[w] & puDataR[w] ) + if ( puData[w] & puDataR[w] & p->pCareSet[w] ) // care set + break; + if ( w == p->nWords ) + { + Vec_PtrPush( p->vDivs1UN, Abc_ObjNot(pObj) ); + continue; + } + } // add the node to binates Vec_PtrPush( p->vDivs1B, pObj ); } @@ -1081,14 +1102,38 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) // check positive unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | puData1[w]) != puDataR[w] ) - if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } if ( w == p->nWords ) { p->nUsedNode1Or++; @@ -1099,14 +1144,38 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & puData1[w]) != puDataR[w] ) - if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + if ( Abc_ObjIsComplement(pObj0) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((~puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } if ( w == p->nWords ) { p->nUsedNode1And++; @@ -1137,31 +1206,84 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) // check positive unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj2, j, k + 1 ) { - puData2 = (unsigned *)pObj2->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) - if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else assert( 0 ); if ( w == p->nWords ) { - LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) ); + LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) ); assert( LevelMax <= Required - 1 ); pObjMax = NULL; - if ( (int)pObj0->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax ) pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2; - if ( (int)pObj1->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2; } - if ( (int)pObj2->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1; @@ -1178,31 +1300,84 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 ) { - puData1 = (unsigned *)pObj1->pData; + puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj2, j, k + 1 ) { - puData2 = (unsigned *)pObj2->pData; - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) - if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; + if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((~puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else assert( 0 ); if ( w == p->nWords ) { - LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) ); + LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) ); assert( LevelMax <= Required - 1 ); pObjMax = NULL; - if ( (int)pObj0->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax ) pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2; - if ( (int)pObj1->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2; } - if ( (int)pObj2->Level == LevelMax ) + if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax ) { if ( pObjMax ) continue; pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1; @@ -1239,40 +1414,74 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) // check positive unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UP0, pObj1, k ) { pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, k ); puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; - if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj1) ) + if ( Abc_ObjIsComplement(pObj0) ) { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } - else + else { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } if ( w == p->nWords ) { @@ -1284,40 +1493,74 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i ) { - puData0 = (unsigned *)pObj0->pData; + puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData; Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj1, k ) { pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UN1, k ); puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData; puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData; - if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj1) ) + if ( Abc_ObjIsComplement(pObj0) ) { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; - } - else if ( Abc_ObjIsComplement(pObj2) ) - { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((~puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } - else + else { - for ( w = 0; w < p->nWords; w++ ) -// if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) - if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set - break; + if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj1) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else if ( Abc_ObjIsComplement(pObj2) ) + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } + else + { + for ( w = 0; w < p->nWords; w++ ) + // if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set + break; + } } if ( w == p->nWords ) { @@ -1472,6 +1715,7 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ) } } } + /* // check negative unate divisors Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj0, i ) @@ -1493,85 +1737,85 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ) { case 0: // 0000 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 1: // 0001 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 2: // 0010 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 3: // 0011 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 4: // 0100 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 5: // 0101 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 6: // 0110 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 7: // 0111 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 8: // 1000 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 9: // 1001 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 10: // 1010 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 11: // 1011 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 12: // 1100 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 13: // 1101 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 14: // 1110 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 15: // 1111 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index be099be4..922e0521 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -132,7 +132,7 @@ int Abc_RealMain( int argc, char * argv[] ) break; case 'm': { -#ifndef WIN32 +#if !defined(WIN32) && !defined(ABC_NO_RLIMIT) int maxMb = atoi(globalUtilOptarg); printf("Limiting memory use to %d MB\n", maxMb); struct rlimit limit = { @@ -144,7 +144,7 @@ int Abc_RealMain( int argc, char * argv[] ) break; } case 'l': { -#ifndef WIN32 +#if !defined(WIN32) && !defined(ABC_NO_RLIMIT) rlim_t maxTime = atoi(globalUtilOptarg); printf("Limiting time to %d seconds\n", (int)maxTime); struct rlimit limit = { |