Version abc80130_2

1 files changed, 177 insertions, 474 deletions

diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 165777f8..8e8e8719 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -6,7 +6,7 @@
 
   PackageName [Network and node package.]
 
-  Synopsis    [Procedures which transform an AIG into the network of SOP logic nodes.]
+  Synopsis    []
 
   Author      [Alan Mishchenko]
   
@@ -19,479 +19,172 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "reo.h"
+#include "if.h"
+#include "kit.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-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 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 DdNode *    Abc_NtkRenodeDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFanins );
+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 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 );
+static int nDsdCounter = 0;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFITIONS                           ///
+///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Transforms the AIG into nodes.]
+  Synopsis    [Performs renoding as technology mapping.]
 
-  Description [Threhold is the max number of nodes duplicated at a node.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple )
+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 )
 {
+    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( "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
-        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 );
-
-    // 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 )
+        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 )
     {
-//        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 );
+        pPars->fArea = 1;
+        pPars->pFuncCost = Abc_NtkRenodeEvalCnf;
     }
-//printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
+    else if ( fUseMv )
+        pPars->pFuncCost = Abc_NtkRenodeEvalMv;
+    else
+        pPars->pFuncCost = Abc_NtkRenodeEvalAig;
 
-    // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkNew ) )
+    // start the manager
+    if ( fUseBdds )
     {
-        printf( "Abc_NtkRenode: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
+        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;
     }
-    return pNtkNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transforms the AIG into nodes.]
-
-  Description [Threhold is the max number of nodes duplicated at a node.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    ProgressBar * pProgress;
-    Abc_Obj_t * pNode, * pConst1, * pNodeNew;
-    int i;
-
-    // set the constant node
-    pConst1 = Abc_AigConst1(pNtk->pManFunc);
-    if ( Abc_ObjFanoutNum(pConst1) > 0 )
+    else
     {
-        pNodeNew = Abc_NtkCreateNode( pNtkNew );  
-        pNodeNew->pData = Cudd_ReadOne( pNtkNew->pManFunc );   Cudd_Ref( pNodeNew->pData );
-        pConst1->pCopy = pNodeNew;
+        assert( s_vMemory == NULL );
+        s_vMemory  = Vec_IntAlloc( 1 << 16 );
+        s_vMemory2 = Vec_IntAlloc( 1 << 16 );
     }
 
-    // perform renoding for POs
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
-    {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
-            continue;
-        Abc_NtkRenode_rec( pNtkNew, Abc_ObjFanin0(pNode) );
-    }
-    Extra_ProgressBarStop( pProgress );
+    // perform mapping/renoding
+    pNtkNew = Abc_NtkIf( pNtk, pPars );
 
-    // clean the boundaries and data field in the old network
-    Abc_NtkForEachObj( pNtk, pNode, i )
+    // start the manager
+    if ( fUseBdds )
     {
-        pNode->fMarkA = 0;
-        pNode->pData = NULL;
+        Extra_StopManager( s_pDd );
+        Extra_ReorderQuit( s_pReo );
+        s_pReo = NULL;
+        s_pDd  = NULL;
     }
-}
-
-/**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    [Derives the local BDD of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld )
-{
-    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++ )
+    else
     {
-        pFaninOld = vFaninsOld->pArray[i];
-        Cudd_RecursiveDeref( dd, pFaninOld->pData );
-        pFaninOld->fMarkC = 0;
+        Vec_IntFree( s_vMemory );
+        Vec_IntFree( s_vMemory2 );
+        s_vMemory = NULL;
+        s_vMemory2 = NULL;
     }
-    Cudd_Deref( bFunc );
-    return bFunc;
-}
 
-/**Function*************************************************************
+//    printf( "Decomposed %d functions.\n", nDsdCounter );
 
-  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 )
-{
-    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;
+    return pNtkNew;
 }
 
-
-
 /**Function*************************************************************
 
-  Synopsis    [Limits the cones to be no more than the given size.]
+  Synopsis    [Computes the cost based on the factored form.]
 
-  Description [Returns 1 if the last cone was limited. Returns 0 if no changes.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkRenodeLimit_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax, int fCanStop, int fFirst )
+int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
 {
-    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 )
+    Kit_Graph_t * pGraph;
+    int i, nNodes;
+/*
+extern void Kit_DsdTest( unsigned * pTruth, int nVars );
+if ( If_CutLeaveNum(pCut) == 8 )
 {
-    vCone->nSize = 0;
-    return Abc_NtkRenodeLimit_rec( pNode, vCone, nFaninMax, 1, 1 );
+    nDsdCounter++;
+    Kit_DsdTest( If_CutTruth(pCut), If_CutLeaveNum(pCut) );
 }
-
-/**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 )
-    {
-        // skip PI/PO nodes
-        if ( Abc_NodeIsConst(pNode) )
-            continue;
-        if ( pNode->fMarkA == 0 )
-            continue;
-        Abc_NtkRenodeCone( pNode, vCone );
-        assert( vCone->nSize <= nFaninMax );    
-    }
 */
-}
-
-/**Function*************************************************************
-
-  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 )
+    pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
+    if ( pGraph == NULL )
     {
-        // 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;
-        }
+        for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
+            pCut->pPerm[i] = 100;
+        return IF_COST_MAX;
     }
+    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;
+}
 
-    // 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.]
+  Synopsis    [Computes the cost based on the BDD size after reordering.]
 
   Description []
                
@@ -500,44 +193,27 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
+int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut )
 {
-    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;
+    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; 
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Sets a simple boundary.]
+  Synopsis    [Computes the cost based on ISOP.]
 
   Description []
                
@@ -546,21 +222,21 @@ void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk )
+int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
 {
-    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;
+    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 );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collects the fanins of a large node.]
+  Synopsis    [Computes the cost based on two ISOPs.]
 
   Description []
                
@@ -569,21 +245,32 @@ void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRenodeCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
+int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
 {
-    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 );
+    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;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collects the fanins of a large node.]
+  Synopsis    [Computes the cost of MV-SOP of the cut function.]
 
   Description []
                
@@ -592,13 +279,29 @@ void Abc_NtkRenodeCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
+int Abc_NtkRenodeEvalMv( If_Cut_t * pCut )
 {
-    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 );
+    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;
 }
 
 ////////////////////////////////////////////////////////////////////////