Version abc70723

abc.dsp

@@ -2746,6 +2746,10 @@ SOURCE=.\src\aig\aig\aigMem.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigMffc.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigObj.c
 # End Source File
 # Begin Source File
@@ -2766,8 +2770,16 @@ SOURCE=.\src\aig\aig\aigTiming.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\aig\aigTruth.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\aig\aigUtil.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\aig\aigWin.c
+# End Source File
 # End Group
 # End Group
 # End Group

abc.rc

@@ -168,6 +168,7 @@ alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
 #alias t        "r c/16/csat_147.bench; st; dfraig -C 10 -v -r"
 #alias t        "r i10.blif; st; ps; csweep; ps; cec"
 #alias t        "r c/5/csat_777.bench; st; csweep -v"
-alias t        "r i10.blif; st; drw -v"
+#alias t        "r i10.blif; st; drw -v"
+alias t        "r c.blif; st; drf"
 
 

src/aig/aig/aig.h

@@ -274,6 +274,9 @@ static inline void Aig_ManRecycleMemory( Aig_Man_t * p, Aig_Obj_t * pEntry )
 // iterator over all nodes
 #define Aig_ManForEachNode( p, pObj, i )                                        \
     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL || !Aig_ObjIsNode(pObj) ) {} else
+// iterator over the nodes whose IDs are stored in the array
+#define Aig_ManForEachNodeVec( p, vIds, pObj, i )                               \
+    for ( i = 0; i < Vec_IntSize(vIds) && ((pObj) = Aig_ManObj(p, Vec_IntEntry(vIds,i))); i++ )
 
 // these two procedures are only here for the use inside the iterator
 static inline int     Aig_ObjFanout0Int( Aig_Man_t * p, int ObjId )  { assert(ObjId < p->nFansAlloc);  return p->pFanData[5*ObjId];                         }
@@ -299,6 +302,7 @@ extern int             Aig_DagSize( Aig_Obj_t * pObj );
 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
 extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
+extern void            Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
@@ -314,6 +318,13 @@ extern void            Aig_ManPrintStats( Aig_Man_t * p );
 /*=== aigMem.c ==========================================================*/
 extern void            Aig_ManStartMemory( Aig_Man_t * p );
 extern void            Aig_ManStopMemory( Aig_Man_t * p );
+/*=== aigMffc.c ==========================================================*/
+extern int             Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin );
+extern int             Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin );
+extern int             Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
+extern int             Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode );
+extern int             Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
+extern int             Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
 /*=== aigObj.c ==========================================================*/
 extern Aig_Obj_t *     Aig_ObjCreatePi( Aig_Man_t * p );
 extern Aig_Obj_t *     Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver );
@@ -341,6 +352,7 @@ extern Aig_Obj_t *     Aig_CreateExor( Aig_Man_t * p, int nVars );
 extern int             Aig_ManSeqStrash( Aig_Man_t * p, int nLatches, int * pInits );
 /*=== aigTable.c ========================================================*/
 extern Aig_Obj_t *     Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost );
+extern Aig_Obj_t *     Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 );
 extern void            Aig_TableInsert( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_TableDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern int             Aig_TableCountEntries( Aig_Man_t * p );
@@ -351,10 +363,13 @@ extern void            Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIn
 extern void            Aig_ManStopReverseLevels( Aig_Man_t * p );
 extern void            Aig_ManUpdateLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
 extern void            Aig_ManUpdateReverseLevel( Aig_Man_t * p, Aig_Obj_t * pObjNew );
+/*=== aigTruth.c ========================================================*/
+extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore );
 /*=== aigUtil.c =========================================================*/
 extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
 extern int             Aig_ManLevels( Aig_Man_t * p );
+extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
 extern void            Aig_ManCleanData( Aig_Man_t * p );
 extern void            Aig_ObjCleanData_rec( Aig_Obj_t * pObj );
 extern void            Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
@@ -367,6 +382,8 @@ extern void            Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_
 extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
 extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
 extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
+/*=== aigWin.c =========================================================*/
+extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
  
 /*=== aigMem.c ===========================================================*/
 // fixed-size-block memory manager

src/aig/aig/aigDfs.c

@@ -433,6 +433,64 @@ Aig_Obj_t * Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, in
     return Aig_NotCond( Aig_Regular(pRoot)->pData, Aig_IsComplement(pRoot) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the internal nodes of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCollectCut_rec( Aig_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+//    Aig_Obj_t * pFan0 = Aig_ObjFanin0(pNode);
+//    Aig_Obj_t * pFan1 = Aig_ObjFanin1(pNode);
+    if ( pNode->fMarkA )
+        return;
+    pNode->fMarkA = 1;
+    assert( Aig_ObjIsNode(pNode) );
+    Aig_ManCollectCut_rec( Aig_ObjFanin0(pNode), vNodes );
+    Aig_ManCollectCut_rec( Aig_ObjFanin1(pNode), vNodes );
+    Vec_PtrPush( vNodes, pNode );
+//printf( "added %d  ", pNode->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the internal nodes of the cut.]
+
+  Description [Does not include the leaves of the cut.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // collect and mark the leaves
+    Vec_PtrClear( vNodes );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    {
+        assert( pObj->fMarkA == 0 );
+        pObj->fMarkA = 1;
+//        printf( "%d " , pObj->Id );
+    }
+//printf( "\n" );
+    // collect and mark the nodes
+    Aig_ManCollectCut_rec( pRoot, vNodes );
+    // clean the nodes
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->fMarkA = 0;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkA = 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/aig/aigMffc.c

+/**CFile****************************************************************
+
+  FileName    [aigMffc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Computation of MFFCs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigMffc.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Dereferences the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin )
+{
+    Aig_Obj_t * pFanin;
+    int Counter = 0;
+    if ( Aig_ObjIsPi(pNode) )
+        return 0;
+    // consider the first fanin
+    pFanin = Aig_ObjFanin0(pNode);
+    assert( pFanin->nRefs > 0 );
+    if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+        Counter += Aig_NodeDeref_rec( pFanin, LevelMin );
+    // skip the buffer
+    if ( Aig_ObjIsBuf(pNode) )
+        return Counter;
+    assert( Aig_ObjIsNode(pNode) );
+    // consider the second fanin
+    pFanin = Aig_ObjFanin1(pNode);
+    assert( pFanin->nRefs > 0 );
+    if ( --pFanin->nRefs == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+        Counter += Aig_NodeDeref_rec( pFanin, LevelMin );
+    return Counter + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin )
+{
+    Aig_Obj_t * pFanin;
+    int Counter = 0;
+    if ( Aig_ObjIsPi(pNode) )
+        return 0;
+    // consider the first fanin
+    pFanin = Aig_ObjFanin0(pNode);
+    if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+        Counter += Aig_NodeRef_rec( pFanin, LevelMin );
+    // skip the buffer
+    if ( Aig_ObjIsBuf(pNode) )
+        return Counter;
+    assert( Aig_ObjIsNode(pNode) );
+    // consider the second fanin
+    pFanin = Aig_ObjFanin1(pNode);
+    if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+        Counter += Aig_NodeRef_rec( pFanin, LevelMin );
+    return Counter + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [References the node's MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeRefLabel_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin )
+{
+    Aig_Obj_t * pFanin;
+    int Counter = 0;
+    if ( Aig_ObjIsPi(pNode) )
+        return 0;
+    Aig_ObjSetTravIdCurrent( p, pNode );
+    // consider the first fanin
+    pFanin = Aig_ObjFanin0(pNode);
+    if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+        Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
+    if ( Aig_ObjIsBuf(pNode) )
+        return Counter;
+    assert( Aig_ObjIsNode(pNode) );
+    // consider the second fanin
+    pFanin = Aig_ObjFanin1(pNode);
+    if ( pFanin->nRefs++ == 0 && (!LevelMin || pFanin->Level > LevelMin) )
+        Counter += Aig_NodeRefLabel_rec( p, pFanin, LevelMin );
+    return Counter + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the internal and boundary nodes in the derefed MFFC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip )
+{
+    // skip visited nodes
+    if ( Aig_ObjIsTravIdCurrent(p, pNode) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pNode);
+    // add to the new support nodes
+    if ( !fTopmost && pNode != pObjSkip && (Aig_ObjIsPi(pNode) || pNode->nRefs > 0 || pNode->Level <= LevelMin) )
+    {
+        if ( vSupp ) Vec_PtrPush( vSupp, pNode );
+        return;
+    }
+    assert( Aig_ObjIsNode(pNode) );
+    // recur on the children
+    Aig_NodeMffsSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
+    Aig_NodeMffsSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the support of depth-limited MFFC.]
+
+  Description [Returns the number of internal nodes in the MFFC.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
+{
+    int ConeSize1, ConeSize2;
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_ObjIsNode(pNode) );
+    if ( vSupp ) Vec_PtrClear( vSupp );
+    Aig_ManIncrementTravId( p );
+    ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin );
+    Aig_NodeMffsSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
+    ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin );
+    assert( ConeSize1 == ConeSize2 );
+    assert( ConeSize1 > 0 );
+    return ConeSize1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels the nodes in the MFFC.]
+
+  Description [Returns the number of internal nodes in the MFFC.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode )
+{
+    int ConeSize1, ConeSize2;
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_ObjIsNode(pNode) );
+    Aig_ManIncrementTravId( p );
+    ConeSize1 = Aig_NodeDeref_rec( pNode, 0 );
+    ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
+    assert( ConeSize1 == ConeSize2 );
+    assert( ConeSize1 > 0 );
+    return ConeSize1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Labels the nodes in the MFFC.]
+
+  Description [Returns the number of internal nodes in the MFFC.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves )
+{
+    Aig_Obj_t * pObj;
+    int i, ConeSize1, ConeSize2;
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_ObjIsNode(pNode) );
+    Aig_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->nRefs++;
+    ConeSize1 = Aig_NodeDeref_rec( pNode, 0 );
+    ConeSize2 = Aig_NodeRefLabel_rec( p, pNode, 0 );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->nRefs--;
+    assert( ConeSize1 == ConeSize2 );
+    assert( ConeSize1 > 0 );
+    return ConeSize1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Expands the cut by adding the most closely related node.]
+
+  Description [Returns 1 if the cut exists.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult )
+{
+    Aig_Obj_t * pObj, * pLeafBest;
+    int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest;
+    // dereference the current cut
+    LevelMax = 0;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        LevelMax = AIG_MAX( LevelMax, (int)pObj->Level );
+    if ( LevelMax == 0 )
+        return 0;
+    // dereference the cut
+    ConeSize1 = Aig_NodeDeref_rec( pNode, 0 );
+    // try expanding each node in the boundary
+    ConeBest = AIG_INFINITY;
+    pLeafBest = NULL;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    {
+        if ( (int)pObj->Level != LevelMax )
+            continue;
+        ConeCur1 = Aig_NodeDeref_rec( pObj, 0 );
+        if ( ConeBest > ConeCur1 )
+        {
+            ConeBest = ConeCur1;
+            pLeafBest = pObj;
+        }
+        ConeCur2 = Aig_NodeRef_rec( pObj, 0 );
+        assert( ConeCur1 == ConeCur2 );
+    }
+    assert( pLeafBest != NULL );
+    assert( Aig_ObjIsNode(pLeafBest) );
+    // deref the best leaf
+    ConeCur1 = Aig_NodeDeref_rec( pLeafBest, 0 );
+    // collect the cut nodes
+    Vec_PtrClear( vResult );
+    Aig_ManIncrementTravId( p );
+    Aig_NodeMffsSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
+    // ref the nodes
+    ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 );
+    assert( ConeCur1 == ConeCur2 );
+    // ref the original node
+    ConeSize2 = Aig_NodeRef_rec( pNode, 0 );
+    assert( ConeSize1 == ConeSize2 );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/aig/aigObj.c

@@ -380,12 +380,13 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
         // delete the new object
         Aig_ObjDelete( p, pObjNew );
         // update levels
-        if ( fUpdateLevel )
+        if ( p->pFanData )
         {
             pObjOld->Level = LevelOld;
             Aig_ManUpdateLevel( p, pObjOld );
-            Aig_ManUpdateReverseLevel( p, pObjOld );
         }
+        if ( fUpdateLevel )
+            Aig_ManUpdateReverseLevel( p, pObjOld );
     }
     p->nObjs[pObjOld->Type]++;
     // store buffers if fanout is allocated

src/aig/aig/aigTable.c

@@ -146,6 +146,33 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
 
 /**Function*************************************************************
 
+  Synopsis    [Checks if node with the given attributes is in the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_TableLookupTwo( Aig_Man_t * p, Aig_Obj_t * pFanin0, Aig_Obj_t * pFanin1 )
+{
+    Aig_Obj_t * pGhost;
+    // consider simple cases
+    if ( pFanin0 == pFanin1 )
+        return pFanin0;
+    if ( pFanin0 == Aig_Not(pFanin1) )
+        return Aig_ManConst0(p);
+    if ( Aig_Regular(pFanin0) == Aig_ManConst1(p) )
+        return pFanin0 == Aig_ManConst1(p) ? pFanin1 : Aig_ManConst0(p);
+    if ( Aig_Regular(pFanin1) == Aig_ManConst1(p) )
+        return pFanin1 == Aig_ManConst1(p) ? pFanin0 : Aig_ManConst0(p);
+    pGhost = Aig_ObjCreateGhost( p, pFanin0, pFanin1, AIG_OBJ_AND );
+    return Aig_TableLookup( p, pGhost );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Adds the new node to the hash table.]
 
   Description []

src/aig/aig/aigTruth.c

+/**CFile****************************************************************
+
+  FileName    [aigTruth.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Computes truth table for the cut.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigTruth.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Aig_ManCutTruthOne( Aig_Obj_t * pNode, unsigned * pTruth, int nWords )
+{
+    unsigned * pTruth0, * pTruth1;
+    int i;
+    pTruth0 = Aig_ObjFanin0(pNode)->pData;
+    pTruth1 = Aig_ObjFanin1(pNode)->pData;
+    if ( Aig_ObjIsExor(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] ^ pTruth1[i];
+    else if ( !Aig_ObjFaninC0(pNode) && !Aig_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & pTruth1[i];
+    else if ( !Aig_ObjFaninC0(pNode) && Aig_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & ~pTruth1[i];
+    else if ( Aig_ObjFaninC0(pNode) && !Aig_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & pTruth1[i];
+    else // if ( Aig_ObjFaninC0(pNode) && Aig_ObjFaninC1(pNode) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description [The returned pointer should be used immediately.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vTruthElem, Vec_Ptr_t * vTruthStore )
+{
+    Aig_Obj_t * pObj;
+    int i, nWords;
+    assert( Vec_PtrSize(vLeaves) <= Vec_PtrSize(vTruthElem) );
+    assert( Vec_PtrSize(vNodes) <= Vec_PtrSize(vTruthStore) );
+    assert( Vec_PtrSize(vNodes) == 0 || pRoot == Vec_PtrEntryLast(vNodes) );  
+    // assign elementary truth tables
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->pData = Vec_PtrEntry( vTruthElem, i );
+    // compute truths for other nodes
+    nWords = Aig_TruthWordNum( Vec_PtrSize(vLeaves) );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pData = Aig_ManCutTruthOne( pObj, Vec_PtrEntry(vTruthStore, i), nWords );
+    return pRoot->pData;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/aig/aigUtil.c

@@ -104,6 +104,25 @@ int Aig_ManLevels( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Checks if the markA is reset.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCheckMarkA( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        assert( pObj->fMarkA == 0 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Cleans the data pointers for the nodes.]
 
   Description []
@@ -144,6 +163,7 @@ void Aig_ObjCleanData_rec( Aig_Obj_t * pObj )
     pObj->pData = NULL;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Detects multi-input gate rooted at this node.]

src/aig/aig/aigWin.c

+/**CFile****************************************************************
+
+  FileName    [aigWin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Window computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigWin.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the cost of removing the node from the set of leaves.]
+
+  Description [Returns the number of new leaves that will be brought in.
+  Returns large number if the node cannot be removed from the set of leaves.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_NodeGetLeafCostOne( Aig_Obj_t * pNode, int nFanoutLimit )
+{
+    int Cost;
+    // make sure the node is in the construction zone
+    assert( pNode->fMarkA );  
+    // cannot expand over the PI node
+    if ( Aig_ObjIsPi(pNode) )
+        return 999;
+    // get the cost of the cone
+    Cost = (!Aig_ObjFanin0(pNode)->fMarkA) + (!Aig_ObjFanin1(pNode)->fMarkA);
+    // always accept if the number of leaves does not increase
+    if ( Cost < 2 )
+        return Cost;
+    // skip nodes with many fanouts
+    if ( (int)pNode->nRefs > nFanoutLimit )
+        return 999;
+    // return the number of nodes that will be on the leaves if this node is removed
+    return Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds reconvergence-driven cut by changing one leaf at a time.]
+
+  Description [This procedure looks at the current leaves and tries to change 
+  one leaf at a time in such a way that the cut grows as little as possible.
+  In evaluating the fanins, this procedure looks only at their immediate 
+  predecessors (this is why it is called a one-level construction procedure).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManFindCut_int( Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit )
+{
+    Aig_Obj_t * pNode, * pFaninBest, * pNext;
+    int CostBest, CostCur, i;
+    // find the best fanin
+    CostBest   = 100;
+    pFaninBest = NULL;
+//printf( "Evaluating fanins of the cut:\n" );
+    Vec_PtrForEachEntry( vFront, pNode, i )
+    {
+        CostCur = Aig_NodeGetLeafCostOne( pNode, nFanoutLimit );
+//printf( "    Fanin %s has cost %d.\n", Aig_ObjName(pNode), CostCur );
+        if ( CostBest > CostCur ||
+            (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
+        {
+            CostBest   = CostCur;
+            pFaninBest = pNode;
+        }
+        if ( CostBest == 0 )
+            break;
+    }
+    if ( pFaninBest == NULL )
+        return 0;
+    assert( CostBest < 3 );
+    if ( Vec_PtrSize(vFront) - 1 + CostBest > nSizeLimit )
+        return 0;
+    assert( Aig_ObjIsNode(pFaninBest) );
+    // remove the node from the array
+    Vec_PtrRemove( vFront, pFaninBest );
+//printf( "Removing fanin %s.\n", Aig_ObjName(pFaninBest) );
+
+    // add the left child to the fanins
+    pNext = Aig_ObjFanin0(pFaninBest);
+    if ( !pNext->fMarkA )
+    {
+//printf( "Adding fanin %s.\n", Aig_ObjName(pNext) );
+        pNext->fMarkA = 1;
+        Vec_PtrPush( vFront, pNext );
+        Vec_PtrPush( vVisited, pNext );
+    }
+    // add the right child to the fanins
+    pNext = Aig_ObjFanin1(pFaninBest);
+    if ( !pNext->fMarkA )
+    {
+//printf( "Adding fanin %s.\n", Aig_ObjName(pNext) );
+        pNext->fMarkA = 1;
+        Vec_PtrPush( vFront, pNext );
+        Vec_PtrPush( vVisited, pNext );
+    }
+    assert( Vec_PtrSize(vFront) <= nSizeLimit );
+    // keep doing this
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes one sequential cut of the given size.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit )
+{
+    Aig_Obj_t * pNode;
+    int i;
+
+    assert( !Aig_IsComplement(pRoot) );
+    assert( Aig_ObjIsNode(pRoot) );
+    assert( Aig_ObjChild0(pRoot) );
+    assert( Aig_ObjChild1(pRoot) );
+
+    // start the cut 
+    Vec_PtrClear( vFront );
+    Vec_PtrPush( vFront, Aig_ObjFanin0(pRoot) );
+    Vec_PtrPush( vFront, Aig_ObjFanin1(pRoot) );
+
+    // start the visited nodes
+    Vec_PtrClear( vVisited );
+    Vec_PtrPush( vVisited, pRoot );
+    Vec_PtrPush( vVisited, Aig_ObjFanin0(pRoot) );
+    Vec_PtrPush( vVisited, Aig_ObjFanin1(pRoot) );
+
+    // mark these nodes
+    assert( !pRoot->fMarkA );
+    assert( !Aig_ObjFanin0(pRoot)->fMarkA );
+    assert( !Aig_ObjFanin1(pRoot)->fMarkA );
+    pRoot->fMarkA = 1;
+    Aig_ObjFanin0(pRoot)->fMarkA = 1;
+    Aig_ObjFanin1(pRoot)->fMarkA = 1;
+
+    // compute the cut
+    while ( Aig_ManFindCut_int( vFront, vVisited, nSizeLimit, nFanoutLimit ) );
+    assert( Vec_PtrSize(vFront) <= nSizeLimit );
+
+    // clean the visit markings
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        pNode->fMarkA = 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/aig/aig/module.make

@@ -2,10 +2,13 @@ SRC +=    src/aig/aig/aigCheck.c \
     src/aig/aig/aigDfs.c \
     src/aig/aig/aigFanout.c \
     src/aig/aig/aigMan.c \
+    src/aig/aig/aigMffc.c \
     src/aig/aig/aigMem.c \
     src/aig/aig/aigObj.c \
     src/aig/aig/aigOper.c \
     src/aig/aig/aigSeq.c \
     src/aig/aig/aigTable.c \
     src/aig/aig/aigTiming.c \
-    src/aig/aig/aigUtil.c 
+    src/aig/aig/aigTruth.c \
+    src/aig/aig/aigUtil.c \ 
+    src/aig/aig/aigWin.c 

src/aig/dar/dar.h

@@ -37,10 +37,10 @@ extern "C" {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Dar_Par_t_            Dar_Par_t;
+typedef struct Dar_RwrPar_t_            Dar_RwrPar_t;
+typedef struct Dar_RefPar_t_            Dar_RefPar_t;
 
-// the rewriting parameters
-struct Dar_Par_t_  
+struct Dar_RwrPar_t_  
 {
     int              nCutsMax;       // the maximum number of cuts to try
     int              nSubgMax;       // the maximum number of subgraphs to try
@@ -50,6 +50,18 @@ struct Dar_Par_t_
     int              fVeryVerbose;   // enables very verbose output
 };
 
+struct Dar_RefPar_t_  
+{
+    int              nMffcMin;       // the min MFFC size for which refactoring is used
+    int              nLeafMax;       // the max number of leaves of a cut
+    int              nCutsMax;       // the max number of cuts to consider  
+    int              fExtend;        // extends the cut below MFFC
+    int              fUpdateLevel;   // updates the level after each move
+    int              fUseZeros;      // perform zero-cost replacements
+    int              fVerbose;       // verbosity level
+    int              fVeryVerbose;   // enables very verbose output
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -62,10 +74,17 @@ struct Dar_Par_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== darBalance.c ========================================================*/
+extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
 /*=== darCore.c ========================================================*/
-extern void            Dar_ManDefaultParams( Dar_Par_t * pPars );
-extern int             Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars );
+extern void            Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
+extern int             Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
 extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig );
+/*=== darRefact.c ========================================================*/
+extern void            Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
+extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
+/*=== darScript.c ========================================================*/
+extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose );
 
 #ifdef __cplusplus
 }

src/aig/dar/darCore.c

@@ -39,9 +39,9 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Dar_ManDefaultParams( Dar_Par_t * pPars )
+void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
 {
-    memset( pPars, 0, sizeof(Dar_Par_t) );
+    memset( pPars, 0, sizeof(Dar_RwrPar_t) );
     pPars->nCutsMax     =  8;
     pPars->nSubgMax     =  5; // 5 is a "magic number"
     pPars->fUpdateLevel =  0;
@@ -61,7 +61,7 @@ void Dar_ManDefaultParams( Dar_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-int Dar_ManRewrite( Aig_Man_t * pAig, Dar_Par_t * pPars )
+int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
 {
     Dar_Man_t * p;
     ProgressBar * pProgress;
@@ -128,7 +128,7 @@ p->timeCuts += clock() - clk;
 
         // evaluate the cuts
         p->GainBest = -1;
-        Required = 1000000;
+        Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
         Dar_ObjForEachCut( pObj, pCut, k )
             Dar_LibEval( p, pObj, pCut, Required );
         // check the best gain

src/aig/dar/darInt.h

@@ -64,8 +64,8 @@ struct Dar_Cut_t_  // 6 words
 // the AIG manager
 struct Dar_Man_t_
 {
-    // input data;
-    Dar_Par_t *      pPars;          // rewriting parameters
+    // input data
+    Dar_RwrPar_t *   pPars;          // rewriting parameters
     Aig_Man_t *      pAig;           // AIG manager 
     // various data members
     Aig_MmFixed_t *  pMemCuts;       // memory manager for cuts
@@ -125,7 +125,6 @@ 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 void            Dar_ManCutsStart( Dar_Man_t * p );
@@ -144,7 +143,7 @@ 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 ============================================================*/
-extern Dar_Man_t *     Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars );
+extern Dar_Man_t *     Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
 extern void            Dar_ManStop( Dar_Man_t * p );
 extern void            Dar_ManPrintStats( Dar_Man_t * p );
 

src/aig/dar/darLib.c

@@ -707,65 +707,6 @@ int Dar_LibCutMatch( Dar_Man_t * p, Dar_Cut_t * pCut )
 
 /**Function*************************************************************
 
-  Synopsis    [Dereferences the node's MFFC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeDeref_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
-{
-    Aig_Obj_t * pFanin;
-    int Counter = 0;
-    if ( Aig_ObjIsPi(pNode) )
-        return Counter;
-    pFanin = Aig_ObjFanin0( pNode );
-    assert( pFanin->nRefs > 0 );
-    if ( --pFanin->nRefs == 0 )
-        Counter += Aig_NodeDeref_rec( p, pFanin );
-    if ( Aig_ObjIsBuf(pNode) )
-        return Counter;
-    pFanin = Aig_ObjFanin1( pNode );
-    assert( pFanin->nRefs > 0 );
-    if ( --pFanin->nRefs == 0 )
-        Counter += Aig_NodeDeref_rec( p, pFanin );
-    return 1 + Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [References the node's MFFC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
-{
-    Aig_Obj_t * pFanin;
-    int Counter = 0;
-    if ( Aig_ObjIsPi(pNode) )
-        return Counter;
-    Aig_ObjSetTravIdCurrent( p, pNode );
-    pFanin = Aig_ObjFanin0( pNode );
-    if ( pFanin->nRefs++ == 0 )
-        Counter += Aig_NodeRef_rec( p, pFanin );
-    if ( Aig_ObjIsBuf(pNode) )
-        return Counter;
-    pFanin = Aig_ObjFanin1( pNode );
-    if ( pFanin->nRefs++ == 0 )
-        Counter += Aig_NodeRef_rec( p, pFanin );
-    return 1 + Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Marks the MFFC of the node.]
 
   Description []
@@ -777,19 +718,16 @@ int Aig_NodeRef_rec( Aig_Man_t * p, Aig_Obj_t * pNode )
 ***********************************************************************/
 int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves )
 {
-    int i, nNodes1, nNodes2;
+    int i, nNodes;
     // mark the cut leaves
     for ( i = 0; i < nLeaves; i++ )
         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++;
     // label MFFC with current ID
-    Aig_ManIncrementTravId( p );
-    nNodes1 = Aig_NodeDeref_rec( p, pRoot );
-    nNodes2 = Aig_NodeRef_rec( p, pRoot );
-    assert( nNodes1 == nNodes2 );
+    nNodes = Aig_NodeMffsLabel( p, pRoot );
     // unmark the cut leaves
     for ( i = 0; i < nLeaves; i++ )
         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--;
-    return nNodes1;
+    return nNodes;
 }
 
 /**Function*************************************************************
@@ -836,7 +774,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
 {
     Dar_LibObj_t * pObj;
     Dar_LibDat_t * pData, * pData0, * pData1;
-    Aig_Obj_t * pGhost, * pFanin0, * pFanin1;
+    Aig_Obj_t * pFanin0, * pFanin1;
     int i;
     for ( i = 0; i < s_DarLib->nNodes0[Class]; i++ )
     {
@@ -859,22 +797,7 @@ void Dar_LibEvalAssignNums( Dar_Man_t * p, int Class )
             continue;
         pFanin0 = Aig_NotCond( pData0->pFunc, pObj->fCompl0 );
         pFanin1 = Aig_NotCond( pData1->pFunc, pObj->fCompl1 );
-
-        // consider simple cases
-        if ( pFanin0 == pFanin1 )
-            pData->pFunc = pFanin0;
-        else if ( pFanin0 == Aig_Not(pFanin1) )
-            pData->pFunc = Aig_ManConst0(p->pAig);
-        else if ( Aig_Regular(pFanin0) == Aig_ManConst1(p->pAig) )
-            pData->pFunc = pFanin0 == Aig_ManConst1(p->pAig) ? pFanin1 : Aig_ManConst0(p->pAig);
-        else if ( Aig_Regular(pFanin1) == Aig_ManConst1(p->pAig) )
-            pData->pFunc = pFanin1 == Aig_ManConst1(p->pAig) ? pFanin0 : Aig_ManConst0(p->pAig);
-        else
-        {
-            pGhost = Aig_ObjCreateGhost( p->pAig, pFanin0, pFanin1, AIG_OBJ_AND );
-            pData->pFunc = Aig_TableLookup( p->pAig, pGhost );
-        }
-
+        pData->pFunc = Aig_TableLookupTwo( p->pAig, pFanin0, pFanin1 );
         // clear the node if it is part of MFFC
         if ( pData->pFunc != NULL && Aig_ObjIsTravIdCurrent(p->pAig, pData->pFunc) )
             pData->fMffc = 1;

src/aig/dar/darMan.c

@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_Par_t * pPars )
+Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
 {
     Dar_Man_t * p;
     // start the manager

src/aig/dar/darRefact.c

@@ -19,17 +19,151 @@
 ***********************************************************************/
 
 #include "darInt.h"
+#include "kit.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// the refactoring manager
+typedef struct Ref_Man_t_            Ref_Man_t;
+struct Ref_Man_t_
+{
+    // input data
+    Dar_RefPar_t *   pPars;          // rewriting parameters
+    Aig_Man_t *      pAig;           // AIG manager 
+    // computed cuts
+    Vec_Vec_t *      vCuts;          // the storage for cuts
+    // truth table and ISOP
+    Vec_Ptr_t *      vTruthElem;     // elementary truth tables
+    Vec_Ptr_t *      vTruthStore;    // storage for truth tables
+    Vec_Int_t *      vMemory;        // storage for ISOP
+    Vec_Ptr_t *      vCutNodes;      // storage for internal nodes of the cut
+    // various data members
+    Vec_Ptr_t *      vLeavesBest;    // the best set of leaves
+    Kit_Graph_t *    pGraphBest;     // the best factored form
+    int              GainBest;       // the best gain
+    int              LevelBest;      // the level of node with the best gain
+    // node statistics
+    int              nNodesInit;     // the initial number of nodes
+    int              nNodesTried;    // the number of nodes tried
+    int              nNodesBelow;    // the number of nodes below the level limit
+    int              nNodesExten;    // the number of nodes with extended cut
+    int              nCutsUsed;      // the number of rewriting steps
+    int              nCutsTried;     // the number of cuts tries
+    // timing statistics
+    int              timeCuts;
+    int              timeEval;
+    int              timeOther;
+    int              timeTotal;
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the structure with default assignment of parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars )
+{
+    memset( pPars, 0, sizeof(Dar_RefPar_t) );
+    pPars->nMffcMin     =  2;  // the min MFFC size for which refactoring is used
+    pPars->nLeafMax     = 12;  // the max number of leaves of a cut
+    pPars->nCutsMax     =  5;  // the max number of cuts to consider  
+    pPars->fUpdateLevel =  0;
+    pPars->fUseZeros    =  0;
+    pPars->fVerbose     =  0;
+    pPars->fVeryVerbose =  0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the rewriting manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
+{
+    Ref_Man_t * p;
+    // start the manager
+    p = ALLOC( Ref_Man_t, 1 );
+    memset( p, 0, sizeof(Ref_Man_t) );
+    p->pAig         = pAig;
+    p->pPars        = pPars;
+    // other data
+    p->vCuts        = Vec_VecStart( pPars->nCutsMax );
+    p->vTruthElem   = Vec_PtrAllocTruthTables( pPars->nLeafMax );
+    p->vTruthStore  = Vec_PtrAllocSimInfo( 256, Kit_TruthWordNum(pPars->nLeafMax) );
+    p->vMemory      = Vec_IntAlloc( 1 << 16 );
+    p->vCutNodes    = Vec_PtrAlloc( 256 );
+    p->vLeavesBest  = Vec_PtrAlloc( pPars->nLeafMax );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints out the statistics of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManRefPrintStats( Ref_Man_t * p )
+{
+    int Gain = p->nNodesInit - Aig_ManNodeNum(p->pAig);
+    printf( "NodesBeg = %8d. NodesEnd = %8d. Gain = %6d. (%6.2f %%).\n", 
+        p->nNodesInit, Aig_ManNodeNum(p->pAig), Gain, 100.0*Gain/p->nNodesInit );
+    printf( "Tried = %6d. Below = %5d. Extended = %5d.  Used = %5d.\n", 
+        p->nNodesTried, p->nNodesBelow, p->nNodesExten, p->nCutsUsed );
+    PRT( "Cuts  ", p->timeCuts );
+    PRT( "Eval  ", p->timeEval );
+    PRT( "Other ", p->timeOther );
+    PRT( "TOTAL ", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the rewriting manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ManRefStop( Ref_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+        Dar_ManRefPrintStats( p );
+    Vec_VecFree( p->vCuts );
+    Vec_PtrFree( p->vTruthElem );
+    Vec_PtrFree( p->vTruthStore );
+    Vec_PtrFree( p->vLeavesBest );
+    Vec_IntFree( p->vMemory );
+    Vec_PtrFree( p->vCutNodes );
+    free( p );
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -39,7 +173,405 @@
   SeeAlso     []
 
 ***********************************************************************/
+void Ref_ObjComputeCuts( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Vec_t * vCuts )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ref_ObjPrint( Aig_Obj_t * pObj )
+{
+    printf( "%d", pObj? Aig_Regular(pObj)->Id : -1 );
+    if ( pObj )
+        printf( "(%d) ", Aig_IsComplement(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of new nodes added when using this graph.]
+
+  Description [AIG nodes for the fanins should be assigned to pNode->pFunc 
+  of the leaves of the graph before calling this procedure. 
+  Returns -1 if the number of nodes and levels exceeded the given limit or 
+  the number of levels exceeded the maximum allowed level.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_RefactTryGraph( Aig_Man_t * pAig, Aig_Obj_t * pRoot, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph, int NodeMax, int LevelMax )
+{
+    Kit_Node_t * pNode, * pNode0, * pNode1;
+    Aig_Obj_t * pAnd, * pAnd0, * pAnd1;
+    int i, Counter, LevelNew, LevelOld;
+    // check for constant function or a literal
+    if ( Kit_GraphIsConst(pGraph) || Kit_GraphIsVar(pGraph) )
+        return 0;
+    // set the levels of the leaves
+    Kit_GraphForEachLeaf( pGraph, pNode, i )
+    {
+        pNode->pFunc = Vec_PtrEntry(vCut, i);
+        pNode->Level = Aig_Regular(pNode->pFunc)->Level;
+        assert( Aig_Regular(pNode->pFunc)->Level < (1<<14)-1 );
+    }
+//printf( "Trying:\n" );
+    // compute the AIG size after adding the internal nodes
+    Counter = 0;
+    Kit_GraphForEachNode( pGraph, pNode, i )
+    {
+        // get the children of this node
+        pNode0 = Kit_GraphNode( pGraph, pNode->eEdge0.Node );
+        pNode1 = Kit_GraphNode( pGraph, pNode->eEdge1.Node );
+        // get the AIG nodes corresponding to the children 
+        pAnd0 = pNode0->pFunc; 
+        pAnd1 = pNode1->pFunc; 
+        if ( pAnd0 && pAnd1 )
+        {
+            // if they are both present, find the resulting node
+            pAnd0 = Aig_NotCond( pAnd0, pNode->eEdge0.fCompl );
+            pAnd1 = Aig_NotCond( pAnd1, pNode->eEdge1.fCompl );
+            pAnd  = Aig_TableLookupTwo( pAig, pAnd0, pAnd1 );
+            // return -1 if the node is the same as the original root
+            if ( Aig_Regular(pAnd) == pRoot )
+                return -1;
+        }
+        else
+            pAnd = NULL;
+        // count the number of added nodes
+        if ( pAnd == NULL || Aig_ObjIsTravIdCurrent(pAig, Aig_Regular(pAnd)) )
+        {
+            if ( ++Counter > NodeMax )
+                return -1;
+        }
+        // count the number of new levels
+        LevelNew = 1 + AIG_MAX( pNode0->Level, pNode1->Level );
+        if ( pAnd )
+        {
+            if ( Aig_Regular(pAnd) == Aig_ManConst1(pAig) )
+                LevelNew = 0;
+            else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd0) )
+                LevelNew = (int)Aig_Regular(pAnd0)->Level;
+            else if ( Aig_Regular(pAnd) == Aig_Regular(pAnd1) )
+                LevelNew = (int)Aig_Regular(pAnd1)->Level;
+            LevelOld = (int)Aig_Regular(pAnd)->Level;
+//            assert( LevelNew == LevelOld );
+        }
+        if ( LevelNew > LevelMax )
+            return -1;
+        pNode->pFunc = pAnd;
+        pNode->Level = LevelNew;
+/*
+printf( "Checking " );
+Ref_ObjPrint( pAnd0 );
+printf( " and " );
+Ref_ObjPrint( pAnd1 );
+printf( "  Result " );
+Ref_ObjPrint( pNode->pFunc );
+printf( "\n" );
+*/
+    }
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_t * pGraph )
+{
+    Aig_Obj_t * pAnd0, * pAnd1;
+    Kit_Node_t * pNode;
+    int i;
+    // check for constant function
+    if ( Kit_GraphIsConst(pGraph) )
+        return Aig_NotCond( Aig_ManConst1(pAig), Kit_GraphIsComplement(pGraph) );
+    // set the leaves
+    Kit_GraphForEachLeaf( pGraph, pNode, i )
+        pNode->pFunc = Vec_PtrEntry(vCut, i);
+    // check for a literal
+    if ( Kit_GraphIsVar(pGraph) )
+        return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) );
+    // build the AIG nodes corresponding to the AND gates of the graph
+//printf( "Building (current number %d):\n", Aig_ManObjIdMax(pAig) );
+    Kit_GraphForEachNode( pGraph, pNode, i )
+    {
+        pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
+        pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
+        pNode->pFunc = Aig_And( pAig, pAnd0, pAnd1 );
+/*
+printf( "Checking " );
+Ref_ObjPrint( pAnd0 );
+printf( " and " );
+Ref_ObjPrint( pAnd1 );
+printf( "  Result " );
+Ref_ObjPrint( pNode->pFunc );
+printf( "\n" );
+*/
+    }
+    // complement the result if necessary
+    return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, int Required )
+{
+    Vec_Ptr_t * vCut;
+    Kit_Graph_t * pGraphCur;
+    int k, RetValue, GainCur, nNodesAdded;
+    unsigned * pTruth;
+
+    p->GainBest = -1;
+    p->pGraphBest = NULL;
+    Vec_VecForEachLevel( p->vCuts, vCut, k )
+    {
+        if ( Vec_PtrSize(vCut) == 0 )
+            continue;
+//        if ( Vec_PtrSize(vCut) != 0 && Vec_PtrSize(Vec_VecEntry(p->vCuts, k+1)) != 0 )
+//            continue;
+
+        p->nCutsTried++;
+        // get the cut nodes
+        Aig_ManCollectCut( pObj, vCut, p->vCutNodes );
+        // get the truth table
+        pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
+        // try the positive phase
+        RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
+        if ( RetValue > -1 )
+        {
+            pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
+            nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
+            if ( nNodesAdded > -1 )
+            {
+                GainCur = nNodesSaved - nNodesAdded;
+                if ( p->GainBest < GainCur || (p->GainBest == GainCur && 
+                    (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
+                {
+                    p->GainBest = GainCur;
+                    if ( p->pGraphBest )
+                        Kit_GraphFree( p->pGraphBest );
+                    p->pGraphBest = pGraphCur;
+                    Vec_PtrCopy( p->vLeavesBest, vCut );
+                }
+                else
+                    Kit_GraphFree( pGraphCur );
+            }
+            else
+                Kit_GraphFree( pGraphCur );
+        }
+        // try negative phase
+        Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
+        RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
+        if ( RetValue > -1 )
+        {
+            pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
+            nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
+            if ( nNodesAdded > -1 )
+            {
+                GainCur = nNodesSaved - nNodesAdded;
+                if ( p->GainBest < GainCur || (p->GainBest == GainCur && 
+                    (Kit_GraphIsConst(pGraphCur) || Kit_GraphRootLevel(pGraphCur) < Kit_GraphRootLevel(p->pGraphBest))) )
+                {
+                    p->GainBest = GainCur;
+                    if ( p->pGraphBest )
+                        Kit_GraphFree( p->pGraphBest );
+                    p->pGraphBest = pGraphCur;
+                    Vec_PtrCopy( p->vLeavesBest, vCut );
+                }
+                else
+                    Kit_GraphFree( pGraphCur );
+            }
+            else
+                Kit_GraphFree( pGraphCur );
+        }
+    }
+    return p->GainBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if a non-PI node has nLevelMin or below.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( vCut, pObj, i )
+        if ( !Aig_ObjIsPi(pObj) && (int)pObj->Level <= nLevelMin )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
+{
+    ProgressBar * pProgress;
+    Ref_Man_t * p;
+    Vec_Ptr_t * vCut, * vCut2;
+    Aig_Obj_t * pObj, * pObjNew;
+    int nNodesOld, nNodeBefore, nNodeAfter, nNodesSaved, nNodesSaved2;
+    int i, Required, nLevelMin, clkStart, clk;
+
+    // start the manager
+    p = Dar_ManRefStart( 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 );
+
+    // resynthesize each node once
+    clkStart = clock();
+    vCut = Vec_VecEntry( p->vCuts, 0 );
+    vCut2 = Vec_VecEntry( p->vCuts, 1 );
+    p->nNodesInit = Aig_ManNodeNum(pAig);
+    nNodesOld = Vec_PtrSize( pAig->vObjs );
+    pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( !Aig_ObjIsNode(pObj) )
+            continue;
+        if ( i > nNodesOld )
+            break;
+        Vec_VecClear( p->vCuts );
+
+        if ( pObj->Id == 738 )
+        {
+            int x = 0;
+        }
+
+//printf( "\nConsidering node %d.\n", pObj->Id );
+        // get the bounded MFFC size
+clk = clock();
+        nLevelMin = AIG_MAX( 0, Aig_ObjLevel(pObj) - 10 );
+        nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
+        if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
+        {
+p->timeCuts += clock() - clk;
+            continue; 
+        }
+        p->nNodesTried++;
+        if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut
+        {
+            Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 );
+            nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+        }
+        else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
+        {
+            if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
+            {
+                if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) )
+                {
+                    nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+                    assert( nNodesSaved2 == nNodesSaved );
+                }
+                if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax )
+                    Vec_PtrClear(vCut2);
+                if ( Vec_PtrSize(vCut2) > 0 )
+                {
+                    p->nNodesExten++;
+//                    printf( "%d(%d) ", Vec_PtrSize(vCut), Vec_PtrSize(vCut2) );
+                }
+            }
+            else
+                p->nNodesBelow++;
+        }
+p->timeCuts += clock() - clk;
+
+        // try the cuts
+clk = clock();
+        Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : AIG_INFINITY;
+        Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
+p->timeEval += clock() - clk;
+
+        // check the best gain
+        if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
+        {
+            if ( p->pGraphBest )
+                Kit_GraphFree( p->pGraphBest );
+            continue;
+        }
+//printf( "\n" );
+
+        // if we end up here, a rewriting step is accepted
+        nNodeBefore = Aig_ManNodeNum( pAig );
+        pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
+        assert( (int)Aig_Regular(pObjNew)->Level <= Required );
+        // replace the node
+        Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
+        // compare the gains
+        nNodeAfter = Aig_ManNodeNum( pAig );
+        assert( p->GainBest <= nNodeBefore - nNodeAfter );
+        Kit_GraphFree( p->pGraphBest );
+        p->nCutsUsed++;
+//        break;
+    }
+p->timeTotal = clock() - clkStart;
+p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
+
+    Extra_ProgressBarStop( pProgress );
+    // put the nodes into the DFS order and reassign their IDs
+//    Aig_NtkReassignIds( p );
+    // fix the levels
+    Aig_ManDeleteFanout( pAig );
+    if ( p->pPars->fUpdateLevel )
+        Aig_ManStopReverseLevels( pAig );
+
+    // stop the rewriting manager
+    Dar_ManRefStop( p );
+    if ( !Aig_ManCheck( pAig ) )
+    {
+        printf( "Dar_ManRefactor: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
 
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/aig/dar/darScript.c

@@ -30,15 +30,215 @@
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Reproduces script "compress2".]
 
   Description []
                
-  SideEffects []
+  SideEffects [This procedure does not tighten level during restructuring.]
 
   SeeAlso     []
 
 ***********************************************************************/
+Aig_Man_t * Dar_ManCompress2_old( Aig_Man_t * pAig, int fVerbose )
+//alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+{
+    Aig_Man_t * pTemp;
+    int fBalance = 0;
+
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+    Dar_ManDefaultRwrParams( pParsRwr );
+    Dar_ManDefaultRefParams( pParsRef );
+
+    pParsRwr->fVerbose = fVerbose;
+    pParsRef->fVerbose = fVerbose;
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    pParsRwr->fUseZeros = 1;
+    pParsRef->fUseZeros = 1;
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2".]
+
+  Description []
+               
+  SideEffects [This procedure does not tighten level during restructuring.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManCompress2_no_z( Aig_Man_t * pAig, int fVerbose )
+//alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+{
+    Aig_Man_t * pTemp;
+    int fBalance = 0;
+
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+    Dar_ManDefaultRwrParams( pParsRwr );
+    Dar_ManDefaultRefParams( pParsRef );
+
+    pParsRwr->fVerbose = fVerbose;
+    pParsRef->fVerbose = fVerbose;
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2".]
+
+  Description []
+               
+  SideEffects [This procedure does not tighten level during restructuring.]
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fVerbose )
+//alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+{
+    Aig_Man_t * pTemp;
+    int fBalance = 0;
+
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+    Dar_ManDefaultRwrParams( pParsRwr );
+    Dar_ManDefaultRefParams( pParsRef );
+
+    pParsRwr->fVerbose = fVerbose;
+    pParsRef->fVerbose = fVerbose;
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+/*
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+*/    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    pParsRwr->fUseZeros = 1;
+    pParsRef->fUseZeros = 1;
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fBalance );
+    Aig_ManStop( pTemp );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    return pAig;
+}
 
 
 ////////////////////////////////////////////////////////////////////////

src/aig/kit/kit.h

@@ -217,6 +217,7 @@ static inline Kit_Node_t * Kit_GraphVar( Kit_Graph_t * pGraph )
 static inline int          Kit_GraphVarInt( Kit_Graph_t * pGraph )                        { assert( Kit_GraphIsVar( pGraph ) );    return Kit_GraphNodeInt( pGraph, Kit_GraphVar(pGraph) ); }
 static inline Kit_Node_t * Kit_GraphNodeFanin0( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge0.Node);     }
 static inline Kit_Node_t * Kit_GraphNodeFanin1( Kit_Graph_t * pGraph, Kit_Node_t * pNode ){ return Kit_GraphNodeIsVar(pGraph, pNode)? NULL : Kit_GraphNode(pGraph, pNode->eEdge1.Node);     }
+static inline int          Kit_GraphRootLevel( Kit_Graph_t * pGraph )                     { return Kit_GraphNode(pGraph, pGraph->eRoot.Node)->Level;                                        }
 
 static inline int          Kit_Float2Int( float Val )     { return *((int *)&Val);               }
 static inline float        Kit_Int2Float( int Num )       { return *((float *)&Num);             }

src/base/abci/abc.c

@@ -111,6 +111,8 @@ static int Abc_CommandIStrash        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandICut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDRefactor      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDCompress2     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandISat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -269,6 +271,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "icut",          Abc_CommandICut,             0 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "drw",           Abc_CommandDRewrite,         1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "drf",           Abc_CommandDRefactor,        1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "dcompress2",    Abc_CommandDCompress2,       1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "isat",          Abc_CommandISat,             1 );
@@ -6619,17 +6623,17 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    Dar_Par_t Pars, * pPars = &Pars;
+    Dar_RwrPar_t Pars, * pPars = &Pars;
     int c;
 
-    extern Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars );
+    extern Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    Dar_ManDefaultParams( pPars );
+    Dar_ManDefaultRwrParams( pPars );
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "CNlzvwh" ) ) != EOF )
     {
@@ -6692,9 +6696,129 @@ int Abc_CommandDRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: drw [-C num] [-N num] [-lzvwh]\n" );
-    fprintf( pErr, "\t         perform combinational AIG rewriting\n" );
-    fprintf( pErr, "\t-C num : limit on the number of cuts at a node [default = %d]\n", pPars->nCutsMax );
-    fprintf( pErr, "\t-N num : limit on the number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
+    fprintf( pErr, "\t         performs combinational AIG rewriting\n" );
+    fprintf( pErr, "\t-C num : the max number of cuts at a node [default = %d]\n", pPars->nCutsMax );
+    fprintf( pErr, "\t-N num : the max number of subgraphs tried [default = %d]\n", pPars->nSubgMax );
+    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
+    fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggle very verbose printout [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    Dar_RefPar_t Pars, * pPars = &Pars;
+    int c;
+
+    extern Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Dar_ManDefaultRefParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MKCelzvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nMffcMin = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nMffcMin < 0 ) 
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLeafMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLeafMax < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCutsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCutsMax < 0 ) 
+                goto usage;
+            break;
+        case 'e':
+            pPars->fExtend ^= 1;
+            break;
+        case 'l':
+            pPars->fUpdateLevel ^= 1;
+            break;
+        case 'z':
+            pPars->fUseZeros ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( pPars->nLeafMax < 4 || pPars->nLeafMax > 15 )
+    {
+        fprintf( pErr, "This command only works for cut sizes 4 <= K <= 15.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDRefactor( pNtk, pPars );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: drf [-M num] [-K num] [-C num] [-elzvwh]\n" );
+    fprintf( pErr, "\t         performs combinational AIG refactoring\n" );
+    fprintf( pErr, "\t-M num : the min MFFC size to attempt refactoring [default = %d]\n", pPars->nMffcMin );
+    fprintf( pErr, "\t-K num : the max number of cuts leaves [default = %d]\n", pPars->nLeafMax );
+    fprintf( pErr, "\t-C num : the max number of cuts to try at a node [default = %d]\n", pPars->nCutsMax );
+    fprintf( pErr, "\t-e     : toggle extending tbe cut below MFFC [default = %s]\n", pPars->fExtend? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", pPars->fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-z     : toggle using zero-cost replacements [default = %s]\n", pPars->fUseZeros? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
@@ -6714,6 +6838,68 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandDCompress2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int fVerbose, c;
+
+    extern Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDCompress2( pNtk, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dcompress2 [-vh]\n" );
+    fprintf( pErr, "\t         performs combinational AIG optimization\n" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;

src/base/abci/abcDar.c

@@ -291,7 +291,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
 */
 
 //    Aig_ManDumpBlif( pMan, "aig_temp.blif" );
-//    pMan->pPars = Dar_ManDefaultParams();
+//    pMan->pPars = Dar_ManDefaultRwrParams();
     Dar_ManRewrite( pMan, NULL );
     Aig_ManPrintStats( pMan );
 //    Dar_ManComputeCuts( pMan );
@@ -519,7 +519,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars )
+Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
@@ -537,7 +537,77 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_Par_t * pPars )
 clk = clock();
     pMan = Aig_ManDup( pTemp = pMan, 0 ); 
     Aig_ManStop( pTemp );
-PRT( "time", clock() - clk );
+//PRT( "time", clock() - clk );
+
+//    Aig_ManPrintStats( pMan );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
+{
+    Aig_Man_t * pMan, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    int clk;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManPrintStats( pMan );
+
+    Dar_ManRefactor( pMan, pPars );
+//    pMan = Dar_ManBalance( pTemp = pMan, pPars->fUpdateLevel );
+//    Aig_ManStop( pTemp );
+
+clk = clock();
+    pMan = Aig_ManDup( pTemp = pMan, 0 ); 
+    Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
+
+//    Aig_ManPrintStats( pMan );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    Aig_Man_t * pMan;//, * pTemp;
+    Abc_Ntk_t * pNtkAig;
+    int clk;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+//    Aig_ManPrintStats( pMan );
+
+clk = clock();
+    pMan = Dar_ManCompress2( pMan, fVerbose ); 
+//    Aig_ManStop( pTemp );
+//PRT( "time", clock() - clk );
 
 //    Aig_ManPrintStats( pMan );
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );

src/base/abci/abcRefactor.c

@@ -43,6 +43,8 @@ struct Abc_ManRef_t_
     int              nNodesConsidered;
     int              nNodesRefactored;
     int              nNodesGained;
+    int              nNodesBeg;
+    int              nNodesEnd;
     // runtime statistics
     int              timeCut;
     int              timeBdd;
@@ -103,6 +105,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
         Abc_NtkStartReverseLevels( pNtk, 0 );
 
     // resynthesize each node once
+    pManRef->nNodesBeg = Abc_NtkNodeNum(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
     Abc_NtkForEachNode( pNtk, pNode, i )
@@ -142,6 +145,7 @@ pManRef->timeNtk += clock() - clk;
     }
     Extra_ProgressBarStop( pProgress );
 pManRef->timeTotal = clock() - clkStart;
+    pManRef->nNodesEnd = Abc_NtkNodeNum(pNtk);
 
     // print statistics of the manager
     if ( fVerbose )
@@ -355,7 +359,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
     printf( "Refactoring statistics:\n" );
     printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
     printf( "Nodes refactored  = %8d.\n", p->nNodesRefactored );
-    printf( "Calculated gain   = %8d.\n", p->nNodesGained     );
+    printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
     PRT( "Cuts       ", p->timeCut );
     PRT( "Resynthesis", p->timeRes );
     PRT( "    BDD    ", p->timeBdd );

src/base/abci/abcResub.c

@@ -86,6 +86,8 @@ struct Abc_ManRes_t_
     int                nTotalDivs;
     int                nTotalLeaves;
     int                nTotalGain;
+    int                nNodesBeg;
+    int                nNodesEnd;
 };
 
 // external procedures
@@ -166,6 +168,7 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLeve
             pNode->pNext = pNode->pData;
 
     // resynthesize each node once
+    pManRes->nNodesBeg = Abc_NtkNodeNum(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
     Abc_NtkForEachNode( pNtk, pNode, i )
@@ -230,6 +233,7 @@ pManRes->timeNtk += clock() - clk;
     }
     Extra_ProgressBarStop( pProgress );
 pManRes->timeTotal = clock() - clkStart;
+    pManRes->nNodesEnd = Abc_NtkNodeNum(pNtk);
 
     // print statistics
     if ( fVerbose )
@@ -385,7 +389,8 @@ void Abc_ManResubPrint( Abc_ManRes_t * p )
                                                    );                          PRT( "TOTAL ", p->timeTotal );
     printf( "Total leaves   = %8d.\n", p->nTotalLeaves );
     printf( "Total divisors = %8d.\n", p->nTotalDivs );
-    printf( "Total gain     = %8d.\n", p->nTotalGain );
+//    printf( "Total gain     = %8d.\n", p->nTotalGain );
+    printf( "Gain           = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
 }
 
 

src/base/abci/abcRewrite.c

@@ -94,6 +94,7 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
         Rwr_ScoresClean( pManRwr );
 
     // resynthesize each node once
+    pManRwr->nNodesBeg = Abc_NtkNodeNum(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
     pProgress = Extra_ProgressBarStart( stdout, nNodes );
     Abc_NtkForEachNode( pNtk, pNode, i )
@@ -137,6 +138,7 @@ Rwr_ManAddTimeUpdate( pManRwr, clock() - clk );
     Extra_ProgressBarStop( pProgress );
 Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
     // print stats
+    pManRwr->nNodesEnd = Abc_NtkNodeNum(pNtk);
     if ( fVerbose )
         Rwr_ManPrintStats( pManRwr );
 //        Rwr_ManPrintStatsFile( pManRwr );

src/misc/vec/vecPtr.h

@@ -562,6 +562,25 @@ static inline void Vec_PtrClear( Vec_Ptr_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Copies the interger array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrCopy( Vec_Ptr_t * pDest, Vec_Ptr_t * pSour )
+{
+    pDest->nSize = 0;
+    Vec_PtrGrow( pDest, pSour->nSize );
+    memcpy( pDest->pArray, pSour->pArray, sizeof(void *) * pSour->nSize );
+    pDest->nSize = pSour->nSize;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []

src/opt/rwr/rwr.h

@@ -77,6 +77,8 @@ struct Rwr_Man_t_
     int                nNodesConsidered;
     int                nNodesRewritten;
     int                nNodesGained;
+    int                nNodesBeg;
+    int                nNodesEnd;
     int                nScores[222];
     int                nCutsGood;
     int                nCutsBad;

src/opt/rwr/rwrMan.c

@@ -150,7 +150,7 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
     printf( "Used NPN classes  = %8d.\n", Counter );
     printf( "Nodes considered  = %8d.\n", p->nNodesConsidered );
     printf( "Nodes rewritten   = %8d.\n", p->nNodesRewritten );
-    printf( "Calculated gain   = %8d.\n", p->nNodesGained     );
+    printf( "Gain              = %8d. (%6.2f %%).\n", p->nNodesBeg-p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg );
     PRT( "Start       ", p->timeStart );
     PRT( "Cuts        ", p->timeCut );
     PRT( "Resynthesis ", p->timeRes );