diff options
Diffstat (limited to 'src/misc/extra')
-rw-r--r-- | src/misc/extra/extraUtilEnum.c | 204 |
1 files changed, 204 insertions, 0 deletions
diff --git a/src/misc/extra/extraUtilEnum.c b/src/misc/extra/extraUtilEnum.c index f4ce65cd..432cb4d1 100644 --- a/src/misc/extra/extraUtilEnum.c +++ b/src/misc/extra/extraUtilEnum.c @@ -24,6 +24,7 @@ #include <assert.h> #include "misc/vec/vec.h" #include "misc/vec/vecHsh.h" +#include "bool/kit/kit.h" ABC_NAMESPACE_IMPL_START @@ -414,6 +415,209 @@ void Abc_EnumerateFunctions( int nDecMax ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#define ABC_ENUM_MAX 32 +static word s_Truths6[6] = { + ABC_CONST(0xAAAAAAAAAAAAAAAA), + ABC_CONST(0xCCCCCCCCCCCCCCCC), + ABC_CONST(0xF0F0F0F0F0F0F0F0), + ABC_CONST(0xFF00FF00FF00FF00), + ABC_CONST(0xFFFF0000FFFF0000), + ABC_CONST(0xFFFFFFFF00000000) +}; +typedef struct Abc_EnuMan_t_ Abc_EnuMan_t; +struct Abc_EnuMan_t_ +{ + int nVars; // support size + int nVarsFree; // number of PIs used + int fVerbose; // verbose flag + int nNodeMax; // the max number of nodes + int nNodes; // current number of gates + int nTops; // the number of fanoutless gates + int pFans0[ABC_ENUM_MAX]; // fanins + int pFans1[ABC_ENUM_MAX]; // fanins + int fCompl0[ABC_ENUM_MAX]; // complements + int fCompl1[ABC_ENUM_MAX]; // complements + int pRefs[ABC_ENUM_MAX]; // references + word pTruths[ABC_ENUM_MAX]; // truth tables + word nTries; // attempts to build a gate + word nBuilds; // actually built gates + word nFinished; // finished structures +}; +static inline void Abc_EnumRef( Abc_EnuMan_t * p, int i ) +{ + assert( p->pRefs[i] >= 0 ); + if ( p->pRefs[i]++ == 0 ) + p->nTops--; +} +static inline void Abc_EnumDeref( Abc_EnuMan_t * p, int i ) +{ + if ( --p->pRefs[i] == 0 ) + p->nTops++; + assert( p->pRefs[i] >= 0 ); +} +static inline void Abc_EnumRefNode( Abc_EnuMan_t * p, int i ) +{ + Abc_EnumRef( p, p->pFans0[i] ); + Abc_EnumRef( p, p->pFans1[i] ); + p->nTops++; + p->nNodes++; + assert( i < p->nNodes ); +} +static inline void Abc_EnumDerefNode( Abc_EnuMan_t * p, int i ) +{ + assert( i < p->nNodes ); + Abc_EnumDeref( p, p->pFans0[i] ); + Abc_EnumDeref( p, p->pFans1[i] ); + p->nTops--; + p->nNodes--; +} +static inline void Abc_EnumPrintOne( Abc_EnuMan_t * p ) +{ + int i; + Kit_DsdPrintFromTruth( (unsigned *)(p->pTruths + p->nNodes - 1), p->nVars ); + for ( i = p->nVars; i < p->nNodes; i++ ) + printf( " %c=%s%c%s%c", 'a'+i, p->fCompl0[i]?"!":"", 'a'+p->pFans0[i], p->fCompl1[i]?"!":"", 'a'+p->pFans1[i] ); + printf( "\n" ); +} +void Abc_EnumerateFuncs_rec( Abc_EnuMan_t * p ) +{ + word uTruth, uTemp; + word * pTruth = p->pTruths; + int f = p->nVarsFree; + int n = p->nNodes; + int i, k, c0, c1, t, a, b; + p->nBuilds++; + // terminate when enough and no new tops + if ( n == p->nNodeMax && p->nTops == 1 ) + { + if ( p->fVerbose ) + Abc_EnumPrintOne( p ); + p->nFinished++; + return; + } + if ( p->nTops > p->nNodeMax - n + 1 ) + return; + assert( n < p->nNodeMax ); + // try new gates with two inputs + if ( f >= 2 ) + { + p->pFans0[n] = f - 2; + p->pFans1[n] = f - 1; + p->fCompl0[n] = 0; + p->fCompl1[n] = 0; + p->pTruths[n] = pTruth[f - 2] & pTruth[f - 1]; + p->nVarsFree -= 2; + Abc_EnumRefNode( p, n ); + Abc_EnumerateFuncs_rec( p ); + Abc_EnumDerefNode( p, n ); + p->nVarsFree += 2; + return; + } + // try new gates with one input + if ( f > 0 ) + { + for ( i = f; i < n; i++ ) + for ( c0 = 0; c0 < 2; c0++ ) + { + uTruth = pTruth[f - 1] & (c0 ? ~pTruth[i] : pTruth[i]); + p->pFans0[n] = f - 1; + p->pFans1[n] = i; + p->fCompl0[n] = 0; + p->fCompl1[n] = c0; + p->pTruths[n] = uTruth; + p->nVarsFree--; + Abc_EnumRefNode( p, n ); + Abc_EnumerateFuncs_rec( p ); + Abc_EnumDerefNode( p, n ); + p->nVarsFree++; + } + return; + } + // try new gates without inputs + for ( i = f; i < n; i++ ) + for ( k = i+1; k < n; k++ ) + for ( c0 = 0; c0 < 2; c0++ ) + for ( c1 = 0; c1 < 2; c1++ ) + { + uTruth = (c0 ? ~pTruth[i] : pTruth[i]) & (c1 ? ~pTruth[k] : pTruth[k]); + if ( uTruth == 0 || ~uTruth == 0 ) + continue; + for ( t = f; t < n; t++ ) + if ( uTruth == p->pTruths[t] || ~uTruth == p->pTruths[t] ) + break; + if ( t < n ) + continue; + for ( a = f; a <= i; a++ ) + { + for ( b = a + 1; b <= k; b++ ) + { + if ( a == i && b == k ) + continue; + uTemp = p->pTruths[a] & p->pTruths[b]; + if ( uTruth == uTemp || ~uTruth == uTemp ) + break; + uTemp = p->pTruths[a] & ~p->pTruths[b]; + if ( uTruth == uTemp || ~uTruth == uTemp ) + break; + uTemp = ~p->pTruths[a] & p->pTruths[b]; + if ( uTruth == uTemp || ~uTruth == uTemp ) + break; + uTemp = ~p->pTruths[a] & ~p->pTruths[b]; + if ( uTruth == uTemp || ~uTruth == uTemp ) + break; + } + if ( b <= k ) + break; + } + if ( a <= i ) + continue; + p->pFans0[n] = i; + p->pFans1[n] = k; + p->fCompl0[n] = c0; + p->fCompl1[n] = c1; + p->pTruths[n] = uTruth; + Abc_EnumRefNode( p, n ); + Abc_EnumerateFuncs_rec( p ); + Abc_EnumDerefNode( p, n ); + } +} +void Abc_EnumerateFuncs( int nVars, int nGates, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Abc_EnuMan_t P, * p = &P; int i; + if ( nVars > nGates + 1 ) + { + printf( "The gate count %d is not enough to have functions with %d inputs.\n", nGates, nVars ); + return; + } + assert( nVars >= 3 && nVars <= 6 ); + assert( nGates > 0 && nVars + nGates < 16 ); + memset( p, 0, sizeof(Abc_EnuMan_t) ); + p->fVerbose = fVerbose; + p->nVars = nVars; + p->nVarsFree = nVars; + p->nNodeMax = nVars + nGates; + p->nNodes = nVars; + p->nTops = nVars; + for ( i = 0; i < nVars; i++ ) + p->pTruths[i] = s_Truths6[i]; + Abc_EnumerateFuncs_rec( p ); + printf( "Vars = %d. Gates = %d. Tries = %u. Builds = %u. Finished = %d. ", + nVars, nGates, (unsigned)p->nTries, (unsigned)p->nBuilds, (unsigned)p->nFinished ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |