Modified command 'eliminate' to perform traditional 'eliminate -1'.

src/aig/hop/hop.h

@@ -281,11 +281,13 @@ extern Vec_Ptr_t *     Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode );
 extern int             Hop_ManCountLevels( Hop_Man_t * p );
 extern void            Hop_ManCreateRefs( Hop_Man_t * p );
 extern int             Hop_DagSize( Hop_Obj_t * pObj );
+extern int             Hop_ObjFanoutCount( Hop_Obj_t * pObj, Hop_Obj_t * pPivot );
 extern void            Hop_ConeUnmark_rec( Hop_Obj_t * pObj );
 extern Hop_Obj_t *     Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars );
 extern Hop_Obj_t *     Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar );
 extern Hop_Obj_t *     Hop_Complement( Hop_Man_t * p, Hop_Obj_t * pRoot, int iVar );
 extern Hop_Obj_t *     Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars );
+extern Hop_Obj_t *     Hop_Permute( Hop_Man_t * p, Hop_Obj_t * pRoot, int nRootVars, int * pPermute );
 /*=== hopMan.c ==========================================================*/
 extern Hop_Man_t *     Hop_ManStart();
 extern Hop_Man_t *     Hop_ManDup( Hop_Man_t * p );

src/aig/hop/hopDfs.c

@@ -286,6 +286,38 @@ int Hop_DagSize( Hop_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts how many fanout the given node has.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Hop_ObjFanoutCount_rec( Hop_Obj_t * pObj, Hop_Obj_t * pPivot )
+{
+    int Counter;
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return (int)(pObj == pPivot);
+    Counter = Hop_ObjFanoutCount_rec( Hop_ObjFanin0(pObj), pPivot ) + 
+              Hop_ObjFanoutCount_rec( Hop_ObjFanin1(pObj), pPivot );
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+    return Counter;
+}
+int Hop_ObjFanoutCount( Hop_Obj_t * pObj, Hop_Obj_t * pPivot )
+{
+    int Counter;
+    assert( !Hop_IsComplement(pPivot) );
+    Counter = Hop_ObjFanoutCount_rec( Hop_Regular(pObj), pPivot );
+    Hop_ConeUnmark_rec( Hop_Regular(pObj) );
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers the AIG from one manager into another.]
 
   Description []
@@ -517,6 +549,39 @@ Hop_Obj_t * Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVa
     return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Permute the AIG according to the given permutation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Hop_Permute( Hop_Man_t * p, Hop_Obj_t * pRoot, int nRootVars, int * pPermute )
+{
+    Hop_Obj_t * pObj;
+    int i;
+    // return if constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+        return pRoot;
+    // create mapping
+    Hop_ManForEachPi( p, pObj, i )
+    {
+        if ( i == nRootVars )
+            break;
+        assert( pPermute[i] >= 0 && pPermute[i] < Hop_ManPiNum(p) );
+        pObj->pData = Hop_IthVar( p, pPermute[i] );
+    }
+    // recursively perform composition
+    Hop_Remap_rec( p, Hop_Regular(pRoot) );
+    // clear the markings
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+    return Hop_NotCond( (Hop_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcMinBase.c

@@ -354,9 +354,10 @@ int Abc_NodeCollapsePermMap( Abc_Obj_t * pNode, Abc_Obj_t * pSkip, Vec_Ptr_t * v
 }
 
 
+
 /**Function*************************************************************
 
-  Synopsis    [Computes support of the node.]
+  Synopsis    [Eliminates the nodes into their fanouts if the node size does not exceed this number.]
 
   Description []
                
@@ -400,18 +401,6 @@ DdNode * Abc_NodeCollapseFunc( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_
     Cudd_Deref( bFanout );
     return bFanout;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Collapses one node into its fanout.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_NodeCollapse( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
 {
     Abc_Obj_t * pFanoutNew, * pObj;
@@ -437,10 +426,76 @@ int Abc_NodeCollapse( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFani
     Abc_NtkDeleteObj_rec( pFanout, 1 );
     return 1;
 }
+int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose )
+{
+    extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
+    Vec_Ptr_t * vFanouts, * vFanins, * vNodes;
+    Abc_Obj_t * pNode, * pFanout;
+    int * pPermFanin, * pPermFanout;
+    int RetValue, i, k;
+    assert( nMaxSize > 0 );
+    assert( Abc_NtkIsLogic(pNtk) ); 
+    // convert network to BDD representation
+    if ( !Abc_NtkToBdd(pNtk) )
+    {
+        fprintf( stdout, "Converting to BDD has failed.\n" );
+        return 0;
+    }
+    // prepare nodes for sweeping
+    Abc_NtkRemoveDupFanins( pNtk );
+    Abc_NtkMinimumBase( pNtk );
+    Abc_NtkCleanup( pNtk, 0 );
+    // get the nodes in the given order
+    vNodes = fReverse? Abc_NtkDfsReverse( pNtk ) : Abc_NtkDfs( pNtk, 0 );
+    // go through the nodes and decide is they can be eliminated
+    pPermFanin = ABC_ALLOC( int, nMaxSize + 1000 );
+    pPermFanout = ABC_ALLOC( int, nMaxSize + 1000 );
+    vFanins = Vec_PtrAlloc( 1000 );
+    vFanouts = Vec_PtrAlloc( 1000 );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
+    {
+        if ( !Abc_ObjIsNode(pNode) ) // skip deleted nodes
+            continue;
+        if ( Abc_NodeFindCoFanout(pNode) != NULL )
+            continue;
+        if ( Abc_ObjFaninNum(pNode) > nMaxSize )
+            continue;
+        Abc_ObjForEachFanout( pNode, pFanout, k )
+            if ( Abc_NodeCollapseSuppSize(pNode, pFanout, vFanins) > nMaxSize )
+                break;
+        if ( k < Abc_ObjFanoutNum(pNode) )
+            continue;
+        // perform elimination
+        Abc_NodeCollectFanouts( pNode, vFanouts );
+        Vec_PtrForEachEntry( Abc_Obj_t *, vFanouts, pFanout, k )
+        {
+            if ( fVerbose )
+                printf( "Collapsing fanin %5d (supp =%2d) into fanout %5d (supp =%2d) ",
+                    Abc_ObjId(pNode), Abc_ObjFaninNum(pNode), Abc_ObjId(pFanout), Abc_ObjFaninNum(pFanout) ); 
+            RetValue = Abc_NodeCollapse( pNode, pFanout, vFanins, pPermFanin, pPermFanout );
+            assert( RetValue );
+            if ( fVerbose )
+            {
+                Abc_Obj_t * pNodeNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk) - 1 );
+                if ( pNodeNew )
+                    printf( "resulting in node %5d (supp =%2d).\n", Abc_ObjId(pNodeNew), Abc_ObjFaninNum(pNodeNew) );
+            }
+        }
+    }
+    Abc_NtkBddReorder( pNtk, 0 );
+    Vec_PtrFree( vFanins );
+    Vec_PtrFree( vFanouts );
+    Vec_PtrFree( vNodes );
+    ABC_FREE( pPermFanin );
+    ABC_FREE( pPermFanout );
+    return 1;
+}
+
+
 
 /**Function*************************************************************
 
-  Synopsis    [Eliminates the nodes into their fanouts if the node size does not exceed this number.]
+  Synopsis    [Check how many times fanin appears in the FF of the fanout.]
 
   Description []
                
@@ -449,9 +504,74 @@ int Abc_NodeCollapse( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFani
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose )
+int Abc_NodeCountAppearances( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout )
+{
+    Hop_Man_t * pMan = (Hop_Man_t *)pFanin->pNtk->pManFunc;
+    int iFanin = Abc_NodeFindFanin( pFanout, pFanin );
+    assert( iFanin >= 0 && iFanin < Hop_ManPiNum(pMan) );
+    return Hop_ObjFanoutCount( (Hop_Obj_t *)pFanout->pData, Hop_IthVar(pMan, iFanin) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs traditional eliminate -1.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeCollapseFunc1( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
+{
+    Hop_Man_t * pMan = (Hop_Man_t *)pFanin->pNtk->pManFunc;
+    Hop_Obj_t * bFanin, * bFanout;
+    int RetValue, nSize, iFanin;
+    // can only eliminate if fanin occurs in the fanin list of the fanout exactly once
+    if ( Abc_NodeCheckDupFanin( pFanin, pFanout, &iFanin ) != 1 )
+        return NULL;
+    // find the new number of fanins after collapsing
+    nSize = Abc_NodeCollapseSuppSize( pFanin, pFanout, vFanins );
+    Hop_IthVar( pMan, nSize ); // use additional var for fanin variable
+    assert( nSize + 1 <= Hop_ManPiNum(pMan) );
+    // find the permutation after collapsing
+    RetValue = Abc_NodeCollapsePermMap( pFanin, NULL, vFanins, pPermFanin );
+    assert( RetValue );
+    RetValue = Abc_NodeCollapsePermMap( pFanout, pFanin, vFanins, pPermFanout );
+    assert( RetValue );
+    // include fanin's variable
+    pPermFanout[iFanin] = nSize;
+    // create new function of fanin and fanout
+    bFanin  = Hop_Permute( pMan, (Hop_Obj_t *)pFanin->pData,  Abc_ObjFaninNum(pFanin),  pPermFanin );
+    bFanout = Hop_Permute( pMan, (Hop_Obj_t *)pFanout->pData, Abc_ObjFaninNum(pFanout), pPermFanout );
+    // compose fanin into fanout
+    return Hop_Compose( pMan, bFanout, bFanin, nSize );
+}
+int Abc_NodeCollapse1( Abc_Obj_t * pFanin, Abc_Obj_t * pFanout, Vec_Ptr_t * vFanins, int * pPermFanin, int * pPermFanout )
+{
+    Abc_Obj_t * pFanoutNew, * pObj;
+    Hop_Obj_t * bFanoutNew;
+    int i;
+    assert( Abc_NtkIsAigLogic(pFanin->pNtk) );
+    assert( Abc_ObjIsNode(pFanin) );
+    assert( Abc_ObjIsNode(pFanout) );
+    bFanoutNew = Abc_NodeCollapseFunc1( pFanin, pFanout, vFanins, pPermFanin, pPermFanout );  
+    if ( bFanoutNew == NULL )
+        return 0;
+    // create the new node
+    pFanoutNew = Abc_NtkCreateNode( pFanin->pNtk );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vFanins, pObj, i )
+        Abc_ObjAddFanin( pFanoutNew, pObj );
+    pFanoutNew->pData = bFanoutNew;
+    // transfer the fanout
+    Abc_ObjTransferFanout( pFanout, pFanoutNew );
+    assert( Abc_ObjFanoutNum( pFanout ) == 0 );
+    Abc_NtkDeleteObj_rec( pFanout, 1 );
+    return 1;
+}
+int Abc_NtkEliminate1( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose )
 {
-    extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
     Vec_Ptr_t * vFanouts, * vFanins, * vNodes;
     Abc_Obj_t * pNode, * pFanout;
     int * pPermFanin, * pPermFanout;
@@ -459,28 +579,32 @@ int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose
     assert( nMaxSize > 0 );
     assert( Abc_NtkIsLogic(pNtk) ); 
     // convert network to BDD representation
-    if ( !Abc_NtkToBdd(pNtk) )
+    if ( !Abc_NtkToAig(pNtk) )
     {
-        fprintf( stdout, "Converting to BDD has failed.\n" );
+        fprintf( stdout, "Converting to AIG has failed.\n" );
         return 0;
     }
-    // prepare nodes for sweeping
-    Abc_NtkRemoveDupFanins( pNtk );
-    Abc_NtkMinimumBase( pNtk );
-    Abc_NtkCleanup( pNtk, 0 );
     // get the nodes in the given order
     vNodes = fReverse? Abc_NtkDfsReverse( pNtk ) : Abc_NtkDfs( pNtk, 0 );
     // go through the nodes and decide is they can be eliminated
-    pPermFanin = ABC_ALLOC( int, nMaxSize + 100 );
-    pPermFanout = ABC_ALLOC( int, nMaxSize + 100 );
-    vFanins = Vec_PtrAlloc( 100 );
-    vFanouts = Vec_PtrAlloc( 100 );
+    pPermFanin = ABC_ALLOC( int, nMaxSize + 1000 );
+    pPermFanout = ABC_ALLOC( int, nMaxSize + 1000 );
+    vFanins = Vec_PtrAlloc( 1000 );
+    vFanouts = Vec_PtrAlloc( 1000 );
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
     {
+        if ( !Abc_ObjIsNode(pNode) ) // skip deleted nodes
+            continue;
         if ( Abc_NodeFindCoFanout(pNode) != NULL )
             continue;
         if ( Abc_ObjFaninNum(pNode) > nMaxSize )
             continue;
+        // skip nodes with more than one fanout
+        if ( Abc_ObjFanoutNum(pNode) != 1 ) 
+            continue;
+        // skip nodes that appear in the FF of their fanout more than once
+        if ( Abc_NodeCountAppearances( pNode, Abc_ObjFanout(pNode, 0) ) != 1 ) 
+            continue;       
         Abc_ObjForEachFanout( pNode, pFanout, k )
             if ( Abc_NodeCollapseSuppSize(pNode, pFanout, vFanins) > nMaxSize )
                 break;
@@ -490,11 +614,19 @@ int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose
         Abc_NodeCollectFanouts( pNode, vFanouts );
         Vec_PtrForEachEntry( Abc_Obj_t *, vFanouts, pFanout, k )
         {
-            RetValue = Abc_NodeCollapse( pNode, pFanout, vFanins, pPermFanin, pPermFanout );
+            if ( fVerbose )
+                printf( "Collapsing fanin %5d (supp =%2d) into fanout %5d (supp =%2d) ",
+                    Abc_ObjId(pNode), Abc_ObjFaninNum(pNode), Abc_ObjId(pFanout), Abc_ObjFaninNum(pFanout) ); 
+            RetValue = Abc_NodeCollapse1( pNode, pFanout, vFanins, pPermFanin, pPermFanout );
             assert( RetValue );
+            if ( fVerbose )
+            {
+                Abc_Obj_t * pNodeNew = Abc_NtkObj( pNtk, Abc_NtkObjNumMax(pNtk) - 1 );
+                if ( pNodeNew )
+                    printf( "resulting in node %5d (supp =%2d).\n", Abc_ObjId(pNodeNew), Abc_ObjFaninNum(pNodeNew) );
+            }
         }
     }
-    Abc_NtkBddReorder( pNtk, 0 );
     Vec_PtrFree( vFanins );
     Vec_PtrFree( vFanouts );
     Vec_PtrFree( vNodes );

src/base/abci/abc.c

@@ -3641,8 +3641,8 @@ usage:
     Abc_Print( -2, "\t           performs unate fast extract on the current network\n");
     Abc_Print( -2, "\t-S <num> : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
     Abc_Print( -2, "\t-D <num> : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
-    Abc_Print( -2, "\t-N <num> : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );
-    Abc_Print( -2, "\t-W <num> : only extract divisors with weight more than this [default = %d]\n", p->nSingleMax );
+    Abc_Print( -2, "\t-N <num> : max number of divisors to extract during this run [default = %d]\n", p->nNodesExt );
+    Abc_Print( -2, "\t-W <num> : only extract divisors with weight more than this [default = %d]\n", p->WeightMax );
     Abc_Print( -2, "\t-s       : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" );
     Abc_Print( -2, "\t-d       : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );
     Abc_Print( -2, "\t-z       : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
@@ -3668,17 +3668,20 @@ int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int nMaxSize;
+    int fGreedy;
     int fReverse;
     int fVerbose;
     int c;
     extern int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose );
+    extern int Abc_NtkEliminate1( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose );
 
     // set the defaults
-    nMaxSize  = 8;
-    fReverse  = 0;
-    fVerbose  = 0;
+    nMaxSize = 30;
+    fGreedy  =  0;
+    fReverse =  0;
+    fVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "Nrvh")) != EOF )
+    while ( (c = Extra_UtilGetopt(argc, argv, "Ngrvh")) != EOF )
     {
         switch (c)
         {
@@ -3693,6 +3696,9 @@ int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv )
                 if ( nMaxSize <= 0 )
                     goto usage;
                 break;
+            case 'g':
+                fGreedy ^= 1;
+                break;
             case 'r':
                 fReverse ^= 1;
                 break;
@@ -3725,14 +3731,18 @@ int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    // the nodes to be merged are linked into the special linked list
-    Abc_NtkEliminate( pNtk, nMaxSize, fReverse, fVerbose );
+    if ( fGreedy )
+        Abc_NtkEliminate( pNtk, nMaxSize, fReverse, fVerbose );
+    else
+        Abc_NtkEliminate1( pNtk, nMaxSize, fReverse, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: eliminate [-N <num>] [-rvh]\n");
-    Abc_Print( -2, "\t           greedily eliminates nodes by collapsing them into fanouts\n");
-    Abc_Print( -2, "\t-N <num> : the maximum support size after collapsing [default = %d]\n", nMaxSize );
+    Abc_Print( -2, "usage: eliminate [-N <num>] [-grvh]\n");
+    Abc_Print( -2, "\t           traditional \"eliminate -1\", which collapses the node into its fanout\n");
+    Abc_Print( -2, "\t           if the node's variable appears in the fanout's factored form only once\n");
+    Abc_Print( -2, "\t-N <num> : the maximum node support after collapsing [default = %d]\n", nMaxSize );
+    Abc_Print( -2, "\t-g       : toggle using greedy eliminate (without \"value\") [default = %s]\n", fGreedy? "yes": "no" );
     Abc_Print( -2, "\t-r       : use the reverse topological order [default = %s]\n", fReverse? "yes": "no" );
     Abc_Print( -2, "\t-v       : print verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n");

src/base/abci/abcFxu.c

@@ -52,15 +52,15 @@ extern int  Fxu_FastExtract( Fxu_Data_t * pData );
 void Abc_NtkSetDefaultParams( Fxu_Data_t * p )
 {
     memset( p, 0, sizeof(Fxu_Data_t) );
-    p->nSingleMax = 20000;
-    p->nPairsMax  = 30000;
-    p->nNodesExt  = 10000;
-    p->WeightMax  = 0;
-    p->fOnlyS     = 0;
-    p->fOnlyD     = 0;
-    p->fUse0      = 0;
-    p->fUseCompl  = 1;
-    p->fVerbose   = 0;
+    p->nSingleMax =  20000;
+    p->nPairsMax  =  30000;
+    p->nNodesExt  = 100000;
+    p->WeightMax  =      0;
+    p->fOnlyS     =      0;
+    p->fOnlyD     =      0;
+    p->fUse0      =      0;
+    p->fUseCompl  =      1;
+    p->fVerbose   =      0;
 }
 
 /**Function*************************************************************