summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/base/abci/abc.c1
-rw-r--r--src/base/abci/abcNpn.c28
-rw-r--r--src/opt/dau/dau.h1
-rw-r--r--src/opt/dau/dauCanon.c143
4 files changed, 170 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index afd2bcfe..7db89a44 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6159,6 +6159,7 @@ usage:
Abc_Print( -2, "\t 4: Jake's hybrid semi-canonical form (high-effort)\n" );
Abc_Print( -2, "\t 5: new fast hybrid semi-canonical form\n" );
Abc_Print( -2, "\t 6: new phase canonical form\n" );
+ Abc_Print( -2, "\t 7: new hierarchical matching\n" );
Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
Abc_Print( -2, "\t-d : toggle dumping resulting functions into a file [default = %s]\n", fDumpRes? "yes": "no" );
Abc_Print( -2, "\t-b : toggle dumping in binary format [default = %s]\n", fBinary? "yes": "no" );
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index 87a00651..e667a074 100644
--- a/src/base/abci/abcNpn.c
+++ b/src/base/abci/abcNpn.c
@@ -181,7 +181,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
char pCanonPerm[16];
unsigned uCanonPhase=0;
abctime clk = Abc_Clock();
- int i;
+ int i, nClasses = -1;
char * pAlgoName = NULL;
if ( NpnType == 0 )
@@ -198,6 +198,8 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
pAlgoName = "new hybrid fast ";
else if ( NpnType == 6 )
pAlgoName = "new phase flipping ";
+ else if ( NpnType == 7 )
+ pAlgoName = "new hier. matching ";
assert( p->nVars <= 16 );
if ( pAlgoName )
@@ -289,9 +291,29 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );
}
}
+ else if ( NpnType == 7 )
+ {
+ extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm );
+ extern Abc_TtMan_t * Abc_TtManStart( int nVars );
+ extern void Abc_TtManStop( Abc_TtMan_t * p );
+ extern int Abc_TtManNumClasses( Abc_TtMan_t * p );
+
+ Abc_TtMan_t * pMan = Abc_TtManStart( p->nVars );
+ for ( i = 0; i < p->nFuncs; i++ )
+ {
+ if ( fVerbose )
+ printf( "%7d : ", i );
+ uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm );
+ if ( fVerbose )
+// Extra_PrintHex( stdout, (unsigned *)p->pFuncs[i], p->nVars ), Abc_TruthNpnPrint(NULL, uCanonPhase, p->nVars), printf( "\n" );
+ printf( "\n" );
+ }
+ nClasses = Abc_TtManNumClasses( pMan );
+ Abc_TtManStop( pMan );
+ }
else assert( 0 );
clk = Abc_Clock() - clk;
- printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
+ printf( "Classes =%9d ", nClasses == -1 ? Abc_TruthNpnCountUnique(p) : nClasses );
Abc_PrintTime( 1, "Time", clk );
}
@@ -352,7 +374,7 @@ int Abc_NpnTest( char * pFileName, int NpnType, int nVarNum, int fDumpRes, int f
{
if ( fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName );
- if ( NpnType >= 0 && NpnType <= 6 )
+ if ( NpnType >= 0 && NpnType <= 7 )
Abc_TruthNpnTest( pFileName, NpnType, nVarNum, fDumpRes, fBinary, fVerbose );
else
printf( "Unknown canonical form value (%d).\n", NpnType );
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index ddffa905..1fa22494 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -59,6 +59,7 @@ typedef enum {
} Dau_DsdType_t;
typedef struct Dss_Man_t_ Dss_Man_t;
+typedef struct Abc_TtMan_t_ Abc_TtMan_t;
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index 26edca9b..4fd8361c 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -20,6 +20,7 @@
#include "dauInt.h"
#include "misc/util/utilTruth.h"
+#include "misc/vec/vecMem.h"
ABC_NAMESPACE_IMPL_START
@@ -1041,6 +1042,148 @@ unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
}
+/**Function*************************************************************
+
+ Synopsis [Hierarchical semi-canonical form computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+#define TT_NUM_TABLES 4
+
+struct Abc_TtMan_t_
+{
+ Vec_Mem_t * vTtMem[TT_NUM_TABLES]; // truth table memory and hash tables
+};
+
+Abc_TtMan_t * Abc_TtManStart( int nVars )
+{
+ Abc_TtMan_t * p = ABC_CALLOC( Abc_TtMan_t, 1 );
+ int i, nWords = Abc_TtWordNum( nVars );
+ for ( i = 0; i < TT_NUM_TABLES; i++ )
+ {
+ p->vTtMem[i] = Vec_MemAlloc( nWords, 12 );
+ Vec_MemHashAlloc( p->vTtMem[i], 10000 );
+ }
+ return p;
+}
+void Abc_TtManStop( Abc_TtMan_t * p )
+{
+ int i;
+ for ( i = 0; i < TT_NUM_TABLES; i++ )
+ {
+ Vec_MemHashFree( p->vTtMem[i] );
+ Vec_MemFreeP( &p->vTtMem[i] );
+ }
+ ABC_FREE( p );
+}
+int Abc_TtManNumClasses( Abc_TtMan_t * p )
+{
+ return Vec_MemEntryNum( p->vTtMem[TT_NUM_TABLES-1] );
+}
+
+unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm )
+{
+ int fNaive = 1;
+ int pStore[17];
+ static word pTruth[1024];
+ unsigned uCanonPhase = 0;
+ int nOnes, nWords = Abc_TtWordNum( nVars );
+ int i, k, truthId;
+ int * pSpot;
+ assert( nVars <= 16 );
+
+ Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
+
+ for ( i = 0; i < nVars; i++ )
+ pCanonPerm[i] = i;
+
+ // normalize polarity
+ nOnes = Abc_TtCountOnesInTruth( pTruth, nVars );
+ if ( nOnes > nWords * 32 )
+ {
+ Abc_TtNot( pTruth, nWords );
+ nOnes = nWords*64 - nOnes;
+ uCanonPhase |= (1 << nVars);
+ }
+ // check cache
+ pSpot = Vec_MemHashLookup( p->vTtMem[0], pTruth );
+ if ( *pSpot != -1 )
+ return 0;
+ truthId = Vec_MemHashInsert( p->vTtMem[0], pTruth );
+
+ // normalize phase
+ Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
+ pStore[nVars] = nOnes;
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pStore[i] >= nOnes - pStore[i] )
+ continue;
+ Abc_TtFlip( pTruth, nWords, i );
+ uCanonPhase |= (1 << i);
+ pStore[i] = nOnes - pStore[i];
+ }
+ // check cache
+ pSpot = Vec_MemHashLookup( p->vTtMem[1], pTruth );
+ if ( *pSpot != -1 )
+ return 0;
+ truthId = Vec_MemHashInsert( p->vTtMem[1], pTruth );
+
+ // normalize permutation
+ {
+ int k, BestK;
+ for ( i = 0; i < nVars - 1; i++ )
+ {
+ BestK = i + 1;
+ for ( k = i + 2; k < nVars; k++ )
+ if ( pStore[BestK] > pStore[k] )
+ BestK = k;
+ if ( pStore[i] <= pStore[BestK] )
+ continue;
+ ABC_SWAP( int, pCanonPerm[i], pCanonPerm[BestK] );
+ ABC_SWAP( int, pStore[i], pStore[BestK] );
+ if ( ((uCanonPhase >> i) & 1) != ((uCanonPhase >> BestK) & 1) )
+ {
+ uCanonPhase ^= (1 << i);
+ uCanonPhase ^= (1 << BestK);
+ }
+ Abc_TtSwapVars( pTruth, nVars, i, BestK );
+ }
+ }
+ // check cache
+ pSpot = Vec_MemHashLookup( p->vTtMem[2], pTruth );
+ if ( *pSpot != -1 )
+ return 0;
+ truthId = Vec_MemHashInsert( p->vTtMem[2], pTruth );
+
+ // iterate TT permutations for tied variables
+ for ( k = 0; k < 5; k++ )
+ {
+ int fChanges = 0;
+ for ( i = nVars - 2; i >= 0; i-- )
+ if ( pStore[i] == pStore[i+1] )
+ fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
+ if ( !fChanges )
+ break;
+ fChanges = 0;
+ for ( i = 1; i < nVars - 1; i++ )
+ if ( pStore[i] == pStore[i+1] )
+ fChanges |= Abc_TtCofactorPerm( pTruth, i, nWords, pStore[i] != pStore[nVars]/2, pCanonPerm, &uCanonPhase, fNaive );
+ if ( !fChanges )
+ break;
+ }
+ // check cache
+ pSpot = Vec_MemHashLookup( p->vTtMem[3], pTruth );
+ if ( *pSpot != -1 )
+ return 0;
+ truthId = Vec_MemHashInsert( p->vTtMem[3], pTruth );
+ return 0;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////