Changes to LUT mappers.

src/base/abci/abc.c

@@ -2201,7 +2201,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     extern void Kit_DsdTest( unsigned * pTruth, int nVars );
     extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose );
-    extern void Dau_DecTrySets( word * p, int nVars );
+    extern void Dau_DecTrySets( word * p, int nVars, int fVerbose );
 
     // set defaults
     nCofLevel = 1;
@@ -2274,7 +2274,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
 //        Abc_Print( -1, "\n" );
         if ( fPrintDec )//&&Abc_ObjFaninNum(pObj) <= 6 )
-            Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj) );
+            Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj), 1 );
         if ( fProfile )
             Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) );
         else if ( fCofactor )

src/base/abci/abcDec.c

@@ -25,6 +25,7 @@
 #include "bool/dec/dec.h"
 #include "bool/kit/kit.h"
 #include "opt/dau/dau.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -564,11 +565,13 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
     {
         for ( i = 0; i < p->nFuncs; i++ )
         {
-            extern void Dau_DecTrySets( word * pInit, int nVars );
+            extern void Dau_DecTrySets( word * pInit, int nVars, int fVerbose );
+            int nSuppSize = Abc_TtSupportSize( p->pFuncs[i], p->nVars );
             if ( fVerbose )
                 printf( "%7d :      ", i );
-            Dau_DecTrySets( p->pFuncs[i], p->nVars );
-            printf( "\n" );
+            Dau_DecTrySets( p->pFuncs[i], nSuppSize, fVerbose );
+            if ( fVerbose )
+                printf( "\n" );
         }
     }
     else assert( 0 );

src/map/if/if.h

@@ -35,9 +35,9 @@
 #include "misc/mem/mem.h"
 #include "misc/tim/tim.h"
 #include "misc/util/utilNam.h"
-#include "opt/dau/dau.h"
 #include "misc/vec/vecMem.h"
 #include "misc/util/utilTruth.h"
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -153,8 +153,8 @@ struct If_Par_t_
     float *            pTimesArr;     // arrival times
     float *            pTimesReq;     // required times
     int (* pFuncCost)  (If_Man_t *, If_Cut_t *);  // procedure to compute the user's cost of a cut
-    int (* pFuncUser)  (If_Man_t *, If_Obj_t *, If_Cut_t *); //  procedure called for each cut when cut computation is finished
-    int (* pFuncCell)  (If_Man_t *, unsigned *, int, int, char *);       //  procedure called for cut functions
+    int (* pFuncUser)  (If_Man_t *, If_Obj_t *, If_Cut_t *);        //  procedure called for each cut when cut computation is finished
+    int (* pFuncCell)  (If_Man_t *, unsigned *, int, int, char *);  //  procedure called for cut functions
     void *             pReoMan;       // reordering manager
 };
 
@@ -233,6 +233,7 @@ struct If_Man_t_
     int                nCuts5, nCuts5a;
     If_DsdMan_t *      pIfDsdMan;
     Vec_Mem_t *        vTtMem;        // truth table memory and hash table
+    Vec_Int_t *        vDsds;         // mapping of truth table into DSD
     int                nBestCutSmall[2];
 
     // timing manager
@@ -518,7 +519,8 @@ 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 int             If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm );
+extern int             If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
+extern int             If_DsdManCheckDec( If_DsdMan_t * pIfMan, int iDsd );
 /*=== ifLib.c =============================================================*/
 extern If_LibLut_t *   If_LibLutRead( char * FileName );
 extern If_LibLut_t *   If_LibLutDup( If_LibLut_t * p );

src/map/if/ifDsd.c

@@ -44,7 +44,8 @@ struct If_DsdObj_t_
     unsigned       Id;             // node ID
     unsigned       Type    :  3;   // node type
     unsigned       nSupp   :  5;   // variable
-    unsigned       Count   : 19;   // variable
+    unsigned       fMark   :  1;   // user mark
+    unsigned       Count   : 18;   // variable
     unsigned       nFans   :  5;   // fanin count
     unsigned       pFans[0];       // fanins
 };
@@ -58,10 +59,10 @@ struct If_DsdMan_t_
     Mem_Flex_t *   pMem;           // memory for nodes
     Vec_Ptr_t *    vObjs;          // objects
     Vec_Int_t *    vNexts;         // next pointers
-    Vec_Int_t *    vLeaves;        // temp
-    Vec_Int_t *    vCopies;        // temp
+    Vec_Int_t *    vNodes;         // temp
     word **        pTtElems;       // elementary TTs
     Vec_Mem_t *    vTtMem;         // truth table memory and hash table
+    Vec_Ptr_t *    vTtDecs;        // truth table decompositions
     int            nUniqueHits;    // statistics
     int            nUniqueMisses;  // statistics
     abctime        timeBeg;        // statistics
@@ -90,13 +91,15 @@ static inline If_DsdObj_t * If_DsdVecVar( Vec_Ptr_t * p, int v )
 static inline int           If_DsdVecObjSuppSize( Vec_Ptr_t * p, int iObj )            { return If_DsdVecObj( p, iObj )->nSupp;                                             }
 static inline int           If_DsdVecLitSuppSize( Vec_Ptr_t * p, int iLit )            { return If_DsdVecObjSuppSize( p, Abc_Lit2Var(iLit) );                               }
 static inline int           If_DsdVecObjRef( Vec_Ptr_t * p, int iObj )                 { return If_DsdVecObj( p, iObj )->Count;                                             }
-static inline void          If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj )              { if ( If_DsdVecObjRef(p, iObj) < 0x7FFFF ) If_DsdVecObj( p, iObj )->Count++;        }
+static inline void          If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj )              { if ( If_DsdVecObjRef(p, iObj) < 0x3FFFF ) If_DsdVecObj( p, iObj )->Count++;        }
 static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
+static inline int           If_DsdVecObjMark( Vec_Ptr_t * p, int iObj )                { return If_DsdVecObj( p, iObj )->fMark;                                             }
+static inline void          If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj )             { If_DsdVecObj( p, iObj )->fMark = 1;                                                }
 
 #define If_DsdVecForEachObj( vVec, pObj, i )                \
     Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )
-#define If_DsdVecForEachObjVec( vLits, vVec, pObj, i )      \
-    for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ )
+#define If_DsdVecForEachObjVec( vNodes, vVec, pObj, i )      \
+    for ( i = 0; (i < Vec_IntSize(vNodes)) && ((pObj) = If_DsdVecObj(vVec, Vec_IntEntry(vNodes,i))); i++ )
 #define If_DsdVecForEachNode( vVec, pObj, i )               \
     Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )     \
         if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR ) {} else
@@ -183,6 +186,7 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
     pObj->Type   = Type;
     pObj->nFans  = nFans;
     pObj->Id     = Vec_PtrSize( p->vObjs );
+    pObj->fMark  = 0;
     pObj->Count  = 0;
     Vec_PtrPush( p->vObjs, pObj );
     Vec_IntPush( p->vNexts, 0 );
@@ -263,10 +267,11 @@ If_DsdMan_t * If_DsdManAlloc( int nVars )
     p->vNexts = Vec_IntAlloc( 10000 );
     If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
     If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
-    p->vLeaves  = Vec_IntAlloc( 32 );
-    p->vCopies  = Vec_IntAlloc( 32 );
+    p->vNodes   = Vec_IntAlloc( 32 );
     p->pTtElems = If_ManDsdTtElems();
-    p->vTtMem   = Vec_MemAllocForTT( nVars );
+    p->vTtDecs  = Vec_PtrAlloc( 1000 );
+    p->vTtMem   = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 );
+    Vec_MemHashAlloc( p->vTtMem, 10000 );
     return p;
 }
 void If_DsdManFree( If_DsdMan_t * p )
@@ -282,10 +287,10 @@ void If_DsdManFree( If_DsdMan_t * p )
         Abc_PrintTime( 1, "Time lookup", p->timeLook );
         Abc_PrintTime( 1, "Time end   ", p->timeEnd );
     }
+    Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
     Vec_MemHashFree( p->vTtMem );
     Vec_MemFreeP( &p->vTtMem );
-    Vec_IntFreeP( &p->vCopies );
-    Vec_IntFreeP( &p->vLeaves );
+    Vec_IntFreeP( &p->vNodes );
     Vec_IntFreeP( &p->vNexts );
     Vec_PtrFreeP( &p->vObjs );
     Mem_FlexStop( p->pMem, 0 );
@@ -331,20 +336,21 @@ void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, unsigned ch
         If_DsdManPrint_rec( pFile, p, iFanin, pPermLits, pnSupp );
     fprintf( pFile, "%c", CloseType[If_DsdObjType(pObj)] );
 }
-void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits )
+void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits, int fNewLine )
 {
     int nSupp = 0;
     fprintf( pFile, "%6d : ", iObjId );
     fprintf( pFile, "%2d ",   If_DsdVecObjSuppSize(p->vObjs, iObjId) );
     fprintf( pFile, "%8d ",   If_DsdVecObjRef(p->vObjs, iObjId) );
     If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp );
-    fprintf( pFile, "\n" );
+    if ( fNewLine )
+        fprintf( pFile, "\n" );
     assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) );
 }
 void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
 {
     If_DsdObj_t * pObj;
-    int CountNonDsd = 0, CountNonDsdStr = 0;
+    int DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0;
     int i, clk = Abc_Clock();
     FILE * pFile;
     pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
@@ -355,17 +361,20 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
     }
     If_DsdVecForEachObj( p->vObjs, pObj, i )
     {
-        CountNonDsd += (If_DsdObjType(pObj) == IF_DSD_PRIME);
+        if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
+            DsdMax = Abc_MaxInt( DsdMax, pObj->nFans ); 
         CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id );
+        CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 );
     }
     fprintf( pFile, "Total number of objects    = %8d\n", Vec_PtrSize(p->vObjs) );
-    fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", Vec_MemEntryNum(p->vTtMem), CountNonDsd );
+    fprintf( pFile, "Externally used objects    = %8d\n", CountUsed );
+    fprintf( pFile, "Non-DSD objects (max =%2d)  = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) );
     fprintf( pFile, "Non-DSD structures         = %8d\n", CountNonDsdStr );
-    fprintf( pFile, "Memory used for objects    = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
-    fprintf( pFile, "Memory used for array      = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
-    fprintf( pFile, "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
     fprintf( pFile, "Unique table hits          = %8d\n", p->nUniqueHits );
     fprintf( pFile, "Unique table misses        = %8d\n", p->nUniqueMisses );
+    fprintf( pFile, "Memory used for objects    = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
+    fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
+    fprintf( pFile, "Memory used for array      = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
     Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
 //    If_DsdManHashProfile( p );
 //    If_DsdManDump( p );
@@ -376,7 +385,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
     {
 //        if ( i == 50 )
 //            break;
-        If_DsdManPrintOne( pFile, p, pObj->Id, NULL );
+        If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 );
     }
     fprintf( pFile, "\n" );
     if ( pFileName )
@@ -403,13 +412,39 @@ void If_DsdManDump( If_DsdMan_t * p )
         fprintf( pFile, "\n" );
         printf( "    " );
         Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
-        printf( "\n" );
     }
     fclose( pFile );
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Collect nodes of the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+{
+    int i, iFanin;
+    If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
+    if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
+        return;
+    If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
+        If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
+    Vec_IntPush( vNodes, Id );
+}
+void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+{
+    Vec_IntClear( vNodes );
+    If_DsdManCollect_rec( p, Id, vNodes );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -470,6 +505,12 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
     unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
     if ( *pSpot )
         return *pSpot;
+    if ( truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem)-1 )
+    {
+        Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits );
+        Vec_PtrPush( p->vTtDecs, vSets );
+//        Dau_DecPrintSets( vSets, nLits );
+    }
     *pSpot = Vec_PtrSize( p->vObjs );
     return If_DsdObjCreate( p, Type, pLits, nLits, truthId );
 }
@@ -768,6 +809,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
         assert( j == nSSize );
         for ( j = 0; j < nSSize; j++ )
             pPerm[j] = pPermNew[j];
+        Abc_TtStretch6( pTruth, nLits, p->nVars );
     }
     else assert( 0 );
     // create new graph
@@ -864,6 +906,158 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if XY-decomposability holds to this LUT size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+// collect supports of the node
+void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
+{
+    If_DsdObj_t * pFanin; int i;
+    If_DsdObjForEachFanin( p->vObjs, pObj, pFanin, i )
+        pSSizes[i] = If_DsdObjSuppSize(pFanin);    
+}
+// checks if there is a way to package some fanins 
+int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
+{
+    int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
+    int nFans = If_DsdObjFaninNum(pObj);
+    assert( pObj->nFans > 2 );
+    assert( If_DsdObjSuppSize(pObj) > LutSize );
+    If_DsdManGetSuppSizes( p, pObj, pSSizes );
+    LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
+    assert( LimitOut < LutSize );
+    for ( i[0] = 0;      i[0] < nFans; i[0]++ )
+    for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
+    {
+        SizeIn = pSSizes[i[0]] + pSSizes[i[1]];
+        SizeOut = pObj->nSupp - SizeIn;
+        if ( SizeIn > LutSize || SizeOut > LimitOut )
+            continue;
+        return (1 << i[0]) | (1 << i[1]);
+    }
+    if ( pObj->nFans == 3 )
+        return 0;
+    for ( i[0] = 0;      i[0] < nFans; i[0]++ )
+    for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
+    for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
+    {
+        SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]];
+        SizeOut = pObj->nSupp - SizeIn;
+        if ( SizeIn > LutSize || SizeOut > LimitOut )
+            continue;
+        return (1 << i[0]) | (1 << i[1]) | (1 << i[2]);
+    }
+    return 0;
+}
+// checks if there is a way to package some fanins 
+int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
+{
+    int fVerbose = 0;
+    int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
+    int truthId = If_DsdObjTruthId( p, pObj );
+    int nFans = If_DsdObjFaninNum(pObj);
+    Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId);
+if ( fVerbose )
+printf( "\n" );
+if ( fVerbose )
+Dau_DecPrintSets( vSets, nFans );
+    assert( pObj->nFans > 2 );
+    assert( If_DsdObjSuppSize(pObj) > LutSize );
+    If_DsdManGetSuppSizes( p, pObj, pSSizes );
+    LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
+    assert( LimitOut < LutSize );
+    Vec_IntForEachEntry( vSets, set, i )
+    {
+        SizeIn = SizeOut = 0;
+        for ( v = 0; v < nFans; v++ )
+        {
+            int Value = ((set >> (v << 1)) & 3);
+            if ( Value == 0 )
+                SizeOut += pSSizes[v];
+            else if ( Value == 1 )
+                SizeIn += pSSizes[v];
+            else if ( Value == 3 )
+            {
+                SizeIn += pSSizes[v];
+                SizeOut += pSSizes[v];
+            }
+            else assert( Value == 0 );
+            if ( SizeIn > LutSize || SizeOut > LimitOut )
+                break;
+        }
+        if ( v == nFans )
+            return set;
+    }
+    return 0;
+}
+int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
+{
+    int fVerbose = 0;
+    If_DsdObj_t * pObj, * pTemp; int i, Mask;
+    pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
+    if ( fVerbose )
+    If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
+    if ( If_DsdObjSuppSize(pObj) <= LutSize )
+    {
+        if ( fVerbose )
+        printf( "    Trivial\n" );
+        return 1;
+    }
+    If_DsdManCollect( p, pObj->Id, p->vNodes );
+    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+        if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 )
+        {
+            if ( fVerbose )
+            printf( "    Dec using node " );
+            if ( fVerbose )
+            If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
+            return 1;
+        }
+    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+        if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
+        {
+            if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) )
+            {
+                if ( fVerbose )
+                printf( "    " );
+                if ( fVerbose )
+                Abc_TtPrintBinary( (word *)&Mask, 4 ); 
+                if ( fVerbose )
+                printf( "    Using multi-input AND/XOR node\n" );
+                return 1;
+            }
+        }
+    If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+        if ( If_DsdObjType(pTemp) == IF_DSD_PRIME )
+        {
+            if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) )
+            {
+                if ( fVerbose )
+                printf( "    " );
+                if ( fVerbose )
+                Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 );
+                if ( fVerbose )
+                printf( "    Using prime node\n" );
+                return 1;
+            }
+        }
+    if ( fVerbose )
+    printf( "    UNDEC\n" );
+    return 0;
+}
+int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize ) 
+{
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Add the function to the DSD manager.]
 
   Description []
@@ -873,7 +1067,7 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
   SeeAlso     []
 
 ***********************************************************************/
-int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm )
+int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct )
 {
     word pCopy[DAU_MAX_WORD], * pRes;
     char pDsd[DAU_MAX_STR];
@@ -897,14 +1091,25 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
 //        If_DsdManPrint( p, NULL );
         printf( "\n" );
         printf( "Verification failed!\n" );
-        Dau_DsdPrintFromTruth( pTruth, nLeaves ); printf( "\n" );
-        Dau_DsdPrintFromTruth( pRes, nLeaves ); printf( "\n" );
-        If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm );
+        Dau_DsdPrintFromTruth( pTruth, nLeaves );
+        Dau_DsdPrintFromTruth( pRes, nLeaves );
+        If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
         printf( "\n" );
     }
     If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
+    if ( pLutStruct )
+    {
+        int LutSize = (int)(pLutStruct[0] - '0');
+        assert( pLutStruct[2] == 0 );
+        if ( If_DsdManCheckXY( p, iDsd, LutSize ) )
+            If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) );
+    }
     return iDsd;
 }
+int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
+{
+    return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/map/if/ifMan.c

@@ -84,7 +84,12 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->puTemp[3] = p->puTemp[2] + p->nTruth6Words*2;
     p->puTempW   = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL;
     if ( pPars->fUseDsd )
+    {
         p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize );
+        p->vDsds = Vec_IntAlloc( 1000 );
+        Vec_IntPush( p->vDsds, 0 );
+        Vec_IntPush( p->vDsds, 2 );
+    }
     // create the constant node
     p->pConst1   = If_ManSetupObj( p );
     p->pConst1->Type   = IF_CONST1;
@@ -165,9 +170,10 @@ void If_ManStop( If_Man_t * p )
     Vec_WrdFreeP( &p->vAnds );
     Vec_WrdFreeP( &p->vAndGate );
     Vec_WrdFreeP( &p->vOrGate );
-    if ( p->vObjsRev )    Vec_PtrFree( p->vObjsRev );
-    if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder );
-    if ( p->vLags )       Vec_IntFree( p->vLags );
+    Vec_PtrFreeP( &p->vObjsRev );
+    Vec_PtrFreeP( &p->vLatchOrder );
+    Vec_IntFreeP( &p->vLags );
+    Vec_IntFreeP( &p->vDsds );
     Vec_MemHashFree( p->vTtMem );
     Vec_MemFreeP( &p->vTtMem );
     Mem_FixedStop( p->pMemObj, 0 );

src/map/if/ifMap.c

@@ -217,6 +217,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
 //            abctime clk = Abc_Clock();
             If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
 //            p->timeTruth += Abc_Clock() - clk;
+            // run user functions
             pCut->fUseless = 0;
             if ( p->pPars->pFuncCell )
             {
@@ -250,9 +251,26 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                         p->nCuts5a++;
                 }
             }
+            if ( p->pPars->fUseDsd )
+            {
+                int truthId = Abc_Lit2Var(pCut->iCutFunc);
+                if ( Vec_IntSize(p->vDsds) <= truthId || Vec_IntEntry(p->vDsds, truthId) == -1 )
+                {
+                    pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
+                    while ( Vec_IntSize(p->vDsds) <= truthId )
+                        Vec_IntPush( p->vDsds, -1 );
+                    Vec_IntWriteEntry( p->vDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+                }
+                else
+                    pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+                if ( p->pPars->pLutStruct )
+                {
+                    int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
+                    if ( Value != (int)pCut->fUseless )
+                        printf( "Difference\n" );
+                }
+            }
         }
-        if ( p->pPars->fUseDsd && Abc_Lit2Var(pCut->iCutFunc) == Vec_MemEntryNum(p->vTtMem)-1 )
-            pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm );
         
         // compute the application-specific cost and depth
         pCut->fUser = (p->pPars->pFuncCost != NULL);

src/opt/dau/dau.h

@@ -97,6 +97,11 @@ extern void *        Dsm_ManDeriveGia( void * p, int fUseMuxes );
 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( word * pInit, int nVars );
+extern void          Dau_DecPrintSets( Vec_Int_t * vSets, int nVars );
+extern void          Dau_DecPrintSet( unsigned set, int nVars, int fNewLine );
+
 /*=== dauTree.c  ==========================================================*/
 extern Dss_Man_t *   Dss_ManAlloc( int nVars, int nNonDecLimit );
 extern void          Dss_ManFree( Dss_Man_t * p );

src/opt/dau/dauNonDsd.c

@@ -459,7 +459,7 @@ 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 * p, int nVars )
+Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
 {
     Vec_Int_t * vSets = Vec_IntAlloc( 32 );
     int V2P[16], P2V[16], pVarsB[16];
@@ -467,6 +467,8 @@ Vec_Int_t * Dau_DecFindSets( word * p, int 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++ )
@@ -703,7 +705,7 @@ int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD )
     printf( "\n" );
     return 1;
 }
-int Dau_DecPerform( word * p, int nVars, unsigned uSet )
+int Dau_DecPerform6( word * p, int nVars, unsigned uSet )
 {
     word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD;
     char pDsdC[1000], pDsdD[1000];
@@ -760,7 +762,7 @@ int Dau_DecPerform( word * p, int nVars, unsigned uSet )
     return 1;
 }
 
-int Dau_DecPerform2( word * pInit, int nVars, unsigned uSet )
+int Dau_DecPerform( word * pInit, int nVars, unsigned uSet )
 {
     word p[1<<10], pDec[1<<10], pComp[1<<10]; // at most 2^10 words
     char pDsdC[5000], pDsdD[5000];  // at most 2^12 hex digits
@@ -820,15 +822,18 @@ int Dau_DecPerform2( word * pInit, int nVars, unsigned uSet )
     Dau_DecVerify( pInit, nVars, pDsdC, pDsdD );
     return 1;
 }
-void Dau_DecTrySets( word * pInit, int nVars )
+void Dau_DecTrySets( word * pInit, int nVars, int fVerbose )
 {
-    word p[1<<10]; 
     Vec_Int_t * vSets;
     int i, Entry;
     assert( nVars <= 16 );
-    memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
-    vSets = Dau_DecFindSets( p, nVars );
-    Dau_DsdPrintFromTruth( p, nVars ); 
+    vSets = Dau_DecFindSets( pInit, nVars );
+    if ( !fVerbose )
+    {
+        Vec_IntFree( vSets );
+        return;
+    }
+    Dau_DsdPrintFromTruth( pInit, nVars ); 
     printf( "This %d-variable function has %d decomposable variable sets:\n", nVars, Vec_IntSize(vSets) );
     Vec_IntForEachEntry( vSets, Entry, i )
     {
@@ -837,12 +842,12 @@ void Dau_DecTrySets( word * pInit, int nVars )
         if ( nVars > 6 )
         {
             Dau_DecPrintSet( uSet, nVars, 0 );
-            Dau_DecPerform2( pInit, nVars, uSet );
+            Dau_DecPerform( pInit, nVars, uSet );
         }
         else
         {
             Dau_DecPrintSet( uSet, nVars, 1 );
-            Dau_DecPerform( pInit, nVars, uSet );
+            Dau_DecPerform6( pInit, nVars, uSet );
         }
     }
     Vec_IntFree( vSets );
@@ -860,7 +865,7 @@ void Dau_DecFindSetsTest3()
 //    char * pStr = "Abcd";
 //    char * pStr = "ab";
     unsigned uSet = Dau_DecReadSet( pStr );
-    Dau_DecPerform( &t, nVars, uSet );
+    Dau_DecPerform6( &t, nVars, uSet );
 }
 
 void Dau_DecFindSetsTest()
@@ -879,7 +884,7 @@ void Dau_DecFindSetsTest()
 //    word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
 //    word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
 //    word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
-    Dau_DecTrySets( &t, nVars );
+    Dau_DecTrySets( &t, nVars, 1 );
 }