1 files changed, 474 insertions, 177 deletions

diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 8e8e8719..165777f8 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    []
+  Synopsis    [Procedures which transform an AIG into the network of SOP logic nodes.]
 
   Author      [Alan Mishchenko]
   
@@ -19,135 +19,181 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "reo.h"
-#include "if.h"
-#include "kit.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalMv( If_Cut_t * pCut );
+static void        Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld );
 
-static reo_man * s_pReo       = NULL;
-static DdManager * s_pDd      = NULL;
-static Vec_Int_t * s_vMemory  = NULL;
-static Vec_Int_t * s_vMemory2 = NULL;
+static DdNode *    Abc_NtkRenodeDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFanins );
 
-static int nDsdCounter = 0;
+static void        Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax );
+static void        Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk );
+static void        Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh );
+static void        Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk );
+static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs renoding as technology mapping.]
+  Synopsis    [Transforms the AIG into nodes.]
 
-  Description []
+  Description [Threhold is the max number of nodes duplicated at a node.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nFlowIters, int nAreaIters, int fArea, int fUseBdds, int fUseSops, int fUseCnfs, int fUseMv, int fVerbose )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple )
 {
-    extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
-    If_Par_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtkNew;
 
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( nThresh >= 0 );
+    assert( nFaninMax > 1 );
+
+    // print a warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
-        printf( "Performing renoding with choices.\n" );
-
-    nDsdCounter = 0;
-
-    // set defaults
-    memset( pPars, 0, sizeof(If_Par_t) );
-    // user-controlable paramters
-    pPars->nLutSize    =  nFaninMax;
-    pPars->nCutsMax    =  nCubeMax;
-    pPars->nFlowIters  =  nFlowIters;
-    pPars->nAreaIters  =  nAreaIters;
-    pPars->DelayTarget = -1;
-    pPars->fPreprocess =  1;
-    pPars->fArea       =  fArea;
-    pPars->fFancy      =  0;
-    pPars->fExpRed     =  0; //
-    pPars->fLatchPaths =  0;
-    pPars->fSeqMap     =  0;
-    pPars->fVerbose    =  fVerbose;
-    // internal parameters
-    pPars->fTruth      =  1;
-    pPars->fUsePerm    =  1; 
-    pPars->nLatches    =  0;
-    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
-    pPars->pTimesArr   =  NULL; 
-    pPars->pTimesArr   =  NULL;   
-    pPars->fUseBdds    =  fUseBdds;
-    pPars->fUseSops    =  fUseSops;
-    pPars->fUseCnfs    =  fUseCnfs;
-    pPars->fUseMv      =  fUseMv;
-    if ( fUseBdds )
-        pPars->pFuncCost = Abc_NtkRenodeEvalBdd;
-    else if ( fUseSops )
-        pPars->pFuncCost = Abc_NtkRenodeEvalSop;
-    else if ( fUseCnfs )
-    {
-        pPars->fArea = 1;
-        pPars->pFuncCost = Abc_NtkRenodeEvalCnf;
-    }
-    else if ( fUseMv )
-        pPars->pFuncCost = Abc_NtkRenodeEvalMv;
+        printf( "Warning: The choice nodes in the AIG are removed by renoding.\n" );
+
+    // define the boundary
+    if ( fCnf )
+        Abc_NtkRenodeSetBoundsCnf( pNtk );
+    else if ( fMulti )
+        Abc_NtkRenodeSetBoundsMulti( pNtk, nThresh );
+    else if ( fSimple )
+        Abc_NtkRenodeSetBoundsSimple( pNtk );
     else
-        pPars->pFuncCost = Abc_NtkRenodeEvalAig;
+        Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax );
+
+    // perform renoding for this boundary
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_TYPE_LOGIC, ABC_FUNC_BDD );
+    Abc_NtkRenodeInt( pNtk, pNtkNew );
+    Abc_NtkFinalize( pNtk, pNtkNew );
 
-    // start the manager
-    if ( fUseBdds )
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtkNew );
+
+    // fix the problem with complemented and duplicated CO edges
+    Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
+
+    // report the number of CNF objects
+    if ( fCnf )
     {
-        assert( s_pReo == NULL );
-        s_pDd  = Cudd_Init( nFaninMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-        s_pReo = Extra_ReorderInit( nFaninMax, 100 );
-        pPars->pReoMan  = s_pReo;
+//        int nClauses = Abc_NtkGetClauseNum(pNtkNew) + 2*Abc_NtkPoNum(pNtkNew) + 2*Abc_NtkLatchNum(pNtkNew);
+//        printf( "CNF variables = %d. CNF clauses = %d.\n",  Abc_NtkNodeNum(pNtkNew), nClauses );
     }
-    else
+//printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
+
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
     {
-        assert( s_vMemory == NULL );
-        s_vMemory  = Vec_IntAlloc( 1 << 16 );
-        s_vMemory2 = Vec_IntAlloc( 1 << 16 );
+        printf( "Abc_NtkRenode: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
     }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the AIG into nodes.]
+
+  Description [Threhold is the max number of nodes duplicated at a node.]
+               
+  SideEffects []
+
+  SeeAlso     []
 
-    // perform mapping/renoding
-    pNtkNew = Abc_NtkIf( pNtk, pPars );
+***********************************************************************/
+void Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode, * pConst1, * pNodeNew;
+    int i;
 
-    // start the manager
-    if ( fUseBdds )
+    // set the constant node
+    pConst1 = Abc_AigConst1(pNtk->pManFunc);
+    if ( Abc_ObjFanoutNum(pConst1) > 0 )
     {
-        Extra_StopManager( s_pDd );
-        Extra_ReorderQuit( s_pReo );
-        s_pReo = NULL;
-        s_pDd  = NULL;
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );  
+        pNodeNew->pData = Cudd_ReadOne( pNtkNew->pManFunc );   Cudd_Ref( pNodeNew->pData );
+        pConst1->pCopy = pNodeNew;
     }
-    else
+
+    // perform renoding for POs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        Vec_IntFree( s_vMemory );
-        Vec_IntFree( s_vMemory2 );
-        s_vMemory = NULL;
-        s_vMemory2 = NULL;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+            continue;
+        Abc_NtkRenode_rec( pNtkNew, Abc_ObjFanin0(pNode) );
     }
+    Extra_ProgressBarStop( pProgress );
 
-//    printf( "Decomposed %d functions.\n", nDsdCounter );
+    // clean the boundaries and data field in the old network
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        pNode->fMarkA = 0;
+        pNode->pData = NULL;
+    }
+}
 
-    return pNtkNew;
+/**Function*************************************************************
+
+  Synopsis    [Find the best multi-input node rooted at the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
+{
+    Vec_Ptr_t * vCone;
+    Abc_Obj_t * pNodeNew;
+    int i;
+
+    assert( !Abc_ObjIsComplement(pNodeOld) );
+    // return if the result if known
+    if ( pNodeOld->pCopy )
+        return pNodeOld->pCopy;
+    assert( Abc_ObjIsNode(pNodeOld) );
+    assert( !Abc_NodeIsConst(pNodeOld) );
+    assert( pNodeOld->fMarkA );
+
+    // collect the renoding cone
+    vCone = Vec_PtrAlloc( 10 );
+    Abc_NtkRenodeCone( pNodeOld, vCone );
+
+    // create a new node 
+    pNodeNew = Abc_NtkCreateNode( pNtkNew ); 
+    for ( i = 0; i < vCone->nSize; i++ )
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkRenode_rec(pNtkNew, vCone->pArray[i]) );
+
+    // derive the function of this node
+    pNodeNew->pData = Abc_NtkRenodeDeriveBdd( pNtkNew->pManFunc, pNodeOld, vCone );    
+    Cudd_Ref( pNodeNew->pData );
+    Vec_PtrFree( vCone );
+
+    // remember the node
+    pNodeOld->pCopy = pNodeNew;
+    return pNodeOld->pCopy;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Computes the cost based on the factored form.]
+  Synopsis    [Derives the local BDD of the node.]
 
   Description []
                
@@ -156,35 +202,296 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
+DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld )
 {
-    Kit_Graph_t * pGraph;
-    int i, nNodes;
-/*
-extern void Kit_DsdTest( unsigned * pTruth, int nVars );
-if ( If_CutLeaveNum(pCut) == 8 )
+    Abc_Obj_t * pFaninOld;
+    DdNode * bFunc;
+    int i;
+    assert( !Abc_NodeIsConst(pNodeOld) );
+    assert( Abc_ObjIsNode(pNodeOld) );
+    // set the elementary BDD variables for the input nodes
+    for ( i = 0; i < vFaninsOld->nSize; i++ )
+    {
+        pFaninOld = vFaninsOld->pArray[i];
+        pFaninOld->pData = Cudd_bddIthVar( dd, i );    Cudd_Ref( pFaninOld->pData );
+        pFaninOld->fMarkC = 1;
+    }
+    // call the recursive BDD computation
+    bFunc = Abc_NtkRenodeDeriveBdd_rec( dd, pNodeOld, vFaninsOld );  Cudd_Ref( bFunc );
+    // dereference the intermediate nodes
+    for ( i = 0; i < vFaninsOld->nSize; i++ )
+    {
+        pFaninOld = vFaninsOld->pArray[i];
+        Cudd_RecursiveDeref( dd, pFaninOld->pData );
+        pFaninOld->fMarkC = 0;
+    }
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the local BDD of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkRenodeDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins )
 {
-    nDsdCounter++;
-    Kit_DsdTest( If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    // if the result is available return
+    if ( pNode->fMarkC )
+    {
+        assert( pNode->pData ); // network has a cycle
+        return pNode->pData;
+    }
+    // mark the node as visited
+    pNode->fMarkC = 1;
+    Vec_PtrPush( vFanins, pNode );
+    // compute the result for both branches
+    bFunc0 = Abc_NtkRenodeDeriveBdd_rec( dd, Abc_ObjFanin(pNode,0), vFanins ); Cudd_Ref( bFunc0 );
+    bFunc1 = Abc_NtkRenodeDeriveBdd_rec( dd, Abc_ObjFanin(pNode,1), vFanins ); Cudd_Ref( bFunc1 );
+    bFunc0 = Cudd_NotCond( bFunc0, Abc_ObjFaninC0(pNode) );
+    bFunc1 = Cudd_NotCond( bFunc1, Abc_ObjFaninC1(pNode) );
+    // get the final result
+    bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( dd, bFunc0 );
+    Cudd_RecursiveDeref( dd, bFunc1 );
+    // set the result
+    pNode->pData = bFunc;
+    assert( pNode->pData );
+    return bFunc;
 }
-*/
-    pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
-    if ( pGraph == NULL )
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Limits the cones to be no more than the given size.]
+
+  Description [Returns 1 if the last cone was limited. Returns 0 if no changes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRenodeLimit_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax, int fCanStop, int fFirst )
+{
+    int nNodes0, nNodes1;
+    assert( !Abc_ObjIsComplement(pNode) );
+    // check if the node should be added to the fanins
+    if ( !fFirst && (pNode->fMarkA || !Abc_ObjIsNode(pNode)) )
+    {
+        Vec_PtrPushUnique( vCone, pNode );
+        return 0;
+    }
+    // if we cannot stop in this branch, collect all nodes
+    if ( !fCanStop )
+    {
+        Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,0), vCone, nFaninMax, 0, 0 );
+        Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
+        return 0;
+    }
+    // if we can stop, try the left branch first, and return if we stopped
+    assert( vCone->nSize == 0 );
+    if ( Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,0), vCone, nFaninMax, 1, 0 ) )
+        return 1;
+    // save the number of nodes in the left branch and call for the right branch
+    nNodes0 = vCone->nSize;
+    assert( nNodes0 <= nFaninMax );
+    Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
+    // check the number of nodes
+    if ( vCone->nSize <= nFaninMax )
+        return 0;
+    // the number of nodes exceeds the limit
+
+    // get the number of nodes in the right branch
+    vCone->nSize = 0;
+    Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 0, 0 );
+    // if this number exceeds the limit, solve the problem for this branch
+    if ( vCone->nSize > nFaninMax )
+    {
+        int RetValue;
+        vCone->nSize = 0;
+        RetValue = Abc_NtkRenodeLimit_rec( Abc_ObjFanin(pNode,1), vCone, nFaninMax, 1, 0 );
+        assert( RetValue == 1 );
+        return 1;
+    }
+
+    nNodes1 = vCone->nSize; 
+    assert( nNodes1 <= nFaninMax );
+    if ( nNodes0 >= nNodes1 )
+    { // the left branch is larger - cut it
+        assert( Abc_ObjFanin(pNode,0)->fMarkA == 0 );
+        Abc_ObjFanin(pNode,0)->fMarkA = 1;
+    }
+    else
+    { // the right branch is larger - cut it
+        assert( Abc_ObjFanin(pNode,1)->fMarkA == 0 );
+        Abc_ObjFanin(pNode,1)->fMarkA = 1;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Limits the cones to be no more than the given size.]
+
+  Description [Returns 1 if the last cone was limited. Returns 0 if no changes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRenodeLimit( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax )
+{
+    vCone->nSize = 0;
+    return Abc_NtkRenodeLimit_rec( pNode, vCone, nFaninMax, 1, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the expansion boundary for multi-input nodes.]
+
+  Description [The boundary includes the set of PIs and all nodes such that 
+  when expanding over the node we duplicate no more than nThresh nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
+{
+    Vec_Ptr_t * vCone = pNtk->vPtrTemp;
+    Abc_Obj_t * pNode;
+    int i, nFanouts, nConeSize;
+
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        // mark the nodes with multiple fanouts
+        nFanouts = Abc_ObjFanoutNum(pNode);
+        nConeSize = Abc_NodeMffcSize(pNode);
+        if ( (nFanouts - 1) * nConeSize > nThresh )
+            pNode->fMarkA = 1;
+    }
+
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+
+    // make sure the fanin limit is met
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        if ( pNode->fMarkA == 0 )
+            continue;
+        // continue cutting branches ntil it meets the fanin limit
+        while ( Abc_NtkRenodeLimit(pNode, vCone, nFaninMax) );
+        assert( vCone->nSize <= nFaninMax );  
+    }
+/*
+    // make sure the fanin limit is met
+    Abc_NtkForEachNode( pNtk, pNode, i )
     {
-        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-            pCut->pPerm[i] = 100;
-        return IF_COST_MAX;
+        // skip PI/PO nodes
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        if ( pNode->fMarkA == 0 )
+            continue;
+        Abc_NtkRenodeCone( pNode, vCone );
+        assert( vCone->nSize <= nFaninMax );    
     }
-    nNodes = Kit_GraphNodeNum( pGraph );
-    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-        pCut->pPerm[i] = Kit_GraphLeafDepth_rec( pGraph, Kit_GraphNodeLast(pGraph), Kit_GraphNode(pGraph, i) );
-    Kit_GraphFree( pGraph );
-    return nNodes;
+*/
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the cost based on the BDD size after reordering.]
+  Synopsis    [Sets the expansion boundary for conversion into CNF.]
+
+  Description [The boundary includes the set of PIs, the roots of MUXes,
+  the nodes with multiple fanouts and the nodes with complemented outputs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, nMuxes;
+
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        // mark the nodes with multiple fanouts
+        if ( Abc_ObjFanoutNum(pNode) > 1 )
+            pNode->fMarkA = 1;
+        // mark the nodes that are roots of MUXes
+        if ( Abc_NodeIsMuxType( pNode ) )
+        {
+            pNode->fMarkA = 1;
+            Abc_ObjFanin0( Abc_ObjFanin0(pNode) )->fMarkA = 1;
+            Abc_ObjFanin0( Abc_ObjFanin1(pNode) )->fMarkA = 1;
+            Abc_ObjFanin1( Abc_ObjFanin0(pNode) )->fMarkA = 1;
+            Abc_ObjFanin1( Abc_ObjFanin1(pNode) )->fMarkA = 1;
+        }
+        else  // mark the complemented edges
+        {
+            if ( Abc_ObjFaninC0(pNode) )
+                Abc_ObjFanin0(pNode)->fMarkA = 1;
+            if ( Abc_ObjFaninC1(pNode) )
+                Abc_ObjFanin1(pNode)->fMarkA = 1;
+        }
+    }
+
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+
+    // count the number of MUXes
+    nMuxes = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        if ( Abc_NodeIsMuxType(pNode) && 
+            Abc_ObjFanin0(pNode)->fMarkA == 0 &&
+            Abc_ObjFanin1(pNode)->fMarkA == 0 )
+            nMuxes++;
+    }
+    printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) );
+} 
+ 
+/**Function*************************************************************
+
+  Synopsis    [Sets the expansion boundary for conversion into multi-input AND graph.]
 
   Description []
                
@@ -193,27 +500,44 @@ if ( If_CutLeaveNum(pCut) == 8 )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut )
+void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
 {
-    int pOrder[IF_MAX_LUTSIZE];
-    DdNode * bFunc, * bFuncNew;
-    int i, k, nNodes;
-    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-        pCut->pPerm[i] = pOrder[i] = -100;
-    bFunc = Kit_TruthToBdd( s_pDd, If_CutTruth(pCut), If_CutLeaveNum(pCut), 0 );  Cudd_Ref( bFunc );
-    bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, pOrder );                     Cudd_Ref( bFuncNew );
-    for ( i = k = 0; i < If_CutLeaveNum(pCut); i++ )
-        if ( pOrder[i] >= 0 )
-            pCut->pPerm[pOrder[i]] = ++k; // double-check this!
-    nNodes = -1 + Cudd_DagSize( bFuncNew );
-    Cudd_RecursiveDeref( s_pDd, bFuncNew );
-    Cudd_RecursiveDeref( s_pDd, bFunc );
-    return nNodes; 
+    Abc_Obj_t * pNode;
+    int i, nFanouts, nConeSize;
+
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip PI/PO nodes
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        // mark the nodes with multiple fanouts
+//        if ( Abc_ObjFanoutNum(pNode) > 1 )
+//            pNode->fMarkA = 1;
+        // mark the nodes with multiple fanouts
+        nFanouts = Abc_ObjFanoutNum(pNode);
+        nConeSize = Abc_NodeMffcSizeStop(pNode);
+        if ( (nFanouts - 1) * nConeSize > nThresh )
+            pNode->fMarkA = 1;
+        // mark the children if they are pointed by the complemented edges
+        if ( Abc_ObjFaninC0(pNode) )
+            Abc_ObjFanin0(pNode)->fMarkA = 1;
+        if ( Abc_ObjFaninC1(pNode) )
+            Abc_ObjFanin1(pNode)->fMarkA = 1;
+    }
+
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the cost based on ISOP.]
+  Synopsis    [Sets a simple boundary.]
 
   Description []
                
@@ -222,21 +546,21 @@ int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
+void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk )
 {
-    int i, RetValue;
-    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-        pCut->pPerm[i] = 1;
-    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 1 );
-    if ( RetValue == -1 )
-        return IF_COST_MAX;
-    assert( RetValue == 0 || RetValue == 1 );
-    return Vec_IntSize( s_vMemory );
+    Abc_Obj_t * pNode;
+    int i;
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->fMarkA = 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the cost based on two ISOPs.]
+  Synopsis    [Collects the fanins of a large node.]
 
   Description []
                
@@ -245,32 +569,21 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
+void Abc_NtkRenodeCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
 {
-    int i, RetValue, nClauses;
-    // set internal mapper parameters
-    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-        pCut->pPerm[i] = 1;
-    // compute ISOP for the positive phase
-    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
-    if ( RetValue == -1 )
-        return IF_COST_MAX;
-    assert( RetValue == 0 || RetValue == 1 );
-    nClauses = Vec_IntSize( s_vMemory );
-    // compute ISOP for the negative phase
-    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
-    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
-    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
-    if ( RetValue == -1 )
-        return IF_COST_MAX;
-    assert( RetValue == 0 || RetValue == 1 );
-    nClauses += Vec_IntSize( s_vMemory );
-    return nClauses;
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( pNode->fMarkA || !Abc_ObjIsNode(pNode) )
+    {
+        Vec_PtrPushUnique( vCone, pNode );
+        return;
+    }
+    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,0), vCone );
+    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,1), vCone );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Computes the cost of MV-SOP of the cut function.]
+  Synopsis    [Collects the fanins of a large node.]
 
   Description []
                
@@ -279,29 +592,13 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeEvalMv( If_Cut_t * pCut )
+void Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
 {
-    int i, RetValue;
-    // set internal mapper parameters
-    for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
-        pCut->pPerm[i] = 1;
-    // compute ISOP for the positive phase
-    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
-    if ( RetValue == -1 )
-        return IF_COST_MAX;
-    assert( RetValue == 0 || RetValue == 1 );
-    // compute ISOP for the negative phase
-    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
-    RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory2, 0 );
-    Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
-    if ( RetValue == -1 )
-        return IF_COST_MAX;
-    assert( RetValue == 0 || RetValue == 1 );
-    // return the cost of the cut 
-    RetValue = Abc_NodeEvalMvCost( If_CutLeaveNum(pCut), s_vMemory, s_vMemory2 );
-    if ( RetValue >= IF_COST_MAX )
-        return IF_COST_MAX;
-    return RetValue;
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( Abc_ObjIsNode(pNode) );
+    vCone->nSize = 0;
+    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,0), vCone );
+    Abc_NtkRenodeCone_rec( Abc_ObjFanin(pNode,1), vCone );
 }
 
 ////////////////////////////////////////////////////////////////////////