Changes to LUT mappers.

src/aig/gia/giaIf.c

@@ -1193,7 +1193,7 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p
         return RetValue;
     }
     // find the bound set
-    uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, pCutBest->iCutDsd, nLutSize, 1, 0 );
+    uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, pCutBest->iCutDsd, nLutSize, 1, 1, 0 );
     // remap bound set
     uSetNew = 0;
     for ( k = 0; k < If_CutLeaveNum(pCutBest); k++ )

src/base/io/io.c

@@ -216,6 +216,8 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
         sprintf( Command, "read_constr %s", pFileName );
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "c" ) )
         sprintf( Command, "so %s", pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
+        sprintf( Command, "dsd_load %s", pFileName );
     if ( Command[0] )
     {
         Cmd_CommandExecute( pAbc, Command );
@@ -1330,6 +1332,8 @@ int IoCommandWrite( Abc_Frame_t * pAbc, int argc, char **argv )
         sprintf( Command, "write_genlib %s", pFileName );
     else if ( !strcmp( Extra_FileNameExtension(pFileName), "lib" ) )
         sprintf( Command, "write_liberty %s", pFileName );
+    else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
+        sprintf( Command, "dsd_save %s", pFileName );
     if ( Command[0] )
     {
         Cmd_CommandExecute( pAbc, Command );

src/map/if/if.h

@@ -529,7 +529,7 @@ extern char *          If_DsdManFileName( If_DsdMan_t * p );
 extern int             If_DsdManVarNum( If_DsdMan_t * p );
 extern int             If_DsdManLutSize( If_DsdMan_t * p );
 extern int             If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
-extern unsigned        If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose );
+extern unsigned        If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose );
 /*=== 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

@@ -684,7 +684,7 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
     }
 */
     // check decomposability
-    if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0) )
+    if ( p->LutSize && !If_DsdManCheckXY(p, Abc_Var2Lit(pObj->Id, 0), p->LutSize, 0, 0, 0) )
         If_DsdVecObjSetMark( p->vObjs, pObj->Id );
     return pObj->Id;
 }
@@ -1551,11 +1551,10 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri
 //    If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
     return 0;
 }
-unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose )
 {
     unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, fVerbose );
-/*
-    if ( uSet == 0 )
+    if ( uSet == 0 && fHighEffort )
     {
         abctime clk = Abc_Clock();
         int nVars = If_DsdVecLitSuppSize( p->vObjs, iDsd );
@@ -1569,7 +1568,6 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
 //        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
         p->timeCheck2 += Abc_Clock() - clk;
     }
-*/
     return uSet;
 }
 
@@ -1698,7 +1696,7 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec
         if ( fAdd && !pObj->fMark )
             continue;
         pObj->fMark = 0;
-        if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) )
+        if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0, 0) )
             continue;
         if ( fFast )
             Value = 0;

src/map/if/ifMap.c

@@ -313,7 +313,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                             z = If_Dec6Perform( t, 1 );
                             If_DecPrintConfig( z );
 
-                            s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 0, 1 );
+                            s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 0, 0, 1 );
                             printf( "Confirm %d\n", s );
                             s = 0;
                         }