diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-20 23:56:48 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-20 23:56:48 -0700 |
commit | c4a715ed61353ae00bb418a5fb5646f1d8ddbbad (patch) | |
tree | 23df9477189353b3321896c99a78d31be9327ead /src | |
parent | 76f2adb54f011c319776eca9cdb278b753730e76 (diff) | |
download | abc-c4a715ed61353ae00bb418a5fb5646f1d8ddbbad.tar.gz abc-c4a715ed61353ae00bb418a5fb5646f1d8ddbbad.tar.bz2 abc-c4a715ed61353ae00bb418a5fb5646f1d8ddbbad.zip |
Experiments with permutations.
Diffstat (limited to 'src')
-rw-r--r-- | src/misc/extra/extraUtilPerm.c | 867 | ||||
-rw-r--r-- | src/misc/extra/module.make | 1 |
2 files changed, 868 insertions, 0 deletions
diff --git a/src/misc/extra/extraUtilPerm.c b/src/misc/extra/extraUtilPerm.c new file mode 100644 index 00000000..d5b8e080 --- /dev/null +++ b/src/misc/extra/extraUtilPerm.c @@ -0,0 +1,867 @@ +/**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_MULTIPLY, + 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; + int 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++; + 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 All = %d Hits = %d Miss = %d ", + p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses ); + printf( "Mem = %.2f MB\n", 4.0*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_ZddMultiply( Abc_ZddMan * p, int a, int Var ) +{ + Abc_ZddObj * A; + int r0, r1, r; + if ( a == 0 ) return 0; + if ( a == 1 ) return Abc_ZddIthVar(Var); + if ( (r = Abc_ZddCacheLookup(p, a, Var, ABC_ZDD_OPER_MULTIPLY)) >= 0 ) + return r; + A = Abc_ZddNode( p, a ); + if ( (int)A->Var > Var ) + r = Abc_ZddUniqueCreate( p, Var, a, 0 ); + else if ( (int)A->Var < Var ) + { + r0 = Abc_ZddMultiply( p, A->False, Var ), + r1 = Abc_ZddMultiply( p, A->True, Var ); + r = Abc_ZddUniqueCreate( p, A->Var, r1, r0 ); + } + else assert( 0 ); + return Abc_ZddCacheInsert( p, a, Var, ABC_ZDD_OPER_MULTIPLY, 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_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 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 ( (int)A->Var == Var ) + r = Abc_ZddUniqueCreate( p, A->Var, A->False, A->True ); + else if ( p->pV2TI[A->Var] > p->pV2TJ[Var] ) + r = Abc_ZddUniqueCreate( p, Var, a, 0 ); + else + { + int r0, r1, VarTop, VarPerm; + 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 ); + if ( Ai == Bj || (Ai == Bi && Aj > Bj) || (Aj == Bj && Ai > Bi) ) + VarTop = Var, + VarPerm = A->Var; + else if ( Ai == Bi ) + VarTop = A->Var, + VarPerm = Abc_ZddVarIJ(p, Aj, Bj); + else if ( Aj == Bj ) + VarTop = Abc_ZddVarIJ(p, Ai, Bi), + VarPerm = Abc_ZddVarIJ(p, Bi, Bj); + else if ( Aj == Bi ) + VarTop = A->Var, + VarPerm = Abc_ZddVarIJ(p, Ai, Bj); + else // no clash + VarTop = A->Var, + VarPerm = Var; + r0 = Abc_ZddPerm( p, A->False, Var ); + r1 = Abc_ZddPerm( p, A->True, VarPerm ); + if ( VarTop < Abc_ZddObjVar(p, r0) && VarTop < Abc_ZddObjVar(p, r1) ) + r = Abc_ZddUniqueCreate( p, VarTop, r1, r0 ); + else + { + r1 = Abc_ZddMultiply( p, r1, VarTop ); + 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 * A, * 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; + A = Abc_ZddNode( p, a ); + B = Abc_ZddNode( p, b ); + if ( Abc_ZddVarsClash(p, A->Var, B->Var) ) + { + 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, r1, r0 ); + assert( Abc_MinInt(A->Var, B->Var) <= (int)Abc_ZddObjVar(p, r) ); + } + else + { + if ( A->Var < B->Var ) + r0 = Abc_ZddPermProduct( p, A->False, b ), + r1 = Abc_ZddPermProduct( p, A->True, b ); + else if ( A->Var > B->Var ) + r0 = Abc_ZddPermProduct( p, a, B->False ), + r1 = Abc_ZddPermProduct( p, a, B->True ); + else assert( 0 ); + r = Abc_ZddUniqueCreate( p, Abc_MinInt(A->Var, B->Var), r1, r0 ); + } + 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( " %d", pPerm[i] ); + printf( " }\n" ); +} +void Abc_ZddCombPrint( int * pComb, int nTrans ) +{ + int i; + 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[10], pComb[10], i; + assert( p->nPermSize <= 10 ); + 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 ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index a21fd103..9c13c146 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -12,6 +12,7 @@ SRC += src/misc/extra/extraBddAuto.c \ src/misc/extra/extraUtilFile.c \ src/misc/extra/extraUtilMemory.c \ src/misc/extra/extraUtilMisc.c \ + src/misc/extra/extraUtilPerm.c \ src/misc/extra/extraUtilProgress.c \ src/misc/extra/extraUtilReader.c \ src/misc/extra/extraUtilTruth.c \ |