Changes to the lazy man's synthesis code.

src/aig/kit/kitTruth.c

@@ -1666,6 +1666,7 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
     uCanonPhase = 0;
 
     nOnes = Kit_TruthCountOnes(pIn, nVars);
+    //if(pIn[0] & 1)
     if ( (nOnes > nWords * 16) )//|| ((nOnes == nWords * 16) && (pIn[0] & 1)) )
     {
         uCanonPhase |= (1 << nVars);

src/base/abc/abc.h

@@ -777,6 +777,7 @@ extern ABC_DLL void               Abc_NtkRecStop();
 extern ABC_DLL void               Abc_NtkRecAdd( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkRecPs();
 extern ABC_DLL void               Abc_NtkRecFilter(int nLimit);
+extern ABC_DLL void               Abc_NtkRecLibMerge(Abc_Ntk_t * pNtk);
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkRecUse();
 extern ABC_DLL int                Abc_NtkRecIsRunning();
 extern ABC_DLL int                Abc_NtkRecIsInTrimMode();

src/base/abci/abc.c

@@ -212,6 +212,7 @@ static int Abc_CommandRecAdd                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandRecPs                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecUse                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecFilter              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRecMerge               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandMap                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAmap                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -671,6 +672,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_ps",        Abc_CommandRecPs,            0 );
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_use",       Abc_CommandRecUse,           1 );
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_filter",    Abc_CommandRecFilter,        1 );
+    Cmd_CommandAdd( pAbc, "Choicing",     "rec_merge",     Abc_CommandRecMerge,         1 );
 
     Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "amap",          Abc_CommandAmap,             1 );
@@ -11947,7 +11949,7 @@ int Abc_CommandRecStart( Abc_Frame_t * pAbc, int argc, char ** argv )
     pNtk = Abc_FrameReadNtk(pAbc);
     // set defaults
     nVars = 6;
-    nCuts = 8;
+    nCuts = 32;
     fTrim = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "KCth" ) ) != EOF )
@@ -12254,6 +12256,50 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandRecMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( !Abc_NtkRecIsRunning() )
+    {
+        Abc_Print( -1, "This command works for AIGs only after calling \"rec_start\".\n" );
+        return 0;
+    }
+    Abc_NtkRecLibMerge(pNtk);
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: rec_merge [-h]\n" );
+    Abc_Print( -2, "\t        merge libraries\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 

src/base/abci/abcRec.c

@@ -24,7 +24,7 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
+//#define LibOut
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -48,6 +48,7 @@ struct Rec_Obj_t_
     Rec_Obj_t* pNext;           // link to the next structure of the same functional class
     Rec_Obj_t* pCopy;           // link to the next functional class in the same bucket
     int Id;                     // structure's ID
+    unsigned nFrequency;        // appear times of this functional class among benchmarks
     unsigned char cost;         // structure's cost
     char* pinToPinDelay;        // structure's pin-to-pin delay
 };
@@ -110,6 +111,7 @@ struct Abc_ManRec_t_
     int               timeCanon;                // the runtime to canonicize
     int               timeInsert;               // the runtime to insert a structure.
     int               timeBuild;                // the runtime to build a new structure in the library.
+    int               timeMerge;                // the runtime to merge libraries;
     int               timeOther;                // the runtime of other
     int               timeTotal;                // the runtime to total.
 };
@@ -120,6 +122,7 @@ struct Abc_ManRec_t_
 static Rec_Obj_t ** Abc_NtkRecTableLookup( Abc_ManRec_t * p, unsigned * pTruth, int nVars );
 static int          Abc_NtkRecComputeTruth( Abc_Obj_t * pObj, Vec_Ptr_t * vTtNodes, int nVars );
 static int          Abc_NtkRecAddCutCheckCycle_rec( Abc_Obj_t * pRoot, Abc_Obj_t * pObj );
+static void         Abc_NtkRecAddFromLib( Abc_Ntk_t* pNtk, Abc_Obj_t * pRoot, int nVars );
 
 static Abc_ManRec_t * s_pMan = NULL;
 
@@ -127,6 +130,13 @@ static inline void Abc_ObjSetMax( Abc_Obj_t * pObj, int Value ) { assert( pObj->
 static inline void Abc_ObjClearMax( Abc_Obj_t * pObj )          { pObj->Level = (pObj->Level & 0xff); }
 static inline int  Abc_ObjGetMax( Abc_Obj_t * pObj )            { return (pObj->Level >> 8) & 0xff; }
 
+static inline void Abc_NtkRecFrequencyInc(Rec_Obj_t* entry)     
+{   
+    // the hit number of this functional class increased
+    if (entry != NULL && entry->nFrequency < 0xffffffff)
+        entry->nFrequency += 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -180,6 +190,7 @@ Rec_Obj_t* Rec_ObjAlloc(Abc_ManRec_t* p, Abc_Obj_t* pObj, char* pinToPinDelay, c
     for (i = 0; i < nVar; i++)
         pRecObj->pinToPinDelay[i] = pinToPinDelay[i];
     pRecObj->cost = cost;   
+    pRecObj->nFrequency = 0;
     return pRecObj;
 }
 
@@ -493,9 +504,10 @@ void Abc_NtkRecInsertToLookUpTable(Abc_ManRec_t* p, Rec_Obj_t** ppSpot, Abc_Obj_
         pLeaf =Abc_ObjRegular(pLeaf);
         delayFromStruct[i] = If_CutDepthRecComput_rec(pObj, pLeaf->Id);
     }
+    if(fTrim)
+    {       
         while(1)
         {
-        
             if (current == NULL)
             {
                 p->nAdded++;
@@ -509,6 +521,7 @@ void Abc_NtkRecInsertToLookUpTable(Abc_ManRec_t* p, Rec_Obj_t** ppSpot, Abc_Obj_
                     // new functional class found
                     p->nAddedFuncs++;
                     *ppSpot = entry;
+                    entry->nFrequency = 1;
                 }
                 break;
             }
@@ -518,21 +531,16 @@ void Abc_NtkRecInsertToLookUpTable(Abc_ManRec_t* p, Rec_Obj_t** ppSpot, Abc_Obj_
                 // when delay profile is equal, replace only if it has smaller cost.
                 if(costFromStruct < current->cost)
                 {   
-                if(fTrim)
                     Abc_NtkRecDeleteSubGragh(p, current->obj);
                     Rec_ObjSet(p, current, pObj, delayFromStruct, costFromStruct, nVars);
                 }
                 else
-            {
-                if(fTrim)
                     Abc_NtkRecDeleteSubGragh(p, pObj);
-            }
                 break;
             }
             // when the new structure can dominate others, sweep them out of the library, delete them if required.
             else if(result == REC_DOMINANCE)
             {
-            if(fTrim)
                 Abc_NtkRecDeleteSubGragh(p, current->obj);
                 Rec_ObjSet(p, current, pObj, delayFromStruct, costFromStruct, nVars);
                 Abc_NtkRecSweepDominance(p,current,current->pNext,delayFromStruct, nVars, fTrim);       
@@ -541,7 +549,6 @@ void Abc_NtkRecInsertToLookUpTable(Abc_ManRec_t* p, Rec_Obj_t** ppSpot, Abc_Obj_
             // when the new structure is domianted by an existed one, don't store it.
             else if (result == REC_BEDOMINANCED)
             {
-            if(fTrim)
                 Abc_NtkRecDeleteSubGragh(p, pObj);
                 break;
             }
@@ -565,7 +572,9 @@ void Abc_NtkRecInsertToLookUpTable(Abc_ManRec_t* p, Rec_Obj_t** ppSpot, Abc_Obj_
                 {
                     entry->pNext = current;
                     entry->pCopy = (*ppSpot)->pCopy;
+                    entry->nFrequency = (*ppSpot)->nFrequency;
                     (*ppSpot)->pCopy = NULL;
+                    (*ppSpot)->nFrequency = 0;
                     *ppSpot = entry;
                 }
                 Abc_NtkRecSweepDominance(p,current,current->pNext,delayFromStruct, nVars, fTrim);           
@@ -575,6 +584,25 @@ void Abc_NtkRecInsertToLookUpTable(Abc_ManRec_t* p, Rec_Obj_t** ppSpot, Abc_Obj_
                 assert(0);      
         }
     }
+    else
+    {
+        if (current == NULL)
+        {
+            p->nAdded++;
+            entry = Rec_ObjAlloc(p, pObj, delayFromStruct, costFromStruct, nVars);          
+            p->nAddedFuncs++;
+            *ppSpot = entry;
+            entry->nFrequency = 1;
+        }
+        else
+        {
+            p->nAdded++;
+            entry = Rec_ObjAlloc(p, pObj, delayFromStruct, costFromStruct, nVars);  
+            entry->pNext = (*ppSpot)->pNext;
+            (*ppSpot)->pNext = entry;
+        }
+    }
+}
 
 /**Function*************************************************************
 
@@ -628,6 +656,7 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut )
     unsigned *pInOut = s_pMan->pTemp1;
     unsigned *pTemp = s_pMan->pTemp2;
     int time = clock();
+    int fCompl = 0;
 #ifdef Dervie
     static FILE* pFile;
 #endif
@@ -640,6 +669,12 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut )
     uCanonPhase = Kit_TruthSemiCanonicize(pInOut, pTemp, nLeaves, pCanonPerm, (short*)s_pMan->pMints);
     If_CutTruthStretch(pInOut, nLeaves, nVars);
     ppSpot = Abc_NtkRecTableLookup( s_pMan, pInOut, nVars );
+    if (*ppSpot == NULL)
+    {
+        Kit_TruthNot(pInOut, pInOut, nVars);
+        ppSpot = Abc_NtkRecTableLookup( s_pMan, pInOut, nVars );
+        fCompl = 1;
+    }
     assert(*ppSpot != NULL);
     DelayMin = ABC_INFINITY;
     pCandMin = NULL;
@@ -662,6 +697,11 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut )
     assert( pCandMin != NULL );
     if ( s_pMan->vLabels == NULL )
         s_pMan->vLabels = Vec_PtrStart( Abc_NtkObjNumMax(pAig));
+    else
+    {
+        Vec_PtrGrow(s_pMan->vLabels, Abc_NtkObjNumMax(pAig));
+        s_pMan->vLabels->nSize = s_pMan->vLabels->nCap;
+    }
     for (i = 0; i < nLeaves; i++)
     {
         pAbcObj = Abc_NtkPi( pAig, i );
@@ -674,7 +714,7 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut )
     pHopObj = Abc_NtkRecBuildUp_rec(pMan, pCandMin->obj, s_pMan->vLabels);
     s_pMan->timeIfDerive += clock() - time;
     s_pMan->timeIfTotal += clock() - time;
-    return Hop_NotCond(pHopObj, (pCut->fCompl)^(((uCanonPhase & (1 << nLeaves)) > 0)));    
+    return Hop_NotCond(pHopObj, (pCut->fCompl)^(((uCanonPhase & (1 << nLeaves)) > 0)) ^ fCompl);    
 }
 
 /**Function*************************************************************
@@ -781,36 +821,20 @@ void Abc_RecUpdateHashTable()
 ***********************************************************************/
 void Abc_NtkRecFilter(int nLimit)
 {
-    Abc_Obj_t * pObj;
-//    void * temp;
     Rec_Obj_t * previous = NULL, * entry = NULL, * pTemp;
-    int i, counter = 0;
+    int i;
-//    int j;
     Abc_Ntk_t * pNtk = s_pMan->pNtk;
     int time = clock();
     if (nLimit > 0)
     {
-        Abc_NtkForEachPi( pNtk, pObj, i )
-            Abc_ObjSetMax( pObj, i+1 );
-        Abc_AigForEachAnd( pNtk, pObj, i )
-            Abc_ObjSetMax( pObj, ABC_MAX( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
         for ( i = 0; i < s_pMan->nBins; i++ )
         {
             previous = NULL;
             for ( entry = s_pMan->pBins[i]; entry; entry = entry->pCopy)
             {
-                //make sure the structures with 2 variables stay in the library.
+                assert(entry->nFrequency != 0);
-                if(Abc_ObjGetMax(entry->obj) == 2)
+                // only filter the functional classed with frequency less than nLimit.
-                    continue;
+                if((int)entry->nFrequency > nLimit)
-                counter = 0;
-                for ( pTemp = entry; pTemp; pTemp = pTemp->pNext)
-                {
-                    counter++;
-                    if(counter > nLimit)
-                        break;
-                }
-                // only filter the functional classed with subgragh less than nLimit.
-                if(counter > nLimit)
                 {
                     previous = entry;
                     continue;
@@ -833,11 +857,6 @@ void Abc_NtkRecFilter(int nLimit)
                 }
             }
         }
-        // clean level info.
-        Abc_NtkForEachObj( pNtk, pObj, i )
-        {
-            Abc_ObjClearMax( pObj );
-        }
     }
 
     // remove dangling nodes and POs driven by constants
@@ -916,6 +935,54 @@ Vec_Int_t * Abc_NtkRecMemory()
     return s_pMan->vMemory;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Starts the record for the given network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecLibMerge(Abc_Ntk_t* pNtk)
+{
+    int i;
+    Abc_Obj_t * pObj;
+    Abc_ManRec_t * p = s_pMan;
+    int clk = clock();
+    if ( Abc_NtkPiNum(pNtk) > s_pMan->nVars )
+    {
+        printf( "The library has more inputs than the record.\n");
+        return;
+    }
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_ObjSetMax( pObj, i+1 );
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        Abc_ObjSetMax( pObj, ABC_MAX( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
+
+    // insert the PO nodes into the table
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        p->nTried++;
+        //if the PO's input is a constant, skip it.
+        if (Abc_ObjChild0(pObj) == Abc_ObjNot( Abc_AigConst1(pNtk)))
+        {
+            p->nTrimed++;
+            continue;
+        }   
+        pObj = Abc_ObjFanin0(pObj); 
+        Abc_NtkRecAddFromLib(pNtk, pObj, Abc_ObjGetMax(pObj) );     
+    }
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        Abc_ObjClearMax( pObj );
+    }
+    s_pMan->timeMerge += clock() - clk;
+    s_pMan->timeTotal += clock() - clk;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Starts the record for the given network.]
@@ -1055,7 +1122,7 @@ p->timeTruth += clock() - clk;
     p->pTemp1 = ABC_ALLOC( unsigned, p->nWords );
     p->pTemp2 = ABC_ALLOC( unsigned, p->nWords );
     p->vNodes = Vec_PtrAlloc( 100 );
-    p->vTtTemps = Vec_PtrAllocSimInfo( 64, p->nWords );
+    p->vTtTemps = Vec_PtrAllocSimInfo( 1024, p->nWords );
     p->vMemory = Vec_IntAlloc( Abc_TruthWordNum(p->nVars) * 1000 );
 
     // set the manager
@@ -1184,11 +1251,46 @@ void Abc_NtkRecPs()
     Rec_Obj_t * pEntry, * pTemp;
     Abc_Obj_t * pObj;
     int i;
+#ifdef LibOut
+    FILE * pFile;
+    unsigned* pTruth;
+    Rec_Obj_t* entry;
+    int j;
+    int nVars = 6;
+#endif
     // set the max PI number
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_ObjSetMax( pObj, i+1 );
     Abc_AigForEachAnd( pNtk, pObj, i )
         Abc_ObjSetMax( pObj, ABC_MAX( Abc_ObjGetMax(Abc_ObjFanin0(pObj)), Abc_ObjGetMax(Abc_ObjFanin1(pObj)) ) );
+#ifdef LibOut
+pFile = fopen( "tt10.txt", "wb" );
+for ( i = 0; i < p->nBins; i++ )
+    for ( entry = p->pBins[i]; entry; entry = entry->pCopy )
+    {
+        int tmp = 0;
+        pTruth = Vec_PtrEntry(p->vTtNodes, entry->Id);
+        /*if ( (int)Kit_TruthSupport(pTruth, nVars) != (1<<nVars)-1 )
+            continue;*/
+        Extra_PrintHex( pFile, pTruth, nVars );
+        fprintf( pFile, " : nVars:  %d, Frequency:%d  :  ", Abc_ObjGetMax(entry->obj), entry->nFrequency);
+        Kit_DsdPrintFromTruth2( pFile, pTruth, Abc_ObjGetMax(entry->obj) );
+        fprintf( pFile, "\n" );
+        for ( pTemp = entry; pTemp; pTemp = pTemp->pNext )
+        {
+            fprintf(pFile,"%d :", tmp);
+            for (j = 0; j <Abc_ObjGetMax(pTemp->obj); j++)
+            {
+                fprintf(pFile, " %d, ", pTemp->pinToPinDelay[j]);
+            }
+            fprintf(pFile, "cost = %d\n", pTemp->cost);             
+            tmp++;
+        }
+        fprintf( pFile, "\n");
+        fprintf( pFile, "\n");
+    }
+    fclose( pFile) ;
+#endif
     // go through the table
     Counter = CounterS = 0;
     for ( i = 0; i < p->nBins; i++ )
@@ -1232,11 +1334,12 @@ void Abc_NtkRecPs()
     printf( "Functions added                             = %10d. (%6.2f %%)\n", p->nAddedFuncs,   !p->nTried? 0 : 100.0*p->nAddedFuncs/p->nTried );
     if(s_pMan->fTrim)
         printf( "Functions trimed                            = %10d. (%6.2f %%)\n", p->nTrimed,       !p->nTried? 0 : 100.0*p->nTrimed/p->nTried );
-    p->timeOther = p->timeTotal - p->timeCollect - p->timeTruth - p->timeCanon - p->timeInsert - p->timeBuild - p->timeTrim;
+    p->timeOther = p->timeTotal - p->timeCollect - p->timeTruth - p->timeCanon - p->timeInsert - p->timeBuild - p->timeTrim - p->timeMerge;
     ABC_PRTP( "Collecting nodes ", p->timeCollect, p->timeTotal);
     ABC_PRTP( "Computing truth  ", p->timeTruth, p->timeTotal );
     ABC_PRTP( "Canonicizing     ", p->timeCanon, p->timeTotal );
     ABC_PRTP( "Building         ", p->timeBuild, p->timeTotal );
+    ABC_PRTP( "Merge            ", p->timeMerge, p->timeTotal );
     ABC_PRTP( "Insert           ", p->timeInsert, p->timeTotal);
     if(s_pMan->fTrim)
         ABC_PRTP( "Filter           ", p->timeTrim, p->timeTotal);
@@ -1380,6 +1483,7 @@ void Abc_NtkRecAdd( Abc_Ntk_t * pNtk )
     pPars->fUseSops    =  0;
     pPars->fUseCnfs    =  0;
     pPars->fUseMv      =  0;
+    pPars->fSkipCutFilter = 1;
     pPars->pFuncCost   =  NULL;
     pPars->pFuncUser   =  Abc_NtkRecAddCut;
 
@@ -1414,6 +1518,26 @@ void Abc_NtkRecCollectNodes_rec( If_Obj_t * pNode, Vec_Ptr_t * vNodes )
     Vec_PtrPush( vNodes, pNode );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecCollectNodesFromLib_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    if ( Abc_ObjIsPi(pNode))
+        return;
+    Abc_NtkRecCollectNodesFromLib_rec( Abc_ObjFanin0(pNode), vNodes );
+    Abc_NtkRecCollectNodesFromLib_rec( Abc_ObjFanin1(pNode), vNodes );
+    Vec_PtrPush( vNodes, pNode );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Adds the cut function to the internal storage.]
@@ -1477,6 +1601,30 @@ int Abc_NtkRecCollectNodes( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecCollectNodesFromLib(Abc_Ntk_t* pNtk, Abc_Obj_t * pRoot, Vec_Ptr_t * vNodes , int nVars)
+{
+    int i;
+    // collect the internal nodes of the cut
+    Vec_PtrClear( vNodes );
+    for ( i = 0; i < nVars; i++ )
+        Vec_PtrPush( vNodes, Abc_NtkPi(pNtk, i));
+
+
+    // collect other nodes
+    Abc_NtkRecCollectNodesFromLib_rec( pRoot, vNodes );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Computes truth tables of nodes in the cut.]
@@ -1574,6 +1722,50 @@ int Abc_NtkRecCutTruth( Vec_Ptr_t * vNodes, int nLeaves, Vec_Ptr_t * vTtTemps, V
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes truth tables of nodes in the cut.]
+
+  Description [Returns 0 if the TT does not depend on some cut variables.
+  Or if the TT can be expressed simpler using other nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecCutTruthFromLib( Vec_Ptr_t * vNodes, int nLeaves, Vec_Ptr_t * vTtTemps, Vec_Ptr_t * vTtElems )
+{
+    unsigned * pSims, * pSims0, * pSims1;
+    unsigned * pTemp = s_pMan->pTemp2;
+    Abc_Obj_t * pObj, * pRoot;
+    int i, nInputs = s_pMan->nVars;
+
+    assert( Vec_PtrSize(vNodes) > nLeaves );
+
+    // set the elementary truth tables and compute the truth tables of the nodes
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        pObj->pTemp = Vec_PtrEntry(vTtTemps, i);
+        pSims = (unsigned *)pObj->pTemp;
+        if ( i < nLeaves )
+        {
+            Kit_TruthCopy( pSims, (unsigned *)Vec_PtrEntry(vTtElems, i), nInputs );
+            continue;
+        }
+        // get hold of the simulation information
+        pSims0 = (unsigned *)Abc_ObjFanin0(pObj)->pTemp;
+        pSims1 = (unsigned *)Abc_ObjFanin1(pObj)->pTemp;
+        // simulate the node
+        Kit_TruthAndPhase( pSims, pSims0, pSims1, nInputs, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    }
+
+    // check the support size
+    pRoot = (Abc_Obj_t *)Vec_PtrEntryLast( vNodes );
+    pSims = (unsigned *)pRoot->pTemp;
+    assert ( Kit_TruthSupport(pSims, nInputs) == Kit_BitMask(nLeaves) );
+}
+
 /**Function*************************************************************
 
   Synopsis    [Adds the cut function to the internal storage.]
@@ -1626,6 +1818,7 @@ int Abc_NtkRecAddCut( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
     int i, RetValue, nNodes, nNodesBeg, nInputs = s_pMan->nVars, nLeaves = If_CutLeaveNum(pCut);
     unsigned uCanonPhase;
     int clk, timeInsert, timeBuild;
+    int begin = clock();
     assert( nInputs <= 16 );
     assert( nInputs == (int)pCut->nLimit );
     s_pMan->nTried++;
@@ -1725,7 +1918,7 @@ clk = clock();
         }
     }
     assert(pObj);
-    s_pMan->timeBuild = clock() - timeBuild;
+    s_pMan->timeBuild += clock() - timeBuild;
     pTruth = (unsigned *)Vec_PtrEntry( s_pMan->vTtNodes, pObj->Id );
     if ( Kit_TruthSupport(pTruth, nInputs) != Kit_BitMask(nLeaves) )
     {
@@ -1743,13 +1936,17 @@ clk = clock();
     }
 //    Extra_PrintBinary( stdout, pInOut, 8 ); printf( "\n" );
 
+    // look up in the hash table and increase the hit number of the functional class
+    ppSpot = Abc_NtkRecTableLookup( s_pMan, pTruth, nInputs );
+    Abc_NtkRecFrequencyInc(*ppSpot);
+
     // if not new nodes were added and the node has a CO fanout
     if ( nNodesBeg == Abc_NtkObjNumMax(pAig) && Abc_NodeFindCoFanout(pObj) != NULL )
     {
         s_pMan->nFilterSame++;
+        assert(*ppSpot != NULL);
         return 1;
     }
-    //s_pMan->nAdded++;
 
     // create PO for this node
     pObjPo = Abc_NtkCreatePo(pAig);
@@ -1770,12 +1967,127 @@ clk = clock();
 
     // add the resulting truth table to the hash table 
     timeInsert = clock();
-    ppSpot = Abc_NtkRecTableLookup( s_pMan, pTruth, nInputs );
     Abc_NtkRecInsertToLookUpTable(s_pMan, ppSpot, pObj, nLeaves, s_pMan->fTrim);
     s_pMan->timeInsert += clock() - timeInsert;
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut function to the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRecAddFromLib( Abc_Ntk_t* pNtk, Abc_Obj_t * pRoot, int nVars )
+{
+    char Buffer[40], Name[20], Truth[20];
+    Abc_Obj_t * pObj = NULL, * pFanin0, * pFanin1, * pObjPo;
+    Rec_Obj_t ** ppSpot;
+    Abc_Ntk_t * pAig = s_pMan->pNtk;
+    Abc_Obj_t * pAbcObj;
+    Vec_Ptr_t * vNodes = s_pMan->vNodes;
+    unsigned * pInOut = s_pMan->pTemp1;
+    unsigned * pTemp = s_pMan->pTemp2;
+    unsigned * pTruth;
+    int i, RetValue, nNodes, nNodesBeg, nInputs = s_pMan->nVars, nLeaves = nVars;
+    assert( nInputs <= 16 );
+
+    
+    // collect internal nodes and skip redundant cuts
+
+    Abc_NtkRecCollectNodesFromLib(pNtk, pRoot, vNodes , nLeaves);
+
+    Abc_NtkRecCutTruthFromLib(vNodes, nLeaves, s_pMan->vTtTemps, s_pMan->vTtElems );
+
+    // copy the truth table
+    Kit_TruthCopy( pInOut, (unsigned *)pRoot->pTemp, nInputs );
+
+    // go through the variables in the new truth table
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        // get hold of the corresponding leaf
+        pAbcObj = Abc_NtkPi(pNtk, i);
+        // get hold of the corresponding new node
+        pObj = Abc_NtkPi( pAig, i );
+        // map them
+        pAbcObj->pCopy = pObj;
+    }
+
+    // build the node and compute its truth table
+    nNodesBeg = Abc_NtkObjNumMax( pAig );
+    Vec_PtrForEachEntryStart( Abc_Obj_t *, vNodes, pAbcObj, i, nLeaves )
+    {
+        pFanin0 = Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin0(pAbcObj)->pCopy, Abc_ObjFaninC0(pAbcObj) );
+        pFanin1 = Abc_ObjNotCond( (Abc_Obj_t *)Abc_ObjFanin1(pAbcObj)->pCopy, Abc_ObjFaninC1(pAbcObj) );
+
+        nNodes = Abc_NtkObjNumMax( pAig );
+        pObj = Abc_AigAnd( (Abc_Aig_t *)pAig->pManFunc, pFanin0, pFanin1 );
+        assert( !Abc_ObjIsComplement(pObj) );
+        pAbcObj->pCopy = pObj;
+
+        if ( pObj->Id == nNodes )
+        {
+            // increase storage for truth tables
+//            if ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id )
+//                Vec_PtrDoubleSimInfo(s_pMan->vTtNodes);
+            while ( Vec_PtrSize(s_pMan->vTtNodes) <= pObj->Id )
+//                Vec_PtrPush( s_pMan->vTtNodes, ABC_ALLOC(unsigned, s_pMan->nWords) );
+                Vec_PtrPush( s_pMan->vTtNodes, Mem_FixedEntryFetch(s_pMan->pMmTruth) );
+
+            // compute the truth table
+            RetValue = Abc_NtkRecComputeTruth( pObj, s_pMan->vTtNodes, nInputs );
+            if ( RetValue == 0 )
+            {
+                s_pMan->nFilterError++;
+                printf( "T" );
+            }
+        }
+    }
+    assert(pObj);
+    pTruth = (unsigned *)Vec_PtrEntry( s_pMan->vTtNodes, pObj->Id );
+    assert ( Kit_TruthSupport(pTruth, nInputs) == Kit_BitMask(nLeaves) );
+    // compare the truth tables
+    assert (Kit_TruthIsEqual( pTruth, pInOut, nInputs ) );
+
+//    Extra_PrintBinary( stdout, pInOut, 8 ); printf( "\n" );
+
+    // look up in the hash table and increase the hit number of the functional class
+    ppSpot = Abc_NtkRecTableLookup( s_pMan, pTruth, nInputs );
+
+    // if not new nodes were added and the node has a CO fanout
+    if ( nNodesBeg == Abc_NtkObjNumMax(pAig) && Abc_NodeFindCoFanout(pObj) != NULL )
+    {
+        s_pMan->nFilterSame++;
+        assert(*ppSpot != NULL);
+        return;
+    }
+
+    // create PO for this node
+    pObjPo = Abc_NtkCreatePo(pAig);
+    Abc_ObjAddFanin( pObjPo, pObj );
+
+    // assign the name to this PO
+    sprintf( Name, "%d_%06d", nLeaves, Abc_NtkPoNum(pAig) );
+    if ( (nInputs <= 6) && 0 )
+    {
+        Extra_PrintHexadecimalString( Truth, pInOut, nInputs );
+        sprintf( Buffer, "%s_%s", Name, Truth );
+    }
+    else
+    {
+        sprintf( Buffer, "%s", Name );
+    }
+    Abc_ObjAssignName( pObjPo, Buffer, NULL );
+
+    // add the resulting truth table to the hash table 
+    Abc_NtkRecInsertToLookUpTable(s_pMan, ppSpot, pObj, nLeaves, s_pMan->fTrim);
+}
+
 
 /**Function*************************************************************
 
@@ -1821,12 +2133,15 @@ int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut)
     If_CutTruthStretch(pInOut, nLeaves, nVars);
     s_pMan->timeIfCanonicize += clock() - timeCanonicize;   
     ppSpot = Abc_NtkRecTableLookup( s_pMan, pInOut, nVars );
+    if (*ppSpot == NULL)
+    {
+        Kit_TruthNot(pInOut, pInOut, nVars);
+        ppSpot = Abc_NtkRecTableLookup( s_pMan, pInOut, nVars );
+    }
     assert (!(*ppSpot == NULL && nLeaves == 2));
     //functional class not found in the library.
     if ( *ppSpot == NULL )
     {
-Kit_DsdPrintFromTruth( pInOut, nLeaves ); printf( "\n" );
-
         s_pMan->nFunsNotFound++;        
         pCut->Cost = IF_COST_MAX;
         pCut->fUser = 1;

src/map/if/if.h

@@ -106,6 +106,7 @@ struct If_Par_t_
     // internal parameters
     int                fDelayOpt;     // special delay optimization
     int                fUserRecLib;   // use recorded library
+    int                fSkipCutFilter;// skip cut filter
     int                fAreaOnly;     // area only mode
     int                fTruth;        // truth table computation enabled
     int                fUsePerm;      // use permutation (delay info)

src/map/if/ifMap.c

@@ -196,7 +196,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         p->nCutsTotal++;
         // check if this cut is contained in any of the available cuts
 //        if ( p->pPars->pFuncCost == NULL && If_CutFilter( p, pCut ) ) // do not filter functionality cuts
-        if ( If_CutFilter( pCutSet, pCut ) )
+        if ( !p->pPars->fSkipCutFilter && If_CutFilter( pCutSet, pCut ) )
             continue;
         // compute the truth table
         pCut->fCompl = 0;