summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abcNpn.c11
-rw-r--r--src/bool/lucky/luckySimple.c119
-rw-r--r--src/opt/dau/dauCanon.c119
3 files changed, 230 insertions, 19 deletions
diff --git a/src/base/abci/abcNpn.c b/src/base/abci/abcNpn.c
index e667a074..8335edda 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, nClasses = -1;
+ int i;
char * pAlgoName = NULL;
if ( NpnType == 0 )
@@ -293,27 +293,28 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
}
else if ( NpnType == 7 )
{
- extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm );
+ extern unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int fExact );
extern Abc_TtMan_t * Abc_TtManStart( int nVars );
extern void Abc_TtManStop( Abc_TtMan_t * p );
extern int Abc_TtManNumClasses( Abc_TtMan_t * p );
+ int fExact = 0;
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 );
+ uCanonPhase = Abc_TtCanonicizeHie( pMan, p->pFuncs[i], p->nVars, pCanonPerm, fExact );
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 );
+ // nClasses = Abc_TtManNumClasses( pMan );
Abc_TtManStop( pMan );
}
else assert( 0 );
clk = Abc_Clock() - clk;
- printf( "Classes =%9d ", nClasses == -1 ? Abc_TruthNpnCountUnique(p) : nClasses );
+ printf( "Classes =%9d ", Abc_TruthNpnCountUnique(p) );
Abc_PrintTime( 1, "Time", clk );
}
diff --git a/src/bool/lucky/luckySimple.c b/src/bool/lucky/luckySimple.c
index f9128f3f..0660c0ad 100644
--- a/src/bool/lucky/luckySimple.c
+++ b/src/bool/lucky/luckySimple.c
@@ -148,6 +148,11 @@ static inline void minWord3(word* a, word* b, word* minimal, int nVars)
if (memCompare(b, minimal, nVars) <= 0)
Kit_TruthCopy_64bit( minimal, b, nVars );
}
+static inline void minWord1(word* a, word* minimal, int nVars)
+{
+ if (memCompare(a, minimal, nVars) <= 0)
+ Kit_TruthCopy_64bit( minimal, a, nVars );
+}
void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars)
{
int i,j=0;
@@ -179,5 +184,119 @@ void simpleMinimal(word* x, word* pAux,word* minimal, permInfo* pi, int nVars)
Kit_TruthCopy_64bit( x, minimal, nVars );
}
+/**
+ * pGroups: we assume that the variables are merged into adjacent groups,
+ * the size of each group is stored in pGroups
+ * nGroups: the number of groups
+ *
+ * pis: we compute all permInfos from 0 to nVars (incl.)
+ */
+void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput)
+{
+ /* variables */
+ int i, j, o, nn;
+ permInfo* pi;
+
+ /* reorder groups and calculate group offsets */
+ int offset[nGroups];
+ o = 0;
+ j = 0;
+
+ for ( i = 0; i < nGroups; ++i )
+ {
+ offset[j] = o;
+ o += pGroups[j];
+ ++j;
+ }
+
+ if ( fFlipOutput )
+ {
+ /* keep regular and inverted version of x */
+ Kit_TruthCopy_64bit( pAux, x, nVars );
+ Kit_TruthNot_64bit( x, nVars );
+
+ minWord(x, pAux, minimal, nVars);
+ }
+ else
+ {
+ Kit_TruthCopy_64bit( minimal, x, nVars );
+ }
+
+ /* iterate through all combinations of pGroups using mixed radix enumeration */
+ nn = ( nGroups << 1 ) + 1;
+ int a[nn];
+ int c[nn];
+ int m[nn];
+
+ /* fill a and m arrays */
+ m[0] = 2;
+ for ( i = 1; i <= nGroups; ++i ) { m[i] = pis[pGroups[i - 1]]->totalFlips + 1; }
+ for ( i = 1; i <= nGroups; ++i ) { m[nGroups + i] = pis[pGroups[i - 1]]->totalSwaps + 1; }
+ for ( i = 0; i < nn; ++i ) { a[i] = c[i] = 0; }
+
+ while ( 1 )
+ {
+ /* consider all flips */
+ for ( i = 1; i <= nGroups; ++i )
+ {
+ if ( !c[i] ) { continue; }
+ if ( !fFlipInput && pGroups[i - 1] == 1 ) { continue; }
+
+ pi = pis[pGroups[i - 1]];
+ j = a[i] == 0 ? 0 : pi->totalFlips - a[i];
+
+ Kit_TruthChangePhase_64bit(x, nVars, offset[i - 1] + pi->flipArray[j]);
+ if ( fFlipOutput )
+ {
+ Kit_TruthChangePhase_64bit(pAux, nVars, offset[i - 1] + pi->flipArray[j]);
+ minWord3(x, pAux, minimal, nVars);
+ }
+ else
+ {
+ minWord1(x, minimal, nVars);
+ }
+ }
+
+ /* consider all swaps */
+ for ( i = 1; i <= nGroups; ++i )
+ {
+ if ( !c[nGroups + i] ) { continue; }
+ if ( pGroups[i - 1] == 1 ) { continue; }
+
+ pi = pis[pGroups[i - 1]];
+ if ( a[nGroups + i] == pi->totalSwaps )
+ {
+ j = 0;
+ }
+ else
+ {
+ j = pi->swapArray[pi->totalSwaps - a[nGroups + i] - 1];
+ }
+ Kit_TruthSwapAdjacentVars_64bit(x, nVars, offset[i - 1] + j);
+ if ( fFlipOutput )
+ {
+ Kit_TruthSwapAdjacentVars_64bit(pAux, nVars, offset[i - 1] + j);
+ minWord3(x, pAux, minimal, nVars);
+ }
+ else
+ {
+ minWord1(x, minimal, nVars);
+ }
+ }
+
+ /* update a's */
+ memset(c, 0, sizeof(int) * nn);
+ j = nn - 1;
+ while ( a[j] == m[j] - 1 ) { c[j] = 1; a[j--] = 0; }
+
+ /* done? */
+ if ( j == 0 ) { break; }
+
+ c[j] = 1;
+ a[j]++;
+ }
+
+ Kit_TruthCopy_64bit( x, minimal, nVars );
+}
ABC_NAMESPACE_IMPL_END
diff --git a/src/opt/dau/dauCanon.c b/src/opt/dau/dauCanon.c
index 4fd8361c..c6ac8288 100644
--- a/src/opt/dau/dauCanon.c
+++ b/src/opt/dau/dauCanon.c
@@ -21,6 +21,7 @@
#include "dauInt.h"
#include "misc/util/utilTruth.h"
#include "misc/vec/vecMem.h"
+#include "bool/lucky/lucky.h"
ABC_NAMESPACE_IMPL_START
@@ -1053,13 +1054,32 @@ unsigned Abc_TtCanonicizePhase( word * pTruth, int nVars )
SeeAlso []
***********************************************************************/
-#define TT_NUM_TABLES 4
+#define TT_NUM_TABLES 5
struct Abc_TtMan_t_
{
Vec_Mem_t * vTtMem[TT_NUM_TABLES]; // truth table memory and hash tables
+ Vec_Int_t ** vRepres; // pointers to the representatives from the last hierarchical level
};
+Vec_Int_t ** Abc_TtRepresStart() {
+ Vec_Int_t ** vRepres = ABC_ALLOC(Vec_Int_t *, TT_NUM_TABLES - 1);
+ int i;
+ // create a list of pointers for each level of the hierarchy
+ for (i = 0; i < (TT_NUM_TABLES - 1); i++) {
+ vRepres[i] = Vec_IntAlloc(1);
+ }
+ return vRepres;
+}
+
+void Abc_TtRepresStop(Vec_Int_t ** vRepres) {
+ int i;
+ for (i = 0; i < (TT_NUM_TABLES - 1); i++) {
+ Vec_IntFree(vRepres[i]);
+ }
+ ABC_FREE( vRepres );
+}
+
Abc_TtMan_t * Abc_TtManStart( int nVars )
{
Abc_TtMan_t * p = ABC_CALLOC( Abc_TtMan_t, 1 );
@@ -1069,6 +1089,7 @@ Abc_TtMan_t * Abc_TtManStart( int nVars )
p->vTtMem[i] = Vec_MemAlloc( nWords, 12 );
Vec_MemHashAlloc( p->vTtMem[i], 10000 );
}
+ p->vRepres = Abc_TtRepresStart();
return p;
}
void Abc_TtManStop( Abc_TtMan_t * p )
@@ -1079,6 +1100,7 @@ void Abc_TtManStop( Abc_TtMan_t * p )
Vec_MemHashFree( p->vTtMem[i] );
Vec_MemFreeP( &p->vTtMem[i] );
}
+ Abc_TtRepresStop(p->vRepres);
ABC_FREE( p );
}
int Abc_TtManNumClasses( Abc_TtMan_t * p )
@@ -1086,7 +1108,7 @@ 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 )
+unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, char * pCanonPerm, int fExact )
{
int fNaive = 1;
int pStore[17];
@@ -1095,6 +1117,9 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
int nOnes, nWords = Abc_TtWordNum( nVars );
int i, k, truthId;
int * pSpot;
+ int vTruthId[TT_NUM_TABLES-1];
+ int fLevelFound;
+ word * pRepTruth;
assert( nVars <= 16 );
Abc_TtCopy( pTruth, pTruthInit, nWords, 0 );
@@ -1112,9 +1137,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
}
// check cache
pSpot = Vec_MemHashLookup( p->vTtMem[0], pTruth );
- if ( *pSpot != -1 )
- return 0;
- truthId = Vec_MemHashInsert( p->vTtMem[0], pTruth );
+ if ( *pSpot != -1 ) {
+ fLevelFound = 0;
+ goto end_repres;
+ }
+ vTruthId[0] = Vec_MemHashInsert( p->vTtMem[0], pTruth );
// normalize phase
Abc_TtCountOnesInCofs( pTruth, nVars, pStore );
@@ -1129,9 +1156,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
}
// check cache
pSpot = Vec_MemHashLookup( p->vTtMem[1], pTruth );
- if ( *pSpot != -1 )
- return 0;
- truthId = Vec_MemHashInsert( p->vTtMem[1], pTruth );
+ if ( *pSpot != -1 ) {
+ fLevelFound = 1;
+ goto end_repres;
+ }
+ vTruthId[1] = Vec_MemHashInsert( p->vTtMem[1], pTruth );
// normalize permutation
{
@@ -1156,9 +1185,11 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
}
// check cache
pSpot = Vec_MemHashLookup( p->vTtMem[2], pTruth );
- if ( *pSpot != -1 )
- return 0;
- truthId = Vec_MemHashInsert( p->vTtMem[2], pTruth );
+ if ( *pSpot != -1 ) {
+ fLevelFound = 2;
+ goto end_repres;
+ }
+ vTruthId[2] = Vec_MemHashInsert( p->vTtMem[2], pTruth );
// iterate TT permutations for tied variables
for ( k = 0; k < 5; k++ )
@@ -1178,9 +1209,69 @@ unsigned Abc_TtCanonicizeHie( Abc_TtMan_t * p, word * pTruthInit, int nVars, cha
}
// check cache
pSpot = Vec_MemHashLookup( p->vTtMem[3], pTruth );
- if ( *pSpot != -1 )
- return 0;
- truthId = Vec_MemHashInsert( p->vTtMem[3], pTruth );
+ if ( *pSpot != -1 ) {
+ fLevelFound = 3;
+ goto end_repres;
+ }
+ vTruthId[3] = Vec_MemHashInsert( p->vTtMem[3], pTruth );
+
+ // perform exact NPN using groups
+ if ( fExact ) {
+ extern void simpleMinimalGroups(word* x, word* pAux, word* minimal, int* pGroups, int nGroups, permInfo** pis, int nVars, int fFlipOutput, int fFlipInput);
+ word pAuxWord[1024], pAuxWord1[1024];
+ int pGroups[nVars];
+ int nGroups = 0;
+ // get groups
+ pGroups[0] = 0;
+ for (i = 0; i < nVars - 1; i++) {
+ if (pStore[i] == pStore[i + 1]) {
+ pGroups[nGroups]++;
+ } else {
+ pGroups[nGroups]++;
+ nGroups++;
+ pGroups[nGroups] = 0;
+ }
+ }
+ pGroups[nGroups]++;
+ nGroups++;
+
+ // compute permInfo from 0 to nVars (incl.)
+ permInfo * pis[nVars+1];
+ for (i = 0; i <= nVars; i++) {
+ pis[i] = setPermInfoPtr(i);
+ }
+
+ // do the exact matching
+ if (nOnes == nWords * 32) /* balanced output */
+ simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 1, 1);
+ else if (pStore[0] != pStore[1] && pStore[0] == (nOnes - pStore[0])) /* balanced singleton input */
+ simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 1);
+ else
+ simpleMinimalGroups(pTruth, pAuxWord, pAuxWord1, pGroups, nGroups, pis, nVars, 0, 0);
+
+ // cleanup
+ for (i = 0; i <= nVars; i++) {
+ freePermInfoPtr(pis[i]);
+ }
+ }
+ // check cache
+ pSpot = Vec_MemHashLookup( p->vTtMem[4], pTruth );
+ fLevelFound = 4;
+ if ( *pSpot != -1 ) {
+ goto end_repres;
+ }
+ *pSpot = Vec_MemHashInsert( p->vTtMem[4], pTruth );
+
+end_repres:
+ // return the class representative
+ if(fLevelFound < (TT_NUM_TABLES - 1))
+ truthId = Vec_IntEntry(p->vRepres[fLevelFound], *pSpot);
+ else truthId = *pSpot;
+ for(i = 0; i < fLevelFound; i++)
+ Vec_IntSetEntry(p->vRepres[i], vTruthId[i], truthId);
+ pRepTruth = Vec_MemReadEntry(p->vTtMem[TT_NUM_TABLES-1], truthId);
+ Abc_TtCopy( pTruthInit, pRepTruth, nWords, 0 );
+
return 0;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 12:07:21 +0000