From 2377ae60e99fd751021cbcac880b584d57c284a1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 19 Feb 2012 14:52:43 -0800 Subject: Isomorphism checking code. --- src/aig/gia/giaDup.c | 2 +- src/aig/gia/giaIso.c | 145 ++++++++++++++++++++++++++++++++++++++++++++--- src/aig/saig/saigIso.c | 15 +++-- src/base/abci/abc.c | 58 ++++++++++++++++++- src/base/abci/abcSweep.c | 2 +- src/proof/ssw/sswSemi.c | 2 +- 6 files changed, 202 insertions(+), 22 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 342332cd..577a0180 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1762,7 +1762,7 @@ void Gia_ManDupCones_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vLeaves, Gia_ManDupCones_rec( p, Gia_ObjFanin1(pObj), vLeaves, vNodes, vRoots ); Vec_PtrPush( vNodes, pObj ); } - else if ( Gia_ObjIsPo(p, pObj) ) + else if ( Gia_ObjIsCo(pObj) ) Gia_ManDupCones_rec( p, Gia_ObjFanin0(pObj), vLeaves, vNodes, vRoots ); else if ( Gia_ObjIsRo(p, pObj) ) Vec_PtrPush( vRoots, Gia_ObjRoToRi(p, pObj) ); diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c index 3ff8ee2f..71733ee9 100644 --- a/src/aig/gia/giaIso.c +++ b/src/aig/gia/giaIso.c @@ -21,7 +21,7 @@ #include "gia.h" ABC_NAMESPACE_IMPL_START - + #define ISO_MASK 0xFF static int s_256Primes[ISO_MASK+1] = @@ -458,11 +458,68 @@ void Gia_IsoSort( Gia_IsoMan_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_IsoTest( Gia_Man_t * pGia ) +Vec_Ptr_t * Gia_IsoCollectCos( Gia_IsoMan_t * p, int fVerbose ) +{ + Vec_Ptr_t * vGroups; + Vec_Int_t * vLevel; + Gia_Obj_t * pObj; + int i, k, iBegin, nSize; + + // add singletons + vGroups = Vec_PtrAlloc( 1000 ); + Gia_ManForEachPo( p->pGia, pObj, i ) + if ( p->pUniques[Gia_ObjId(p->pGia, pObj)] > 0 ) + { + vLevel = Vec_IntAlloc( 1 ); + Vec_IntPush( vLevel, i ); + Vec_PtrPush( vGroups, vLevel ); + } + + // add groups + Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i ) + { + for ( k = 0; k < nSize; k++ ) + { + pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) ); + if ( Gia_ObjIsPo(p->pGia, pObj) ) + break; + } + if ( k == nSize ) + continue; + vLevel = Vec_IntAlloc( 8 ); + for ( k = 0; k < nSize; k++ ) + { + pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) ); + if ( Gia_ObjIsPo(p->pGia, pObj) ) + Vec_IntPush( vLevel, Gia_ObjCioId(pObj) ); + } + Vec_PtrPush( vGroups, vLevel ); + } + // canonicize order + Vec_PtrForEachEntry( Vec_Int_t *, vGroups, vLevel, i ) + Vec_IntSort( vLevel, 0 ); + Vec_VecSortByFirstInt( (Vec_Vec_t *)vGroups, 0 ); +// Vec_VecFree( (Vec_Vec_t *)vGroups ); +// return NULL; + return vGroups; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fVerbose ) { - int fVerbose = 1; - int nIterMax = 50; + Vec_Ptr_t * vEquivs; Gia_IsoMan_t * p; + int nIterMax = 1000; int i, clk = clock(), clkTotal = clock(); Gia_ManCleanValue( pGia ); @@ -470,9 +527,9 @@ void Gia_IsoTest( Gia_Man_t * pGia ) Gia_IsoPrepare( p ); Gia_IsoAssignUnique( p ); p->timeStart = clock() - clk; - // Gia_IsoPrintClasses( p ); - Gia_IsoPrint( p, 0, clock() - clkTotal ); + if ( fVerbose ) + Gia_IsoPrint( p, 0, clock() - clkTotal ); for ( i = 0; i < nIterMax; i++ ) { clk = clock(); @@ -484,11 +541,11 @@ void Gia_IsoTest( Gia_Man_t * pGia ) p->timeRefine += clock() - clk; // Gia_IsoPrintClasses( p ); - Gia_IsoPrint( p, i+1, clock() - clkTotal ); + if ( fVerbose ) + Gia_IsoPrint( p, i+1, clock() - clkTotal ); if ( p->nSingles == 0 ) break; } - if ( fVerbose ) { p->timeTotal = clock() - clkTotal; @@ -501,11 +558,81 @@ void Gia_IsoTest( Gia_Man_t * pGia ) ABC_PRTP( "Other ", p->timeOther, p->timeTotal ); ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); } - + vEquivs = Gia_IsoCollectCos( p, fVerbose ); Gia_IsoManStop( p ); + return vEquivs; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose ) +{ + Gia_Man_t * pPart; + Vec_Ptr_t * vEquivs; + Vec_Int_t * vRemain, * vLevel; + int i, clk = clock(); + // create equivalences + vEquivs = Gia_IsoDeriveEquivPos( pGia, fVerbose ); + // collect the first ones + vRemain = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i ) + Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) ); + // derive the resulting AIG + pPart = Gia_ManDupCones( pGia, Vec_IntArray(vRemain), Vec_IntSize(vRemain) ); + Vec_IntFree( vRemain ); + // report the results + printf( "Reduced %d outputs to %d outputs. ", Gia_ManPoNum(pGia), Gia_ManPoNum(pPart) ); + Abc_PrintTime( 1, "Time", clock() - clk ); + if ( fVerbose ) + { + printf( "Nontrivial classes:\n" ); + Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 ); + } + if ( pvPosEquivs ) + *pvPosEquivs = vEquivs; + else + Vec_VecFree( (Vec_Vec_t *)vEquivs ); +// Gia_ManStopP( &pPart ); + return pPart; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_IsoTest( Gia_Man_t * pGia, int fVerbose ) +{ + Vec_Ptr_t * vEquivs; + int clk = clock(); + vEquivs = Gia_IsoDeriveEquivPos( pGia, fVerbose ); + printf( "Reduced %d outputs to %d. ", Gia_ManPoNum(pGia), Vec_PtrSize(vEquivs) ); + Abc_PrintTime( 1, "Time", clock() - clk ); + if ( fVerbose ) + { + printf( "Nontrivial classes:\n" ); + Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 ); + } + Vec_VecFree( (Vec_Vec_t *)vEquivs ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c index 95d0cdae..c3d1af9d 100644 --- a/src/aig/saig/saigIso.c +++ b/src/aig/saig/saigIso.c @@ -428,6 +428,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV Vec_Str_t * vStr, * vPrev; int i, nPos, nUnique = 0, clk = clock(); int clkDup = 0, clkAig = 0, clkIso = 0, clk2; + *pvPosEquivs = NULL; // derive AIG for each PO nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); @@ -521,13 +522,6 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV // return (Vec_Vec_t *)vClasses; // Vec_VecFree( (Vec_Vec_t *)vClasses ); *pvPosEquivs = vClasses; - if ( fVerbose && vClasses ) - { - printf( "Non-trivial equivalence clases of primary outputs:\n" ); - Vec_VecPrintInt( (Vec_Vec_t *)vClasses, 1 ); - } - -// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter ); return pPart; } @@ -570,7 +564,12 @@ Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int f pPart = Iso_ManFilterPos( pAig, pvPosEquivs, fVerbose ); printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) ); Abc_PrintTime( 1, "Time", clock() - clk ); -// Aig_ManStop( pPart ); + if ( fVerbose && *pvPosEquivs ) + { + printf( "Nontrivial classes:\n" ); + Vec_VecPrintInt( (Vec_Vec_t *)*pvPosEquivs, 1 ); + } +// Aig_ManStopP( &pPart ); return pPart; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 15e314db..c9640db0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -352,6 +352,7 @@ static int Abc_CommandAbc9ReachP ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9ReachN ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReachY ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Undo ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -782,6 +783,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&reachn", Abc_CommandAbc9ReachN, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reachy", Abc_CommandAbc9ReachY, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&undo", Abc_CommandAbc9Undo, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); Cmd_CommandAdd( pAbc, "Liveness", "l2s", Abc_CommandAbcLivenessToSafety, 0 ); @@ -27824,6 +27826,58 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose ); + + Gia_Man_t * pAig; + Vec_Ptr_t * vPosEquivs; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Iso(): There is no AIG.\n" ); + return 1; + } + pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, fVerbose ); + // update the internal storage of PO equivalences + Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs ); + // update the AIG + Abc_CommandUpdate9( pAbc, pAig ); + return 0; + +usage: + Abc_Print( -2, "usage: &iso [-vh]\n" ); + Abc_Print( -2, "\t removes POs with isomorphic sequential COI\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -27843,7 +27897,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern Gia_Man_t * Gia_VtaTest( Gia_Man_t * p ); // extern int Gia_ManSuppSizeTest( Gia_Man_t * p ); // extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose ); - extern void Gia_IsoTest( Gia_Man_t * p ); + extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -27882,7 +27936,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ManSuppSizeTest( pAbc->pGia ); // Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 ); - Gia_IsoTest( pAbc->pGia ); + Gia_IsoTest( pAbc->pGia, fVerbose ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index a898f26c..a5649794 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -177,7 +177,7 @@ void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [Collects equivalence classses of node in the network.] + Synopsis [Collects equivalence classes of node in the network.] Description [] diff --git a/src/proof/ssw/sswSemi.c b/src/proof/ssw/sswSemi.c index 74305adf..ec50ab50 100644 --- a/src/proof/ssw/sswSemi.c +++ b/src/proof/ssw/sswSemi.c @@ -6,7 +6,7 @@ PackageName [Inductive prover with constraints.] - Synopsis [Semiformal for equivalence clases.] + Synopsis [Semiformal for equivalence classes.] Author [Alan Mishchenko] -- cgit v1.2.3