summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2021-11-08 21:17:37 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2021-11-08 21:17:37 -0800
commit079a309a0d0bbe89eccfb64cdae55d1db73ca03a (patch)
tree979c02b5c81d79eabe850de25db7fb49f3ac2512 /src/proof
parent621d6355f475670cfdba5b685c65ee4dfd4207ea (diff)
downloadabc-079a309a0d0bbe89eccfb64cdae55d1db73ca03a.tar.gz
abc-079a309a0d0bbe89eccfb64cdae55d1db73ca03a.tar.bz2
abc-079a309a0d0bbe89eccfb64cdae55d1db73ca03a.zip
Bug fix in processing NDR.
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/acec/acecFadds.c30
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 ///
////////////////////////////////////////////////////////////////////////