diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-11-30 11:30:38 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-11-30 11:30:38 -0800 |
| commit | 329cee498196f8751f5ca111ed786e3fc1211c86 (patch) | |
| tree | a92135c674e65df92c5e25a58cef59899dae88c7 /src/proof | |
| parent | 5d61e53c7a09d544e4cdbb74e31fc919680f0e4e (diff) | |
| download | abc-329cee498196f8751f5ca111ed786e3fc1211c86.tar.gz abc-329cee498196f8751f5ca111ed786e3fc1211c86.tar.bz2 abc-329cee498196f8751f5ca111ed786e3fc1211c86.zip | |
Small changes in handling arithmetic logic.
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/acec/acecCo.c | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/proof/acec/acecCo.c b/src/proof/acec/acecCo.c index 000f530a..1b73c36f 100644 --- a/src/proof/acec/acecCo.c +++ b/src/proof/acec/acecCo.c @@ -44,11 +44,14 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ void Gia_PolynCoreNonXors_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj, Vec_Int_t * vXorPairs ) { + extern int Gia_ManSuppSizeOne( Gia_Man_t * p, Gia_Obj_t * pObj ); Gia_Obj_t * pFan0, * pFan1; if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) return; Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan0), vXorPairs ); Gia_PolynCoreNonXors_rec( pGia, Gia_Regular(pFan1), vXorPairs ); + //if ( Gia_ManSuppSizeOne(pGia, pObj) > 4 ) + //if ( Gia_ObjId(pGia, pObj) >= 73 ) Vec_IntPushTwo( vXorPairs, Gia_ObjId(pGia, Gia_Regular(pFan0)), Gia_ObjId(pGia, Gia_Regular(pFan1)) ); } Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia ) @@ -95,7 +98,7 @@ Vec_Int_t * Gia_PolynCoreOrder( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t * Vec_Int_t * vLeaves = Vec_IntAlloc( 2 * Gia_ManCiNum(pGia) ); Vec_Wec_t * vMap = Vec_WecStart( Gia_ManObjNum(pGia) ); int i, k, Index, Driver, Entry1, Entry2 = -1; - // nodes driven by adders into adder indexes + // map nodes driven by adders into adder indexes for ( i = 0; 5*i < Vec_IntSize(vAdds); i++ ) { Entry1 = Vec_IntEntry( vAdds, 5*i + 3 ); @@ -318,8 +321,11 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos, Vec_Int_t * vAdds = Ree_ManComputeCuts( pGia, 1 ); Vec_Int_t * vLeaves, * vRoots, * vOrder = Gia_PolynCoreOrder( pGia, vAdds, vAddCos, &vLeaves, &vRoots ); Vec_Int_t * vNodes = Gia_PolynCoreCollect( pGia, vAdds, vOrder ); + + //Gia_ManShow( pGia, vNodes, 0 ); + printf( "Detected %d FAs/HAs. Roots = %d. Leaves = %d. Nodes = %d. Adds = %d. ", - Vec_IntSize(vAdds), Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) ); + Vec_IntSize(vAdds)/5, Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose ); |