Changes to LUT mappers.

src/aig/gia/giaIf.c

@@ -1528,8 +1528,7 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
     If_Man_t * pIfMan;
     If_Par_t * pPars = (If_Par_t *)pp;
     // disable cut minimization when GIA strucure is needed
-//    if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts )
-    if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->pLutStruct )
+    if ( !pPars->fDelayOpt && !pPars->fUserRecLib && ((!pPars->fDeriveLuts && !pPars->fUseDsd) || !pPars->pLutStruct) )
         pPars->fCutMin = 0;
 
     // reconstruct GIA according to the hierarchy manager

src/map/if/if.h

@@ -574,7 +574,10 @@ extern int             If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, i
 extern void            If_ManImproveMapping( If_Man_t * p );
 /*=== ifSat.c ==========================================================*/
 extern void *          If_ManSatBuildXY( int nLutSize );
+extern void *          If_ManSatBuildXYZ( int nLutSize );
+extern void            If_ManSatUnbuild( void * p );
 extern int             If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits );
+extern unsigned        If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits );
 /*=== ifSeq.c =============================================================*/
 extern int             If_ManPerformMappingSeq( If_Man_t * p );
 /*=== ifTime.c ============================================================*/

src/map/if/ifDsd.c

@@ -67,6 +67,7 @@ struct If_DsdMan_t_
     word **        pTtElems;       // elementary TTs
     Vec_Mem_t *    vTtMem;         // truth table memory and hash table
     Vec_Ptr_t *    vTtDecs;        // truth table decompositions
+    void *         pSat;           // SAT solver
     int *          pSched[16];     // grey code schedules
     int            nUniqueHits;    // statistics
     int            nUniqueMisses;  // statistics
@@ -207,6 +208,8 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
     Vec_MemHashAlloc( p->vTtMem, 10000 );
     for ( v = 2; v < nVars; v++ )
         p->pSched[v] = Extra_GreyCodeSchedule( v );
+    if ( LutSize )
+    p->pSat     = If_ManSatBuildXY( LutSize );
     return p;
 }
 void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
@@ -234,6 +237,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
     Vec_IntFreeP( &p->vNexts );
     Vec_PtrFreeP( &p->vObjs );
     Mem_FlexStop( p->pMem, 0 );
+    If_ManSatUnbuild( p->pSat );
     ABC_FREE( p->pStore );
     ABC_FREE( p->pBins );
     ABC_FREE( p );
@@ -618,6 +622,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
     p->pStore = Abc_UtilStrsav( pFileName );
     RetValue = fread( &Num, 4, 1, pFile );
     p->LutSize = Num;
+    p->pSat  = If_ManSatBuildXY( p->LutSize );
     RetValue = fread( &Num, 4, 1, pFile );
     assert( Num >= 2 );
     Vec_PtrFillExtra( p->vObjs, Num, NULL );
@@ -770,7 +775,7 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
     }
     else
         If_DsdManComputeTruth_rec( p, iDsd, pRes, pPermLits, &nSupp );
-    assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, Abc_Lit2Var(iDsd)) );
+    assert( nSupp == If_DsdVecLitSuppSize(p->vObjs, iDsd) );
     return pRes;
 }
 
@@ -785,74 +790,6 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
   SeeAlso     []
 
 ***********************************************************************/
-int If_DsdManOperation2( If_DsdMan_t * p, int Type, int * pLits, int nLits )
-{
-    If_DsdObj_t * pObj;
-    int nChildren = 0, pChildren[DAU_MAX_VAR];
-    int i, k, Id, iFanin, fCompl = 0;
-    if ( Type == IF_DSD_AND )
-    {
-        for ( k = 0; k < nLits; k++ )
-        {
-            pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(pLits[k]) );
-            if ( Abc_LitIsCompl(pLits[k]) || If_DsdObjType(pObj) != IF_DSD_AND )
-                pChildren[nChildren++] = pLits[k];
-            else
-                If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-                    pChildren[nChildren++] = iFanin;
-        }
-        If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
-    }
-    else if ( Type == IF_DSD_XOR )
-    {
-        for ( k = 0; k < nLits; k++ )
-        {
-            fCompl ^= Abc_LitIsCompl(pLits[k]);
-            pObj = If_DsdVecObj( p->vObjs, Abc_LitRegular(pLits[k]) );
-            if ( If_DsdObjType(pObj) != IF_DSD_XOR )
-                pChildren[nChildren++] = pLits[k];
-            else
-                If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
-                {
-                    assert( !Abc_LitIsCompl(iFanin) );
-                    pChildren[nChildren++] = iFanin;
-                }
-        }
-        If_DsdObjSort( p->vObjs, pChildren, nChildren, NULL );
-    }
-    else if ( Type == IF_DSD_MUX )
-    {
-        if ( Abc_LitIsCompl(pLits[0]) )
-        {
-            pLits[0] = Abc_LitNot(pLits[0]);
-            ABC_SWAP( int, pLits[1], pLits[2] );
-        }
-        if ( Abc_LitIsCompl(pLits[1]) )
-        {
-            pLits[1] = Abc_LitNot(pLits[1]);
-            pLits[2] = Abc_LitNot(pLits[2]);
-            fCompl ^= 1;
-        }
-        for ( k = 0; k < nLits; k++ )
-            pChildren[nChildren++] = pLits[k];
-    }
-    else assert( 0 );
-    // create new graph
-    Id = If_DsdObjFindOrAdd( p, Type, pChildren, nChildren, NULL );
-    return Abc_Var2Lit( Id, fCompl );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs DSD operation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int If_DsdManComputeFirstArray( If_DsdMan_t * p, int * pLits, int nLits, int * pFirsts )
 {
     int i, nSSize = 0;
@@ -1290,15 +1227,17 @@ Dau_DecPrintSets( vSets, nFans );
     }
     return 0;
 }
-unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
 {
     If_DsdObj_t * pObj, * pTemp; 
     int i, Mask, iFirst;
+/*
     if ( 193 == iDsd )
     {
         int s = 0;
         If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
     }
+*/
     pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
     if ( fVerbose )
     If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
@@ -1366,6 +1305,26 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
 //    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 uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, fVerbose );
+/*
+    if ( uSet == 0 )
+    {
+//        abctime clk = Abc_Clock();
+        int nVars = If_DsdVecLitSuppSize( p->vObjs, iDsd );
+        word * pRes = If_DsdManComputeTruth( p, iDsd, NULL );
+        uSet = If_ManSatCheckXYall( p->pSat, LutSize, pRes, nVars, p->vTemp1 );
+        if ( uSet )
+        {
+//            If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
+//            Dau_DecPrintSet( uSet, nVars, 1 );
+        }
+//        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
+*/
+    return uSet;
+}
 
 /**Function*************************************************************
 

src/map/if/ifMap.c

@@ -223,7 +223,6 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
                 if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
                 {
                     pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
-//                    printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
                     while ( Vec_IntSize(p->vTtDsds) <= truthId )
                     {
                         Vec_IntPush( p->vTtDsds, -1 );

src/sat/bsat/satSolver.h

@@ -414,6 +414,70 @@ static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, i
     assert( Cid );
     return 6;
 }
+static inline int sat_solver_add_mux41( sat_solver * pSat, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3, int iVarZ )
+{
+    lit Lits[4];
+    int Cid;
+    assert( iVarC0 >= 0 && iVarC1 >= 0 && iVarD0 >= 0 && iVarD1 >= 0 && iVarD2 >= 0 && iVarD3 >= 0 && iVarZ >= 0 );
+
+    Lits[0] = toLitCond( iVarD0, 1 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD1, 1 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD2, 1 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD3, 1 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  0 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+
+    Lits[0] = toLitCond( iVarD0, 0 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD1, 0 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 0 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD2, 0 );
+    Lits[1] = toLitCond( iVarC0, 0 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+
+    Lits[0] = toLitCond( iVarD3, 0 );
+    Lits[1] = toLitCond( iVarC0, 1 );
+    Lits[2] = toLitCond( iVarC1, 1 );
+    Lits[3] = toLitCond( iVarZ,  1 );
+    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
+    assert( Cid );
+    return 8;
+}
 static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
 {
     // F = (a (+) b) * c