From c497acde5db6fcc4b7f272c04c65dbcaad7d02a0 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 8 Sep 2018 08:30:11 +0300
Subject: Expriments with functions.
---
src/base/abci/abc.c | 14 ++--
src/opt/dau/dauNpn.c | 228 ++++++++++++++++++++++++++++++++++++++++++---------
2 files changed, 195 insertions(+), 47 deletions(-)
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 95aef8ad..45b7c166 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22991,7 +22991,7 @@ int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose );
int c, nInputs = 4, nVars = 4, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "SNvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "SIvh" ) ) != EOF )
{
switch ( c )
{
@@ -23006,10 +23006,10 @@ int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nInputs < 0 )
goto usage;
break;
- case 'N':
+ case 'I':
if ( globalUtilOptind >= argc )
{
- Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
nVars = atoi(argv[globalUtilOptind]);
@@ -23029,12 +23029,12 @@ int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( nVars < 2 || nVars > 6 )
{
- Abc_Print( -1, "The number of inputs should be 2 <= N <= 6.\n" );
+ Abc_Print( -1, "The number of inputs should be 2 <= I <= 6.\n" );
goto usage;
}
if ( nInputs < nVars || nInputs > 6 )
{
- Abc_Print( -1, "The intermediate support size should be N <= S <= 6.\n" );
+ Abc_Print( -1, "The intermediate support size should be I <= S <= 6.\n" );
goto usage;
}
@@ -23042,10 +23042,10 @@ int Abc_CommandFunEnum( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: funenum [-SN num] [-vh]\n" );
+ Abc_Print( -2, "usage: funenum [-SI num] [-vh]\n" );
Abc_Print( -2, "\t enumerates minimum 2-input-gate implementations\n" );
Abc_Print( -2, "\t-S num : the maximum intermediate support size [default = %d]\n", nInputs );
- Abc_Print( -2, "\t-N num : the number of inputs of Boolean functions [default = %d]\n", nVars );
+ Abc_Print( -2, "\t-I num : the number of inputs of Boolean functions [default = %d]\n", nVars );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
diff --git a/src/opt/dau/dauNpn.c b/src/opt/dau/dauNpn.c
index 7850a9a1..23b1df69 100644
--- a/src/opt/dau/dauNpn.c
+++ b/src/opt/dau/dauNpn.c
@@ -386,6 +386,45 @@ void Dau_NetworkEnumTest()
+/**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 = 0; j < i; j++ )
+ nPairs += Abc_TtVarsAreSymmetric(&t, nVars, i, j, &Cof0, &Cof1);
+ return nPairs;
+}
+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.]
@@ -449,6 +488,83 @@ void Dau_ExactNpnPrint( Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup, int nVars, int
fflush(stdout);
}
+/**Function*************************************************************
+
+ Synopsis [Saving hash tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dau_TablesSave( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Mem_t * vTtMemA, Vec_Int_t * vNodSup, Vec_Int_t * vMapping )
+{
+ FILE * pFile;
+ char FileName[100];
+ int i, nWords = Abc_TtWordNum(nInputs);
+ // functions
+ sprintf( FileName, "fun%d%d.ttd", nInputs, nVars );
+ pFile = fopen( FileName, "wb" );
+ for ( i = 0; i < Vec_MemEntryNum(vTtMemA); i++ )
+ fwrite( Vec_MemReadEntry(vTtMemA, i), 8, nWords, pFile );
+ fwrite( Vec_IntArray(vMapping), 4, Vec_IntSize(vMapping), pFile );
+ fclose( pFile );
+ // 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 functions and %10d classes.\n", Vec_IntSize(vMapping), Vec_IntSize(vNodSup) );
+}
+void Dau_TablesLoad( int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Mem_t * vTtMemA, Vec_Int_t * vNodSup, Vec_Int_t * vMapping )
+{
+ char FileName1[100], FileName2[100];
+ int i, FileSize1, FileSize2, nWords = Abc_TtWordNum(nInputs);
+ // functions
+ sprintf( FileName1, "fun%d%d.ttd", nInputs, nVars );
+ FileSize1 = Extra_FileSize( FileName1 );
+ if ( FileSize1 )
+ {
+ word uTruth;
+ FILE * pFile = fopen( FileName1, "rb" );
+ int nEntries = FileSize1 / 12;
+ assert( FileSize1 % 12 == 0 );
+ for ( i = 0; i < nEntries; i++ )
+ {
+ fread( &uTruth, 8, nWords, pFile );
+ Vec_MemHashInsert( vTtMem, &uTruth );
+ }
+ Vec_IntFill( vNodSup, nEntries, -1 );
+ fread( Vec_IntArray(vNodSup), 4, Vec_IntSize(vNodSup), pFile );
+ fclose( pFile );
+ }
+ // classes
+ sprintf( FileName2, "npn%d%d.ttd", nInputs, nVars );
+ FileSize2 = Extra_FileSize( FileName2 );
+ if ( FileSize2 )
+ {
+ word uTruth;
+ FILE * pFile = fopen( FileName2, "rb" );
+ int nEntries = FileSize2 / 12;
+ assert( FileSize2 % 12 == 0 );
+ for ( i = 0; i < nEntries; i++ )
+ {
+ fread( &uTruth, 8, nWords, pFile );
+ Vec_MemHashInsert( vTtMemA, &uTruth );
+ }
+ Vec_IntFill( vMapping, nEntries, -1 );
+ fread( Vec_IntArray(vMapping), 4, Vec_IntSize(vMapping), pFile );
+ fclose( pFile );
+ }
+ if ( FileSize1 )
+ printf( "Loaded file \"%s\" with %10d functions and file \"%s\" with %10d classes.\n",
+ FileName1, FileSize1, FileName2, FileSize2 );
+}
+
/**Function*************************************************************
Synopsis [Function enumeration.]
@@ -480,21 +596,37 @@ int Dau_PrintStats( int nNodes, int nInputs, int nVars, Vec_Int_t * vNodSup, int
fflush(stdout);
return nNew;
}
-int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Int_t * vNodSup )
+int Dau_InsertFunction( Abc_TtHieMan_t * pMan, word * pCur, int nNodes, int nInputs, int nVars, Vec_Mem_t * vTtMem, Vec_Mem_t * vTtMemA, Vec_Int_t * vNodSup, Vec_Int_t * vMapping )
{
- char Perm[16] = {0};
- int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs );
- unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 );
- int nEntries = Vec_MemEntryNum(vTtMem);
- int Entry = Vec_MemHashInsert( vTtMem, pCur );
- if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new
+ int DumpDelta = 100000000;
+ int nEntries = Vec_MemEntryNum(vTtMemA);
+ Vec_MemHashInsert( vTtMemA, pCur );
+ if ( nEntries == Vec_MemEntryNum(vTtMemA) ) // found in the table - not new
return 0;
- Phase = 0;
- Entry = 0;
- // this is a new class
- Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew );
- assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) );
- return 1;
+ else // this is a new function
+ {
+ char Perm[16] = {0};
+ int nVarsNew = Abc_TtMinBase( pCur, NULL, nVars, nInputs );
+ unsigned Phase = Abc_TtCanonicizeHie( pMan, pCur, nVarsNew, Perm, 1 );
+ int nEntries = Vec_MemEntryNum(vTtMem);
+ int Entry = Vec_MemHashInsert( vTtMem, pCur );
+ Vec_IntPush( vMapping, Entry );
+ assert( Vec_MemEntryNum(vTtMemA) == Vec_IntSize(vMapping) );
+ if ( nEntries == Vec_MemEntryNum(vTtMem) ) // found in the table - not new
+ {
+ if ( Vec_IntSize(vMapping) % DumpDelta == 0 )
+ Dau_TablesSave( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping );
+ return 0;
+ }
+ Phase = 0;
+ //printf( "%d ", Dau_CountCompl(pCur[0], nVarsNew) );
+ // this is a new class
+ Vec_IntPush( vNodSup, (nNodes << 16) | nVarsNew );
+ assert( Vec_MemEntryNum(vTtMem) == Vec_IntSize(vNodSup) );
+ if ( Vec_IntSize(vMapping) % DumpDelta == 0 )
+ Dau_TablesSave( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping );
+ return 1;
+ }
}
void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose )
{
@@ -502,19 +634,31 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose )
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_Mem_t * vTtMemA = Vec_MemAlloc( nWords, 16 );
Vec_Int_t * vNodSup = Vec_IntAlloc( 1 << 16 );
+ Vec_Int_t * vMapping = Vec_IntAlloc( 1 << 16 );
int v, g, k, m, n, Entry, nNew, iStart = 1, iStop = 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
+ Vec_MemHashAlloc( vTtMem, 1<<16 );
+ Vec_MemHashAlloc( vTtMemA, 1<<16 );
+ if ( 0 ) // load from file
+ Dau_TablesLoad( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping );
+ else
+ {
+ // add constant 0
+ Vec_MemHashInsert( vTtMem, Truth );
+ Vec_MemHashInsert( vTtMemA, Truth );
+ Vec_IntPush( vNodSup, 0 ); // nodes=0, supp=0
+ Vec_IntPush( vMapping, 0 );
+ // add buffer/inverter
+ Abc_TtIthVar( Truth, 0, nInputs );
+ Abc_TtNot( Truth, nWords );
+ Vec_MemHashInsert( vTtMem, Truth );
+ Vec_MemHashInsert( vTtMemA, Truth );
+ Vec_IntPush( vNodSup, 1 ); // nodes=0, supp=1
+ Vec_IntPush( vMapping, 1 );
+ }
Dau_PrintStats( 0, nInputs, nVars, vNodSup, 0, 2, nSteps, clk );
// numerate other functions based on how many nodes they have
for ( n = 1; n < 32; n++ )
@@ -543,16 +687,16 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose )
{
tGate = s_Truths6[v] & s_Truths6[nSupp];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vTtMemA, vNodSup, vMapping );
tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vTtMemA, vNodSup, vMapping );
}
else
{
tGate = s_Truths6[v] ^ s_Truths6[nSupp];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp+1, vTtMem, vTtMemA, vNodSup, vMapping );
}
}
nSteps += 3;
@@ -566,23 +710,23 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose )
{
tGate = s_Truths6[v] & s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tGate = s_Truths6[v] & ~s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
}
else
{
tGate = s_Truths6[v] ^ s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
}
nSteps += 5;
}
@@ -597,37 +741,37 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose )
{
tGate = s_Truths6[m] & s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tGate = s_Truths6[m] & ~s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tGate = ~s_Truths6[m] & s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tGate = ~s_Truths6[m] & ~s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
tCur = (tGate & Cof0) | (~tGate & Cof1);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
}
else
{
tGate = s_Truths6[m] ^ s_Truths6[k];
tCur = (tGate & Cof1) | (~tGate & Cof0);
- Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vNodSup );
+ Dau_InsertFunction( pMan, &tCur, n, nInputs, nSupp, vTtMem, vTtMemA, vNodSup, vMapping );
}
nSteps += 9;
}
@@ -640,12 +784,16 @@ void Dau_FunctionEnum( int nInputs, int nVars, int fVerbose )
if ( nNew == 0 )
break;
}
+ Dau_TablesSave( nInputs, nVars, vTtMem, vTtMemA, vNodSup, vMapping );
Abc_PrintTime( 1, "Total time", Abc_Clock() - clk );
- //Dau_ExactNpnPrint( vTtMem, vNodSup, nVars, nInputs, n );
+ //Dau_ExactNpnPrint( vTtMem, vTtMemA, vNodSup, nVars, nInputs, n );
Abc_TtHieManStop( pMan );
Vec_MemHashFree( vTtMem );
+ Vec_MemHashFree( vTtMemA );
Vec_MemFreeP( &vTtMem );
+ Vec_MemFreeP( &vTtMemA );
Vec_IntFree( vNodSup );
+ Vec_IntFree( vMapping );
fflush(stdout);
}
--
cgit v1.2.3