/**CFile****************************************************************
FileName [giaIso.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Graph isomorphism.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
#define ISO_MASK 0xFF
static int s_256Primes[ISO_MASK+1] =
{
0x984b6ad9,0x18a6eed3,0x950353e2,0x6222f6eb,0xdfbedd47,0xef0f9023,0xac932a26,0x590eaf55,
0x97d0a034,0xdc36cd2e,0x22736b37,0xdc9066b0,0x2eb2f98b,0x5d9c7baf,0x85747c9e,0x8aca1055,
0x50d66b74,0x2f01ae9e,0xa1a80123,0x3e1ce2dc,0xebedbc57,0x4e68bc34,0x855ee0cf,0x17275120,
0x2ae7f2df,0xf71039eb,0x7c283eec,0x70cd1137,0x7cf651f3,0xa87bfa7a,0x14d87f02,0xe82e197d,
0x8d8a5ebe,0x1e6a15dc,0x197d49db,0x5bab9c89,0x4b55dea7,0x55dede49,0x9a6a8080,0xe5e51035,
0xe148d658,0x8a17eb3b,0xe22e4b38,0xe5be2a9a,0xbe938cbb,0x3b981069,0x7f9c0c8e,0xf756df10,
0x8fa783f7,0x252062ce,0x3dc46b4b,0xf70f6432,0x3f378276,0x44b137a1,0x2bf74b77,0x04892ed6,
0xfd318de1,0xd58c235e,0x94c6d25b,0x7aa5f218,0x35c9e921,0x5732fbbb,0x06026481,0xf584a44f,
0x946e1b5f,0x8463d5b2,0x4ebca7b2,0x54887b15,0x08d1e804,0x5b22067d,0x794580f6,0xb351ea43,
0xbce555b9,0x19ae2194,0xd32f1396,0x6fc1a7f1,0x1fd8a867,0x3a89fdb0,0xea49c61c,0x25f8a879,
0xde1e6437,0x7c74afca,0x8ba63e50,0xb1572074,0xe4655092,0xdb6f8b1c,0xc2955f3c,0x327f85ba,
0x60a17021,0x95bd261d,0xdea94f28,0x04528b65,0xbe0109cc,0x26dd5688,0x6ab2729d,0xc4f029ce,
0xacf7a0be,0x4c912f55,0x34c06e65,0x4fbb938e,0x1533fb5f,0x03da06bd,0x48262889,0xc2523d7d,
0x28a71d57,0x89f9713a,0xf574c551,0x7a99deb5,0x52834d91,0x5a6f4484,0xc67ba946,0x13ae698f,
0x3e390f34,0x34fc9593,0x894c7932,0x6cf414a3,0xdb7928ab,0x13a3b8a3,0x4b381c1d,0xa10b54cb,
0x55359d9d,0x35a3422a,0x58d1b551,0x0fd4de20,0x199eb3f4,0x167e09e2,0x3ee6a956,0x5371a7fa,
0xd424efda,0x74f521c5,0xcb899ff6,0x4a42e4f4,0x747917b6,0x4b08df0b,0x090c7a39,0x11e909e4,
0x258e2e32,0xd9fad92d,0x48fe5f69,0x0545cde6,0x55937b37,0x9b4ae4e4,0x1332b40e,0xc3792351,
0xaff982ef,0x4dba132a,0x38b81ef1,0x28e641bf,0x227208c1,0xec4bbe37,0xc4e1821c,0x512c9d09,
0xdaef1257,0xb63e7784,0x043e04d7,0x9c2cea47,0x45a0e59a,0x281315ca,0x849f0aac,0xa4071ed3,
0x0ef707b3,0xfe8dac02,0x12173864,0x471f6d46,0x24a53c0a,0x35ab9265,0xbbf77406,0xa2144e79,
0xb39a884a,0x0baf5b6d,0xcccee3dd,0x12c77584,0x2907325b,0xfd1adcd2,0xd16ee972,0x345ad6c1,
0x315ebe66,0xc7ad2b8d,0x99e82c8d,0xe52da8c8,0xba50f1d3,0x66689cd8,0x2e8e9138,0x43e15e74,
0xf1ced14d,0x188ec52a,0xe0ef3cbb,0xa958aedc,0x4107a1bc,0x5a9e7a3e,0x3bde939f,0xb5b28d5a,
0x596fe848,0xe85ad00c,0x0b6b3aae,0x44503086,0x25b5695c,0xc0c31dcd,0x5ee617f0,0x74d40c3a,
0xd2cb2b9f,0x1e19f5fa,0x81e24faf,0xa01ed68f,0xcee172fc,0x7fdf2e4d,0x002f4774,0x664f82dd,
0xc569c39a,0xa2d4dcbe,0xaadea306,0xa4c947bf,0xa413e4e3,0x81fb5486,0x8a404970,0x752c980c,
0x98d1d881,0x5c932c1e,0xeee65dfb,0x37592cdd,0x0fd4e65b,0xad1d383f,0x62a1452f,0x8872f68d,
0xb58c919b,0x345c8ee3,0xb583a6d6,0x43d72cb3,0x77aaa0aa,0xeb508242,0xf2db64f8,0x86294328,
0x82211731,0x1239a9d5,0x673ba5de,0xaf4af007,0x44203b19,0x2399d955,0xa175cd12,0x595928a7,
0x6918928b,0xde3126bb,0x6c99835c,0x63ba1fa2,0xdebbdff0,0x3d02e541,0xd6f7aac6,0xe80b4cd0,
0xd0fa29f1,0x804cac5e,0x2c226798,0x462f624c,0xad05b377,0x22924fcd,0xfbea205c,0x1b47586d
};
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Gia_IsoMan_t_ Gia_IsoMan_t;
struct Gia_IsoMan_t_
{
Gia_Man_t * pGia;
int nObjs;
int nUniques;
int nSingles;
int nEntries;
// internal data
int * pLevels;
int * pUniques;
word * pStoreW;
unsigned * pStoreU;
// equivalence classes
Vec_Int_t * vLevCounts;
Vec_Int_t * vClasses;
Vec_Int_t * vClasses2;
// statistics
abctime timeStart;
abctime timeSim;
abctime timeRefine;
abctime timeSort;
abctime timeOther;
abctime timeTotal;
};
static inline unsigned Gia_IsoGetValue( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i]); }
static inline unsigned Gia_IsoGetItem( Gia_IsoMan_t * p, int i ) { return (unsigned)(p->pStoreW[i] >> 32); }
static inline void Gia_IsoSetValue( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[0] = v; }
static inline void Gia_IsoSetItem( Gia_IsoMan_t * p, int i, unsigned v ) { ((unsigned *)(p->pStoreW + i))[1] = v; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_IsoMan_t * Gia_IsoManStart( Gia_Man_t * pGia )
{
Gia_IsoMan_t * p;
p = ABC_CALLOC( Gia_IsoMan_t, 1 );
p->pGia = pGia;
p->nObjs = Gia_ManObjNum( pGia );
p->nUniques = 1;
p->nEntries = p->nObjs;
// internal data
p->pLevels = ABC_CALLOC( int, p->nObjs );
p->pUniques = ABC_CALLOC( int, p->nObjs );
p->pStoreW = ABC_CALLOC( word, p->nObjs );
// class representation
p->vClasses = Vec_IntAlloc( p->nObjs/4 );
p->vClasses2 = Vec_IntAlloc( p->nObjs/4 );
return p;
}
void Gia_IsoManStop( Gia_IsoMan_t * p )
{
// class representation
Vec_IntFree( p->vClasses );
Vec_IntFree( p->vClasses2 );
// internal data
ABC_FREE( p->pLevels );
ABC_FREE( p->pUniques );
ABC_FREE( p->pStoreW );
ABC_FREE( p );
}
void Gia_IsoManTransferUnique( Gia_IsoMan_t * p )
{
Gia_Obj_t * pObj;
int i;
// copy unique numbers into the nodes
Gia_ManForEachObj( p->pGia, pObj, i )
pObj->Value = p->pUniques[i];
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_IsoPrintClasses( Gia_IsoMan_t * p )
{
int fVerbose = 0;
int i, k, iBegin, nSize;
printf( "The total of %d classes:\n", Vec_IntSize(p->vClasses)/2 );
Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
{
printf( "%5d : (%3d,%3d) ", i/2, iBegin, nSize );
if ( fVerbose )
{
printf( "{" );
for ( k = 0; k < nSize; k++ )
printf( " %3d,%08x", Gia_IsoGetItem(p, iBegin+k), Gia_IsoGetValue(p, iBegin+k) );
printf( " }" );
}
printf( "\n" );
}
}
void Gia_IsoPrint( Gia_IsoMan_t * p, int Iter, abctime Time )
{
printf( "Iter %4d : ", Iter );
printf( "Entries =%8d. ", p->nEntries );
// printf( "Classes =%8d. ", Vec_IntSize(p->vClasses)/2 );
printf( "Uniques =%8d. ", p->nUniques );
printf( "Singles =%8d. ", p->nSingles );
printf( "%9.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) );
printf( "\n" );
fflush( stdout );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_IsoPrepare( Gia_IsoMan_t * p )
{
Gia_Obj_t * pObj;
int * pLevBegins, * pLevSizes;
int i, iObj, MaxLev = 0;
// assign levels
p->pLevels[0] = 0;
Gia_ManForEachCi( p->pGia, pObj, i )
p->pLevels[Gia_ObjId(p->pGia, pObj)] = 0;
Gia_ManForEachAnd( p->pGia, pObj, i )
p->pLevels[i] = 1 + Abc_MaxInt( p->pLevels[Gia_ObjFaninId0(pObj, i)], p->pLevels[Gia_ObjFaninId1(pObj, i)] );
Gia_ManForEachCo( p->pGia, pObj, i )
{
iObj = Gia_ObjId(p->pGia, pObj);
p->pLevels[iObj] = 1 + p->pLevels[Gia_ObjFaninId0(pObj, iObj)]; // "1 +" is different!
MaxLev = Abc_MaxInt( MaxLev, p->pLevels[Gia_ObjId(p->pGia, pObj)] );
}
// count nodes on each level
pLevSizes = ABC_CALLOC( int, MaxLev+1 );
for ( i = 1; i < p->nObjs; i++ )
pLevSizes[p->pLevels[i]]++;
// start classes
Vec_IntClear( p->vClasses );
Vec_IntPush( p->vClasses, 0 );
Vec_IntPush( p->vClasses, 1 );
// find beginning of each level
pLevBegins = ABC_CALLOC( int, MaxLev+2 );
pLevBegins[0] = 1;
for ( i = 0; i <= MaxLev; i++ )
{
assert( pLevSizes[i] > 0 ); // we do not allow AIG with a const node and no PIs
Vec_IntPush( p->vClasses, pLevBegins[i] );
Vec_IntPush( p->vClasses, pLevSizes[i] );
pLevBegins[i+1] = pLevBegins[i] + pLevSizes[i];
}
assert( pLevBegins[MaxLev+1] == p->nObjs );
// put them into the structure
for ( i = 1; i < p->nObjs; i++ )
Gia_IsoSetItem( p, pLevBegins[p->pLevels[i]]++, i );
ABC_FREE( pLevBegins );
ABC_FREE( pLevSizes );
/*
// print the results
for ( i = 0; i < p->nObjs; i++ )
printf( "%3d : (%d,%d)\n", i, Gia_IsoGetItem(p, i), Gia_IsoGetValue(p, i) );
printf( "\n" );
*/
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_IsoAssignUnique( Gia_IsoMan_t * p )
{
int i, iBegin, nSize;
p->nSingles = 0;
Vec_IntClear( p->vClasses2 );
Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
{
if ( nSize == 1 )
{
assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
p->nSingles++;
}
else
{
Vec_IntPush( p->vClasses2, iBegin );
Vec_IntPush( p->vClasses2, nSize );
}
}
ABC_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 );
p->nEntries -= p->nSingles;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_IsoSort( Gia_IsoMan_t * p )
{
Gia_Obj_t * pObj, * pObj0;
int i, k, fSameValue, iBegin, iBeginOld, nSize, nSizeNew;
int fRefined = 0;
abctime clk;
// go through the equiv classes
p->nSingles = 0;
Vec_IntClear( p->vClasses2 );
Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
{
assert( nSize > 1 );
fSameValue = 1;
pObj0 = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin) );
for ( k = 0; k < nSize; k++ )
{
pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
Gia_IsoSetValue( p, iBegin+k, pObj->Value );
if ( pObj->Value != pObj0->Value )
fSameValue = 0;
}
if ( fSameValue )
{
Vec_IntPush( p->vClasses2, iBegin );
Vec_IntPush( p->vClasses2, nSize );
continue;
}
fRefined = 1;
// sort objects
clk = Abc_Clock();
Abc_QuickSort3( p->pStoreW + iBegin, nSize, 0 );
p->timeSort += Abc_Clock() - clk;
// divide into new classes
iBeginOld = iBegin;
pObj0 = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin) );
for ( k = 1; k < nSize; k++ )
{
pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p,iBegin+k) );
if ( pObj0->Value == pObj->Value )
continue;
nSizeNew = iBegin + k - iBeginOld;
if ( nSizeNew == 1 )
{
assert( p->pUniques[Gia_IsoGetItem(p, iBeginOld)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBeginOld)] = p->nUniques++;
p->nSingles++;
}
else
{
Vec_IntPush( p->vClasses2, iBeginOld );
Vec_IntPush( p->vClasses2, nSizeNew );
}
iBeginOld = iBegin + k;
pObj0 = pObj;
}
// add the last one
nSizeNew = iBegin + k - iBeginOld;
if ( nSizeNew == 1 )
{
assert( p->pUniques[Gia_IsoGetItem(p, iBeginOld)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBeginOld)] = p->nUniques++;
p->nSingles++;
}
else
{
Vec_IntPush( p->vClasses2, iBeginOld );
Vec_IntPush( p->vClasses2, nSizeNew );
}
}
ABC_SWAP( Vec_Int_t *, p->vClasses, p->vClasses2 );
p->nEntries -= p->nSingles;
return fRefined;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_IsoCollectCosClasses( 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 []
***********************************************************************/
static inline unsigned Gia_IsoUpdateValue( int Value, int fCompl )
{
return (Value+1) * s_256Primes[Abc_Var2Lit(Value, fCompl) & ISO_MASK];
}
static inline unsigned Gia_IsoUpdate( Gia_IsoMan_t * p, int Iter, int iObj, int fCompl )
{
if ( Iter == 0 ) return Gia_IsoUpdateValue( p->pLevels[iObj], fCompl );
if ( p->pUniques[iObj] > 0 ) return Gia_IsoUpdateValue( p->pUniques[iObj], fCompl );
// if ( p->pUniques[iObj] > 0 ) return Gia_IsoUpdateValue( 11, fCompl );
return 0;
}
void Gia_IsoSimulate( Gia_IsoMan_t * p, int Iter )
{
Gia_Obj_t * pObj, * pObjF;
int i, iObj;
// initialize constant, inputs, and flops in the first frame
Gia_ManConst0(p->pGia)->Value += s_256Primes[ISO_MASK];
Gia_ManForEachPi( p->pGia, pObj, i )
pObj->Value += s_256Primes[ISO_MASK-1];
if ( Iter == 0 )
Gia_ManForEachRo( p->pGia, pObj, i )
pObj->Value += s_256Primes[ISO_MASK-2];
// simulate nodes
Gia_ManForEachAnd( p->pGia, pObj, i )
{
pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, i), Gia_ObjFaninC0(pObj));
pObj->Value += Gia_ObjFanin1(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId1(pObj, i), Gia_ObjFaninC1(pObj));
}
// simulate COs
Gia_ManForEachCo( p->pGia, pObj, i )
{
iObj = Gia_ObjId(p->pGia, pObj);
pObj->Value += Gia_ObjFanin0(pObj)->Value + Gia_IsoUpdate(p, Iter, Gia_ObjFaninId0(pObj, iObj), Gia_ObjFaninC0(pObj));
}
// transfer flop values
Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i )
pObj->Value += pObjF->Value;
}
void Gia_IsoSimulateBack( Gia_IsoMan_t * p, int Iter )
{
Gia_Obj_t * pObj, * pObjF;
int i, iObj;
// simulate COs
Gia_ManForEachCo( p->pGia, pObj, i )
{
iObj = Gia_ObjId(p->pGia, pObj);
Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, iObj, Gia_ObjFaninC0(pObj));
}
// simulate objects
Gia_ManForEachAndReverse( p->pGia, pObj, i )
{
Gia_ObjFanin0(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC0(pObj));
Gia_ObjFanin1(pObj)->Value += pObj->Value + Gia_IsoUpdate(p, Iter, i, Gia_ObjFaninC1(pObj));
}
// transfer flop values
Gia_ManForEachRiRo( p->pGia, pObjF, pObj, i )
pObjF->Value += pObj->Value;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_IsoAssignOneClass2( Gia_IsoMan_t * p )
{
int i, iBegin = -1, nSize = -1;
// find two variable class
assert( Vec_IntSize(p->vClasses) > 0 );
Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
{
if ( nSize == 2 )
break;
}
assert( nSize > 1 );
if ( nSize == 2 )
{
assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
p->nSingles++;
p->nEntries--;
assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++;
p->nSingles++;
p->nEntries--;
}
else
{
assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
p->nSingles++;
p->nEntries--;
}
for ( ; i < Vec_IntSize(p->vClasses) - 2; i += 2 )
{
p->vClasses->pArray[i+0] = p->vClasses->pArray[i+2];
p->vClasses->pArray[i+1] = p->vClasses->pArray[i+3];
}
Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
printf( "Broke ties in class %d of size %d at level %d.\n", i/2, nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
}
void Gia_IsoAssignOneClass3( Gia_IsoMan_t * p )
{
int iBegin, nSize;
// find the last class
assert( Vec_IntSize(p->vClasses) > 0 );
iBegin = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
nSize = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 1 );
Vec_IntShrink( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
// assign the class
assert( nSize > 1 );
if ( nSize == 2 )
{
assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
p->nSingles++;
p->nEntries--;
assert( p->pUniques[Gia_IsoGetItem(p, iBegin+1)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin+1)] = p->nUniques++;
p->nSingles++;
p->nEntries--;
}
else
{
assert( p->pUniques[Gia_IsoGetItem(p, iBegin)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin)] = p->nUniques++;
p->nSingles++;
p->nEntries--;
}
printf( "Broke ties in last class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
}
void Gia_IsoAssignOneClass( Gia_IsoMan_t * p, int fVerbose )
{
int i, k, iBegin0, iBegin, nSize, Shrink;
// find the classes with the highest level
assert( Vec_IntSize(p->vClasses) > 0 );
iBegin0 = Vec_IntEntry( p->vClasses, Vec_IntSize(p->vClasses) - 2 );
for ( i = Vec_IntSize(p->vClasses) - 2; i >= 0; i -= 2 )
{
iBegin = Vec_IntEntry( p->vClasses, i );
if ( p->pLevels[Gia_IsoGetItem(p, iBegin)] != p->pLevels[Gia_IsoGetItem(p, iBegin0)] )
break;
}
i += 2;
assert( i >= 0 );
// assign all classes starting with this one
for ( Shrink = i; i < Vec_IntSize(p->vClasses); i += 2 )
{
iBegin = Vec_IntEntry( p->vClasses, i );
nSize = Vec_IntEntry( p->vClasses, i + 1 );
for ( k = 0; k < nSize; k++ )
{
assert( p->pUniques[Gia_IsoGetItem(p, iBegin+k)] == 0 );
p->pUniques[Gia_IsoGetItem(p, iBegin+k)] = p->nUniques++;
// Gia_ManObj(p->pGia, Gia_IsoGetItem(p, iBegin+k))->Value += s_256Primes[0]; /// new addition!!!
p->nSingles++;
p->nEntries--;
}
if ( fVerbose )
printf( "Broke ties in class of size %d at level %d.\n", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
}
Vec_IntShrink( p->vClasses, Shrink );
}
/**Function*************************************************************
Synopsis [Report topmost equiv nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_IsoReportTopmost( Gia_IsoMan_t * p )
{
Gia_Obj_t * pObj;
int i, k, iBegin, nSize, Counter = 0;
// go through equivalence classes
Gia_ManIncrementTravId( p->pGia );
Vec_IntForEachEntryDouble( p->vClasses, iBegin, nSize, i )
{
// printf( "%d(%d) ", nSize, p->pLevels[Gia_IsoGetItem(p, iBegin)] );
for ( k = 0; k < nSize; k++ )
{
pObj = Gia_ManObj( p->pGia, Gia_IsoGetItem(p, iBegin+k) );
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin0(pObj) );
Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin1(pObj) );
}
else if ( Gia_ObjIsRo(p->pGia, pObj) )
Gia_ObjSetTravIdCurrent( p->pGia, Gia_ObjFanin0(Gia_ObjRoToRi(p->pGia, pObj)) );
}
}
// printf( "\n" );
// report non-labeled nodes
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_ObjIsTravIdCurrent(p->pGia, pObj) )
{
printf( "%5d : ", ++Counter );
printf( "Obj %6d : Level = %4d. iBegin = %4d. Size = %4d.\n",
Gia_ObjId(p->pGia, pObj), p->pLevels[Gia_ObjId(p->pGia, pObj)], iBegin, nSize );
break;
}
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_IsoRecognizeMuxes( Gia_Man_t * pGia )
{
Gia_Obj_t * pObj, * pObjC, * pObj1, * pObj0;
int i;
Gia_ManForEachAnd( pGia, pObj, i )
{
if ( !Gia_ObjIsMuxType(pObj) )
continue;
pObjC = Gia_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
if ( Gia_Regular(pObj0) == Gia_Regular(pObj1) )
{
// this is XOR
Gia_Regular(pObj)->Value += s_256Primes[233];
Gia_Regular(pObjC)->Value += s_256Primes[234];
Gia_Regular(pObj0)->Value += s_256Primes[234];
}
else
{
// this is MUX
Gia_Regular(pObj)->Value += s_256Primes[235];
Gia_Regular(pObjC)->Value += s_256Primes[236];
Gia_Regular(pObj0)->Value += s_256Primes[237];
Gia_Regular(pObj1)->Value += s_256Primes[237];
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_IsoDeriveEquivPos( Gia_Man_t * pGia, int fForward, int fVerbose )
{
int nIterMax = 10000;
int nFixedPoint = 1;
Gia_IsoMan_t * p;
Vec_Ptr_t * vEquivs = NULL;
int fRefined, fRefinedAll;
int i, c;
abctime clk = Abc_Clock(), clkTotal = Abc_Clock();
assert( Gia_ManCiNum(pGia) > 0 );
assert( Gia_ManPoNum(pGia) > 0 );
Gia_ManCleanValue( pGia );
p = Gia_IsoManStart( pGia );
Gia_IsoPrepare( p );
Gia_IsoAssignUnique( p );
p->timeStart = Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, 0, Abc_Clock() - clkTotal );
// Gia_IsoRecognizeMuxes( pGia );
i = 0;
if ( fForward )
{
for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
{
clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
}
}
else
{
while ( Vec_IntSize(p->vClasses) > 0 )
{
for ( fRefinedAll = 1; i < nIterMax && fRefinedAll; )
{
fRefinedAll = 0;
for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
{
clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
}
for ( c = 0; i < nIterMax && c < nFixedPoint+1; i++, c = fRefined ? 0 : c+1 )
{
clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
}
}
if ( !fRefinedAll )
break;
}
// Gia_IsoReportTopmost( p );
while ( Vec_IntSize(p->vClasses) > 0 )
{
Gia_IsoAssignOneClass( p, fVerbose );
for ( fRefinedAll = 1; i < nIterMax && fRefinedAll; )
{
fRefinedAll = 0;
for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 )
{
clk = Abc_Clock(); Gia_IsoSimulateBack( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
}
for ( c = 0; i < nIterMax && c < nFixedPoint; i++, c = fRefined ? 0 : c+1 )
{
clk = Abc_Clock(); Gia_IsoSimulate( p, i ); p->timeSim += Abc_Clock() - clk;
clk = Abc_Clock(); fRefined = Gia_IsoSort( p ); p->timeRefine += Abc_Clock() - clk;
if ( fVerbose )
Gia_IsoPrint( p, i+1, Abc_Clock() - clkTotal );
fRefinedAll |= fRefined;
// if ( fRefined )
// printf( "Refinedment happened.\n" );
}
}
}
if ( fVerbose )
Gia_IsoPrint( p, i+2, Abc_Clock() - clkTotal );
}
// Gia_IsoPrintClasses( p );
if ( fVerbose )
{
p->timeTotal = Abc_Clock() - clkTotal;
p->timeOther = p->timeTotal - p->timeStart - p->timeSim - p->timeRefine;
ABC_PRTP( "Start ", p->timeStart, p->timeTotal );
ABC_PRTP( "Simulate ", p->timeSim, p->timeTotal );
ABC_PRTP( "Refine ", p->timeRefine-p->timeSort, p->timeTotal );
ABC_PRTP( "Sort ", p->timeSort, p->timeTotal );
ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
if ( Gia_ManPoNum(p->pGia) > 1 )
vEquivs = Gia_IsoCollectCosClasses( p, fVerbose );
Gia_IsoManTransferUnique( p );
Gia_IsoManStop( p );
return vEquivs;
}
/**Function*************************************************************
Synopsis [Finds canonical ordering of CIs/COs/nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ObjCompareByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 )
{
Gia_Obj_t * pObj1 = *pp1;
Gia_Obj_t * pObj2 = *pp2;
// assert( pObj1->Value != pObj2->Value );
return (int)pObj1->Value - (int)pObj2->Value;
}
void Gia_ManFindCaninicalOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vAnds )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
assert( Gia_ObjIsAnd(pObj) );
if ( !Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) || !Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) )
{
Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
}
else
{
assert( Gia_ObjFanin0(pObj)->Value != Gia_ObjFanin1(pObj)->Value );
if ( Gia_ObjFanin0(pObj)->Value < Gia_ObjFanin1(pObj)->Value )
{
Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
}
else
{
Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin1(pObj), vAnds );
Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
}
}
Vec_IntPush( vAnds, Gia_ObjId(p, pObj) );
}
void Gia_ManFindCaninicalOrder( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, Vec_Int_t ** pvPiPerm )
{
Vec_Ptr_t * vTemp;
Gia_Obj_t * pObj;
int i;
vTemp = Vec_PtrAlloc( 1000 );
Vec_IntClear( vCis );
Vec_IntClear( vAnds );
Vec_IntClear( vCos );
// assign unique IDs to PIs
Vec_PtrClear( vTemp );
Gia_ManForEachPi( p, pObj, i )
Vec_PtrPush( vTemp, pObj );
Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
// create the result
Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
Vec_IntPush( vCis, Gia_ObjId(p, pObj) );
// remember PI permutation
if ( pvPiPerm )
{
*pvPiPerm = Vec_IntAlloc( Gia_ManPiNum(p) );
Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
Vec_IntPush( *pvPiPerm, Gia_ObjCioId(pObj) );
}
// assign unique IDs to POs
if ( Gia_ManPoNum(p) == 1 )
Vec_IntPush( vCos, Gia_ObjId(p, Gia_ManPo(p, 0)) );
else
{
Vec_PtrClear( vTemp );
Gia_ManForEachPo( p, pObj, i )
{
pObj->Value = Abc_Var2Lit( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
Vec_PtrPush( vTemp, pObj );
}
Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
Vec_IntPush( vCos, Gia_ObjId(p, pObj) );
}
// assign unique IDs to ROs
Vec_PtrClear( vTemp );
Gia_ManForEachRo( p, pObj, i )
Vec_PtrPush( vTemp, pObj );
Vec_PtrSort( vTemp, (int (*)(void))Gia_ObjCompareByValue );
// create the result
Vec_PtrForEachEntry( Gia_Obj_t *, vTemp, pObj, i )
{
Vec_IntPush( vCis, Gia_ObjId(p, pObj) );
Vec_IntPush( vCos, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) );
}
Vec_PtrFree( vTemp );
// assign unique IDs to internal nodes
Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
Gia_ManForEachObjVec( vCis, p, pObj, i )
Gia_ObjSetTravIdCurrent( p, pObj );
Gia_ManForEachObjVec( vCos, p, pObj, i )
Gia_ManFindCaninicalOrder_rec( p, Gia_ObjFanin0(pObj), vAnds );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose )
{
Gia_Man_t * pRes = NULL;
Vec_Int_t * vCis, * vAnds, * vCos;
Vec_Ptr_t * vEquiv;
if ( Gia_ManCiNum(p) == 0 ) // const AIG
{
assert( Gia_ManPoNum(p) == 1 );
assert( Gia_ManObjNum(p) == 2 );
return Gia_ManDup(p);
}
// derive canonical values
vEquiv = Gia_IsoDeriveEquivPos( p, 0, fVerbose );
Vec_VecFreeP( (Vec_Vec_t **)&vEquiv );
// find canonical order of CIs/COs/nodes
// find canonical order
vCis = Vec_IntAlloc( Gia_ManCiNum(p) );
vAnds = Vec_IntAlloc( Gia_ManAndNum(p) );
vCos = Vec_IntAlloc( Gia_ManCoNum(p) );
Gia_ManFindCaninicalOrder( p, vCis, vAnds, vCos, NULL );
// derive the new AIG
pRes = Gia_ManDupFromVecs( p, vCis, vAnds, vCos, Gia_ManRegNum(p) );
// cleanup
Vec_IntFree( vCis );
Vec_IntFree( vAnds );
Vec_IntFree( vCos );
return pRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_t ** pvPiPerm )
{
Gia_Man_t * pPart;
Vec_Ptr_t * vEquiv;
Vec_Int_t * vCis, * vAnds, * vCos;
Vec_Str_t * vStr;
// duplicate
pPart = Gia_ManDupCones( p, &iPo, 1, 1 );
//Gia_ManPrint( pPart );
assert( Gia_ManPoNum(pPart) == 1 );
if ( Gia_ManCiNum(pPart) == 0 ) // const AIG
{
assert( Gia_ManPoNum(pPart) == 1 );
assert( Gia_ManObjNum(pPart) == 2 );
vStr = Gia_AigerWriteIntoMemoryStr( pPart );
Gia_ManStop( pPart );
if ( pvPiPerm )
*pvPiPerm = Vec_IntAlloc( 0 );
return vStr;
}
// derive canonical values
vEquiv = Gia_IsoDeriveEquivPos( pPart, 0, fVerbose );
Vec_VecFreeP( (Vec_Vec_t **)&vEquiv );
// find canonical order
vCis = Vec_IntAlloc( Gia_ManCiNum(pPart) );
vAnds = Vec_IntAlloc( Gia_ManAndNum(pPart) );
vCos = Vec_IntAlloc( Gia_ManCoNum(pPart) );
Gia_ManFindCaninicalOrder( pPart, vCis, vAnds, vCos, pvPiPerm );
//printf( "Internal: " );
//Vec_IntPrint( vCis );
// derive the AIGER string
vStr = Gia_AigerWriteIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) );
// cleanup
Vec_IntFree( vCis );
Vec_IntFree( vAnds );
Vec_IntFree( vCos );
Gia_ManStop( pPart );
return vStr;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Vec_IntCountNonTrivial( Vec_Ptr_t * vEquivs, int * pnUsed )
{
Vec_Int_t * vClass;
int i, nClasses = 0;
*pnUsed = 0;
Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vClass, i )
{
if ( Vec_IntSize(vClass) < 2 )
continue;
nClasses++;
(*pnUsed) += Vec_IntSize(vClass);
}
return nClasses;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pInit, Vec_Ptr_t ** pvPosEquivs, Vec_Ptr_t ** pvPiPerms, int fEstimate, int fDualOut, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * p, * pPart;
Vec_Ptr_t * vEquivs, * vEquivs2, * vStrings;
Vec_Int_t * vRemain, * vLevel, * vLevel2;
Vec_Str_t * vStr, * vStr2;
int i, k, s, sStart, iPo, Counter;
int nClasses, nUsedPos;
abctime clk = Abc_Clock();
if ( pvPosEquivs )
*pvPosEquivs = NULL;
if ( pvPiPerms )
*pvPiPerms = Vec_PtrStart( Gia_ManPoNum(pInit) );
if ( fDualOut )
{
assert( (Gia_ManPoNum(pInit) & 1) == 0 );
if ( Gia_ManPoNum(pInit) == 2 )
return Gia_ManDup(pInit);
p = Gia_ManTransformMiter( pInit );
p = Gia_ManSeqStructSweep( pPart = p, 1, 1, 0 );
Gia_ManStop( pPart );
}
else
{
if ( Gia_ManPoNum(pInit) == 1 )
return Gia_ManDup(pInit);
p = pInit;
}
// create preliminary equivalences
vEquivs = Gia_IsoDeriveEquivPos( p, 1, fVeryVerbose );
if ( vEquivs == NULL )
{
if ( fDualOut )
Gia_ManStop( p );
return NULL;
}
nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos );
printf( "Reduced %d outputs to %d candidate classes (%d outputs are in %d non-trivial classes). ",
Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fEstimate )
{
Vec_VecFree( (Vec_Vec_t *)vEquivs );
return Gia_ManDup(pInit);
}
// perform refinement of equivalence classes
Counter = 0;
vEquivs2 = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
{
if ( Vec_IntSize(vLevel) < 2 )
{
Vec_PtrPush( vEquivs2, Vec_IntDup(vLevel) );
for ( k = 0; k < Vec_IntSize(vLevel); k++ )
if ( ++Counter % 100 == 0 )
printf( "%6d finished...\r", Counter );
continue;
}
if ( fVerbose )
{
iPo = Vec_IntEntry(vLevel, 0);
printf( "%6d %6d %6d : ", i, Vec_IntSize(vLevel), iPo );
pPart = Gia_ManDupCones( p, &iPo, 1, 1 );
Gia_ManPrintStats(pPart, NULL);
Gia_ManStop( pPart );
}
sStart = Vec_PtrSize( vEquivs2 );
vStrings = Vec_PtrAlloc( 100 );
Vec_IntForEachEntry( vLevel, iPo, k )
{
if ( ++Counter % 100 == 0 )
printf( "%6d finished...\r", Counter );
assert( pvPiPerms == NULL || Vec_PtrArray(*pvPiPerms)[iPo] == NULL );
vStr = Gia_ManIsoFindString( p, iPo, 0, pvPiPerms ? (Vec_Int_t **)Vec_PtrArray(*pvPiPerms) + iPo : NULL );
// printf( "Output %2d : ", iPo );
// Vec_IntPrint( Vec_PtrArray(*pvPiPerms)[iPo] );
// check if this string already exists
Vec_PtrForEachEntry( Vec_Str_t *, vStrings, vStr2, s )
if ( Vec_StrCompareVec(vStr, vStr2) == 0 )
break;
if ( s == Vec_PtrSize(vStrings) )
{
Vec_PtrPush( vStrings, vStr );
Vec_PtrPush( vEquivs2, Vec_IntAlloc(8) );
}
else
Vec_StrFree( vStr );
// add this entry to the corresponding level
vLevel2 = (Vec_Int_t *)Vec_PtrEntry( vEquivs2, sStart + s );
Vec_IntPush( vLevel2, iPo );
}
// if ( Vec_PtrSize(vEquivs2) - sStart > 1 )
// printf( "Refined class %d into %d classes.\n", i, Vec_PtrSize(vEquivs2) - sStart );
Vec_VecFree( (Vec_Vec_t *)vStrings );
}
assert( Counter == Gia_ManPoNum(p) );
Vec_VecSortByFirstInt( (Vec_Vec_t *)vEquivs2, 0 );
Vec_VecFree( (Vec_Vec_t *)vEquivs );
vEquivs = vEquivs2;
// collect the first ones
vRemain = Vec_IntAlloc( 100 );
Vec_PtrForEachEntry( Vec_Int_t *, vEquivs, vLevel, i )
Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) );
if ( fDualOut )
{
Vec_Int_t * vTemp = Vec_IntAlloc( Vec_IntSize(vRemain) );
int i, Entry;
Vec_IntForEachEntry( vRemain, Entry, i )
{
// printf( "%d ", Entry );
Vec_IntPush( vTemp, 2*Entry );
Vec_IntPush( vTemp, 2*Entry+1 );
}
// printf( "\n" );
Vec_IntFree( vRemain );
vRemain = vTemp;
Gia_ManStop( p );
p = pInit;
}
// derive the resulting AIG
pPart = Gia_ManDupCones( p, Vec_IntArray(vRemain), Vec_IntSize(vRemain), 0 );
Vec_IntFree( vRemain );
// report the results
nClasses = Vec_IntCountNonTrivial( vEquivs, &nUsedPos );
if ( !fDualOut )
printf( "Reduced %d outputs to %d equivalence classes (%d outputs are in %d non-trivial classes). ",
Gia_ManPoNum(p), Vec_PtrSize(vEquivs), nUsedPos, nClasses );
else
printf( "Reduced %d dual outputs to %d dual outputs. ", Gia_ManPoNum(p)/2, Gia_ManPoNum(pPart)/2 );
Abc_PrintTime( 1, "Time", Abc_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_IsoTestOld( Gia_Man_t * p, int fVerbose )
{
Vec_Ptr_t * vEquivs;
abctime clk = Abc_Clock();
vEquivs = Gia_IsoDeriveEquivPos( p, 0, fVerbose );
printf( "Reduced %d outputs to %d. ", Gia_ManPoNum(p), vEquivs ? Vec_PtrSize(vEquivs) : 1 );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
if ( fVerbose && vEquivs && Gia_ManPoNum(p) != Vec_PtrSize(vEquivs) )
{
printf( "Nontrivial classes:\n" );
// Vec_VecPrintInt( (Vec_Vec_t *)vEquivs, 1 );
}
Vec_VecFreeP( (Vec_Vec_t **)&vEquivs );
}
/**Function*************************************************************
Synopsis [Test remapping of CEXes for isomorphic POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_IsoTestGenPerm( int nPis )
{
Vec_Int_t * vPerm;
int i, * pArray;
vPerm = Vec_IntStartNatural( nPis );
pArray = Vec_IntArray( vPerm );
for ( i = 0; i < nPis; i++ )
{
int iNew = rand() % nPis;
ABC_SWAP( int, pArray[i], pArray[iNew] );
}
return vPerm;
}
void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
{
Abc_Cex_t * pCexNew;
Vec_Int_t * vPiPerm;
Vec_Ptr_t * vPosEquivs, * vPisPerm;
Vec_Int_t * vPerm0, * vPerm1;
Gia_Man_t * pPerm, * pDouble, * pAig;
assert( Gia_ManPoNum(p) == 1 );
assert( Gia_ManRegNum(p) > 0 );
// generate random permutation of PIs
vPiPerm = Gia_IsoTestGenPerm( Gia_ManPiNum(p) );
printf( "Considering random permutation of the primary inputs of the AIG:\n" );
Vec_IntPrint( vPiPerm );
// create AIG with two primary outputs (original and permuted)
pPerm = Gia_ManDupPerm( p, vPiPerm );
pDouble = Gia_ManDupAppendNew( p, pPerm );
//Gia_AigerWrite( pDouble, "test.aig", 0, 0 );
// analyze the two-output miter
pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0, 0 );
Vec_VecFree( (Vec_Vec_t *)vPosEquivs );
// given CEX for output 0, derive CEX for output 1
vPerm0 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 0 );
vPerm1 = (Vec_Int_t *)Vec_PtrEntry( vPisPerm, 1 );
pCexNew = Abc_CexPermuteTwo( pCex, vPerm0, vPerm1 );
Vec_VecFree( (Vec_Vec_t *)vPisPerm );
// check that original CEX and the resulting CEX is valid
if ( Gia_ManVerifyCex(p, pCex, 0) )
printf( "CEX for the init AIG is valid.\n" );
else
printf( "CEX for the init AIG is not valid.\n" );
if ( Gia_ManVerifyCex(pPerm, pCexNew, 0) )
printf( "CEX for the perm AIG is valid.\n" );
else
printf( "CEX for the perm AIG is not valid.\n" );
// delete
Gia_ManStop( pAig );
Gia_ManStop( pDouble );
Gia_ManStop( pPerm );
Vec_IntFree( vPiPerm );
Abc_CexFree( pCexNew );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END