DSD manager.

src/base/abci/abc.c

@@ -14890,6 +14890,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->nLutSize    =  pPars->nGateSize;
     }
 
+    if ( pPars->fUseDsd )
+    {
+        pPars->fTruth      =  1;
+        pPars->fCutMin     =  1;
+        pPars->fUsePerm    =  1;
+    }
+
     if ( pPars->fUserRecLib )
     {
         if ( Abc_NtkRecIsRunning() + Abc_NtkRecIsRunning2() + Abc_NtkRecIsRunning3() != 1 )
@@ -27461,6 +27468,13 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
         pPars->nLutSize    =  pPars->nGateSize;
     }
 
+    if ( pPars->fUseDsd )
+    {
+        pPars->fTruth      =  1;
+        pPars->fCutMin     =  1;
+        pPars->fUsePerm    =  1;
+    }
+
     // complain if truth tables are requested but the cut size is too large
     if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
     {

src/map/if/if.h

@@ -35,7 +35,7 @@
 #include "misc/mem/mem.h"
 #include "misc/tim/tim.h"
 #include "misc/util/utilNam.h"
-
+#include "opt/dau/dau.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -189,6 +189,7 @@ struct If_Man_t_
     Vec_Int_t *        vSwitching;    // switching activity of each node
     Vec_Int_t **       pDriverCuts;   // temporary driver cuts
     int                pPerm[3][IF_MAX_LUTSIZE]; // permutations
+    unsigned           uSharedMask;   // mask of shared variables
     int                nShared;       // the number of shared variables
     // SOP balancing
     Vec_Int_t *        vCover;        // used to compute ISOP
@@ -218,8 +219,9 @@ struct If_Man_t_
     int                nCutsCount[32];
     int                nCutsCountAll;
     int                nCutsUselessAll;
-    Abc_Nam_t *        pNamDsd;
+//    Abc_Nam_t *        pNamDsd;
     int                iNamVar;
+    Dss_Man_t *        pDsdMan;
 
     // timing manager
     Tim_Man_t *        pManTim;

src/map/if/ifCut.c

@@ -418,11 +418,13 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
         p->nShared = nLimit;
         pC->nLeaves = nLimit;
         pC->uSign = pC0->uSign | pC1->uSign;
+        p->uSharedMask = Abc_InfoMask( nLimit );
         return 1;
     }
 
     // compare two cuts with different numbers
     i = k = c = s = 0;
+    p->uSharedMask = 0;
     while ( 1 )
     {
         if ( c == nLimit ) return 0;
@@ -440,6 +442,7 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
         }
         else
         {
+            p->uSharedMask |= (1 << c);
             p->pPerm[0][i] = p->pPerm[1][k] = p->pPerm[2][s++] = c;
             pC->pLeaves[c++] = pC0->pLeaves[i++]; k++;
             if ( i == nSizeC0 ) goto FlushCut1;

src/map/if/ifMan.c

@@ -83,8 +83,10 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     p->pCutTemp  = (If_Cut_t *)ABC_ALLOC( char, p->nCutBytes );
     if ( pPars->fUseDsd )
     {
-    p->pNamDsd   = Abc_NamStart( 1000, 20 );
-    p->iNamVar   = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL );
+//    p->pNamDsd   = Abc_NamStart( 1000, 20 );
+//    p->iNamVar   = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL );
+        p->pDsdMan = Dss_ManAlloc( pPars->nLutSize );
+        p->iNamVar = 2;
     }
 
     // create the constant node
@@ -150,8 +152,9 @@ void If_ManStop( If_Man_t * p )
                 Abc_Print( 1, "Useless cuts %2d  = %9d  (out of %9d)  (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) );
         Abc_Print( 1, "Useless cuts all = %9d  (out of %9d)  (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) );
     }
-    if ( p->pNamDsd )
+    if ( p->pPars->fUseDsd )
     {
+/*
         if ( p->pPars->fVerbose )
             Abc_Print( 1, "Number of unique entries in the DSD table = %d.  Memory = %.1f MB.\n", 
                 Abc_NamObjNumMax(p->pNamDsd), 1.0*Abc_NamMemAlloc(p->pNamDsd)/(1<<20) );
@@ -161,6 +164,8 @@ void If_ManStop( If_Man_t * p )
         Abc_PrintTime( 1, "Time3", s_TimeComp[3] );
 //        Abc_NamPrint( p->pNamDsd );
         Abc_NamStop( p->pNamDsd );
+*/
+        Dss_ManFree( p->pDsdMan );
     }
 //    Abc_PrintTime( 1, "Truth", p->timeTruth );
 //    Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
@@ -427,7 +432,11 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
     pCut->nLeaves    = 1;
     pCut->pLeaves[0] = p->pPars->fLiftLeaves? (ObjId << 8) : ObjId;
     pCut->uSign      = If_ObjCutSign( pCut->pLeaves[0] );
-    pCut->iDsd       = p->iNamVar;
+    if ( p->pPars->fUseDsd )
+    {
+        pCut->iDsd     = p->iNamVar;
+        pCut->pPerm[0] = 0;
+    }
     // set up elementary truth table of the unit cut
     if ( p->pPars->fTruth )
     {

src/map/if/ifMap.c

@@ -277,6 +277,10 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         }
         if ( p->pPars->fUseDsd )
         {
+            int j, iDsd[2] = { Abc_LitNotCond(pCut0->iDsd, pObj->fCompl0), Abc_LitNotCond(pCut1->iDsd, pObj->fCompl1) };
+            int nFans[2] = { pCut0->nLeaves, pCut1->nLeaves };
+            int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] };
+/*
             char * pName = Dau_DsdMerge( 
                 Abc_NamStr(p->pNamDsd, pCut0->iDsd), 
                 If_CutPerm0(pCut, pCut0), 
@@ -284,6 +288,21 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 If_CutPerm1(pCut, pCut1), 
                 pObj->fCompl0, pObj->fCompl1, pCut->nLimit );
             pCut->iDsd = Abc_NamStrFindOrAdd( p->pNamDsd, pName, NULL );
+*/
+            // create fanins
+            for ( j = 0; j < (int)pCut0->nLeaves; j++ )
+                pFans[0][j] = Abc_Lit2Lit( p->pPerm[0], (int)pCut0->pPerm[j] );
+            for ( j = 0; j < (int)pCut1->nLeaves; j++ )
+                pFans[1][j] = Abc_Lit2Lit( p->pPerm[1], (int)pCut1->pPerm[j] );
+            // canonicize
+            if ( iDsd[0] > iDsd[1] )
+            {
+                ABC_SWAP( int, iDsd[0], iDsd[1] );
+                ABC_SWAP( int, nFans[0], nFans[1] );
+                ABC_SWAP( int *, pFans[0], pFans[1] );
+            }
+            // derive new DSD
+            pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, pCut->pPerm );
         }
         
         // compute the application-specific cost and depth

src/misc/util/abc_global.h

@@ -257,6 +257,7 @@ static inline int      Abc_LitIsCompl( int Lit )              { return Lit & 1;
 static inline int      Abc_LitNot( int Lit )                  { return Lit ^ 1;            }
 static inline int      Abc_LitNotCond( int Lit, int c )       { return Lit ^ (int)(c > 0); }
 static inline int      Abc_LitRegular( int Lit )              { return Lit & ~01;          }
+static inline int      Abc_Lit2Lit( int * pMap, int Lit )     { return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) );   }
 
 enum Abc_VerbLevel
 {

src/opt/dau/dau.h

@@ -87,6 +87,12 @@ extern int           Dau_DsdCountAnds( char * pDsd );
 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 );
 
+/*=== dauMerge.c  ==========================================================*/
+extern Dss_Man_t *   Dss_ManAlloc( int nVars );
+extern void          Dss_ManFree( Dss_Man_t * p );
+extern int           Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPerm );
+
+
 ABC_NAMESPACE_HEADER_END