DSD manager.

5 files changed, 34 insertions, 26 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index f1d78ff4..4505f6d4 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -98,6 +98,7 @@ struct If_Par_t_
     int                nFlowIters;    // the number of iterations of area recovery
     int                nAreaIters;    // the number of iterations of area recovery
     int                nGateSize;     // the max size of the AND/OR gate to map into
+    int                nNonDecLimit;  // the max size of non-dec nodes
     float              DelayTarget;   // delay target
     float              Epsilon;       // value used in comparison floating point numbers
     int                fPreprocess;   // preprossing
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index ca985910..ace197fb 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -856,7 +856,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
         return;
     }
 
-    if ( (p->pPars->fUseBat || p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || p->pPars->fEnableCheck10 || p->pPars->pLutStruct || p->pPars->fUserRecLib) && !pCut->fUseless )
+    if ( (p->pPars->fUseDsd || p->pPars->fUseBat || p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || p->pPars->fEnableCheck10 || p->pPars->pLutStruct || p->pPars->fUserRecLib) && !pCut->fUseless )
     {
         If_Cut_t * pFirst = pCutSet->ppCuts[0];
         if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 )
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 076f74d6..1cc92def 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -85,7 +85,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
     {
 //    p->pNamDsd   = Abc_NamStart( 1000, 20 );
 //    p->iNamVar   = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL );
-        p->pDsdMan = Dss_ManAlloc( pPars->nLutSize );
+        p->pDsdMan = Dss_ManAlloc( pPars->nLutSize, pPars->nNonDecLimit );
         p->iNamVar = 2;
     }
 
@@ -165,6 +165,7 @@ void If_ManStop( If_Man_t * p )
 //        Abc_NamPrint( p->pNamDsd );
         Abc_NamStop( p->pNamDsd );
 */
+        Dss_ManPrint( p->pDsdMan );
         Dss_ManFree( p->pDsdMan );
     }
 //    Abc_PrintTime( 1, "Truth", p->timeTruth );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index ad50e1cc..ac606416 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -277,32 +277,36 @@ 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), 
-                Abc_NamStr(p->pNamDsd, pCut1->iDsd), 
-                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] )
+            if ( pCut0->iDsd < 0 || pCut1->iDsd < 0 )
+                pCut->iDsd = -1;
+            else
+            {
+                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] };
+                // 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, If_CutTruthW(pCut) );
+            }
+            if ( pCut->iDsd < 0 )
             {
-                ABC_SWAP( int, iDsd[0], iDsd[1] );
-                ABC_SWAP( int, nFans[0], nFans[1] );
-                ABC_SWAP( int *, pFans[0], pFans[1] );
+                pCut->fUseless = 1;
+                p->nCutsUselessAll++;
+                p->nCutsUseless[pCut->nLeaves]++;
             }
-            // derive new DSD
-            pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, pCut->pPerm );
+            p->nCutsCountAll++;
+            p->nCutsCount[pCut->nLeaves]++;
         }
         
         // compute the application-specific cost and depth
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 4c7a1d96..c86e4381 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -475,6 +475,7 @@ static inline int If_CutTruthMinimize6( If_Man_t * p, If_Cut_t * pCut )
 // TEMPORARY
     if ( nSuppSize < 2 )
     {
+//printf( "Small supp\n" );
         p->nSmallSupp++;
         return 2;
     }
@@ -602,6 +603,7 @@ static inline int If_CutTruthMinimize2( If_Man_t * p, If_Cut_t * pCut )
 // TEMPORARY
     if ( nSuppSize < 2 )
     {
+//printf( "Small supp\n" );
         p->nSmallSupp++;
         return 2;
     }