Changes to LUT mappers.

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;