| /**CFile**************************************************************** |
| |
| FileName [extraUtilPerm.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [extra] |
| |
| Synopsis [Permutation computation.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: extraUtilPerm.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include <stdio.h> |
| #include <stdlib.h> |
| #include <string.h> |
| #include <assert.h> |
| #include "misc/vec/vec.h" |
| #include "aig/gia/gia.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| typedef enum |
| { |
| ABC_ZDD_OPER_NONE, |
| ABC_ZDD_OPER_DIFF, |
| ABC_ZDD_OPER_UNION, |
| ABC_ZDD_OPER_MIN_UNION, |
| ABC_ZDD_OPER_INTER, |
| ABC_ZDD_OPER_PERM, |
| ABC_ZDD_OPER_PERM_PROD, |
| ABC_ZDD_OPER_COF0, |
| ABC_ZDD_OPER_COF1, |
| ABC_ZDD_OPER_THRESH, |
| ABC_ZDD_OPER_DOT_PROD, |
| ABC_ZDD_OPER_DOT_PROD_6, |
| ABC_ZDD_OPER_INSERT, |
| ABC_ZDD_OPER_PATHS, |
| ABC_ZDD_OPER_NODES, |
| ABC_ZDD_OPER_ITE |
| } Abc_ZddOper; |
| |
| typedef struct Abc_ZddObj_ Abc_ZddObj; |
| struct Abc_ZddObj_ |
| { |
| unsigned Var : 31; |
| unsigned Mark : 1; |
| unsigned True; |
| unsigned False; |
| }; |
| |
| typedef struct Abc_ZddEnt_ Abc_ZddEnt; |
| struct Abc_ZddEnt_ |
| { |
| int Arg0; |
| int Arg1; |
| int Arg2; |
| int Res; |
| }; |
| |
| typedef struct Abc_ZddMan_ Abc_ZddMan; |
| struct Abc_ZddMan_ |
| { |
| int nVars; |
| int nObjs; |
| int nObjsAlloc; |
| int nPermSize; |
| unsigned nUniqueMask; |
| unsigned nCacheMask; |
| int * pUnique; |
| int * pNexts; |
| Abc_ZddEnt * pCache; |
| Abc_ZddObj * pObjs; |
| int nCacheLookups; |
| int nCacheMisses; |
| word nMemory; |
| int * pV2TI; |
| int * pV2TJ; |
| int * pT2V; |
| }; |
| |
| static inline int Abc_ZddIthVar( int i ) { return i + 2; } |
| static inline unsigned Abc_ZddHash( int Arg0, int Arg1, int Arg2 ) { return 12582917 * Arg0 + 4256249 * Arg1 + 741457 * Arg2; } |
| |
| static inline Abc_ZddObj * Abc_ZddNode( Abc_ZddMan * p, int i ) { return p->pObjs + i; } |
| static inline int Abc_ZddObjId( Abc_ZddMan * p, Abc_ZddObj * pObj ) { return pObj - p->pObjs; } |
| static inline int Abc_ZddObjVar( Abc_ZddMan * p, int i ) { return Abc_ZddNode(p, i)->Var; } |
| |
| static inline void Abc_ZddSetVarIJ( Abc_ZddMan * p, int i, int j, int v ) { assert( i < j ); p->pT2V[i * p->nPermSize + j] = v; } |
| static inline int Abc_ZddVarIJ( Abc_ZddMan * p, int i, int j ) { assert( i < j ); return p->pT2V[i * p->nPermSize + j]; } |
| static inline int Abc_ZddVarsClash( Abc_ZddMan * p, int v0, int v1 ) { return p->pV2TI[v0] == p->pV2TI[v1] || p->pV2TJ[v0] == p->pV2TJ[v1] || p->pV2TI[v0] == p->pV2TJ[v1] || p->pV2TJ[v0] == p->pV2TI[v1]; } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Abc_ZddCacheLookup( Abc_ZddMan * p, int Arg0, int Arg1, int Arg2 ) |
| { |
| Abc_ZddEnt * pEnt = p->pCache + (Abc_ZddHash(Arg0, Arg1, Arg2) & p->nCacheMask); |
| p->nCacheLookups++; |
| return (pEnt->Arg0 == Arg0 && pEnt->Arg1 == Arg1 && pEnt->Arg2 == Arg2) ? pEnt->Res : -1; |
| } |
| static inline int Abc_ZddCacheInsert( Abc_ZddMan * p, int Arg0, int Arg1, int Arg2, int Res ) |
| { |
| Abc_ZddEnt * pEnt = p->pCache + (Abc_ZddHash(Arg0, Arg1, Arg2) & p->nCacheMask); |
| pEnt->Arg0 = Arg0; pEnt->Arg1 = Arg1; pEnt->Arg2 = Arg2; pEnt->Res = Res; |
| p->nCacheMisses++; |
| assert( Res >= 0 ); |
| return Res; |
| } |
| static inline int Abc_ZddUniqueLookup( Abc_ZddMan * p, int Var, int True, int False ) |
| { |
| int *q = p->pUnique + (Abc_ZddHash(Var, True, False) & p->nUniqueMask); |
| for ( ; *q; q = p->pNexts + *q ) |
| if ( p->pObjs[*q].Var == (unsigned)Var && p->pObjs[*q].True == (unsigned)True && p->pObjs[*q].False == (unsigned)False ) |
| return *q; |
| return 0; |
| } |
| static inline int Abc_ZddUniqueCreate( Abc_ZddMan * p, int Var, int True, int False ) |
| { |
| assert( Var >= 0 && Var < p->nVars ); |
| assert( Var < Abc_ZddObjVar(p, True) ); |
| assert( Var < Abc_ZddObjVar(p, False) ); |
| if ( True == 0 ) |
| return False; |
| { |
| int *q = p->pUnique + (Abc_ZddHash(Var, True, False) & p->nUniqueMask); |
| for ( ; *q; q = p->pNexts + *q ) |
| if ( p->pObjs[*q].Var == (unsigned)Var && p->pObjs[*q].True == (unsigned)True && p->pObjs[*q].False == (unsigned)False ) |
| return *q; |
| if ( p->nObjs == p->nObjsAlloc ) |
| printf( "Aborting because the number of nodes exceeded %d.\n", p->nObjsAlloc ), fflush(stdout); |
| assert( p->nObjs < p->nObjsAlloc ); |
| *q = p->nObjs++; |
| p->pObjs[*q].Var = Var; |
| p->pObjs[*q].True = True; |
| p->pObjs[*q].False = False; |
| // printf( "Added node %3d: Var = %3d. True = %3d. False = %3d\n", *q, Var, True, False ); |
| return *q; |
| } |
| } |
| int Abc_ZddBuildSet( Abc_ZddMan * p, int * pSet, int Size ) |
| { |
| int i, Res = 1; |
| Vec_IntSelectSort( pSet, Size ); |
| for ( i = Size - 1; i >= 0; i-- ) |
| Res = Abc_ZddUniqueCreate( p, pSet[i], Res, 0 ); |
| return Res; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Abc_ZddMan * Abc_ZddManAlloc( int nVars, int nObjs ) |
| { |
| Abc_ZddMan * p; int i; |
| p = ABC_CALLOC( Abc_ZddMan, 1 ); |
| p->nVars = nVars; |
| p->nObjsAlloc = nObjs; |
| p->nUniqueMask = (1 << Abc_Base2Log(nObjs)) - 1; |
| p->nCacheMask = (1 << Abc_Base2Log(nObjs)) - 1; |
| p->pUnique = ABC_CALLOC( int, p->nUniqueMask + 1 ); |
| p->pNexts = ABC_CALLOC( int, p->nObjsAlloc ); |
| p->pCache = ABC_CALLOC( Abc_ZddEnt, p->nCacheMask + 1 ); |
| p->pObjs = ABC_CALLOC( Abc_ZddObj, p->nObjsAlloc ); |
| p->nObjs = 2; |
| memset( p->pObjs, 0xff, sizeof(Abc_ZddObj) * 2 ); |
| p->pObjs[0].Var = nVars; |
| p->pObjs[1].Var = nVars; |
| for ( i = 0; i < nVars; i++ ) |
| Abc_ZddUniqueCreate( p, i, 1, 0 ); |
| assert( p->nObjs == nVars + 2 ); |
| p->nMemory = sizeof(Abc_ZddMan)/4 + |
| p->nUniqueMask + 1 + p->nObjsAlloc + |
| (p->nCacheMask + 1) * sizeof(Abc_ZddEnt)/4 + |
| p->nObjsAlloc * sizeof(Abc_ZddObj)/4; |
| return p; |
| } |
| void Abc_ZddManCreatePerms( Abc_ZddMan * p, int nPermSize ) |
| { |
| int i, j, v = 0; |
| assert( 2 * p->nVars == nPermSize * (nPermSize - 1) ); |
| assert( p->nPermSize == 0 ); |
| p->nPermSize = nPermSize; |
| p->pV2TI = ABC_FALLOC( int, p->nVars ); |
| p->pV2TJ = ABC_FALLOC( int, p->nVars ); |
| p->pT2V = ABC_FALLOC( int, p->nPermSize * p->nPermSize ); |
| for ( i = 0; i < nPermSize; i++ ) |
| for ( j = i + 1; j < nPermSize; j++ ) |
| { |
| p->pV2TI[v] = i; |
| p->pV2TJ[v] = j; |
| Abc_ZddSetVarIJ( p, i, j, v++ ); |
| } |
| assert( v == p->nVars ); |
| } |
| void Abc_ZddManFree( Abc_ZddMan * p ) |
| { |
| printf( "ZDD stats: Var = %d Obj = %d Alloc = %d Hit = %d Miss = %d ", |
| p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses ); |
| printf( "Mem = %.2f MB\n", 4.0*(int)(p->nMemory/(1<<20)) ); |
| ABC_FREE( p->pT2V ); |
| ABC_FREE( p->pV2TI ); |
| ABC_FREE( p->pV2TJ ); |
| ABC_FREE( p->pUnique ); |
| ABC_FREE( p->pNexts ); |
| ABC_FREE( p->pCache ); |
| ABC_FREE( p->pObjs ); |
| ABC_FREE( p ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_ZddDiff( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * A, * B; |
| int r0, r1, r; |
| if ( a == 0 ) return 0; |
| if ( b == 0 ) return a; |
| if ( a == b ) return 0; |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DIFF)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| B = Abc_ZddNode( p, b ); |
| if ( A->Var < B->Var ) |
| r0 = Abc_ZddDiff( p, A->False, b ), |
| r = Abc_ZddUniqueCreate( p, A->Var, A->True, r0 ); |
| else if ( A->Var > B->Var ) |
| r = Abc_ZddDiff( p, a, B->False ); |
| else |
| r0 = Abc_ZddDiff( p, A->False, B->False ), |
| r1 = Abc_ZddDiff( p, A->True, B->True ), |
| r = Abc_ZddUniqueCreate( p, A->Var, A->True, r0 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DIFF, r ); |
| } |
| int Abc_ZddUnion( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * A, * B; |
| int r0, r1, r; |
| if ( a == 0 ) return b; |
| if ( b == 0 ) return a; |
| if ( a == b ) return a; |
| if ( a > b ) return Abc_ZddUnion( p, b, a ); |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_UNION)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| B = Abc_ZddNode( p, b ); |
| if ( A->Var < B->Var ) |
| r0 = Abc_ZddUnion( p, A->False, b ), |
| r1 = A->True; |
| else if ( A->Var > B->Var ) |
| r0 = Abc_ZddUnion( p, a, B->False ), |
| r1 = B->True; |
| else |
| r0 = Abc_ZddUnion( p, A->False, B->False ), |
| r1 = Abc_ZddUnion( p, A->True, B->True ); |
| r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_UNION, r ); |
| } |
| int Abc_ZddMinUnion( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * A, * B; |
| int r0, r1, r; |
| if ( a == 0 ) return b; |
| if ( b == 0 ) return a; |
| if ( a == b ) return a; |
| if ( a > b ) return Abc_ZddMinUnion( p, b, a ); |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_MIN_UNION)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| B = Abc_ZddNode( p, b ); |
| if ( A->Var < B->Var ) |
| r0 = Abc_ZddMinUnion( p, A->False, b ), |
| r1 = A->True; |
| else if ( A->Var > B->Var ) |
| r0 = Abc_ZddMinUnion( p, a, B->False ), |
| r1 = B->True; |
| else |
| r0 = Abc_ZddMinUnion( p, A->False, B->False ), |
| r1 = Abc_ZddMinUnion( p, A->True, B->True ); |
| r1 = Abc_ZddDiff( p, r1, r0 ); // assume args are minimal |
| r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_MIN_UNION, r ); |
| } |
| int Abc_ZddIntersect( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * A, * B; |
| int r0, r1, r; |
| if ( a == 0 ) return 0; |
| if ( b == 0 ) return 0; |
| if ( a == b ) return a; |
| if ( a > b ) return Abc_ZddIntersect( p, b, a ); |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_INTER)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| B = Abc_ZddNode( p, b ); |
| if ( A->Var < B->Var ) |
| r0 = Abc_ZddIntersect( p, A->False, b ), |
| r1 = A->True; |
| else if ( A->Var > B->Var ) |
| r0 = Abc_ZddIntersect( p, a, B->False ), |
| r1 = B->True; |
| else |
| r0 = Abc_ZddIntersect( p, A->False, B->False ), |
| r1 = Abc_ZddIntersect( p, A->True, B->True ); |
| r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_INTER, r ); |
| } |
| int Abc_ZddCof0( Abc_ZddMan * p, int a, int Var ) |
| { |
| Abc_ZddObj * A; |
| int r0, r1, r; |
| if ( a < 2 ) return a; |
| A = Abc_ZddNode( p, a ); |
| if ( (int)A->Var > Var ) |
| return a; |
| if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_COF0)) >= 0 ) |
| return r; |
| if ( (int)A->Var < Var ) |
| r0 = Abc_ZddCof0( p, A->False, Var ), |
| r1 = Abc_ZddCof0( p, A->True, Var ), |
| r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 ); |
| else |
| r = Abc_ZddCof0( p, A->False, Var ); |
| return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_COF0, r ); |
| } |
| int Abc_ZddCof1( Abc_ZddMan * p, int a, int Var ) |
| { |
| Abc_ZddObj * A; |
| int r0, r1, r; |
| if ( a < 2 ) return a; |
| A = Abc_ZddNode( p, a ); |
| if ( (int)A->Var > Var ) |
| return a; |
| if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_COF1)) >= 0 ) |
| return r; |
| if ( (int)A->Var < Var ) |
| r0 = Abc_ZddCof1( p, A->False, Var ), |
| r1 = Abc_ZddCof1( p, A->True, Var ); |
| else |
| r0 = 0, |
| r1 = Abc_ZddCof1( p, A->True, Var ); |
| r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 ); |
| return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_COF1, r ); |
| } |
| int Abc_ZddCountPaths( Abc_ZddMan * p, int a ) |
| { |
| Abc_ZddObj * A; |
| int r; |
| if ( a < 2 ) return a; |
| if ( (r = Abc_ZddCacheLookup(p, a, 0, ABC_ZDD_OPER_PATHS)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| r = Abc_ZddCountPaths( p, A->False ) + Abc_ZddCountPaths( p, A->True ); |
| return Abc_ZddCacheInsert( p, a, 0, ABC_ZDD_OPER_PATHS, r ); |
| } |
| /* |
| int Abc_ZddCountNodes( Abc_ZddMan * p, int a ) |
| { |
| Abc_ZddObj * A; |
| int r; |
| if ( a < 2 ) return 0; |
| if ( (r = Abc_ZddCacheLookup(p, a, 0, ABC_ZDD_OPER_NODES)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| r = 1 + Abc_ZddCountNodes( p, A->False ) + Abc_ZddCountNodes( p, A->True ); |
| return Abc_ZddCacheInsert( p, a, 0, ABC_ZDD_OPER_NODES, r ); |
| } |
| */ |
| int Abc_ZddCount_rec( Abc_ZddMan * p, int i ) |
| { |
| Abc_ZddObj * A; |
| if ( i < 2 ) |
| return 0; |
| A = Abc_ZddNode( p, i ); |
| if ( A->Mark ) |
| return 0; |
| A->Mark = 1; |
| return 1 + Abc_ZddCount_rec(p, A->False) + Abc_ZddCount_rec(p, A->True); |
| } |
| void Abc_ZddUnmark_rec( Abc_ZddMan * p, int i ) |
| { |
| Abc_ZddObj * A; |
| if ( i < 2 ) |
| return; |
| A = Abc_ZddNode( p, i ); |
| if ( !A->Mark ) |
| return; |
| A->Mark = 0; |
| Abc_ZddUnmark_rec( p, A->False ); |
| Abc_ZddUnmark_rec( p, A->True ); |
| } |
| int Abc_ZddCountNodes( Abc_ZddMan * p, int i ) |
| { |
| int Count = Abc_ZddCount_rec( p, i ); |
| Abc_ZddUnmark_rec( p, i ); |
| return Count; |
| } |
| int Abc_ZddCountNodesArray( Abc_ZddMan * p, Vec_Int_t * vNodes ) |
| { |
| int i, Id, Count = 0; |
| Vec_IntForEachEntry( vNodes, Id, i ) |
| Count += Abc_ZddCount_rec( p, Id ); |
| Vec_IntForEachEntry( vNodes, Id, i ) |
| Abc_ZddUnmark_rec( p, Id ); |
| return Count; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_ZddThresh( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * A; |
| int r0, r1, r; |
| if ( a < 2 ) return a; |
| if ( b == 0 ) return 0; |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_THRESH)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| r0 = Abc_ZddThresh( p, A->False, b ), |
| r1 = Abc_ZddThresh( p, A->True, b-1 ); |
| r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_THRESH, r ); |
| } |
| int Abc_ZddDotProduct( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * A, * B; |
| int r0, r1, b2, t1, t2, r; |
| if ( a == 0 ) return 0; |
| if ( b == 0 ) return 0; |
| if ( a == 1 ) return b; |
| if ( b == 1 ) return a; |
| if ( a > b ) return Abc_ZddDotProduct( p, b, a ); |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DOT_PROD)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| B = Abc_ZddNode( p, b ); |
| if ( A->Var < B->Var ) |
| r0 = Abc_ZddDotProduct( p, A->False, b ), |
| r1 = Abc_ZddDotProduct( p, A->True, b ); |
| else if ( A->Var > B->Var ) |
| r0 = Abc_ZddDotProduct( p, a, B->False ), |
| r1 = Abc_ZddDotProduct( p, a, B->True ); |
| else |
| r0 = Abc_ZddDotProduct( p, A->False, B->False ), |
| b2 = Abc_ZddUnion( p, B->False, B->True ), |
| t1 = Abc_ZddDotProduct( p, A->True, b2 ), |
| t2 = Abc_ZddDotProduct( p, A->False, B->True ), |
| r1 = Abc_ZddUnion( p, t1, t2 ); |
| r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DOT_PROD, r ); |
| } |
| int Abc_ZddDotMinProduct6( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * A, * B; |
| int r0, r1, b2, t1, t2, r; |
| if ( a == 0 ) return 0; |
| if ( b == 0 ) return 0; |
| if ( a == 1 ) return b; |
| if ( b == 1 ) return a; |
| if ( a > b ) return Abc_ZddDotMinProduct6( p, b, a ); |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_DOT_PROD_6)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| B = Abc_ZddNode( p, b ); |
| if ( A->Var < B->Var ) |
| r0 = Abc_ZddDotMinProduct6( p, A->False, b ), |
| r1 = Abc_ZddDotMinProduct6( p, A->True, b ); |
| else if ( A->Var > B->Var ) |
| r0 = Abc_ZddDotMinProduct6( p, a, B->False ), |
| r1 = Abc_ZddDotMinProduct6( p, a, B->True ); |
| else |
| r0 = Abc_ZddDotMinProduct6( p, A->False, B->False ), |
| b2 = Abc_ZddMinUnion( p, B->False, B->True ), |
| t1 = Abc_ZddDotMinProduct6( p, A->True, b2 ), |
| t2 = Abc_ZddDotMinProduct6( p, A->False, B->True ), |
| r1 = Abc_ZddMinUnion( p, t1, t2 ); |
| r1 = Abc_ZddThresh( p, r1, 5 ), |
| r1 = Abc_ZddDiff( p, r1, r0 ); |
| r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_DOT_PROD_6, r ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Abc_ZddPerm( Abc_ZddMan * p, int a, int Var ) |
| { |
| Abc_ZddObj * A; |
| int r0, r1, r; |
| assert( Var < p->nVars ); |
| if ( a == 0 ) return 0; |
| if ( a == 1 ) return Abc_ZddIthVar(Var); |
| if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_PERM)) >= 0 ) |
| return r; |
| A = Abc_ZddNode( p, a ); |
| if ( p->pV2TI[A->Var] > p->pV2TI[Var] ) // Ai > Bi |
| r = Abc_ZddUniqueCreate( p, Var, a, 0 ); |
| else if ( (int)A->Var == Var ) // Ai == Bi && Aj == Bj |
| r0 = Abc_ZddPerm( p, A->False, Var ), |
| r = Abc_ZddUnion( p, r0, A->True ); |
| else |
| { |
| int VarPerm, VarTop; |
| int Ai = p->pV2TI[A->Var]; |
| int Aj = p->pV2TJ[A->Var]; |
| int Bi = p->pV2TI[Var]; |
| int Bj = p->pV2TJ[Var]; |
| assert( Ai < Aj && Bi < Bj && Ai <= Bi ); |
| if ( Aj == Bi ) |
| VarPerm = Var, |
| VarTop = Abc_ZddVarIJ(p, Ai, Bj); |
| else if ( Aj == Bj ) |
| VarPerm = Var, |
| VarTop = Abc_ZddVarIJ(p, Ai, Bi); |
| else if ( Ai == Bi ) |
| VarPerm = Abc_ZddVarIJ(p, Abc_MinInt(Aj, Bj), Abc_MaxInt(Aj, Bj)), |
| VarTop = A->Var; |
| else // no clash |
| VarPerm = Var, |
| VarTop = A->Var; |
| assert( p->pV2TI[VarPerm] > p->pV2TI[VarTop] ); |
| r0 = Abc_ZddPerm( p, A->False, Var ); |
| r1 = Abc_ZddPerm( p, A->True, VarPerm ); |
| assert( Abc_ZddObjVar(p, r1) > VarTop ); |
| if ( Abc_ZddObjVar(p, r0) > VarTop ) |
| r = Abc_ZddUniqueCreate( p, VarTop, r1, r0 ); |
| else |
| r1 = Abc_ZddUniqueCreate( p, VarTop, r1, 0 ), |
| r = Abc_ZddUnion( p, r0, r1 ); |
| } |
| return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_PERM, r ); |
| } |
| int Abc_ZddPermProduct( Abc_ZddMan * p, int a, int b ) |
| { |
| Abc_ZddObj * B; |
| int r0, r1, r; |
| if ( a == 0 ) return 0; |
| if ( a == 1 ) return b; |
| if ( b == 0 ) return 0; |
| if ( b == 1 ) return a; |
| if ( (r = Abc_ZddCacheLookup(p, a, b, ABC_ZDD_OPER_PERM_PROD)) >= 0 ) |
| return r; |
| B = Abc_ZddNode( p, b ); |
| r0 = Abc_ZddPermProduct( p, a, B->False ); |
| r1 = Abc_ZddPermProduct( p, a, B->True ); |
| r1 = Abc_ZddPerm( p, r1, B->Var ); |
| r = Abc_ZddUnion( p, r0, r1 ); |
| return Abc_ZddCacheInsert( p, a, b, ABC_ZDD_OPER_PERM_PROD, r ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Printing permutations and transpositions.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_ZddPermPrint( int * pPerm, int Size ) |
| { |
| int i; |
| printf( "{" ); |
| for ( i = 0; i < Size; i++ ) |
| printf( " %2d", pPerm[i] ); |
| printf( " }\n" ); |
| } |
| void Abc_ZddCombPrint( int * pComb, int nTrans ) |
| { |
| int i; |
| if ( nTrans == 0 ) |
| printf( "Empty set" ); |
| for ( i = 0; i < nTrans; i++ ) |
| printf( "(%d %d)", pComb[i] >> 16, pComb[i] & 0xffff ); |
| printf( "\n" ); |
| } |
| int Abc_ZddPerm2Comb( int * pPerm, int Size, int * pComb ) |
| { |
| int i, j, nTrans = 0; |
| for ( i = 0; i < Size; i++ ) |
| if ( i != pPerm[i] ) |
| { |
| for ( j = i+1; j < Size; j++ ) |
| if ( i == pPerm[j] ) |
| break; |
| pComb[nTrans++] = (i << 16) | j; |
| ABC_SWAP( int, pPerm[i], pPerm[j] ); |
| assert( i == pPerm[i] ); |
| } |
| return nTrans; |
| } |
| void Abc_ZddComb2Perm( int * pComb, int nTrans, int * pPerm, int Size ) |
| { |
| int v; |
| for ( v = 0; v < Size; v++ ) |
| pPerm[v] = v; |
| for ( v = nTrans-1; v >= 0; v-- ) |
| ABC_SWAP( int, pPerm[pComb[v] >> 16], pPerm[pComb[v] & 0xffff] ); |
| } |
| void Abc_ZddPermCombTest() |
| { |
| int Size = 10; |
| int pPerm[10] = { 6, 5, 7, 0, 3, 2, 1, 8, 9, 4 }; |
| int pComb[10], nTrans; |
| Abc_ZddPermPrint( pPerm, Size ); |
| nTrans = Abc_ZddPerm2Comb( pPerm, Size, pComb ); |
| Abc_ZddCombPrint( pComb, nTrans ); |
| Abc_ZddComb2Perm( pComb, nTrans, pPerm, Size ); |
| Abc_ZddPermPrint( pPerm, Size ); |
| Size = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Printing ZDDs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_ZddPrint_rec( Abc_ZddMan * p, int a, int * pPath, int Size ) |
| { |
| Abc_ZddObj * A; |
| if ( a == 0 ) return; |
| // if ( a == 1 ) { Abc_ZddPermPrint( pPath, Size ); return; } |
| if ( a == 1 ) |
| { |
| int pPerm[24], pComb[24], i; |
| assert( p->nPermSize <= 24 ); |
| for ( i = 0; i < Size; i++ ) |
| pComb[i] = (p->pV2TI[pPath[i]] << 16) | p->pV2TJ[pPath[i]]; |
| Abc_ZddCombPrint( pComb, Size ); |
| Abc_ZddComb2Perm( pComb, Size, pPerm, p->nPermSize ); |
| Abc_ZddPermPrint( pPerm, p->nPermSize ); |
| return; |
| } |
| A = Abc_ZddNode( p, a ); |
| Abc_ZddPrint_rec( p, A->False, pPath, Size ); |
| pPath[Size] = A->Var; |
| Abc_ZddPrint_rec( p, A->True, pPath, Size + 1 ); |
| } |
| void Abc_ZddPrint( Abc_ZddMan * p, int a ) |
| { |
| int * pPath = ABC_CALLOC( int, p->nVars ); |
| Abc_ZddPrint_rec( p, a, pPath, 0 ); |
| ABC_FREE( pPath ); |
| } |
| void Abc_ZddPrintTest( Abc_ZddMan * p ) |
| { |
| // int nSets = 2; |
| // int Size = 2; |
| // int pSets[2][2] = { {5, 0}, {3, 11} }; |
| int nSets = 3; |
| int Size = 5; |
| int pSets[3][5] = { {5, 0, 2, 10, 7}, {3, 11, 10, 7, 2}, {0, 2, 5, 10, 7} }; |
| int i, Set, Union = 0; |
| for ( i = 0; i < nSets; i++ ) |
| { |
| Abc_ZddPermPrint( pSets[i], Size ); |
| Set = Abc_ZddBuildSet( p, pSets[i], Size ); |
| Union = Abc_ZddUnion( p, Union, Set ); |
| } |
| printf( "Resulting set:\n" ); |
| Abc_ZddPrint( p, Union ); |
| printf( "\n" ); |
| printf( "Nodes = %d. Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) ); |
| Size = 0; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_ZddGiaTest( Gia_Man_t * pGia ) |
| { |
| Abc_ZddMan * p; |
| Gia_Obj_t * pObj; |
| Vec_Int_t * vNodes; |
| int i, r, Paths = 0; |
| p = Abc_ZddManAlloc( Gia_ManObjNum(pGia), 1 << 24 ); // 576 MB (36 B/node) |
| Gia_ManFillValue( pGia ); |
| Gia_ManForEachCi( pGia, pObj, i ) |
| pObj->Value = Abc_ZddIthVar( Gia_ObjId(pGia, pObj) ); |
| vNodes = Vec_IntAlloc( Gia_ManAndNum(pGia) ); |
| Gia_ManForEachAnd( pGia, pObj, i ) |
| { |
| r = Abc_ZddDotMinProduct6( p, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); |
| r = Abc_ZddUnion( p, r, Abc_ZddIthVar(i) ); |
| pObj->Value = r; |
| Vec_IntPush( vNodes, r ); |
| // print |
| // printf( "Node %d:\n", i ); |
| // Abc_ZddPrint( p, r ); |
| // printf( "Node %d ZddNodes = %d\n", i, Abc_ZddCountNodes(p, r) ); |
| } |
| Gia_ManForEachAnd( pGia, pObj, i ) |
| Paths += Abc_ZddCountPaths(p, pObj->Value); |
| printf( "Paths = %d. Shared nodes = %d.\n", Paths, Abc_ZddCountNodesArray(p, vNodes) ); |
| Vec_IntFree( vNodes ); |
| Abc_ZddManFree( p ); |
| } |
| /* |
| abc 01> &r pj1.aig; &ps; &test |
| pj1 : i/o = 1769/ 1063 and = 16285 lev = 156 (12.91) mem = 0.23 MB |
| Paths = 839934. Shared nodes = 770999. |
| ZDD stats: Var = 19118 Obj = 11578174 All = 16777216 Hits = 25617277 Miss = 40231476 Mem = 576.00 MB |
| */ |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_ZddPermTestInt( Abc_ZddMan * p ) |
| { |
| int nPerms = 3; |
| int Size = 5; |
| int pPerms[3][5] = { {1, 0, 2, 4, 3}, {1, 2, 4, 0, 3}, {0, 3, 2, 1, 4} }; |
| int pComb[5], nTrans; |
| int i, k, Set, Union = 0, iPivot; |
| for ( i = 0; i < nPerms; i++ ) |
| Abc_ZddPermPrint( pPerms[i], Size ); |
| for ( i = 0; i < nPerms; i++ ) |
| { |
| printf( "Perm %d:\n", i ); |
| Abc_ZddPermPrint( pPerms[i], Size ); |
| nTrans = Abc_ZddPerm2Comb( pPerms[i], Size, pComb ); |
| Abc_ZddCombPrint( pComb, nTrans ); |
| for ( k = 0; k < nTrans; k++ ) |
| pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xFFFF ); |
| Abc_ZddPermPrint( pComb, nTrans ); |
| // add to ZDD |
| Set = Abc_ZddBuildSet( p, pComb, nTrans ); |
| Union = Abc_ZddUnion( p, Union, Set ); |
| } |
| printf( "\nResulting set of permutations:\n" ); |
| Abc_ZddPrint( p, Union ); |
| printf( "Nodes = %d. Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) ); |
| |
| iPivot = Abc_ZddVarIJ( p, 3, 4 ); |
| Union = Abc_ZddPerm( p, Union, iPivot ); |
| |
| printf( "\nResulting set of permutations:\n" ); |
| Abc_ZddPrint( p, Union ); |
| printf( "Nodes = %d. Path = %d.\n", Abc_ZddCountNodes(p, Union), Abc_ZddCountPaths(p, Union) ); |
| printf( "\n" ); |
| } |
| |
| void Abc_ZddPermTest() |
| { |
| Abc_ZddMan * p; |
| p = Abc_ZddManAlloc( 10, 1 << 20 ); |
| Abc_ZddManCreatePerms( p, 5 ); |
| Abc_ZddPermTestInt( p ); |
| Abc_ZddManFree( p ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_EnumerateCubeStatesZdd() |
| { |
| int pXYZ[3][9][2] = { |
| { {3, 5}, {3,17}, {3,15}, {1, 6}, {1,16}, {1,14}, {2, 4}, {2,18}, {2,13} }, |
| { {2,14}, {2,24}, {2,12}, {3,13}, {3,23}, {3,10}, {1,15}, {1,22}, {1,11} }, |
| { {1,10}, {1, 7}, {1, 4}, {3,12}, {3, 9}, {3, 6}, {2,11}, {2, 8}, {2, 5} } }; |
| #ifdef WIN32 |
| int LogObj = 24; |
| #else |
| int LogObj = 27; |
| #endif |
| Abc_ZddMan * p; |
| int i, k, pComb[9], pPerm[24], nSize; |
| int ZddTurn1, ZddTurn2, ZddTurn3, ZddTurns, ZddAll; |
| abctime clk = Abc_Clock(); |
| printf( "Enumerating states of 2x2x2 cube.\n" ); |
| p = Abc_ZddManAlloc( 24 * 23 / 2, 1 << LogObj ); // finished with 2^27 (4 GB) |
| Abc_ZddManCreatePerms( p, 24 ); |
| // init state |
| printf( "Iter %2d -> %8d Nodes = %7d Used = %10d ", 0, 1, 0, 2 ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| // first 9 states |
| ZddTurns = 1; |
| for ( i = 0; i < 3; i++ ) |
| { |
| for ( k = 0; k < 24; k++ ) |
| pPerm[k] = k; |
| for ( k = 0; k < 9; k++ ) |
| ABC_SWAP( int, pPerm[pXYZ[i][k][0]-1], pPerm[pXYZ[i][k][1]-1] ); |
| nSize = Abc_ZddPerm2Comb( pPerm, 24, pComb ); |
| assert( nSize == 9 ); |
| for ( k = 0; k < 9; k++ ) |
| pComb[k] = Abc_ZddVarIJ( p, pComb[k] >> 16, pComb[k] & 0xffff ); |
| // add first turn |
| ZddTurn1 = Abc_ZddBuildSet( p, pComb, 9 ); |
| ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn1 ); |
| //Abc_ZddPrint( p, ZddTurn1 ); |
| // add second turn |
| ZddTurn2 = Abc_ZddPermProduct( p, ZddTurn1, ZddTurn1 ); |
| ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn2 ); |
| //Abc_ZddPrint( p, ZddTurn2 ); |
| // add third turn |
| ZddTurn3 = Abc_ZddPermProduct( p, ZddTurn2, ZddTurn1 ); |
| ZddTurns = Abc_ZddUnion( p, ZddTurns, ZddTurn3 ); |
| //Abc_ZddPrint( p, ZddTurn3 ); |
| //printf( "\n" ); |
| } |
| //Abc_ZddPrint( p, ZddTurns ); |
| printf( "Iter %2d -> %8d Nodes = %7d Used = %10d ", 1, Abc_ZddCountPaths(p, ZddTurns), Abc_ZddCountNodes(p, ZddTurns), p->nObjs ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| // other states |
| ZddAll = ZddTurns; |
| for ( i = 2; i <= 100; i++ ) |
| { |
| int ZddAllPrev = ZddAll; |
| ZddAll = Abc_ZddPermProduct( p, ZddAll, ZddTurns ); |
| printf( "Iter %2d -> %8d Nodes = %7d Used = %10d ", i, Abc_ZddCountPaths(p, ZddAll), Abc_ZddCountNodes(p, ZddAll), p->nObjs ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| if ( ZddAllPrev == ZddAll ) |
| break; |
| } |
| Abc_ZddManFree( p ); |
| } |
| |
| /* |
| Enumerating states of 2x2x2 cube. |
| Iter 0 -> 1 Nodes = 0 Used = 2 Time = 0.00 sec |
| Iter 1 -> 10 Nodes = 63 Used = 577 Time = 0.00 sec |
| Iter 2 -> 64 Nodes = 443 Used = 4349 Time = 0.03 sec |
| Iter 3 -> 385 Nodes = 2018 Used = 26654 Time = 0.14 sec |
| Iter 4 -> 2232 Nodes = 7451 Used = 119442 Time = 0.45 sec |
| Iter 5 -> 12224 Nodes = 25178 Used = 490038 Time = 1.10 sec |
| Iter 6 -> 62360 Nodes = 83955 Used = 1919750 Time = 1.79 sec |
| Iter 7 -> 289896 Nodes = 290863 Used = 7182932 Time = 3.15 sec |
| Iter 8 -> 1159968 Nodes = 614845 Used = 25301123 Time = 8.03 sec |
| Iter 9 -> 3047716 Nodes = 585664 Used = 66228369 Time = 20.22 sec |
| Iter 10 -> 3671516 Nodes = 19430 Used = 102292452 Time = 33.41 sec |
| Iter 11 -> 3674160 Nodes = 511 Used = 103545878 Time = 33.92 sec |
| Iter 12 -> 3674160 Nodes = 511 Used = 103566266 Time = 33.93 sec |
| ZDD stats: Var = 276 Obj = 103566266 Alloc = 134217728 Hit = 63996630 Miss = 141768893 Mem = 4608.00 MB |
| */ |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
