/**CFile****************************************************************
FileName [dau.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware unmapping.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dau.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dauInt.h"
#include "misc/util/utilTruth.h"
#include "misc/extra/extra.h"
#include "bool/lucky/lucky.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
//#define USE4VARS 1
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_TruthEnum()
{
int fUseTable = 1;
abctime clk = Abc_Clock();
#ifdef USE4VARS
int nVars = 4;
int nSizeW = 1 << 14;
char * pFileName = "tableW14.data";
#else
int nVars = 5;
int nSizeW = 1 << 30;
char * pFileName = "tableW30.data";
#endif
int nPerms = Extra_Factorial( nVars );
int nMints = 1 << nVars;
int * pPerm = Extra_PermSchedule( nVars );
int * pComp = Extra_GreyCodeSchedule( nVars );
word nFuncs = ((word)1 << (((word)1 << nVars)-1));
word * pPres = ABC_CALLOC( word, 1 << ((1<<nVars)-7) );
unsigned * pTable = fUseTable ? (unsigned *)ABC_CALLOC(word, nSizeW) : NULL;
Vec_Int_t * vNpns = Vec_IntAlloc( 1000 );
word tMask = Abc_Tt6Mask( 1 << nVars );
word tTemp, tCur;
int i, k;
if ( pPres == NULL )
{
printf( "Cannot alloc memory for marks.\n" );
return;
}
if ( pTable == NULL )
printf( "Cannot alloc memory for table.\n" );
for ( tCur = 0; tCur < nFuncs; tCur++ )
{
if ( (tCur & 0x3FFFF) == 0 )
{
printf( "Finished %08x. Classes = %6d. ", (int)tCur, Vec_IntSize(vNpns) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
fflush(stdout);
}
if ( Abc_TtGetBit(pPres, (int)tCur) )
continue;
//Extra_PrintBinary( stdout, (unsigned *)&tCur, 16 ); printf( " %04x\n", (int)tCur );
//Dau_DsdPrintFromTruth( &tCur, 4 ); printf( "\n" );
Vec_IntPush( vNpns, (int)tCur );
tTemp = tCur;
for ( i = 0; i < nPerms; i++ )
{
for ( k = 0; k < nMints; k++ )
{
if ( tCur < nFuncs )
{
if ( pTable ) pTable[(int)tCur] = tTemp;
Abc_TtSetBit( pPres, (int)tCur );
}
if ( (tMask & ~tCur) < nFuncs )
{
if ( pTable ) pTable[(int)(tMask & ~tCur)] = tTemp;
Abc_TtSetBit( pPres, (int)(tMask & ~tCur) );
}
tCur = Abc_Tt6Flip( tCur, pComp[k] );
}
tCur = Abc_Tt6SwapAdjacent( tCur, pPerm[i] );
}
assert( tTemp == tCur );
}
printf( "Computed %d NPN classes of %d variables. ", Vec_IntSize(vNpns), nVars );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
fflush(stdout);
Vec_IntFree( vNpns );
ABC_FREE( pPres );
ABC_FREE( pPerm );
ABC_FREE( pComp );
// write into file
if ( pTable )
{
FILE * pFile = fopen( pFileName, "wb" );
int RetValue = fwrite( pTable, 8, nSizeW, pFile );
RetValue = 0;
fclose( pFile );
ABC_FREE( pTable );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Dau_ReadFile( char * pFileName, int nSizeW )
{
abctime clk = Abc_Clock();
FILE * pFile = fopen( pFileName, "rb" );
unsigned * p = (unsigned *)ABC_CALLOC(word, nSizeW);
int RetValue = pFile ? fread( p, sizeof(word), nSizeW, pFile ) : 0;
RetValue = 0;
if ( pFile )
{
printf( "Finished reading file \"%s\".\n", pFileName );
fclose( pFile );
}
else
printf( "Cannot open input file \"%s\".\n", pFileName );
Abc_PrintTime( 1, "File reading", Abc_Clock() - clk );
return p;
}
int Dau_AddFunction( word tCur, int nVars, unsigned * pTable, Vec_Int_t * vNpns, Vec_Int_t * vNpns_ )
{
int Digit = (1 << nVars)-1;
word tMask = Abc_Tt6Mask( 1 << nVars );
word tNorm = (tCur >> Digit) & 1 ? ~tCur : tCur;
unsigned t = (unsigned)(tNorm & tMask);
unsigned tRep = pTable[t] & 0x7FFFFFFF;
unsigned tRep2 = pTable[tRep];
assert( ((tNorm >> Digit) & 1) == 0 );
if ( (tRep2 >> 31) == 0 ) // first time
{
Vec_IntPush( vNpns, tRep2 );
if ( Abc_TtSupportSize(&tCur, nVars) < nVars )
Vec_IntPush( vNpns_, tRep2 );
pTable[tRep] = tRep2 | (1 << 31);
return tRep2;
}
return 0;
}
void Dau_NetworkEnum()
{
abctime clk = Abc_Clock();
int Limit = 2;
int UseTwo = 0;
#ifdef USE4VARS
int nVars = 4;
int nSizeW = 1 << 14;
char * pFileName = "tableW14.data";
#else
int nVars = 5;
int nSizeW = 1 << 30;
char * pFileName = "tableW30.data";
#endif
unsigned * pTable = Dau_ReadFile( pFileName, nSizeW );
Vec_Wec_t * vNpns = Vec_WecStart( 32 );
Vec_Wec_t * vNpns_ = Vec_WecStart( 32 );
int i, v, u, g, k, m, n, Res, Entry;
unsigned Inv = (unsigned)Abc_Tt6Mask(1 << (nVars-1));
// create constant function and buffer/inverter function
pTable[0] |= (1 << 31);
pTable[Inv] |= (1 << 31);
Vec_IntPushTwo( Vec_WecEntry(vNpns, 0), 0, Inv );
Vec_IntPushTwo( Vec_WecEntry(vNpns_, 0), 0, Inv );
printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
0, Vec_IntSize(Vec_WecEntry(vNpns, 0)), Vec_WecSizeSize(vNpns),
Vec_IntSize(Vec_WecEntry(vNpns_, 0)), Vec_WecSizeSize(vNpns_) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// numerate other functions based on how many nodes they have
for ( n = 1; n < 32; n++ )
{
Vec_Int_t * vFuncsN2 = n > 1 ? Vec_WecEntry( vNpns, n-2 ) : NULL;
Vec_Int_t * vFuncsN1 = Vec_WecEntry( vNpns, n-1 );
Vec_Int_t * vFuncsN = Vec_WecEntry( vNpns, n );
Vec_Int_t * vFuncsN_ = Vec_WecEntry( vNpns_,n );
Vec_IntForEachEntry( vFuncsN1, Entry, i )
{
word uTruth = (((word)Entry) << 32) | (word)Entry;
int nSupp = Abc_TtSupportSize( &uTruth, nVars );
assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
//printf( "Exploring function %4d with %d vars: ", i, nSupp );
//printf( " %04x\n", (int)uTruth );
//Dau_DsdPrintFromTruth( &uTruth, 4 );
for ( v = 0; v < nSupp; v++ )
{
word tGate, tCur;
word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
for ( g = 0; g < Limit; g++ )
{
if ( nSupp < nVars )
{
if ( g == 0 )
{
tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-nSupp];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
}
else
{
tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-nSupp];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
}
}
}
for ( g = 0; g < Limit; g++ )
{
// add one cross bar
for ( k = 0; k < nSupp; k++ ) if ( k != v )
{
if ( g == 0 )
{
tGate = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tGate = s_Truths6[nVars-1-v] & ~s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
}
else
{
tGate = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
}
}
}
for ( g = 0; g < Limit; g++ )
{
// add two cross bars
for ( k = 0; k < nSupp; k++ ) if ( k != v )
for ( m = k+1; m < nSupp; m++ ) if ( m != v )
{
if ( g == 0 )
{
tGate = s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tGate = s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tGate = ~s_Truths6[nVars-1-m] & s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tGate = ~s_Truths6[nVars-1-m] & ~s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
}
else
{
tGate = s_Truths6[nVars-1-m] ^ s_Truths6[nVars-1-k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
}
}
}
}
}
if ( UseTwo && vFuncsN2 )
Vec_IntForEachEntry( vFuncsN2, Entry, i )
{
word uTruth = (((word)Entry) << 32) | (word)Entry;
int nSupp = Abc_TtSupportSize( &uTruth, nVars );
assert( nSupp == 6 || !Abc_Tt6HasVar(uTruth, nVars-1-nSupp) );
//printf( "Exploring function %4d with %d vars: ", i, nSupp );
//printf( " %04x\n", (int)uTruth );
//Dau_DsdPrintFromTruth( &uTruth, 4 );
for ( v = 0; v < nSupp; v++ )
// for ( u = v+1; u < nSupp; u++ ) if ( u != v )
for ( u = 0; u < nSupp; u++ ) if ( u != v )
{
word tGate1, tGate2, tCur;
word Cof0 = Abc_Tt6Cofactor0( uTruth, nVars-1-v );
word Cof1 = Abc_Tt6Cofactor1( uTruth, nVars-1-v );
word Cof00 = Abc_Tt6Cofactor0( Cof0, nVars-1-u );
word Cof01 = Abc_Tt6Cofactor1( Cof0, nVars-1-u );
word Cof10 = Abc_Tt6Cofactor0( Cof1, nVars-1-u );
word Cof11 = Abc_Tt6Cofactor1( Cof1, nVars-1-u );
tGate1 = s_Truths6[nVars-1-v] & s_Truths6[nVars-1-u];
tGate2 = s_Truths6[nVars-1-v] ^ s_Truths6[nVars-1-u];
Cof0 = (tGate2 & Cof00) | (~tGate2 & Cof01);
Cof1 = (tGate2 & Cof10) | (~tGate2 & Cof11);
tCur = (tGate1 & Cof1) | (~tGate1 & Cof0);
Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
if ( Res )
printf( "Found function %d\n", Res );
tCur = (tGate1 & Cof0) | (~tGate1 & Cof1);
Res = Dau_AddFunction( tCur, nVars, pTable, vFuncsN, vFuncsN_ );
if ( Res )
printf( "Found function %d\n", Res );
}
}
printf("Nodes = %2d. New = %6d. Total = %6d. New = %6d. Total = %6d. ",
n, Vec_IntSize(vFuncsN), Vec_WecSizeSize(vNpns), Vec_IntSize(vFuncsN_), Vec_WecSizeSize(vNpns_) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
fflush(stdout);
if ( Vec_IntSize(vFuncsN) == 0 )
break;
}
// printf( "Functions with 7 nodes:\n" );
// Vec_IntForEachEntry( Vec_WecEntry(vNpns_,7), Entry, i )
// printf( "%04x ", Entry );
// printf( "\n" );
Vec_WecFree( vNpns );
Vec_WecFree( vNpns_ );
ABC_FREE( pTable );
Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
fflush(stdout);
}
void Dau_NetworkEnumTest()
{
//Dau_TruthEnum();
Dau_NetworkEnum();
}
/**Function*************************************************************
Synopsis [Count the number of symmetric pairs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_CountSymms( word t, int nVars )
{
word Cof0, Cof1;
int i, j, nPairs = 0;
for ( i = 0; i < nVars; i++ )
for ( j = i+1; j < nVars; j++ )
nPairs += Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1);
return nPairs;
}
int Dau_CountSymms2( word t, int nVars )
{
word Cof0, Cof1;
int i, j, SymVars = 0;
for ( i = 0; i < nVars; i++ )
for ( j = i+1; j < nVars; j++ )
if ( Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1) )
SymVars |= (1 << j);
return SymVars;
}
int Dau_CountCompl1( word t, int v, int nVars )
{
word tNew = Abc_Tt6Flip(t, v);
int k;
if ( tNew == ~t )
return 1;
for ( k = 0; k < nVars; k++ ) if ( k != v )
if ( tNew == Abc_Tt6Flip(t, k) )
return 1;
return 0;
}
int Dau_CountCompl( word t, int nVars )
{
int i, nPairs = 0;
for ( i = 0; i < nVars; i++ )
nPairs += Dau_CountCompl1(t, i, nVars);
return nPairs;
}
/**Function*************************************************************
Synopsis [Performs exact canonicization of semi-canonical classes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wrd_t * Dau_ExactNpnForClasses( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs )
{
Vec_Wrd_t * vCanons = Vec_WrdStart( Vec_IntSize(vNodSup) );
word pAuxWord[1024], pAuxWord1[1024];
word uTruth; int i, Entry;
permInfo * pi = setPermInfoPtr(nVars);
Vec_IntForEachEntry( vNodSup, Entry, i )
{
if ( (Entry & 0xF) > nVars )
continue;
uTruth = *Vec_MemReadEntry( vTtMem, i );
simpleMinimal(&uTruth, pAuxWord, pAuxWord1, pi, nVars);
Vec_WrdWriteEntry( vCanons, i, uTruth );
}
freePermInfoPtr(pi);
return vCanons;
}
void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nInputs, int nNodesMax )
{
abctime clk = Abc_Clock(); int n, nTotal = 0;
Vec_Wrd_t * vCanons = Dau_ExactNpnForClasses( vTtMem, vNodSup, nVars, nInputs );
Vec_Mem_t * vTtMem2 = Vec_MemAlloc( Vec_MemEntrySize(vTtMem), 10 );
Vec_MemHashAlloc( vTtMem2, 1<<10 );
Abc_PrintTime( 1, "Exact NPN computation time", Abc_Clock() - clk );
printf( "Final results:\n" );
for ( n = 0; n <= nNodesMax; n++ )
{
int i, Entry, Entry2, nEntries2, Counter = 0, Counter2 = 0;
Vec_IntForEachEntry( vNodSup, Entry, i )
{
if ( (Entry & 0xF) > nVars || (Entry >> 16) != n )
continue;
Counter++;
nEntries2 = Vec_MemEntryNum(vTtMem2);
Entry2 = Vec_MemHashInsert( vTtMem2, Vec_WrdEntryP(vCanons, i) );
if ( nEntries2 == Vec_MemEntryNum(vTtMem2) ) // found in the table - not new
continue;
Counter2++;
}
nTotal += Counter2;
printf( "Nodes = %2d. ", n );
printf( "Semi-canonical = %8d. ", Counter );
printf( "Canonical = %8d. ", Counter2 );
printf( "Total = %8d.", nTotal );
printf( "\n" );
}
Vec_MemHashFree( vTtMem2 );
Vec_MemFreeP( &vTtMem2 );
Vec_WrdFree( vCanons );
fflush(stdout);
}
/**Function*************************************************************
Synopsis [Saving hash tables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_TablesSave( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk )
{
FILE * pFile;
char FileName[100];
int i, nWords = Abc_TtWordNum(nInputs);
// NPN classes
sprintf( FileName, "npn%d%d.ttd", nInputs, nVars );
pFile = fopen( FileName, "wb" );
for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
fwrite( Vec_MemReadEntry(vTtMem, i), 8, nWords, pFile );
fwrite( Vec_IntArray(vNodSup), 4, Vec_IntSize(vNodSup), pFile );
fclose( pFile );
// printf( "Dumped files with %10d classes after exploring %10d frontiers.\n",
// Vec_IntSize(vNodSup), nFronts );
printf( "Dumped file \"%s\" with %10d classes after exploring %10d frontiers. ",
FileName, Vec_IntSize(vNodSup), nFronts );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
fflush(stdout);
}
/**Function*************************************************************
Synopsis [Dump functions by the number of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DumpFuncs( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int nMax )
{
FILE * pFile[20];
int Counters[20] = {0};
int n, i;
assert( nVars == 4 || nVars == 5 );
for ( n = 0; n <= nMax; n++ )
{
char FileName[100];
sprintf( FileName, "func%d_min%d.tt", nVars, n );
pFile[n] = fopen( FileName, "wb" );
}
for ( i = 0; i < Vec_MemEntryNum(vTtMem); i++ )
{
word * pTruth = Vec_MemReadEntry( vTtMem, i );
int NodSup = Vec_IntEntry( vNodSup, i );
if ( (NodSup & 0xF) != nVars )
continue;
Counters[NodSup >> 16]++;
if ( nVars == 4 )
fprintf( pFile[NodSup >> 16], "%04x\n", (int)(0xFFFF & pTruth[0]) );
else if ( nVars == 5 )
fprintf( pFile[NodSup >> 16], "%08x\n", (int)(0xFFFFFFFF & pTruth[0]) );
}
for ( n = 0; n <= nMax; n++ )
{
printf( "Dumped %8d %d-node %d-input functions into file.\n", Counters[n], n, nVars );
fclose( pFile[n] );
}
}
/**Function*************************************************************
Synopsis [Function enumeration.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_CountFuncs( Vec_Int_t * vNodSup, int iStart, int iStop, int nVars )
{
int i, Entry, Count = 0;
Vec_IntForEachEntryStartStop( vNodSup, Entry, i, iStart, iStop )
Count += ((Entry & 0xF) <= nVars);
return Count;
}
int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int iStart, int iStop, word nSteps, int Count2, abctime clk )
{
int nNew;
printf("N =%2d | ", nNodes );
printf("C =%12.0f ", (double)(iword)nSteps );
printf("New%d =%10d ", nInputs, iStop-iStart );
printf("All%d =%10d | ", nInputs, iStop );
printf("New%d =%8d ", nVars, nNew = Dau_CountFuncs(vNodSup, iStart, iStop, nVars) );
printf("All%d =%8d ", nVars, Dau_CountFuncs(vNodSup, 0, iStop, nVars) );
printf("Two =%6d ", Count2 );
//Abc_PrintTime( 1, "T", Abc_Clock() - clk );
Abc_Print(1, "%9.2f sec\n", 1.0*(Abc_Clock() - clk)/(CLOCKS_PER_SEC));
fflush(stdout);
return nNew;
}
int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars0, int nVars,
Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nFronts, abctime clk )
{
int DumpDelta = 1000000;
char Perm[16] = {0};
int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs );
//unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 );
unsigned Phase = Abc_TtCanonicizeWrap( Abc_TtCanonicizeAda, pMan, pCur, nVarsNew, Perm, 99 );
int nEntries = Vec_MemEntryNum(vTtMem);
int Entry = Vec_MemHashInsert( vTtMem, pCur );
if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new
return 0;
Entry = 0;
Phase = 0;
// this is a new class
Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew );
assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) );
if ( Vec_IntSize(vNodSup) % DumpDelta == 0 )
Dau_TablesSave( nInputs, nVars0, vTtMem, vNodSup, nFronts, clk );
return 1;
}
void Dau_FunctionEnum( int nInputs, int nVars, int nNodeMax, int fUseTwo, int fReduce, int fVerbose )
{
abctime clk = Abc_Clock();
int nWords = Abc_TtWordNum(nInputs); word nSteps = 0;
Abc_TtHieMan_t * pMan = Abc_TtHieManStart( nInputs, 5 );
Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 16 );
Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 );
int v, u, k, m, n, Entry, nNew, Limit[32] = {1, 2};
word Truth[4] = {0};
assert( nVars >= 3 && nVars <= nInputs && nInputs <= 6 );
Vec_MemHashAlloc( vTtMem, 1<<16 );
// add constant 0
Vec_MemHashInsert( vTtMem, Truth );
Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0
// add buffer/inverter
Abc_TtIthVar( Truth, 0, nInputs );
Abc_TtNot( Truth, nWords );
Vec_MemHashInsert( vTtMem, Truth );
Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1
Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, nSteps, 0, clk );
// numerate other functions based on how many nodes they have
for ( n = 1; n <= nNodeMax; n++ )
{
int Count2 = 0;
int fExpand = !(fReduce && n == nNodeMax);
for ( Entry = Limit[n-1]; Entry < Limit[n]; Entry++ )
{
word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
int NodSup = Vec_IntEntry(vNodSup, Entry);
int nSupp = 0xF & NodSup;
int SymVars = Dau_CountSymms2( pTruth[0], nSupp );
assert( n-1 == (NodSup >> 16) );
assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
//printf( "Exploring function %4d with %d vars: ", i, nSupp );
//printf( " %04x\n", (int)uTruth );
//Dau_DsdPrintFromTruth( &uTruth, 4 );
for ( v = 0; v < nSupp; v++ ) if ( (SymVars & (1 << v)) == 0 )
{
word tGate, tCur;
word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
// add one extra variable to support
if ( nSupp < nInputs && fExpand )
{
tGate = s_Truths6[v] & s_Truths6[nSupp];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
tGate = s_Truths6[v] ^ s_Truths6[nSupp];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp+1, vTtMem, vNodSup, Entry, clk );
nSteps += 3;
}
// add one cross bar
if ( fExpand )
for ( k = 0; k < nSupp; k++ ) if ( k != v && ((SymVars & (1 << k)) == 0 || k == v+1) )
{
tGate = s_Truths6[v] & s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tGate = s_Truths6[v] & ~s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tGate = s_Truths6[v] ^ s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
nSteps += 5;
}
// add two cross bars
for ( k = 0; k < nSupp; k++ ) if ( k != v )//&& ((SymVars & (1 << k)) == 0) )
for ( m = k+1; m < nSupp; m++ ) if ( m != v )//&& ((SymVars & (1 << m)) == 0 || m == k+1) )
{
tGate = s_Truths6[m] & s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tGate = s_Truths6[m] & ~s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tGate = ~s_Truths6[m] & s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tGate = ~s_Truths6[m] & ~s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tGate = s_Truths6[m] ^ s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
tGate = s_Truths6[m] ^ s_Truths6[k];
tCur = (tGate & Cof0) | (~tGate & Cof1);
Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
nSteps += 10;
}
}
}
if ( fUseTwo && n > 2 && fExpand )
for ( Entry = Limit[n-2]; Entry < Limit[n-1]; Entry++ )
{
word * pTruth = Vec_MemReadEntry( vTtMem, Entry );
int NodSup = Vec_IntEntry(vNodSup, Entry);
int nSupp = 0xF & NodSup; int g1, g2;
assert( n-2 == (NodSup >> 16) );
assert( !Abc_Tt6HasVar(*pTruth, nSupp) );
for ( v = 0; v < nSupp; v++ )
for ( u = 0; u < nSupp; u++ ) if ( u != v )
{
word Cof0 = Abc_Tt6Cofactor0( *pTruth, v );
word Cof1 = Abc_Tt6Cofactor1( *pTruth, v );
word Cof00 = Abc_Tt6Cofactor0( Cof0, u );
word Cof01 = Abc_Tt6Cofactor1( Cof0, u );
word Cof10 = Abc_Tt6Cofactor0( Cof1, u );
word Cof11 = Abc_Tt6Cofactor1( Cof1, u );
word tGates[5], tCur;
tGates[0] = s_Truths6[v] & s_Truths6[u];
tGates[1] = s_Truths6[v] & ~s_Truths6[u];
tGates[2] = ~s_Truths6[v] & s_Truths6[u];
tGates[3] = s_Truths6[v] | s_Truths6[u];
tGates[4] = s_Truths6[v] ^ s_Truths6[u];
for ( g1 = 0; g1 < 5; g1++ )
for ( g2 = g1+1; g2 < 5; g2++ )
{
Cof0 = (tGates[g1] & Cof01) | (~tGates[g1] & Cof00);
Cof1 = (tGates[g1] & Cof11) | (~tGates[g1] & Cof10);
tCur = (tGates[g2] & Cof1) | (~tGates[g2] & Cof0);
Count2 += Dau_InsertFunction( pMan, &tCur, n, nInputs, nVars, nSupp, vTtMem, vNodSup, Entry, clk );
}
}
}
Limit[n+1] = Vec_IntSize(vNodSup);
nNew = Dau_PrintStats( n, nInputs, nVars, vNodSup, Limit[n], Limit[n+1], nSteps, Count2, clk );
if ( nNew == 0 )
break;
}
Dau_TablesSave( nInputs, nVars, vTtMem, vNodSup, Vec_IntSize(vNodSup), clk );
Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
//Dau_DumpFuncs( vTtMem, vNodSup, nVars, nNodeMax );
//Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n );
Abc_TtHieManStop( pMan );
Vec_MemHashFree( vTtMem );
Vec_MemFreeP( &vTtMem );
Vec_IntFree( vNodSup );
fflush(stdout);
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END