summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2016-11-30 11:30:38 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2016-11-30 11:30:38 -0800
commit329cee498196f8751f5ca111ed786e3fc1211c86 (patch)
treea92135c674e65df92c5e25a58cef59899dae88c7 /src/proof
parent5d61e53c7a09d544e4cdbb74e31fc919680f0e4e (diff)
downloadabc-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.c10
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 );