diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/acec/acecFadds.c | 30 |
1 files changed, 23 insertions, 7 deletions
diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c index d55eefe2..a2bdcfbe 100644 --- a/src/proof/acec/acecFadds.c +++ b/src/proof/acec/acecFadds.c @@ -314,16 +314,21 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I if ( Type == 0 ) continue; vTemp = Type == 1 ? vCutsXor : vCutsMaj; - if ( fVerbose ) - printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" ); - for ( c = 1; c <= pCut[0]; c++ ) + if ( 0 && Type == 2 ) { + fVerbose = 1; + if ( fVerbose ) + printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" ); + for ( c = 1; c <= pCut[0]; c++ ) + { + if ( fVerbose ) + printf( " %d", pCut[c] ); + Vec_IntPush( vTemp, pCut[c] ); + } if ( fVerbose ) - printf( " %d", pCut[c] ); - Vec_IntPush( vTemp, pCut[c] ); + printf( " )\n" ); + fVerbose = 0; } - if ( fVerbose ) - printf( " )\n" ); Vec_IntPush( vTemp, iObj ); } } @@ -450,6 +455,16 @@ Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** p Vec_IntFree( vCutsMaj ); return vFadds; } +void Gia_ManDetectFullAdders2( Gia_Man_t * p, int fVerbose ) +{ + Vec_Int_t * vCutsXor2, * vCutsXor, * vCutsMaj; + Dtc_ManComputeCuts( p, &vCutsXor2, &vCutsXor, &vCutsMaj, fVerbose ); + if ( fVerbose ) + printf( "XOR3 cuts = %d. MAJ cuts = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4 ); + Vec_IntFree( vCutsXor2 ); + Vec_IntFree( vCutsXor ); + Vec_IntFree( vCutsMaj ); +} /**Function************************************************************* @@ -1238,6 +1253,7 @@ Gia_Man_t * Gia_ManDupWithArtificialBoxes( Gia_Man_t * p, int DelayC, int nPathM return pNew; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |