summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/map/if/if.h3
-rw-r--r--src/map/if/ifDsd.c119
-rw-r--r--src/map/if/ifMan.c4
-rw-r--r--src/map/if/ifMap.c33
-rw-r--r--src/map/if/ifSat.c67
-rw-r--r--src/map/if/module.make1
-rw-r--r--src/opt/dau/dau.h1
-rw-r--r--src/opt/dau/dauNonDsd.c14
8 files changed, 201 insertions, 41 deletions
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 13828701..47bd7390 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -236,6 +236,7 @@ struct If_Man_t_
Vec_Int_t * vTtDsds; // mapping of truth table into DSD
Vec_Str_t * vTtPerms; // mapping of truth table into permutations
int nBestCutSmall[2];
+ int nCountNonDec[2];
// timing manager
Tim_Man_t * pManTim;
@@ -519,7 +520,7 @@ extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int
extern If_DsdMan_t * If_DsdManAlloc( int nLutSize );
extern void If_DsdManDump( If_DsdMan_t * p );
extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
-extern void If_DsdManFree( If_DsdMan_t * p );
+extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose );
extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
/*=== ifLib.c =============================================================*/
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index e6c2dfac..23160e62 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "if.h"
+#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
@@ -63,12 +64,13 @@ struct If_DsdMan_t_
word ** pTtElems; // elementary TTs
Vec_Mem_t * vTtMem; // truth table memory and hash table
Vec_Ptr_t * vTtDecs; // truth table decompositions
+ int * pSched[16]; // grey code schedules
int nUniqueHits; // statistics
int nUniqueMisses; // statistics
- abctime timeBeg; // statistics
- abctime timeDec; // statistics
- abctime timeLook; // statistics
- abctime timeEnd; // statistics
+ abctime timeDsd; // statistics
+ abctime timeCanon; // statistics
+ abctime timeCheck; // statistics
+ abctime timeVerify; // statistics
};
static inline int If_DsdObjWordNum( int nFans ) { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
@@ -212,6 +214,8 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
iPrev = pLits[i];
}
}
+ if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 )
+ printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" );
// create new node
pObj = If_DsdObjAlloc( p, Type, nLits );
if ( Type == DAU_DSD_PRIME )
@@ -256,7 +260,7 @@ static inline word ** If_ManDsdTtElems()
}
If_DsdMan_t * If_DsdManAlloc( int nVars )
{
- If_DsdMan_t * p;
+ If_DsdMan_t * p; int v;
p = ABC_CALLOC( If_DsdMan_t, 1 );
p->nVars = nVars;
p->nWords = Abc_TtWordNum( nVars );
@@ -272,21 +276,25 @@ If_DsdMan_t * If_DsdManAlloc( int nVars )
p->vTtDecs = Vec_PtrAlloc( 1000 );
p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 );
Vec_MemHashAlloc( p->vTtMem, 10000 );
+ for ( v = 2; v < nVars; v++ )
+ p->pSched[v] = Extra_GreyCodeSchedule( v );
return p;
}
-void If_DsdManFree( If_DsdMan_t * p )
+void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
{
- int fVerbose = 0;
+ int v;
// If_DsdManDump( p );
If_DsdManPrint( p, NULL, 0 );
Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
if ( fVerbose )
{
- Abc_PrintTime( 1, "Time begin ", p->timeBeg );
- Abc_PrintTime( 1, "Time decomp", p->timeDec );
- Abc_PrintTime( 1, "Time lookup", p->timeLook );
- Abc_PrintTime( 1, "Time end ", p->timeEnd );
+ Abc_PrintTime( 1, "Time DSD ", p->timeDsd );
+ Abc_PrintTime( 1, "Time canon ", p->timeCanon-p->timeCheck );
+ Abc_PrintTime( 1, "Time check ", p->timeCheck );
+ Abc_PrintTime( 1, "Time verify", p->timeVerify );
}
+ for ( v = 2; v < p->nVars; v++ )
+ ABC_FREE( p->pSched[v] );
Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
Vec_MemHashFree( p->vTtMem );
Vec_MemFreeP( &p->vTtMem );
@@ -297,6 +305,23 @@ void If_DsdManFree( If_DsdMan_t * p )
ABC_FREE( p->pBins );
ABC_FREE( p );
}
+void If_DsdManHashProfile( If_DsdMan_t * p )
+{
+ If_DsdObj_t * pObj;
+ unsigned * pSpot;
+ int i, Counter;
+ for ( i = 0; i < p->nBins; i++ )
+ {
+ Counter = 0;
+ for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
+ pObj = If_DsdVecObj( p->vObjs, *pSpot );
+// if ( Counter > 5 )
+// printf( "%d ", Counter );
+// if ( i > 10000 )
+// break;
+ }
+// printf( "\n" );
+}
int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int Id )
{
If_DsdObj_t * pObj;
@@ -454,30 +479,18 @@ void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
SeeAlso []
***********************************************************************/
-void If_DsdManHashProfile( If_DsdMan_t * p )
-{
- If_DsdObj_t * pObj;
- unsigned * pSpot;
- int i, Counter;
- for ( i = 0; i < p->nBins; i++ )
- {
- Counter = 0;
- for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
- pObj = If_DsdVecObj( p->vObjs, *pSpot );
- if ( Counter )
- printf( "%d ", Counter );
- }
- printf( "\n" );
-}
static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
{
- static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
+// static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
+ static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909,
+ 3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281,
+ 5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 };
int i;
unsigned uHash = Type * 7873 + nLits * 8147;
for ( i = 0; i < nLits; i++ )
- uHash += pLits[i] * s_Primes[i & 0x7];
+ uHash += pLits[i] * s_Primes[i & 0xF];
if ( Type == IF_DSD_PRIME )
- uHash += truthId * s_Primes[i & 0x7];
+ uHash += truthId * s_Primes[i & 0xF];
return uHash % p->nBins;
}
unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
@@ -503,15 +516,19 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
{
int truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1;
unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
+abctime clk;
if ( *pSpot )
return *pSpot;
+clk = Abc_Clock();
if ( truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) )
{
- Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits );
+ Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
+// printf( "%d ", Vec_IntSize(vSets) );
assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 );
Vec_PtrPush( p->vTtDecs, vSets );
// Dau_DecPrintSets( vSets, nLits );
}
+p->timeCheck += Abc_Clock() - clk;
*pSpot = Vec_PtrSize( p->vObjs );
return If_DsdObjCreate( p, Type, pLits, nLits, truthId );
}
@@ -686,6 +703,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
unsigned char pPermNew[DAU_MAX_VAR];
int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR];
int i, k, j, Id, iFanin, fComplFan, fCompl = 0, nSSize = 0;
+// abctime clk;
if ( Type == IF_DSD_AND )
{
for ( k = 0; k < nLits; k++ )
@@ -855,7 +873,7 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p
fCompl = 1;
(*p)++;
}
- assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) );
+// assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) );
if ( **p >= 'a' && **p <= 'z' ) // var
{
pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl );
@@ -881,6 +899,22 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p
iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPermStart, pTruth );
return Abc_LitNotCond( iRes, fCompl );
}
+ if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
+ {
+ word pFunc[DAU_MAX_WORD];
+ int nLits = 0, pLits[DAU_MAX_VAR];
+ char * q;
+ int i, nVarsF = Abc_TtReadHex( pFunc, *p );
+ *p += Abc_TtHexDigitNum( nVarsF );
+ q = pStr + pMatches[ *p - pStr ];
+ assert( **p == '{' && *q == '}' );
+ for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
+ pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp );
+ assert( i == nVarsF );
+ assert( *p == q );
+ iRes = If_DsdManOperation( pMan, DAU_DSD_PRIME, pLits, nLits, pPermStart, pFunc );
+ return Abc_LitNotCond( iRes, fCompl );
+ }
assert( 0 );
return -1;
}
@@ -1143,9 +1177,23 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
word pCopy[DAU_MAX_WORD], * pRes;
char pDsd[DAU_MAX_STR];
int iDsd, nSizeNonDec, nSupp = 0;
+ abctime clk;
assert( nLeaves <= DAU_MAX_VAR );
Abc_TtCopy( pCopy, pTruth, p->nWords, 0 );
- nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 0, pDsd );
+clk = Abc_Clock();
+ nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
+p->timeDsd += Abc_Clock() - clk;
+/*
+ if ( nLeaves <= 6 )
+ {
+ word pCopy2[DAU_MAX_WORD], t;
+ char pDsd2[DAU_MAX_STR];
+ Abc_TtCopy( pCopy2, pTruth, p->nWords, 0 );
+ nSizeNonDec = Dau_DsdDecompose( pCopy2, nLeaves, 0, 1, pDsd2 );
+ t = Dau_Dsd6ToTruth( pDsd2 );
+ assert( t == *pTruth );
+ }
+*/
// if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
// {
// int x = 0;
@@ -1153,17 +1201,24 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
if ( nSizeNonDec > 0 )
Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
memset( pPerm, 0xFF, nLeaves );
+clk = Abc_Clock();
iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp );
+p->timeCanon += Abc_Clock() - clk;
assert( nSupp == nLeaves );
// verify the result
+clk = Abc_Clock();
pRes = If_DsdManComputeTruth( p, iDsd, pPerm );
+p->timeVerify += Abc_Clock() - clk;
if ( !Abc_TtEqual(pRes, pTruth, p->nWords) )
{
// If_DsdManPrint( p, NULL );
printf( "\n" );
printf( "Verification failed!\n" );
+ printf( "%s\n", pDsd );
Dau_DsdPrintFromTruth( pTruth, nLeaves );
Dau_DsdPrintFromTruth( pRes, nLeaves );
+// Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" );
+// Kit_DsdPrintFromTruth( (unsigned *)pRes, nLeaves ); printf( "\n" );
If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
printf( "\n" );
}
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 5025429e..d03fc200 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -161,7 +161,9 @@ void If_ManStop( If_Man_t * p )
if ( p->pPars->fVerbose && p->nCuts5 )
Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 );
if ( p->pPars->fUseDsd )
- If_DsdManFree( p->pIfDsdMan );
+ If_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose );
+ if ( p->pPars->fUseDsd )
+ printf( "NonDec0 = %d. NonDec1 = %d.\n", p->nCountNonDec[0], p->nCountNonDec[1] );
// Abc_PrintTime( 1, "Truth", p->timeTruth );
// Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
Vec_IntFreeP( &p->vCoAttrs );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index c719215f..d7b7f4cc 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -279,6 +279,39 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
if ( Value != (int)pCut->fUseless )
{
+ if ( pCut->fUseless && !Value )
+ p->nCountNonDec[0]++;
+ if ( !pCut->fUseless && Value )
+ p->nCountNonDec[1]++;
+/*
+// if ( pCut->fUseless && !Value )
+// printf( "Old does not work. New works.\n" );
+ if ( !pCut->fUseless && Value )
+ printf( "Old works. New does not work. DSD = %d.\n", Abc_Lit2Var(pCut->iCutDsd) );
+ if ( !pCut->fUseless && Value )
+ {
+ extern word If_Dec6Perform( word t, int fDerive );
+ extern word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits );
+ int s;
+
+// word z, t = *If_CutTruthW(p, pCut);
+ word z, t = *If_DsdManComputeTruth( p->pIfDsdMan, pCut->iCutDsd, NULL );
+
+ Extra_PrintHex( stdout, (unsigned *)If_CutTruthW(p, pCut), pCut->nLeaves ); printf( "\n" );
+
+ Dau_DsdPrintFromTruth( &t, pCut->nLeaves );
+// Dau_DsdPrintFromTruth( If_CutTruthW(p, pCut), pCut->nLeaves );
+// If_DsdManPrintOne( stdout, p->pIfDsdMan, Abc_Lit2Var(pCut->iCutDsd), pCut->pPerm, 1 );
+// printf( "Old works. New does not work. DSD = %d.\n", Abc_Lit2Var(pCut->iCutDsd) );
+
+ z = If_Dec6Perform( t, 1 );
+ If_DecPrintConfig( z );
+
+ s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 1 );
+ printf( "Confirm %d\n", s );
+ s = 0;
+ }
+*/
}
}
}
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
index 0afe7ea5..5ddb8241 100644
--- a/src/map/if/ifSat.c
+++ b/src/map/if/ifSat.c
@@ -122,12 +122,12 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
v = 0;
Vec_IntForEachEntry( vLits, Value, m )
{
- printf( "%d", (Value >= 0) ? Value : 2 );
+// printf( "%d", (Value >= 0) ? Value : 2 );
if ( Value >= 0 )
Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
}
Vec_IntShrink( vLits, v );
- printf( " %d\n", Vec_IntSize(vLits) );
+// printf( " %d\n", Vec_IntSize(vLits) );
// run SAT solver
Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
if ( Value != l_True )
@@ -162,7 +162,7 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
SeeAlso []
***********************************************************************/
-void If_ManSatTest()
+void If_ManSatTest2()
{
int nVars = 6;
int nLutSize = 4;
@@ -190,6 +190,67 @@ void If_ManSatTest()
Vec_IntFree( vLits );
}
+void If_ManSatTest()
+{
+ int nVars = 4;
+ int nLutSize = 3;
+ sat_solver * p = If_ManSatBuildXY( nLutSize );
+ word t = 0x183C, * pTruth = &t;
+ word uBound, uFree;
+ unsigned uSet;
+ int RetValue;
+ Vec_Int_t * vLits = Vec_IntAlloc( 100 );
+
+
+ uSet = (3 << 0) | (1 << 2) | (1 << 4);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 0) | (3 << 2) | (1 << 4);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 0) | (1 << 2) | (3 << 4);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+
+
+ uSet = (3 << 0) | (1 << 2) | (1 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 0) | (3 << 2) | (1 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 0) | (1 << 2) | (3 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+
+
+ uSet = (3 << 0) | (1 << 4) | (1 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 0) | (3 << 4) | (1 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 0) | (1 << 4) | (3 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+
+
+ uSet = (3 << 2) | (1 << 4) | (1 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 2) | (3 << 4) | (1 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+ uSet = (1 << 2) | (1 << 4) | (3 << 6);
+ RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
+ printf( "%d", RetValue );
+
+ printf( "\n" );
+
+ sat_solver_delete(p);
+ Vec_IntFree( vLits );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/module.make b/src/map/if/module.make
index c8c18e88..f0c1860f 100644
--- a/src/map/if/module.make
+++ b/src/map/if/module.make
@@ -12,6 +12,7 @@ SRC += src/map/if/ifCom.c \
src/map/if/ifMan.c \
src/map/if/ifMap.c \
src/map/if/ifReduce.c \
+ src/map/if/ifSat.c \
src/map/if/ifSelect.c \
src/map/if/ifSeq.c \
src/map/if/ifTime.c \
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 051abb7d..5699962e 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -98,6 +98,7 @@ extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
/*=== dauNonDsd.c ==========================================================*/
+extern Vec_Int_t * Dau_DecFindSets_int( word * pInit, int nVars, int * pSched[16] );
extern Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars );
extern void Dau_DecSortSet( unsigned set, int nVars, int * pnUnique, int * pnShared, int * pnFree );
extern void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars );
diff --git a/src/opt/dau/dauNonDsd.c b/src/opt/dau/dauNonDsd.c
index 53eafe92..ec16c9ab 100644
--- a/src/opt/dau/dauNonDsd.c
+++ b/src/opt/dau/dauNonDsd.c
@@ -459,20 +459,17 @@ void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB,
Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
assert( c == nVars - sizeB );
}
-Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
+Vec_Int_t * Dau_DecFindSets_int( word * pInit, int nVars, int * pSched[16] )
{
Vec_Int_t * vSets = Vec_IntAlloc( 32 );
int V2P[16], P2V[16], pVarsB[16];
int Limit = (1 << nVars);
int c, v, sizeB, sizeS, maskB, maskS;
- int * pSched[16] = {NULL};
unsigned setMixed;
word p[1<<10];
memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
for ( v = 0; v < nVars; v++ )
assert( Abc_TtHasVar( p, nVars, v ) );
- for ( v = 2; v < nVars; v++ )
- pSched[v] = Extra_GreyCodeSchedule( v );
// initialize permutation
for ( v = 0; v < nVars; v++ )
V2P[v] = P2V[v] = v;
@@ -514,6 +511,15 @@ Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
Vec_IntPush( vSets, setMixed );
}
}
+ return vSets;
+}
+Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
+{
+ Vec_Int_t * vSets;
+ int v, * pSched[16] = {NULL};
+ for ( v = 2; v < nVars; v++ )
+ pSched[v] = Extra_GreyCodeSchedule( v );
+ vSets = Dau_DecFindSets_int( pInit, nVars, pSched );
for ( v = 2; v < nVars; v++ )
ABC_FREE( pSched[v] );
return vSets;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 20:55:49 +0000