#include "gia.h"

Data Structures
struct	Gia_IsoMan_t_

Macros
#define	ISO_MASK 0xFF

Typedefs
typedef struct Gia_IsoMan_t_	Gia_IsoMan_t
	DECLARATIONS ///. More...

Functions
static unsigned	Gia_IsoGetValue (Gia_IsoMan_t *p, int i)

static unsigned	Gia_IsoGetItem (Gia_IsoMan_t *p, int i)

static void	Gia_IsoSetValue (Gia_IsoMan_t *p, int i, unsigned v)

static void	Gia_IsoSetItem (Gia_IsoMan_t *p, int i, unsigned v)

Gia_IsoMan_t *	Gia_IsoManStart (Gia_Man_t *pGia)
	FUNCTION DEFINITIONS ///. More...

void	Gia_IsoManStop (Gia_IsoMan_t *p)

void	Gia_IsoManTransferUnique (Gia_IsoMan_t *p)

void	Gia_IsoPrintClasses (Gia_IsoMan_t *p)

void	Gia_IsoPrint (Gia_IsoMan_t *p, int Iter, abctime Time)

void	Gia_IsoPrepare (Gia_IsoMan_t *p)

void	Gia_IsoAssignUnique (Gia_IsoMan_t *p)

int	Gia_IsoSort (Gia_IsoMan_t *p)

Vec_Ptr_t *	Gia_IsoCollectCosClasses (Gia_IsoMan_t *p, int fVerbose)

static unsigned	Gia_IsoUpdateValue (int Value, int fCompl)

static unsigned	Gia_IsoUpdate (Gia_IsoMan_t *p, int Iter, int iObj, int fCompl)

void	Gia_IsoSimulate (Gia_IsoMan_t *p, int Iter)

void	Gia_IsoSimulateBack (Gia_IsoMan_t *p, int Iter)

void	Gia_IsoAssignOneClass2 (Gia_IsoMan_t *p)

void	Gia_IsoAssignOneClass3 (Gia_IsoMan_t *p)

void	Gia_IsoAssignOneClass (Gia_IsoMan_t *p, int fVerbose)

void	Gia_IsoReportTopmost (Gia_IsoMan_t *p)

void	Gia_IsoRecognizeMuxes (Gia_Man_t *pGia)

Vec_Ptr_t *	Gia_IsoDeriveEquivPos (Gia_Man_t *pGia, int fForward, int fVerbose)

int	Gia_ObjCompareByValue (Gia_Obj_t pp1, Gia_Obj_t pp2)

void	Gia_ManFindCaninicalOrder_rec (Gia_Man_t p, Gia_Obj_t pObj, Vec_Int_t *vAnds)

void	Gia_ManFindCaninicalOrder (Gia_Man_t p, Vec_Int_t vCis, Vec_Int_t vAnds, Vec_Int_t vCos, Vec_Int_t **pvPiPerm)

Gia_Man_t *	Gia_ManIsoCanonicize (Gia_Man_t *p, int fVerbose)

Vec_Str_t *	Gia_ManIsoFindString (Gia_Man_t p, int iPo, int fVerbose, Vec_Int_t *pvPiPerm)

int	Vec_IntCountNonTrivial (Vec_Ptr_t vEquivs, int pnUsed)

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)

void	Gia_IsoTestOld (Gia_Man_t *p, int fVerbose)

Vec_Int_t *	Gia_IsoTestGenPerm (int nPis)

void	Gia_IsoTest (Gia_Man_t p, Abc_Cex_t pCex, int fVerbose)

Variables
static int	s_256Primes [ISO_MASK+1]

Macro Definition Documentation

#define ISO_MASK 0xFF

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

]

Definition at line 26 of file giaIso.c.

Typedef Documentation

typedef struct Gia_IsoMan_t_ Gia_IsoMan_t

DECLARATIONS ///.

Definition at line 67 of file giaIso.c.

Function Documentation

void Gia_IsoAssignOneClass	(	Gia_IsoMan_t *	p,
		int	fVerbose
	)

Definition at line 587 of file giaIso.c.

 {
     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 );
 }

void Gia_IsoAssignOneClass2 ( Gia_IsoMan_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 512 of file giaIso.c.

 {
     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 )

Definition at line 554 of file giaIso.c.

 {
     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_IsoAssignUnique ( Gia_IsoMan_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 265 of file giaIso.c.

 {
     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;
 }

Vec_Ptr_t* Gia_IsoCollectCosClasses	(	Gia_IsoMan_t *	p,
		int	fVerbose
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file giaIso.c.

 {
     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;
 }

Vec_Ptr_t* Gia_IsoDeriveEquivPos	(	Gia_Man_t *	pGia,
		int	fForward,
		int	fVerbose
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 720 of file giaIso.c.

 {
     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;
 }

static unsigned Gia_IsoGetItem	(	Gia_IsoMan_t *	p,
		int	i
	)

inlinestatic

Definition at line 94 of file giaIso.c.

94 { return (unsigned)(p->pStoreW[i] >> 32); }

Gia_IsoMan_t_::pStoreW

word * pStoreW

Definition: giaIso.c:78

static unsigned Gia_IsoGetValue	(	Gia_IsoMan_t *	p,
		int	i
	)

inlinestatic

Definition at line 93 of file giaIso.c.

93 { return (unsigned)(p->pStoreW[i]); }

Gia_IsoMan_t_::pStoreW

word * pStoreW

Definition: giaIso.c:78

Gia_IsoMan_t* Gia_IsoManStart ( Gia_Man_t * pGia )

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file giaIso.c.

 {
     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 )

Definition at line 131 of file giaIso.c.

 {
     // 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 )

Definition at line 142 of file giaIso.c.

 {
     Gia_Obj_t * pObj;
     int i;
     // copy unique numbers into the nodes
     Gia_ManForEachObj( p->pGia, pObj, i )
         pObj->Value = p->pUniques[i];
 }

void Gia_IsoPrepare ( Gia_IsoMan_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file giaIso.c.

 {
     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" );
 */
 }

void Gia_IsoPrint	(	Gia_IsoMan_t *	p,
		int	Iter,
		abctime	Time
	)

Definition at line 181 of file giaIso.c.

 {
     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 );
 }

void Gia_IsoPrintClasses ( Gia_IsoMan_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file giaIso.c.

 {
     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_IsoRecognizeMuxes ( Gia_Man_t * pGia )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 682 of file giaIso.c.

 {
     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];
         }
     }
 }

void Gia_IsoReportTopmost ( Gia_IsoMan_t * p )

Function*************************************************************

Synopsis [Report topmost equiv nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 631 of file giaIso.c.

 {
     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;
             }
         }
     }
 }

static void Gia_IsoSetItem	(	Gia_IsoMan_t *	p,
		int	i,
		unsigned	v
	)

inlinestatic

Definition at line 97 of file giaIso.c.

97 { ((unsigned *)(p->pStoreW + i))[1] = v; }

Gia_IsoMan_t_::pStoreW

word * pStoreW

Definition: giaIso.c:78

static void Gia_IsoSetValue	(	Gia_IsoMan_t *	p,
		int	i,
		unsigned	v
	)

inlinestatic

Definition at line 96 of file giaIso.c.

96 { ((unsigned *)(p->pStoreW + i))[0] = v; }

Gia_IsoMan_t_::pStoreW

word * pStoreW

Definition: giaIso.c:78

void Gia_IsoSimulate	(	Gia_IsoMan_t *	p,
		int	Iter
	)

Definition at line 453 of file giaIso.c.

 {
     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
	)

Definition at line 480 of file giaIso.c.

 {
     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;
 }

int Gia_IsoSort ( Gia_IsoMan_t * p )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 299 of file giaIso.c.

 {
     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;
 }

void Gia_IsoTest	(	Gia_Man_t *	p,
		Abc_Cex_t *	pCex,
		int	fVerbose
	)

Definition at line 1280 of file giaIso.c.

 {
     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 );
 }

Vec_Int_t* Gia_IsoTestGenPerm ( int nPis )

Function*************************************************************

Synopsis [Test remapping of CEXes for isomorphic POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 1267 of file giaIso.c.

 {
     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_IsoTestOld	(	Gia_Man_t *	p,
		int	fVerbose
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1241 of file giaIso.c.

 {
     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 );
 }

static unsigned Gia_IsoUpdate	(	Gia_IsoMan_t *	p,
		int	Iter,
		int	iObj,
		int	fCompl
	)

inlinestatic

Definition at line 446 of file giaIso.c.

 {
     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;
 }

static unsigned Gia_IsoUpdateValue	(	int	Value,
		int	fCompl
	)

inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 442 of file giaIso.c.

 {
     return (Value+1) * s_256Primes[Abc_Var2Lit(Value, fCompl) & ISO_MASK];
 }

void Gia_ManFindCaninicalOrder	(	Gia_Man_t *	p,
		Vec_Int_t *	vCis,
		Vec_Int_t *	vAnds,
		Vec_Int_t *	vCos,
		Vec_Int_t **	pvPiPerm
	)

Definition at line 882 of file giaIso.c.

 {
     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 );
 }

void Gia_ManFindCaninicalOrder_rec	(	Gia_Man_t *	p,
		Gia_Obj_t *	pObj,
		Vec_Int_t *	vAnds
	)

Definition at line 855 of file giaIso.c.

 {
     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) );
 }

Gia_Man_t* Gia_ManIsoCanonicize	(	Gia_Man_t *	p,
		int	fVerbose
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 958 of file giaIso.c.

 {
     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;
 }

Vec_Str_t* Gia_ManIsoFindString	(	Gia_Man_t *	p,
		int	iPo,
		int	fVerbose,
		Vec_Int_t **	pvPiPerm
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 998 of file giaIso.c.

 {
     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;
 }

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
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1075 of file giaIso.c.

 { 
     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;
 }

int Gia_ObjCompareByValue	(	Gia_Obj_t **	pp1,
		Gia_Obj_t **	pp2
	)

Function*************************************************************

Synopsis [Finds canonical ordering of CIs/COs/nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 848 of file giaIso.c.

 {
     Gia_Obj_t * pObj1 = *pp1;
     Gia_Obj_t * pObj2 = *pp2;
 //    assert( pObj1->Value != pObj2->Value );
     return (int)pObj1->Value - (int)pObj2->Value;
 }

int Vec_IntCountNonTrivial	(	Vec_Ptr_t *	vEquivs,
		int *	pnUsed
	)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1049 of file giaIso.c.

 {
     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;
 }

Variable Documentation

int s_256Primes[ISO_MASK+1]

static

Definition at line 27 of file giaIso.c.

Data Structures

Macros

Typedefs

Functions

Variables

Macro Definition Documentation

Typedef Documentation

Function Documentation

Variable Documentation