Version abc80307_2

src/base/abci/abc.c

@@ -10750,7 +10750,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
     pPars->Epsilon     =  (float)0.001;
-    pPars->fPreprocess =  1;
+    pPars->fPreprocess =  1; 
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
     pPars->fExpRed     =  1;
@@ -10898,8 +10898,8 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         // get LUT size from the library
         pPars->nLutSize = pPars->pLutLib->LutMax;
         // if variable pin delay, force truth table computation
-        if ( pPars->pLutLib->fVarPinDelays )
-            pPars->fTruth = 1;
+//        if ( pPars->pLutLib->fVarPinDelays )
+//            pPars->fTruth = 1;
     }
 
     if ( pPars->nLutSize < 3 || pPars->nLutSize > IF_MAX_LUTSIZE )
@@ -10924,11 +10924,15 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( (c = Abc_NtkGetChoiceNum( pNtk )) )
     {
         printf( "Performing LUT mapping with %d choices.\n", c );
-        pPars->fTruth = 1;
+//        pPars->fTruth = 1;
+        pPars->fExpRed = 0;
     }
     // enable truth table computation if cut minimization is selected
     if ( pPars->fCutMin )
+    {
         pPars->fTruth = 1;
+        pPars->fExpRed = 0;
+    }
 
     // complain if truth tables are requested but the cut size is too large
     if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )

src/base/abci/abcDelay.c

@@ -96,7 +96,7 @@ void Abc_NtkDelayTraceSortPins( Abc_Obj_t * pNode, int * pPinPerm, float * pPinD
 ***********************************************************************/
 float Abc_NtkDelayTraceLut( Abc_Ntk_t * pNtk, int fUseLutLib )
 {
-    int fUseSorting = 0;
+    int fUseSorting = 1;
     int pPinPerm[32];
     float pPinDelays[32];
     If_Lib_t * pLutLib;

src/base/abci/abcIf.c

@@ -252,8 +252,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     // create a new node 
     pNodeNew = Abc_NtkCreateNode( pNtkNew );
     pCutBest = If_ObjCutBest( pIfObj );
-    if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
-        If_CutRotatePins( pIfMan, pCutBest );
+//    if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
+//        If_CutRotatePins( pIfMan, pCutBest );
     if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
     {
         If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
@@ -346,6 +346,54 @@ Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_
     return gFunc;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively derives the truth table for the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+{
+    If_Cut_t * pCut;
+    If_Obj_t * pTemp;
+    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
+    // get the best cut
+    pCut = If_ObjCutBest(pIfObj);
+    // if the cut is visited, return the result
+    if ( If_CutData(pCut) )
+        return If_CutData(pCut);
+    // mark the node as visited
+    Vec_PtrPush( vVisited, pCut );
+    // insert the worst case
+    If_CutSetData( pCut, (void *)1 );
+    // skip in case of primary input
+    if ( If_ObjIsCi(pIfObj) )
+        return If_CutData(pCut);
+    // compute the functions of the children
+    for ( pTemp = pIfObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        gFunc0 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin0, vVisited );
+        if ( gFunc0 == (void *)1 )
+            continue;
+        gFunc1 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pTemp->pFanin1, vVisited );
+        if ( gFunc1 == (void *)1 )
+            continue;
+        // both branches are solved
+        gFunc = Hop_And( pHopMan, Hop_NotCond(gFunc0, pTemp->fCompl0), Hop_NotCond(gFunc1, pTemp->fCompl1) ); 
+        if ( pTemp->fPhase != pIfObj->fPhase )
+            gFunc = Hop_Not(gFunc);
+        If_CutSetData( pCut, gFunc );
+        break;
+    }
+    return If_CutData(pCut);
+}
+
 /**Function*************************************************************
 
   Synopsis    [Derives the truth table for one cut.]
@@ -371,7 +419,12 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
         If_CutSetData( If_ObjCutBest(pLeaf), Hop_IthVar(pHopMan, i) );
     // recursively compute the function while collecting visited cuts
     Vec_PtrClear( pIfMan->vTemp );
-    gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+    gFunc = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+    if ( gFunc == (void *)1 )
+    {
+        printf( "Abc_NodeIfToHop(): Computing local AIG has failed.\n" );
+        return NULL;
+    }
 //    printf( "%d ", Vec_PtrSize(p->vTemp) );
     // clean the cuts
     If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )

src/map/if/if.h

@@ -166,6 +166,8 @@ struct If_Man_t_
     int                nSmallSupp;    // the small support
     // timing manager
     Tim_Man_t *        pManTim;
+    // statistics 
+//    int                timeTruth;
 };
 
 // priority cut

src/map/if/ifCore.c

@@ -110,14 +110,14 @@ int If_ManPerformMappingComb( If_Man_t * p )
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, "Delay" );
 
     // try to improve area by expanding and reducing the cuts
-    if ( p->pPars->fExpRed && !p->pPars->fTruth )
+    if ( p->pPars->fExpRed )
         If_ManImproveMapping( p );
 
     // area flow oriented mapping
     for ( i = 0; i < p->pPars->nFlowIters; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 0, "Flow" );
-        if ( p->pPars->fExpRed && !p->pPars->fTruth )
+        if ( p->pPars->fExpRed )
             If_ManImproveMapping( p );
     }
 
@@ -125,7 +125,7 @@ int If_ManPerformMappingComb( If_Man_t * p )
     for ( i = 0; i < p->pPars->nAreaIters; i++ )
     {
         If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 0, "Area" );
-        if ( p->pPars->fExpRed && !p->pPars->fTruth )
+        if ( p->pPars->fExpRed )
             If_ManImproveMapping( p );
     }
 
@@ -139,6 +139,13 @@ int If_ManPerformMappingComb( If_Man_t * p )
 //    printf( "Cross cut memory = %d.\n", Mem_FixedReadMaxEntriesUsed(p->pMemSet) );
     s_MappingTime = clock() - clkTotal;
 //    printf( "Special POs = %d.\n", If_ManCountSpecialPos(p) );
+    {
+    extern int If_CutGetCones( If_Man_t * p );
+    extern int If_CutCountTotalFanins( If_Man_t * p );
+//    If_CutGetCones( p );
+//    If_CutCountTotalFanins( p );
+    }
+
     return 1;
 }
 

src/map/if/ifCut.c

@@ -980,6 +980,149 @@ float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut )
     return aResult;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the cone of the cut in AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutGetCutMinLevel( If_Man_t * p, If_Cut_t * pCut )
+{
+    If_Obj_t * pLeaf;
+    int i, nMinLevel = IF_INFINITY;
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
+        nMinLevel = IF_MIN( nMinLevel, (int)pLeaf->Level );
+    return nMinLevel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cone of the cut in AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutGetCone_rec( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut )
+{
+    If_Obj_t * pTemp;
+    int i, RetValue;
+    // check if the node is in the cut
+    for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        if ( pCut->pLeaves[i] == pObj->Id )
+            return 1;
+        else if ( pCut->pLeaves[i] > pObj->Id )
+            break;
+    // return if we reached the boundary
+    if ( If_ObjIsCi(pObj) )
+        return 0;
+    // check the choice node
+    for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
+    {
+        // check if the node itself is bound
+        RetValue = If_CutGetCone_rec( p, If_ObjFanin0(pTemp), pCut );
+        if ( RetValue )
+            RetValue &= If_CutGetCone_rec( p, If_ObjFanin1(pTemp), pCut );
+        if ( RetValue )
+            return 1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cone of the cut in AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutGetCones( If_Man_t * p )
+{
+    If_Obj_t * pObj;
+    int i, Counter = 0;
+    int clk = clock();
+    If_ManForEachObj( p, pObj, i )
+    {
+        if ( If_ObjIsAnd(pObj) && pObj->nRefs )
+        {
+            Counter += !If_CutGetCone_rec( p, pObj, If_ObjCutBest(pObj) );
+//            printf( "%d ", If_CutGetCutMinLevel( p, If_ObjCutBest(pObj) ) );
+        }
+    }
+    printf( "Cound not find boundary for %d nodes.\n", Counter );
+    PRT( "Cones", clock() - clk );
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cone of the cut in AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void If_CutFoundFanins_rec( If_Obj_t * pObj, Vec_Int_t * vLeaves )
+{
+    if ( pObj->nRefs || If_ObjIsCi(pObj) )
+    {
+        Vec_IntPushUnique( vLeaves, pObj->Id );
+        return;
+    }
+    If_CutFoundFanins_rec( If_ObjFanin0(pObj), vLeaves );
+    If_CutFoundFanins_rec( If_ObjFanin1(pObj), vLeaves );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cone of the cut in AIG with choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int If_CutCountTotalFanins( If_Man_t * p )
+{
+    If_Obj_t * pObj;
+    Vec_Int_t * vLeaves;
+    int i, nFaninsTotal = 0, Counter = 0;
+    int clk = clock();
+    vLeaves = Vec_IntAlloc( 100 );
+    If_ManForEachObj( p, pObj, i )
+    {
+        if ( If_ObjIsAnd(pObj) && pObj->nRefs )
+        {
+            nFaninsTotal += If_ObjCutBest(pObj)->nLeaves;
+            Vec_IntClear( vLeaves );
+            If_CutFoundFanins_rec( If_ObjFanin0(pObj), vLeaves );
+            If_CutFoundFanins_rec( If_ObjFanin1(pObj), vLeaves );
+            Counter += Vec_IntSize(vLeaves);
+        }
+    }
+    printf( "Total cut inputs = %d. Total fanins incremental = %d.\n", nFaninsTotal, Counter );
+    PRT( "Fanins", clock() - clk );
+    Vec_IntFree( vLeaves );
+    return 1;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/map/if/ifMan.c

@@ -124,6 +124,7 @@ void If_ManRestart( If_Man_t * p )
 ***********************************************************************/
 void If_ManStop( If_Man_t * p )
 {
+//    PRT( "Truth", p->timeTruth );
 //    printf( "Small support = %d.\n", p->nSmallSupp );
     Vec_PtrFree( p->vCis );
     Vec_PtrFree( p->vCos );

src/map/if/ifMap.c

@@ -119,7 +119,11 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         // compute the truth table
         pCut->fCompl = 0;
         if ( p->pPars->fTruth )
+        {
+//            int clk = clock();
             If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+//            p->timeTruth += clock() - clk;
+        }
         // compute the application-specific cost and depth
         pCut->fUser = (p->pPars->pFuncCost != NULL);
         pCut->Cost = p->pPars->pFuncCost? p->pPars->pFuncCost(pCut) : 0;

src/opt/mfs/mfsCore.c

@@ -68,7 +68,7 @@ clk = clock();
 p->timeCnf += clock() - clk;
     // create the SAT problem
 clk = clock();
-    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 );
+    p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
     if ( p->pSat == NULL )
     {
         p->nNodesBad++;

src/opt/mfs/mfsInt.h

@@ -85,6 +85,7 @@ struct Mfs_Man_t_
     int                 nNodesBad;
     int                 nTotalDivs;
     int                 nTimeOuts;
+    int                 nDcMints;
     // node/edge stats
     int                 nTotalNodesBeg;
     int                 nTotalNodesEnd;
@@ -115,8 +116,9 @@ struct Mfs_Man_t_
 /*=== mfsDiv.c ==========================================================*/
 extern Vec_Ptr_t *      Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
 /*=== mfsInter.c ==========================================================*/
-extern sat_solver *     Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands );
+extern sat_solver *     Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert );
 extern Hop_Obj_t *      Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
+extern int              Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands );
 /*=== mfsMan.c ==========================================================*/
 extern Mfs_Man_t *      Mfs_ManAlloc( Mfs_Par_t * pPars );
 extern void             Mfs_ManStop( Mfs_Man_t * p );

src/opt/mfs/mfsInter.c

@@ -82,7 +82,7 @@ int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
   SeeAlso     []
 
 ***********************************************************************/
-sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
+sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert )
 {
     sat_solver * pSat;
     Aig_Obj_t * pObjPo;
@@ -90,7 +90,7 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
 
     // get the literal for the output of F
     pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
-    Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 );
+    Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], fInvert );
 
     // collect the outputs of the divisors
     Vec_IntClear( p->vProjVars );
@@ -210,6 +210,100 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
   SeeAlso     []
 
 ***********************************************************************/
+unsigned * Abc_NtkMfsInterplateTruth( Mfs_Man_t * p, int * pCands, int nCands, int fInvert )
+{
+    sat_solver * pSat;
+    Sto_Man_t * pCnf = NULL;
+    unsigned * puTruth;
+    int nFanins, status;
+    int c, i, * pGloVars;
+
+    // derive the SAT solver for interpolation
+    pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, fInvert );
+
+    // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+    if ( status != l_False )
+    {
+        p->nTimeOuts++;
+        return NULL;
+    }
+    // get the learned clauses
+    pCnf = sat_solver_store_release( pSat );
+    sat_solver_delete( pSat );
+
+    // set the global variables
+    pGloVars = Int_ManSetGlobalVars( p->pMan, nCands );
+    for ( c = 0; c < nCands; c++ )
+    {
+        // get the variable number of this divisor
+        i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+        // get the corresponding SAT variable
+        pGloVars[c] = Vec_IntEntry( p->vProjVars, i );
+    }
+
+    // derive the interpolant
+    nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
+    Sto_ManFree( pCnf );
+    assert( nFanins == nCands );
+    return puTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs interpolation.]
+
+  Description [Derives the new function of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands )
+{
+    unsigned * pTruth, uTruth0[2], uTruth1[2];
+    int nCounter;
+    pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 0 );
+    if ( nCands == 6 )
+    {
+        uTruth1[0] = pTruth[0];
+        uTruth1[1] = pTruth[1];
+    }
+    else
+    {
+        uTruth1[0] = pTruth[0];
+        uTruth1[1] = pTruth[0];
+    }
+    pTruth = Abc_NtkMfsInterplateTruth( p, pCands, nCands, 1 );
+    if ( nCands == 6 )
+    {
+        uTruth0[0] = ~pTruth[0];
+        uTruth0[1] = ~pTruth[1];
+    }
+    else
+    {
+        uTruth0[0] = ~pTruth[0];
+        uTruth0[1] = ~pTruth[0];
+    }
+    nCounter  = Extra_WordCountOnes( uTruth0[0] ^ uTruth1[0] );
+    nCounter += Extra_WordCountOnes( uTruth0[1] ^ uTruth1[1] );
+//    printf( "%d ", nCounter );
+    return nCounter;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs interpolation.]
+
+  Description [Derives the new function of the node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
 {
     extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
@@ -222,8 +316,10 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
     int nFanins, status;
     int c, i, * pGloVars;
 
+//    p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
+
     // derive the SAT solver for interpolation
-    pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
+    pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 );
 
     // solve the problem
     status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->pPars->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );

src/opt/mfs/mfsMan.c

@@ -122,6 +122,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
                 p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );
         else
             Abc_NtkMfsPrintResubStats( p );
+//        printf( "Average ratio of DCs in the resubed nodes = %.2f.\n", 1.0*p->nDcMints/(64 * p->nNodesResub) );
     }
     else
     {

src/sat/bsat/module.make

 SRC +=  src/sat/bsat/satMem.c \
     src/sat/bsat/satInter.c \
     src/sat/bsat/satInterA.c \
+    src/sat/bsat/satInterP.c \
     src/sat/bsat/satSolver.c \
     src/sat/bsat/satStore.c \
     src/sat/bsat/satTrace.c \