mirror of https://github.com/YosysHQ/abc.git
Experiments with permutations.
This commit is contained in:
Alan Mishchenko
parent
76f2adb54f
commit
c4a715ed61
|
|
@ -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
|
||||
|
||||
|
|
@ -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 \
|
||||
|
|
|
|||
Loading…
Reference in New Issue