Version abc70714

11 files changed, 469 insertions, 100 deletions

diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index a1502382..969e5253 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -49,7 +49,7 @@ static Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig
 Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
 {
     Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t * pObj, * pDriver, * pObjNew;
     Vec_Vec_t * vStore;
     int i;
     // create the new manager 
@@ -63,14 +63,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     vStore = Vec_VecAlloc( 50 );
     Aig_ManForEachPo( p, pObj, i )
     {
-        pObjNew = Dar_Balance_rec( pNew, Aig_ObjFanin0(pObj), vStore, 0, fUpdateLevel );
-        Aig_ObjCreatePo( pNew, Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ) );
+        pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+        pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
+        pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
+        Aig_ObjCreatePo( pNew, pObjNew );
     }
     Vec_VecFree( vStore );
     // remove dangling nodes
-//    Aig_ManCreateRefs( pNew );
-//    if ( i = Aig_ManCleanup( pNew ) )
-//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+    if ( i = Aig_ManCleanup( pNew ) )
+        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
     // check the resulting AIG
     if ( !Aig_ManCheck(pNew) )
         printf( "Dar_ManBalance(): The check has failed.\n" );
@@ -94,6 +95,7 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     Vec_Ptr_t * vSuper;
     int i;
     assert( !Aig_IsComplement(pObjOld) );
+    assert( !Aig_ObjIsBuf(pObjOld) );
     // return if the result is known
     if ( pObjOld->pData )
         return pObjOld->pData;
@@ -157,8 +159,8 @@ int Dar_BalanceCone_rec( Aig_Obj_t * pRoot, Aig_Obj_t * pObj, Vec_Ptr_t * vSuper
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsNode(pObj) );
     // go through the branches
-    RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild0(pObj), vSuper );
-    RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjChild1(pObj), vSuper );
+    RetValue1 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild0(pObj) ), vSuper );
+    RetValue2 = Dar_BalanceCone_rec( pRoot, Aig_ObjReal_rec( Aig_ObjChild1(pObj) ), vSuper );
     if ( RetValue1 == -1 || RetValue2 == -1 )
         return -1;
     // return 1 if at least one branch has a duplicate
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index a617f5d6..e7186e83 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -43,7 +43,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Dar_Par_t) );
     pPars->nCutsMax     = 8;
-    pPars->nSubgMax     = 4;
+    pPars->nSubgMax     = 5; // 5 is a "magic number"
     pPars->fUpdateLevel = 0;
     pPars->fUseZeros    = 0;
     pPars->fVerbose     = 0;
@@ -69,18 +69,18 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
     Aig_Obj_t * pObj, * pObjNew;
     int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required;
     int clk = 0, clkStart;
+    // prepare the library
+    Dar_LibPrepare( pPars->nSubgMax ); 
     // create rewriting manager
     p = Dar_ManStart( pAig, pPars );
     // remove dangling nodes
     Aig_ManCleanup( pAig );
+    // if updating levels is requested, start fanout and timing
+    Aig_ManCreateFanout( pAig );
+    if ( p->pPars->fUpdateLevel )
+        Aig_ManStartReverseLevels( pAig, 0 );
     // set elementary cuts for the PIs
-//    Dar_ManSetupPis( p );
-    Aig_ManCleanData( pAig );
-    Dar_ObjPrepareCuts( p, Aig_ManConst1(pAig) );
-    Aig_ManForEachPi( pAig, pObj, i )
-        Dar_ObjPrepareCuts( p, pObj );
-//    if ( p->pPars->fUpdateLevel )
-//        Aig_NtkStartReverseLevels( p );
+    Dar_ManCutsStart( p );
     // resynthesize each node once
     clkStart = clock();
     p->nNodesInit = Aig_ManNodeNum(pAig);
@@ -93,6 +93,10 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
             continue;
         if ( i > nNodesOld )
             break;
+        // consider freeing the cuts
+//        if ( (i & 0xFFF) == 0 && Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) > 100 )
+//            Dar_ManCutsStart( p );
+
         // compute cuts for the node
 clk = clock();
         Dar_ObjComputeCuts_rec( p, pObj );
@@ -100,7 +104,7 @@ p->timeCuts += clock() - clk;
 
         // check if there is a trivial cut
         Dar_ObjForEachCut( pObj, pCut, k )
-            if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id) )
+            if ( pCut->nLeaves == 0 || (pCut->nLeaves == 1 && pCut->pLeaves[0] != pObj->Id && Aig_ManObj(p->pAig, pCut->pLeaves[0])) )
                 break;
         if ( k < (int)pObj->nCuts )
         {
@@ -115,10 +119,10 @@ p->timeCuts += clock() - clk;
                 assert( pCut->uTruth == 0xAAAA || pCut->uTruth == 0x5555 );
                 pObjNew = Aig_NotCond( Aig_ManObj(p->pAig, pCut->pLeaves[0]), pCut->uTruth==0x5555 );
             }
-            // replace the node
-            Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
             // remove the old cuts
             Dar_ObjSetCuts( pObj, NULL );
+            // replace the node
+            Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
             continue;
         }
 
@@ -128,17 +132,17 @@ p->timeCuts += clock() - clk;
         Dar_ObjForEachCut( pObj, pCut, k )
             Dar_LibEval( p, pObj, pCut, Required );
         // check the best gain
-        if ( !(p->GainBest > 0 || p->GainBest == 0 && p->pPars->fUseZeros) )
+        if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
             continue;
+        // remove the old cuts
+        Dar_ObjSetCuts( pObj, NULL );
         // if we end up here, a rewriting step is accepted
         nNodeBefore = Aig_ManNodeNum( pAig );
         pObjNew = Dar_LibBuildBest( p );
         pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
         // replace the node
-        Aig_ObjReplace( pAig, pObj, pObjNew, 1 );
-        // remove the old cuts
-        Dar_ObjSetCuts( pObj, NULL );
+        Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
         // compare the gains
         nNodeAfter = Aig_ManNodeNum( pAig );
         assert( p->GainBest <= nNodeBefore - nNodeAfter );
@@ -151,13 +155,14 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
     Extra_ProgressBarStop( pProgress );
     p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20);
     Dar_ManCutsFree( p );
-    // stop the rewriting manager
-    Dar_ManStop( p );
     // put the nodes into the DFS order and reassign their IDs
 //    Aig_NtkReassignIds( p );
     // fix the levels
-//    if ( p->pPars->fUpdateLevel )
-//        Aig_NtkStopReverseLevels( p );
+    Aig_ManDeleteFanout( pAig );
+    if ( p->pPars->fUpdateLevel )
+        Aig_ManStopReverseLevels( pAig );
+    // stop the rewriting manager
+    Dar_ManStop( p );
     // check
     if ( !Aig_ManCheck( pAig ) )
     {
@@ -190,9 +195,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig )
     // remove dangling nodes
     Aig_ManCleanup( pAig );
     // set elementary cuts for the PIs
-//    Dar_ManSetupPis( p );
-    Aig_ManForEachPi( pAig, pObj, i )
-        Dar_ObjPrepareCuts( p, pObj );
+    Dar_ManCutsStart( p );
     // compute cuts for each nodes in the topological order
     Aig_ManForEachObj( pAig, pObj, i )
     {
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index af9d1227..08bd77a9 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -62,20 +62,25 @@ static inline int Dar_WordCountOnes( unsigned uWord )
 static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
 {
     Aig_Obj_t * pLeaf;
-    int i, Value;
+    int i, Value, nOnes;
     assert( pCut->fUsed );
-    if ( pCut->nLeaves < 2 )
-        return 1001;
     Value = 0;
+    nOnes = 0;
     Dar_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
     {
         if ( pLeaf == NULL )
             return 0;
         assert( pLeaf != NULL );
         Value += pLeaf->nRefs;
+        nOnes += (pLeaf->nRefs == 1);
     }
+    if ( pCut->nLeaves < 2 )
+        return 1001;
+//    Value = Value * 100 / pCut->nLeaves;
     if ( Value > 1000 )
         Value = 1000;
+    if ( nOnes > 3 )
+        Value = 5 - nOnes;
     return Value;
 }
 
@@ -83,7 +88,7 @@ static inline int Dar_CutFindValue( Dar_Man_t * p, Dar_Cut_t * pCut )
 
   Synopsis    [Returns the next free cut to use.]
 
-  Description []
+  Description [Uses the cut with the smallest value.]
                
   SideEffects []
 
@@ -114,6 +119,14 @@ static inline Dar_Cut_t * Dar_CutFindFree( Dar_Man_t * p, Aig_Obj_t * pObj )
                 pCutMax = pCut;
         }
     }
+    if ( pCutMax == NULL )
+    {
+        Dar_ObjForEachCutAll( pObj, pCut, i )
+        {
+            if ( pCutMax == NULL || pCutMax->Value > pCut->Value )
+                pCutMax = pCut;
+        }
+    }
     assert( pCutMax != NULL );
     pCutMax->fUsed = 0;
     return pCutMax;
@@ -466,7 +479,6 @@ static inline int Dar_CutSuppMinimize( Dar_Cut_t * pCut )
     unsigned uPhase = 0, uTruth = 0xFFFF & pCut->uTruth;
     int i, k, nLeaves;
     assert( pCut->fUsed );
-    assert( pCut->nLeaves > 0 );
     // compute the truth support of the cut's function
     nLeaves = pCut->nLeaves;
     for ( i = 0; i < (int)pCut->nLeaves; i++ )
@@ -566,6 +578,28 @@ Dar_Cut_t * Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
+void Dar_ManCutsStart( Dar_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManCleanData( p->pAig );
+    Aig_MmFixedRestart( p->pMemCuts );
+    Dar_ObjPrepareCuts( p, Aig_ManConst1(p->pAig) );
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        Dar_ObjPrepareCuts( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
@@ -612,10 +646,6 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
         // minimize support of the cut
         if ( Dar_CutSuppMinimize( pCut ) )
         {
-            // if a simple cut is found return immediately
-            if ( pCut->nLeaves < 2 )
-                return pCutSet;
-            // otherwise, filter the cuts again
             RetValue = Dar_CutFilter( pObj, pCut );
             assert( !RetValue );
         }
@@ -628,6 +658,8 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
             p->nCutsSkipped++;
             pCut->fUsed = 0;
         }
+        else if ( pCut->nLeaves < 2 )
+            return pCutSet;
     }
     // count the number of nontrivial cuts cuts
     Dar_ObjForEachCut( pObj, pCut, i )
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 0eb8f9fe..f496a73f 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -101,7 +101,7 @@ struct Dar_Man_t_
 };
 
 static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return pObj->pData;    }
-static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )   { pObj->pData = pCuts;   }
+static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )   { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts;   }
 
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
@@ -126,22 +126,24 @@ static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )
 
 /*=== darBalance.c ========================================================*/
 extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
-/*=== darCore.c ========================================================*/
-/*=== darCut.c ========================================================*/
-extern Dar_Cut_t *     Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+/*=== darCore.c ===========================================================*/
+/*=== darCut.c ============================================================*/
+extern void            Dar_ManCutsStart( Dar_Man_t * p );
 extern void            Dar_ManCutsFree( Dar_Man_t * p );
 extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
 extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
-/*=== darData.c ========================================================*/
+/*=== darData.c ===========================================================*/
 extern Vec_Int_t *     Dar_LibReadNodes();
 extern Vec_Int_t *     Dar_LibReadOuts();
 extern Vec_Int_t *     Dar_LibReadPrios();
-/*=== darLib.c ==========================================================*/
+/*=== darLib.c ============================================================*/
 extern void            Dar_LibStart();
 extern void            Dar_LibStop();
+extern void            Dar_LibPrepare( int nSubgraphs );
+extern void            Dar_LibReturnCanonicals( unsigned * pCanons );
 extern void            Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
 extern Aig_Obj_t *     Dar_LibBuildBest( Dar_Man_t * p );
-/*=== darMan.c ==========================================================*/
+/*=== darMan.c ============================================================*/
 extern Dar_Man_t *     Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars );
 extern void            Dar_ManStop( Dar_Man_t * p );
 extern void            Dar_ManPrintStats( Dar_Man_t * p );
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index fce6155b..c3d57b52 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -44,7 +44,7 @@ struct Dar_LibDat_t_ // library object data
     Aig_Obj_t *      pFunc;         // the corresponding AIG node if it exists
     int              Level;         // level of this node after it is constructured
     int              TravId;        // traversal ID of the library object data
-    unsigned char    Area;          // area of the node
+    unsigned char    fMffc;         // set to one if node is part of MFFC
     unsigned char    nLats[3];      // the number of latches on the input/output stem
 };
 
@@ -54,9 +54,6 @@ struct Dar_Lib_t_ // library
     Dar_LibObj_t *   pObjs;         // the set of library objects
     int              nObjs;         // the number of objects used
     int              iObj;          // the current object
-    // object data
-    Dar_LibDat_t *   pDatas;
-    int              nDatas;
     // structures by class
     int              nSubgr[222];   // the number of subgraphs by class
     int *            pSubgr[222];   // the subgraphs for each class
@@ -75,8 +72,24 @@ struct Dar_Lib_t_ // library
     int              nNodes[222];   // the number of nodes by class
     int *            pNodes[222];   // the nodes for each class
     int *            pNodesMem;     // memory for nodes pointers
-    int              pNodesTotal;   // the total number of nodes
-    // information by NPN classes
+    int              nNodesTotal;   // the total number of nodes
+    // prepared library
+    int              nSubgraphs;
+    int              nNodes0Max;
+    // nodes by class
+    int              nNodes0[222];   // the number of nodes by class
+    int *            pNodes0[222];   // the nodes for each class
+    int *            pNodes0Mem;     // memory for nodes pointers
+    int              nNodes0Total;   // the total number of nodes
+    // structures by class
+    int              nSubgr0[222];   // the number of subgraphs by class
+    int *            pSubgr0[222];   // the subgraphs for each class
+    int *            pSubgr0Mem;     // memory for subgraph pointers
+    int              nSubgr0Total;   // the total number of subgraph
+    // object data
+    Dar_LibDat_t *   pDatas;
+    int              nDatas;
+    // information about NPN classes
     char **          pPerms4;
     unsigned short * puCanons; 
     char *           pPhases; 
@@ -104,7 +117,7 @@ static inline int            Dar_LibObjTruth( Dar_LibObj_t * pObj ) { return pOb
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
+Dar_Lib_t * Dar_LibAlloc( int nObjs )
 {
     unsigned uTruths[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
     Dar_Lib_t * p;
@@ -115,10 +128,6 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs, int nDatas )
     p->nObjs = nObjs;
     p->pObjs = ALLOC( Dar_LibObj_t, nObjs );
     memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs );
-    // allocate datas
-    p->nDatas = nDatas;
-    p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
-    memset( p->pObjs, 0, sizeof(Dar_LibDat_t) * nDatas );
     // allocate canonical data
     p->pPerms4 = Extra_Permutations( 4 );
     Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
@@ -149,7 +158,9 @@ void Dar_LibFree( Dar_Lib_t * p )
     free( p->pObjs );
     free( p->pDatas );
     free( p->pNodesMem );
+    free( p->pNodes0Mem );
     free( p->pSubgrMem );
+    free( p->pSubgr0Mem );
     free( p->pPriosMem );
     FREE( p->pPlaceMem );
     FREE( p->pScoreMem );
@@ -163,6 +174,31 @@ void Dar_LibFree( Dar_Lib_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns canonical truth tables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibReturnCanonicals( unsigned * pCanons )
+{
+    int Visits[222] = {0};
+    int i, k;
+    // find canonical truth tables
+    for ( i = k = 0; i < (1<<16); i++ )
+        if ( !Visits[s_DarLib->pMap[i]] )
+        {
+            Visits[s_DarLib->pMap[i]] = 1;
+            pCanons[k++] = ((i<<16) | i);
+        }
+    assert( k == 222 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Adds one AND to the library.]
 
   Description []
@@ -196,14 +232,14 @@ void Dar_LibAddNode( Dar_Lib_t * p, int Id0, int Id1, int fCompl0, int fCompl1 )
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class )
+void Dar_LibSetup_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
 {
     if ( pObj->fTerm || (int)pObj->Num == Class )
         return;
     pObj->Num = Class;
-    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class );
-    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class );
-    if ( p->pNodesMem )
+    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
+    Dar_LibSetup_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
+    if ( fCollect )
         p->pNodes[Class][ p->nNodes[Class]++ ] = pObj-p->pObjs;
     else
         p->nNodes[Class]++;
@@ -239,10 +275,12 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
     }
     // allocate memory for the roots of each class
     p->pSubgrMem = ALLOC( int, Vec_IntSize(vOuts) );
+    p->pSubgr0Mem = ALLOC( int, Vec_IntSize(vOuts) );
     p->nSubgrTotal = 0;
     for ( i = 0; i < 222; i++ )
     {
         p->pSubgr[i] = p->pSubgrMem + p->nSubgrTotal;
+        p->pSubgr0[i] = p->pSubgr0Mem + p->nSubgrTotal;
         p->nSubgrTotal += p->nSubgr[i];
         p->nSubgr[i] = 0;
     }
@@ -321,18 +359,20 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
     // count nodes in each class
     for ( i = 0; i < 222; i++ )
         for ( k = 0; k < p->nSubgr[i]; k++ )
-            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
+            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 0 );
     // count the total number of nodes
-    p->pNodesTotal = 0;
+    p->nNodesTotal = 0;
     for ( i = 0; i < 222; i++ )
-        p->pNodesTotal += p->nNodes[i];
+        p->nNodesTotal += p->nNodes[i];
     // allocate memory for the nodes of each class
-    p->pNodesMem = ALLOC( int, p->pNodesTotal );
-    p->pNodesTotal = 0;
+    p->pNodesMem = ALLOC( int, p->nNodesTotal );
+    p->pNodes0Mem = ALLOC( int, p->nNodesTotal );
+    p->nNodesTotal = 0;
     for ( i = 0; i < 222; i++ )
     {
-        p->pNodes[i] = p->pNodesMem + p->pNodesTotal;
-        p->pNodesTotal += p->nNodes[i];
+        p->pNodes[i] = p->pNodesMem + p->nNodesTotal;
+        p->pNodes0[i] = p->pNodes0Mem + p->nNodesTotal;
+        p->nNodesTotal += p->nNodes[i];
         p->nNodes[i] = 0;
     }
     // create traversal IDs
@@ -343,11 +383,11 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
     for ( i = 0; i < 222; i++ )
     {
          for ( k = 0; k < p->nSubgr[i]; k++ )
-            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i );
+            Dar_LibSetup_rec( p, Dar_LibObj(p, p->pSubgr[i][k]), i, 1 );
          nNodesTotal += p->nNodes[i];
 //printf( "Class %3d : Subgraphs = %4d. Nodes = %5d.\n", i, p->nSubgr[i], p->nNodes[i] );
     }
-    assert( nNodesTotal == p->pNodesTotal );
+    assert( nNodesTotal == p->nNodesTotal );
      // prepare the number of the PI nodes
     for ( i = 0; i < 4; i++ )
         Dar_LibObj(p, i)->Num = i;
@@ -355,6 +395,133 @@ void Dar_LibSetup( Dar_Lib_t * p, Vec_Int_t * vOuts, Vec_Int_t * vPrios )
 
 /**Function*************************************************************
 
+  Synopsis    [Starts the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibCreateData( Dar_Lib_t * p, int nDatas )
+{
+    if ( p->nDatas == nDatas )
+        return;
+    FREE( p->pDatas );
+    // allocate datas
+    p->nDatas = nDatas;
+    p->pDatas = ALLOC( Dar_LibDat_t, nDatas );
+    memset( p->pDatas, 0, sizeof(Dar_LibDat_t) * nDatas );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one AND to the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibSetup0_rec( Dar_Lib_t * p, Dar_LibObj_t * pObj, int Class, int fCollect )
+{
+    if ( pObj->fTerm || (int)pObj->Num == Class )
+        return;
+    pObj->Num = Class;
+    Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan0), Class, fCollect );
+    Dar_LibSetup0_rec( p, Dar_LibObj(p, pObj->Fan1), Class, fCollect );
+    if ( fCollect )
+        p->pNodes0[Class][ p->nNodes0[Class]++ ] = pObj-p->pObjs;
+    else
+        p->nNodes0[Class]++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_LibPrepare( int nSubgraphs )
+{
+    Dar_Lib_t * p = s_DarLib;
+    int i, k, nNodes0Total;
+    if ( p->nSubgraphs == nSubgraphs )
+        return;
+
+    // favor special classes:
+    //  1 : F = (!d*!c*!b*!a)
+    //  4 : F = (!d*!c*!(b*a))
+    // 12 : F = (!d*!(c*!(!b*!a)))
+    // 20 : F = (!d*!(c*b*a))
+
+    // set the subgraph counters 
+    p->nSubgr0Total = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+//        if ( i == 1 || i == 4 || i == 12 || i == 20 ) // special classes 
+        if ( i == 1 ) // special classes 
+            p->nSubgr0[i] = p->nSubgr[i];
+        else
+            p->nSubgr0[i] = AIG_MIN( p->nSubgr[i], nSubgraphs );
+        p->nSubgr0Total += p->nSubgr0[i];
+        for ( k = 0; k < p->nSubgr0[i]; k++ )
+            p->pSubgr0[i][k] = p->pSubgr[i][ p->pPrios[i][k] ];
+    }
+
+    // count the number of nodes
+    // clean node counters
+    for ( i = 0; i < 222; i++ )
+        p->nNodes0[i] = 0;
+    // create traversal IDs
+    for ( i = 0; i < p->iObj; i++ )
+        Dar_LibObj(p, i)->Num = 0xff;
+    // count nodes in each class
+    // count the total number of nodes and the largest class
+    p->nNodes0Total = 0;
+    p->nNodes0Max = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+        for ( k = 0; k < p->nSubgr0[i]; k++ )
+            Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 0 );
+        p->nNodes0Total += p->nNodes0[i];
+        p->nNodes0Max = AIG_MAX( p->nNodes0Max, p->nNodes0[i] );
+    }
+
+    // clean node counters
+    for ( i = 0; i < 222; i++ )
+        p->nNodes0[i] = 0;
+    // create traversal IDs
+    for ( i = 0; i < p->iObj; i++ )
+        Dar_LibObj(p, i)->Num = 0xff;
+    // add the nodes to storage
+    nNodes0Total = 0;
+    for ( i = 0; i < 222; i++ )
+    {
+        for ( k = 0; k < p->nSubgr0[i]; k++ )
+            Dar_LibSetup0_rec( p, Dar_LibObj(p, p->pSubgr0[i][k]), i, 1 );
+         nNodes0Total += p->nNodes0[i];
+    }
+    assert( nNodes0Total == p->nNodes0Total );
+     // prepare the number of the PI nodes
+    for ( i = 0; i < 4; i++ )
+        Dar_LibObj(p, i)->Num = i;
+
+    // realloc the datas
+    Dar_LibCreateData( p, p->nNodes0Max + 32 ); 
+    // allocated more because Dar_LibBuildBest() sometimes requires more entries
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads library from array.]
 
   Description []
@@ -374,7 +541,7 @@ Dar_Lib_t * Dar_LibRead()
     vOuts  = Dar_LibReadOuts();
     vPrios = Dar_LibReadPrios();
     // create library
-    p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4, 6000 );
+    p = Dar_LibAlloc( Vec_IntSize(vObjs)/2 + 4 );
     // create nodes
     for ( i = 0; i < vObjs->nSize; i += 2 )
         Dar_LibAddNode( p, vObjs->pArray[i] >> 1, vObjs->pArray[i+1] >> 1,
@@ -383,6 +550,7 @@ Dar_Lib_t * Dar_LibRead()
     Dar_LibSetup( p, vOuts, vPrios );
     Vec_IntFree( vObjs );
     Vec_IntFree( vOuts );
+    Vec_IntFree( vPrios );
     return p;
 }
 
@@ -670,15 +838,20 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
     Dar_LibDat_t * pData, * pData0, * pData1;
     Aig_Obj_t * pGhost, * pFanin0, * pFanin1;
     int i;
-    for ( i = 0; i < s_DarLib->nNodes[Class]; i++ )
+    for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
     {
         // get one class node, assign its temporary number and set its data
-        pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes[Class][i]);
+        pObj = Dar_LibObj(s_DarLib, s_DarLib->pNodes0[Class][i]);
         pObj->Num = 4 + i;
+        assert( (int)pObj->Num < s_DarLib->nNodes0Max + 4 );
         pData = s_DarLib->pDatas + pObj->Num;
+        pData->fMffc = 0;
         pData->pFunc = NULL;
         pData->TravId = 0xFFFF;
+
         // explore the fanins
+        assert( (int)Dar_LibObj(s_DarLib, pObj->Fan0)->Num < s_DarLib->nNodes0Max + 4 );
+        assert( (int)Dar_LibObj(s_DarLib, pObj->Fan1)->Num < s_DarLib->nNodes0Max + 4 );
         pData0 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan0)->Num;
         pData1 = s_DarLib->pDatas + Dar_LibObj(s_DarLib, pObj->Fan1)->Num;
         pData->Level = 1 + AIG_MAX(pData0->Level, pData1->Level);
@@ -704,9 +877,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
 
         // clear the node if it is part of MFFC
         if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) )
-            pData->pFunc = NULL;
-//if ( Class == 7 )
-//printf( "Evaling node %d at data %d\n", pData->pFunc? pData->pFunc->Id : -1, pObj->Num );
+            pData->fMffc = 1;
     }
 }
 
@@ -729,20 +900,22 @@ int Dar_LibEval_rec( Dar_LibObj_t * pObj, int Out, int nNodesSaved, int Required
         return 0;
     assert( pObj->Num > 3 );
     pData = s_DarLib->pDatas + pObj->Num;
-    if ( pData->pFunc )
+    if ( pData->pFunc && !pData->fMffc )
         return 0;
     if ( pData->Level > Required )
         return 0xff;
     if ( pData->TravId == Out )
-        return pData->Area;
+        return 0;
     pData->TravId = Out;
-    Area = 1 + Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required );
+    // this is a new node - get a bound on the area of its branches
+    nNodesSaved--;
+    Area = Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan0), Out, nNodesSaved, Required+1 );
     if ( Area > nNodesSaved )
-        return pData->Area = 0xff;
-    Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required );
+        return 0xff;
+    Area += Dar_LibEval_rec( Dar_LibObj(s_DarLib, pObj->Fan1), Out, nNodesSaved, Required+1 );
     if ( Area > nNodesSaved )
-        return pData->Area = 0xff;
-    return pData->Area = Area;
+        return 0xff;
+    return Area + 1;
 }
 
 /**Function*************************************************************
@@ -773,25 +946,27 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
     Class = s_DarLib->pMap[pCut->uTruth];
     Dar_LibEvalAssignNums( p, Class );
     // profile outputs by their savings
-    p->nTotalSubgs += s_DarLib->nSubgr[Class];
-    p->ClassSubgs[Class] += s_DarLib->nSubgr[Class];
-    for ( Out = 0; Out < s_DarLib->nSubgr[Class]; Out++ )
+    p->nTotalSubgs += s_DarLib->nSubgr0[Class];
+    p->ClassSubgs[Class] += s_DarLib->nSubgr0[Class];
+    for ( Out = 0; Out < s_DarLib->nSubgr0[Class]; Out++ )
     {
-        pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr[Class][Out]);
-        nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved, Required );
+        pObj = Dar_LibObj(s_DarLib, s_DarLib->pSubgr0[Class][Out]);
+        if ( Aig_Regular(s_DarLib->pDatas[pObj->Num].pFunc) == pRoot )
+            continue;
+        nNodesAdded = Dar_LibEval_rec( pObj, Out, nNodesSaved - !p->pPars->fUseZeros, Required );
         nNodesGained = nNodesSaved - nNodesAdded;
         if ( fTraining && nNodesGained >= 0 )
             Dar_LibIncrementScore( Class, Out, nNodesGained + 1 );
-        if ( nNodesGained <= 0 )
+        if ( nNodesGained < 0 || (nNodesGained == 0 && !p->pPars->fUseZeros) )
             continue;
-        if ( nNodesGained < p->GainBest || 
-            (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->GainBest) )
+        if ( nNodesGained <  p->GainBest || 
+            (nNodesGained == p->GainBest && s_DarLib->pDatas[pObj->Num].Level >= p->LevelBest) )
             continue;
         // remember this possibility
         Vec_PtrClear( p->vLeavesBest );
         for ( k = 0; k < (int)pCut->nLeaves; k++ )
             Vec_PtrPush( p->vLeavesBest, s_DarLib->pDatas[k].pFunc );
-        p->OutBest    = s_DarLib->pSubgr[Class][Out];
+        p->OutBest    = s_DarLib->pSubgr0[Class][Out];
         p->OutNumBest = Out;
         p->LevelBest  = s_DarLib->pDatas[pObj->Num].Level;
         p->GainBest   = nNodesGained;
@@ -845,7 +1020,6 @@ Aig_Obj_t * Dar_LibBuildBest_rec( Dar_Man_t * p, Dar_LibObj_t * pObj )
     pFanin0 = Aig_NotCond( pFanin0, pObj->fCompl0 );
     pFanin1 = Aig_NotCond( pFanin1, pObj->fCompl1 );
     pData->pFunc = Aig_And( p->pAig, pFanin0, pFanin1 );
-//printf( "Adding node %d for data %d\n", pData->pFunc->Id, pObj->Num );
     return pData->pFunc;
 }
 
diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c
index a209503a..8b7c5afb 100644
--- a/src/aig/dar/darMan.c
+++ b/src/aig/dar/darMan.c
@@ -48,7 +48,7 @@ Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars )
     p->pPars = pPars;
     p->pAig  = pAig;
     // prepare the internal memory manager
-    p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 512 );
+    p->pMemCuts = Aig_MmFixedStart( p->pPars->nCutsMax * sizeof(Dar_Cut_t), 1024 );
     // other data
     p->vLeavesBest = Vec_PtrAlloc( 4 );
     return p;
@@ -89,18 +89,27 @@ void Dar_ManStop( Dar_Man_t * p )
 ***********************************************************************/
 void Dar_ManPrintStats( Dar_Man_t * p )
 {
-    int i, Gain;
+    unsigned pCanons[222];
+    int Gain, i;
+    extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
+
     Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
     printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).  Cut mem = %d Mb\n", 
         p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit, p->nCutMemUsed );
     printf( "Cuts = %8d. Tried = %8d. Used = %8d. Bad = %5d. Skipped = %5d. Ave = %.2f.\n", 
         p->nCutsAll, p->nCutsTried, p->nCutsUsed, p->nCutsBad, p->nCutsSkipped,
         (float)p->nCutsUsed/Aig_ManNodeNum(p->pAig) );
+
+    printf( "Bufs = %5d. BufMax = %5d. BufReplace = %6d. BufFix = %6d.\n", 
+        Aig_ManBufNum(p->pAig), p->pAig->nBufMax, p->pAig->nBufReplaces, p->pAig->nBufFixes );
     PRT( "Cuts  ", p->timeCuts );
     PRT( "Eval  ", p->timeEval );
     PRT( "Other ", p->timeOther );
     PRT( "TOTAL ", p->timeTotal );
-/*
+
+    if ( !p->pPars->fVeryVerbose )
+        return;
+    Dar_LibReturnCanonicals( pCanons );
     for ( i = 0; i < 222; i++ )
     {
         if ( p->ClassGains[i] == 0 && p->ClassTimes[i] == 0 )
@@ -108,10 +117,10 @@ void Dar_ManPrintStats( Dar_Man_t * p )
         printf( "%3d : ", i );
         printf( "G = %6d (%5.2f %%)  ", p->ClassGains[i], Gain? 100.0*p->ClassGains[i]/Gain : 0.0 );
         printf( "S = %8d (%5.2f %%)  ", p->ClassSubgs[i], p->nTotalSubgs? 100.0*p->ClassSubgs[i]/p->nTotalSubgs : 0.0 );
-        printf( "R = %7d  ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
-        PRTP( "T", p->ClassTimes[i], p->timeEval );
+        printf( "R = %7d   ", p->ClassGains[i]? p->ClassSubgs[i]/p->ClassGains[i] : 9999999 );
+        Kit_DsdPrintFromTruth( pCanons + i, 4 );
+//        PRTP( "T", p->ClassTimes[i], p->timeEval );
     }
-*/
 }
 
 
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
new file mode 100644
index 00000000..1bcc0466
--- /dev/null
+++ b/src/aig/dar/darRefact.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [darRefact.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Refactoring.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darRefact.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darResub.c b/src/aig/dar/darResub.c
new file mode 100644
index 00000000..f819934e
--- /dev/null
+++ b/src/aig/dar/darResub.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [darResub.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darResub.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
new file mode 100644
index 00000000..c98a263e
--- /dev/null
+++ b/src/aig/dar/darScript.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [darScript.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [Rewriting scripts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: darScript.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/dar/dar_.c b/src/aig/dar/dar_.c
index 08bd8c3e..12fd7d17 100644
--- a/src/aig/dar/dar_.c
+++ b/src/aig/dar/dar_.c
@@ -18,7 +18,7 @@
 
 ***********************************************************************/
 
-#include "dar.h"
+#include "darInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make
index bcf9a2e6..09b45171 100644
--- a/src/aig/dar/module.make
+++ b/src/aig/dar/module.make
@@ -4,4 +4,7 @@ SRC +=    src/aig/dar/darBalance.c \
     src/aig/dar/darData.c \
     src/aig/dar/darLib.c \
     src/aig/dar/darMan.c \
+    src/aig/dar/darRefact.c \
+    src/aig/dar/darResub.c \
+    src/aig/dar/darScript.c \
     src/aig/dar/darTruth.c