#include "aig.h"
#include "bool/kit/kit.h"
#include "bool/bdc/bdc.h"
#include "aig/ioa/ioa.h"

Data Structures
struct	Aig_VSig_t_

struct	Aig_Tru_t_

struct	Aig_RMan_t_

Macros
#define	RMAN_MAXVARS 12
	DECLARATIONS ///. More...

#define	RMAX_MAXWORD (RMAN_MAXVARS <= 5 ? 1 : (1 << (RMAN_MAXVARS - 5)))

Typedefs
typedef struct Aig_VSig_t_	Aig_VSig_t

typedef struct Aig_Tru_t_	Aig_Tru_t

typedef struct Aig_RMan_t_	Aig_RMan_t

Functions
Aig_RMan_t *	Aig_RManStart ()
	FUNCTION DEFINITIONS ///. More...

static int	Aig_RManTableHash (unsigned pTruth, int nVars, int nBins, int pPrimes)

Aig_Tru_t **	Aig_RManTableLookup (Aig_RMan_t p, unsigned pTruth, int nVars)

void	Aig_RManTableResize (Aig_RMan_t *p)

int	Aig_RManTableFindOrAdd (Aig_RMan_t p, unsigned pTruth, int nVars)

void	Aig_RManStop (Aig_RMan_t *p)

void	Aig_RManQuit ()

void	Aig_RManPrintVarProfile (unsigned pTruth, int nVars, unsigned pTruthAux)

void	Aig_RManSortNums (int *pArray, int nVars)

void	Aig_RManPrintSigs (Aig_VSig_t *pSigs, int nVars)

void	Aig_RManComputeVSigs (unsigned pTruth, int nVars, Aig_VSig_t pSigs, unsigned *pAux)

static int	Aig_RManCompareSigs (Aig_VSig_t p0, Aig_VSig_t p1, int nVars)

int	Aig_RManVarsAreUnique (Aig_VSig_t *pMints, int nVars)

void	Aig_RManPrintUniqueVars (Aig_VSig_t *pMints, int nVars)

unsigned	Aig_RManSemiCanonicize (unsigned pOut, unsigned pIn, int nVars, char pCanonPerm, Aig_VSig_t pSigs, int fReturnIn)

static Aig_Obj_t *	Bdc_FunCopyHop (Bdc_Fun_t *pObj)

void	Aig_RManSaveOne (Aig_RMan_t p, unsigned pTruth, int nVars)

void	Aig_RManRecord (unsigned *pTruth, int nVarsInit)

Variables
static Aig_RMan_t *	s_pRMan = NULL

Macro Definition Documentation

#define RMAN_MAXVARS 12

DECLARATIONS ///.

CFile****************************************************************

FileName [aigCanon.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG package.]

Synopsis [Processing the library of semi-canonical AIGs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:: aigCanon.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]

Definition at line 33 of file aigCanon.c.

#define RMAX_MAXWORD (RMAN_MAXVARS <= 5 ? 1 : (1 << (RMAN_MAXVARS - 5)))

Definition at line 34 of file aigCanon.c.

Typedef Documentation

typedef struct Aig_RMan_t_ Aig_RMan_t

Definition at line 53 of file aigCanon.c.

typedef struct Aig_Tru_t_ Aig_Tru_t

Definition at line 43 of file aigCanon.c.

typedef struct Aig_VSig_t_ Aig_VSig_t

Definition at line 36 of file aigCanon.c.

Function Documentation

static int Aig_RManCompareSigs	(	Aig_VSig_t *	p0,
		Aig_VSig_t *	p1,
		int	nVars
	)

inlinestatic

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

Synopsis [Computs signatures for all variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 410 of file aigCanon.c.

 {
 //    return memcmp( p0, p1, sizeof(int) + sizeof(int) * nVars );
     return memcmp( p0, p1, sizeof(int) );
 }

void Aig_RManComputeVSigs	(	unsigned *	pTruth,
		int	nVars,
		Aig_VSig_t *	pSigs,
		unsigned *	pAux
	)

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

Synopsis [Computes signatures for all variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file aigCanon.c.

 {
     int v;
     for ( v = 0; v < nVars; v++ )
     {
         Kit_TruthCofactor0New( pAux, pTruth, nVars, v );
         pSigs[2*v+0].nOnes = Kit_TruthCountOnes( pAux, nVars );
         Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+0].nCofOnes );
         Aig_RManSortNums( pSigs[2*v+0].nCofOnes, nVars );
 
         Kit_TruthCofactor1New( pAux, pTruth, nVars, v );
         pSigs[2*v+1].nOnes = Kit_TruthCountOnes( pAux, nVars );
         Kit_TruthCountOnesInCofs0( pAux, nVars, pSigs[2*v+1].nCofOnes );
         Aig_RManSortNums( pSigs[2*v+1].nCofOnes, nVars );
     }
 }

void Aig_RManPrintSigs	(	Aig_VSig_t *	pSigs,
		int	nVars
	)

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

Synopsis [Prints signatures for all variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 353 of file aigCanon.c.

 {
     int v, i, k;
     for ( v = 0; v < nVars; v++ )
     {
         printf( "%2d : ", v );
         for ( k = 0; k < 2; k++ )
         {
             printf( "%5d  ", pSigs[2*v+k].nOnes );
             printf( "(" );
             for ( i = 0; i < nVars; i++ )
                 printf( "%4d ", pSigs[2*v+k].nCofOnes[i] );
             printf( ")  " );
         }
         printf( "\n" );
     }
 }

void Aig_RManPrintUniqueVars	(	Aig_VSig_t *	pMints,
		int	nVars
	)

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

Synopsis [Returns 1 if all variables are unique.]

Description []

SideEffects []

SeeAlso []

Definition at line 447 of file aigCanon.c.

 {
     int i;
     for ( i = 0; i < nVars; i++ )
         if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*i+1], nVars ) == 0 )
             printf( "=" );
         else 
             printf( "x" );
     printf( "\n" );
 
     printf( "0" );
     for ( i = 1; i < nVars; i++ )
         if ( Aig_RManCompareSigs( &pMints[2*(i-1)], &pMints[2*i], nVars ) == 0 )
             printf( "-" );
         else if ( i < 10 )
             printf( "%c", '0' + i );
         else 
             printf( "%c", 'A' + i-10 );
     printf( "\n" );
 }

void Aig_RManPrintVarProfile	(	unsigned *	pTruth,
		int	nVars,
		unsigned *	pTruthAux
	)

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

Synopsis [Returns 1 if all variables are unique.]

Description []

SideEffects []

SeeAlso []

Definition at line 308 of file aigCanon.c.

 {
     int pStore2[32];
     int i;
     Kit_TruthCountOnesInCofsSlow( pTruth, nVars, pStore2, pTruthAux );
     for ( i = 0; i < nVars; i++ )
         printf( "%2d/%2d ", pStore2[2*i], pStore2[2*i+1] );
     printf( "\n" );
 }

void Aig_RManQuit ( )

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

Synopsis [Stops recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 283 of file aigCanon.c.

 {
 //    extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
     char Buffer[20];
     if ( s_pRMan == NULL )
         return;
     // dump the library file
     sprintf( Buffer, "aiglib%02d.aig", s_pRMan->nVars );
     Ioa_WriteAiger( s_pRMan->pAig, Buffer, 0, 1 );
     // quit the manager
     Aig_RManStop( s_pRMan );
     s_pRMan = NULL;
 }

void Aig_RManRecord	(	unsigned *	pTruth,
		int	nVarsInit
	)

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

Synopsis [Records one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 598 of file aigCanon.c.

 {
     int fVerify = 1;
     Kit_DsdNtk_t * pNtk;
     Kit_DsdObj_t * pObj;
     unsigned uPhaseC;
     int i, nVars, nWords;
     int fUniqueVars;
 
     if ( nVarsInit > RMAN_MAXVARS )
     {
         printf( "The number of variables in too large.\n" );
         return;
     }
 
     if ( s_pRMan == NULL )
         s_pRMan = Aig_RManStart();
     s_pRMan->nTotal++;
     // canonicize the function
     pNtk = Kit_DsdDecompose( pTruth, nVarsInit );
     pObj = Kit_DsdNonDsdPrimeMax( pNtk );
     if ( pObj == NULL || pObj->nFans == 3 )
     {
         s_pRMan->nTtDsd++;
         Kit_DsdNtkFree( pNtk );
         return;
     }
     nVars = pObj->nFans;
     s_pRMan->nVarFuncs[nVars]++;
     if ( nVars < nVarsInit )
         s_pRMan->nTtDsdPart++;
     else
         s_pRMan->nTtDsdNot++;
     // compute the number of words
     nWords = Abc_TruthWordNum( nVars );
     // copy the function
     memcpy( s_pRMan->pTruthInit, Kit_DsdObjTruth(pObj), 4*nWords );
     Kit_DsdNtkFree( pNtk );
     // canonicize the output
     if ( s_pRMan->pTruthInit[0] & 1 )
         Kit_TruthNot( s_pRMan->pTruthInit, s_pRMan->pTruthInit, nVars );
     memcpy( s_pRMan->pTruth, s_pRMan->pTruthInit, 4*nWords );
 
     // canonize the function
     for ( i = 0; i < nVars; i++ )
         s_pRMan->pPerm[i] = i;
     uPhaseC = Aig_RManSemiCanonicize( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPerm, s_pRMan->pMints, 1 );
     // check unique variables
     fUniqueVars = Aig_RManVarsAreUnique( s_pRMan->pMints, nVars );
     s_pRMan->nUniqueVars += fUniqueVars;
 
 /*
     printf( "%4d : ", s_pRMan->nTotal );
     printf( "%2d %2d  ", nVarsInit, nVars );
     Extra_PrintBinary( stdout, &uPhaseC, nVars );
     printf( "  " );
     for ( i = 0; i < nVars; i++ )
         printf( "%2d/%2d ", s_pRMan->pMints[2*i], s_pRMan->pMints[2*i+1] );
     printf( "\n" );
     Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars );
 Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n\n" );
 */
 /*
     printf( "\n" );
     printf( "%4d : ", s_pRMan->nTotal );
     printf( "%2d %2d  ", nVarsInit, nVars );
     printf( "   " );
     printf( "\n" );
     Aig_RManPrintUniqueVars( s_pRMan->pMints, nVars );
 //    Aig_RManPrintSigs( s_pRMan->pMints, nVars );
 */
 
 //Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n\n" );
 
     if ( Aig_RManTableFindOrAdd( s_pRMan, s_pRMan->pTruth, nVars ) )
         Aig_RManSaveOne( s_pRMan, s_pRMan->pTruth, nVars );
 
     if ( fVerify )
     {
         // derive reverse permutation
         for ( i = 0; i < nVars; i++ )
             s_pRMan->pPermR[i] = s_pRMan->pPerm[i];
         // implement permutation
         Kit_TruthPermute( s_pRMan->pTruthTemp, s_pRMan->pTruth, nVars, s_pRMan->pPermR, 1 );
         // implement polarity
         for ( i = 0; i < nVars; i++ )
             if ( uPhaseC & (1 << i) )
                 Kit_TruthChangePhase( s_pRMan->pTruth, nVars, i );
 
         // perform verification
         if ( fUniqueVars && !Kit_TruthIsEqual( s_pRMan->pTruth, s_pRMan->pTruthInit, nVars ) )
             printf( "Verification failed.\n" );
     }
 //Aig_RManPrintVarProfile( s_pRMan->pTruth, nVars, s_pRMan->pTruthTemp );
 //Extra_PrintBinary( stdout, s_pRMan->pTruth, 1<<nVars ); printf( "\n" );
 }

void Aig_RManSaveOne	(	Aig_RMan_t *	p,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Records one function.]

Description []

SideEffects []

SeeAlso []

Definition at line 558 of file aigCanon.c.

 {
     int i, nNodes, RetValue;
     Bdc_Fun_t * pFunc;
     Aig_Obj_t * pTerm;
     // perform decomposition
     RetValue = Bdc_ManDecompose( p->pBidec, pTruth, NULL, nVars, NULL, 1000 );
     if ( RetValue < 0 )
     {
         printf( "Decomposition failed.\n" );
         return;
     }
     // convert back into HOP
     Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, 0 ), Aig_ManConst1(p->pAig) );
     for ( i = 0; i < nVars; i++ )
         Bdc_FuncSetCopy( Bdc_ManFunc( p->pBidec, i+1 ), Aig_IthVar(p->pAig, i) );
     nNodes = Bdc_ManNodeNum(p->pBidec);
     for ( i = nVars + 1; i < nNodes; i++ )
     {
         pFunc = Bdc_ManFunc( p->pBidec, i );
         Bdc_FuncSetCopy( pFunc, Aig_And( p->pAig, 
             Bdc_FunCopyHop(Bdc_FuncFanin0(pFunc)), 
             Bdc_FunCopyHop(Bdc_FuncFanin1(pFunc)) ) );
     }
     pTerm = Bdc_FunCopyHop( Bdc_ManRoot(p->pBidec) );
     pTerm = Aig_ObjCreateCo( p->pAig, pTerm );
 //    assert( pTerm->fPhase == 0 );
 }

unsigned Aig_RManSemiCanonicize	(	unsigned *	pOut,
		unsigned *	pIn,
		int	nVars,
		char *	pCanonPerm,
		Aig_VSig_t *	pSigs,
		int	fReturnIn
	)

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

Synopsis [Canonicize the truth table.]

Description [Returns the phase. ]

SideEffects []

SeeAlso []

Definition at line 479 of file aigCanon.c.

 {
     Aig_VSig_t TempSig;
     int i, Temp, fChange, Counter;
     unsigned * pTemp, uCanonPhase = 0;
     // collect signatures 
     Aig_RManComputeVSigs( pIn, nVars, pSigs, pOut );
     // canonicize phase
     for ( i = 0; i < nVars; i++ )
     {
 //        if ( pStore[2*i+0] <= pStore[2*i+1] )
         if ( Aig_RManCompareSigs( &pSigs[2*i+0], &pSigs[2*i+1], nVars ) <= 0 )
             continue;
         uCanonPhase |= (1 << i);
         TempSig = pSigs[2*i+0];
         pSigs[2*i+0] = pSigs[2*i+1];
         pSigs[2*i+1] = TempSig;
         Kit_TruthChangePhase( pIn, nVars, i );
     }
     // permute
     Counter = 0;
     do {
         fChange = 0;
         for ( i = 0; i < nVars-1; i++ )
         {
 //            if ( pStore[2*i] <= pStore[2*(i+1)] )
             if ( Aig_RManCompareSigs( &pSigs[2*i], &pSigs[2*(i+1)], nVars ) <= 0 )
                 continue;
             Counter++;
             fChange = 1;
 
             Temp = pCanonPerm[i];
             pCanonPerm[i] = pCanonPerm[i+1];
             pCanonPerm[i+1] = Temp;
 
             TempSig = pSigs[2*i];
             pSigs[2*i] = pSigs[2*(i+1)];
             pSigs[2*(i+1)] = TempSig;
 
             TempSig = pSigs[2*i+1];
             pSigs[2*i+1] = pSigs[2*(i+1)+1];
             pSigs[2*(i+1)+1] = TempSig;
 
             Kit_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
             pTemp = pIn; pIn = pOut; pOut = pTemp;
         }
     } while ( fChange );
 
     // swap if it was moved an even number of times
     if ( fReturnIn ^ !(Counter & 1) )
         Kit_TruthCopy( pOut, pIn, nVars );
     return uCanonPhase;
 }

void Aig_RManSortNums	(	int *	pArray,
		int	nVars
	)

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

Synopsis [Sorts numbers in the increasing order.]

Description []

SideEffects []

SeeAlso []

Definition at line 329 of file aigCanon.c.

 {
     int i, j, best_i, tmp;
     for ( i = 0; i < nVars-1; i++ )
     {
         best_i = i;
         for ( j = i+1; j < nVars; j++ )
             if ( pArray[j] > pArray[best_i] )
                 best_i = j;
         tmp = pArray[i]; pArray[i] = pArray[best_i]; pArray[best_i] = tmp;
     }
 }

Aig_RMan_t* Aig_RManStart ( )

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocates recording manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 99 of file aigCanon.c.

 {
     static Bdc_Par_t Pars = {0}, * pPars = &Pars;
     Aig_RMan_t * p;
     p = ABC_ALLOC( Aig_RMan_t, 1 );
     memset( p, 0, sizeof(Aig_RMan_t) );
     p->nVars = RMAN_MAXVARS;
     p->pAig  = Aig_ManStart( 1000000 );
     Aig_IthVar( p->pAig, p->nVars-1 );
     // create hash table
     p->nBins = Abc_PrimeCudd(5000);
     p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
     p->pMemTrus = Aig_MmFlexStart();
     // bi-decomposition manager
     pPars->nVarsMax = p->nVars;
     pPars->fVerbose = 0;
     p->pBidec = Bdc_ManAlloc( pPars );
     return p;
 }

void Aig_RManStop ( Aig_RMan_t * p )

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

Synopsis [Deallocates recording manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file aigCanon.c.

 {
     int i;
     printf( "Total funcs    = %10d\n", p->nTotal );
     printf( "Full DSD funcs = %10d\n", p->nTtDsd );
     printf( "Part DSD funcs = %10d\n", p->nTtDsdPart );
     printf( "Non- DSD funcs = %10d\n", p->nTtDsdNot );
     printf( "Uniq-var funcs = %10d\n", p->nUniqueVars );
     printf( "Unique   funcs = %10d\n", p->nEntries );
     printf( "Distribution of functions:\n" );
     for ( i = 5; i <= p->nVars; i++ )
         printf( "%2d = %8d\n", i, p->nVarFuncs[i] );
     Aig_MmFlexStop( p->pMemTrus, 0 );
     Aig_ManStop( p->pAig );
     Bdc_ManFree( p->pBidec );
     ABC_FREE( p->pBins );
     ABC_FREE( p );
 }

int Aig_RManTableFindOrAdd	(	Aig_RMan_t *	p,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Find or add new entry.]

Description [Returns 1 if this is a new entry.]

SideEffects []

SeeAlso []

Definition at line 218 of file aigCanon.c.

 {
     Aig_Tru_t ** ppSpot, * pEntry;
     int nBytes;
     ppSpot = Aig_RManTableLookup( p, pTruth, nVars );
     if ( *ppSpot )
     {
         (*ppSpot)->nVisits++;
         return 0;
     }
     nBytes = sizeof(Aig_Tru_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars);
     if ( p->nEntries == 3*p->nBins )
         Aig_RManTableResize( p );
     pEntry = (Aig_Tru_t *)Aig_MmFlexEntryFetch( p->pMemTrus, nBytes );
     pEntry->Id = p->nEntries++;
     pEntry->nVars = nVars;
     pEntry->nVisits = 1;
     pEntry->pNext = NULL;
     memcpy( pEntry->pTruth, pTruth, sizeof(unsigned) * Kit_TruthWordNum(nVars) );
     *ppSpot = pEntry;
     return 1;
 }

static int Aig_RManTableHash	(	unsigned *	pTruth,
		int	nVars,
		int	nBins,
		int *	pPrimes
	)

inlinestatic

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

Synopsis [Returns the hash key.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file aigCanon.c.

 {
     int i, nWords = Kit_TruthWordNum( nVars );
     unsigned uHash = 0;
     for ( i = 0; i < nWords; i++ )
         uHash ^= pTruth[i] * pPrimes[i & 0xf];
     return (int)(uHash % nBins);
 }

Aig_Tru_t** Aig_RManTableLookup	(	Aig_RMan_t *	p,
		unsigned *	pTruth,
		int	nVars
	)

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

Synopsis [Returns the given record.]

Description []

SideEffects []

SeeAlso []

Definition at line 150 of file aigCanon.c.

 {
     static int s_Primes[16] = { 
         1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177, 
         4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
     Aig_Tru_t ** ppSpot, * pEntry;
     ppSpot = p->pBins + Aig_RManTableHash( pTruth, nVars, p->nBins, s_Primes );
     for ( pEntry = *ppSpot; pEntry; ppSpot = &pEntry->pNext, pEntry = pEntry->pNext )
         if ( Kit_TruthIsEqual( pEntry->pTruth, pTruth, nVars ) )
             return ppSpot;
     return ppSpot;
 }

void Aig_RManTableResize ( Aig_RMan_t * p )

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

Synopsis [Find or add new entry.]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file aigCanon.c.

 {
     Aig_Tru_t * pEntry, * pNext;
     Aig_Tru_t ** pBinsOld, ** ppPlace;
     int nBinsOld, Counter, i;
     abctime clk;
     assert( p->pBins != NULL );
 clk = Abc_Clock();
     // save the old Bins
     pBinsOld = p->pBins;
     nBinsOld = p->nBins;
     // get the new Bins
     p->nBins = Abc_PrimeCudd( 3 * nBinsOld ); 
     p->pBins = ABC_CALLOC( Aig_Tru_t *, p->nBins );
     // rehash the entries from the old table
     Counter = 0;
     for ( i = 0; i < nBinsOld; i++ )
     for ( pEntry = pBinsOld[i], pNext = pEntry? pEntry->pNext : NULL; 
           pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL )
     {
         // get the place where this entry goes in the Bins 
         ppPlace = Aig_RManTableLookup( p, pEntry->pTruth, pEntry->nVars );
         assert( *ppPlace == NULL ); // should not be there
         // add the entry to the list
         *ppPlace = pEntry;
         pEntry->pNext = NULL;
         Counter++;
     }
     assert( Counter == p->nEntries );
 //    ABC_PRT( "Time", Abc_Clock() - clk );
     ABC_FREE( pBinsOld );
 }

int Aig_RManVarsAreUnique	(	Aig_VSig_t *	pMints,
		int	nVars
	)

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

Synopsis [Returns 1 if all variables are unique.]

Description []

SideEffects []

SeeAlso []

Definition at line 427 of file aigCanon.c.

 {
     int i;
     for ( i = 0; i < nVars - 1; i++ )
         if ( Aig_RManCompareSigs( &pMints[2*i], &pMints[2*(i+1)], nVars ) == 0 )
             return 0;
     return 1;
 }