Changes to LUT mappers.

abcexe.dsp

@@ -90,10 +90,6 @@ LINK32=link.exe
 
 SOURCE=.\src\base\main\main.c
 # End Source File
-# Begin Source File
-
-SOURCE=.\src\sat\bsat\satSolver.c
-# End Source File
 # End Group
 # Begin Group "Header Files"
 

src/map/if/if.h

@@ -516,7 +516,7 @@ extern int             If_CluCheckExt3( void * p, word * pTruth, int nVars, int
 /*=== ifDsd.c =============================================================*/
 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 );
+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 );
 /*=== ifLib.c =============================================================*/

src/map/if/ifDsd.c

@@ -275,8 +275,8 @@ void If_DsdManFree( If_DsdMan_t * p )
 {
     int fVerbose = 0;
 //    If_DsdManDump( p );
-    If_DsdManPrint( p, NULL );
-    Vec_MemDumpTruthTables( p->vTtMem, NULL, p->nVars );
+    If_DsdManPrint( p, NULL, 0 );
+    Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
     if ( fVerbose )
     {
         Abc_PrintTime( 1, "Time begin ", p->timeBeg );
@@ -343,7 +343,7 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char
     fprintf( pFile, "\n" );
     assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) );
 }
-void If_DsdManPrint( If_DsdMan_t * p, char * pFileName )
+void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
 {
     If_DsdObj_t * pObj;
     int CountNonDsd = 0, CountNonDsdStr = 0;
@@ -372,6 +372,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName )
 //    If_DsdManHashProfile( p );
 //    If_DsdManDump( p );
 //    return;
+    if ( !fVerbose )
+        return;
     If_DsdVecForEachObj( p->vObjs, pObj, i )
     {
 //        if ( i == 50 )
@@ -844,8 +846,10 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
     int iRes = -1, fCompl = 0;
     if ( *pDsd == '!' )
          pDsd++, fCompl = 1;
-    if ( Dau_DsdIsConst(pDsd) )
+    if ( Dau_DsdIsConst0(pDsd) )
         iRes = 0;
+    else if ( Dau_DsdIsConst1(pDsd) )
+        iRes = 1;
     else if ( Dau_DsdIsVar(pDsd) )
     {
         pPerm[(*pnSupp)++] = Dau_DsdReadVar(pDsd);

src/map/if/ifMap.c

@@ -251,7 +251,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 }
             }
         }
-        if ( p->pPars->fUseDsd )
+        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