Version abc61205

10 files changed, 972 insertions, 718 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 08e1323d..27f82d6e 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -698,9 +698,6 @@ extern int                Abc_NodeMffcLabel( Abc_Obj_t * pNode );
 extern void               Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp );
 extern int                Abc_NodeDeref_rec( Abc_Obj_t * pNode );
 extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
-/*=== abcRenode.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
-extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcRefactor.c ==========================================================*/
 extern int                Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 /*=== abcRewrite.c ==========================================================*/
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index dbbe9d7e..77ae4d5a 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -53,6 +53,7 @@ static int Abc_CommandShowCut        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCollapse       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandStrash         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBalance        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMulti          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRenode         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCleanup        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSweep          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -184,6 +185,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Abc_CommandBalance,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "multi",         Abc_CommandMulti,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Abc_CommandRenode,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "sweep",         Abc_CommandSweep,            1 );
@@ -1911,7 +1913,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandMulti( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1920,6 +1922,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fMulti;
     int fSimple;
     int fFactor;
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -1990,7 +1993,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple, fFactor );
+    pNtkRes = Abc_NtkMulti( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple, fFactor );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -2001,7 +2004,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-T num] [-F num] [-msfch]\n" );
+    fprintf( pErr, "usage: multi [-T num] [-F num] [-msfch]\n" );
     fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
     fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
     fprintf( pErr, "\t-T num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
@@ -2027,6 +2030,95 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int nFaninMax, c;
+    int fUseBdds;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFaninMax =  8;
+    fUseBdds  =  0;
+    fVerbose  =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Fbvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFaninMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFaninMax < 0 ) 
+                goto usage;
+            break;
+        case 'b':
+            fUseBdds ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Cannot renode a network that is not an AIG (run \"strash\").\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, fUseBdds, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Renoding has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: renode [-F num] [-bv]\n" );
+    fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
+    fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
+    fprintf( pErr, "\t-b      : toggles cost function (BDD nodes or FF literals) [default = %s]\n", fUseBdds? "BDD nodes": "FF literals" );
+    fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
+    fprintf( pErr, "\t-h      : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -7391,19 +7483,26 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
     pPars->Mode        =  0;
     pPars->nLutSize    =  4;
-//    pPars->pLutLib    =  Abc_FrameReadLibLut();
     pPars->nCutsMax    = 20;
+    pPars->DelayTarget = -1;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
-    pPars->fLatchPaths =  0;
     pPars->fExpRed     =  1;
+    pPars->fLatchPaths =  0;
     pPars->fSeq        =  0;
-    pPars->nLatches    =  0;
-    pPars->DelayTarget = -1;
     pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  1;
+    pPars->nLatches    =  pNtk? Abc_NtkLatchNum(pNtk) : 0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  NULL;   
+
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "MKCDpaflrsvh" ) ) != EOF )
     {
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 704c8ebb..b76385f8 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -28,8 +28,7 @@
 static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj );
-static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut );
-static Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
+static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -75,7 +74,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
         return NULL;
     }
 
-    // transform the result of mapping into a BDD network
+    // transform the result of mapping into the new network
     pNtkNew = Abc_NtkFromIf( pIfMan, pNtk );
     if ( pNtkNew == NULL )
         return NULL;
@@ -163,7 +162,10 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     Abc_Obj_t * pNode, * pNodeNew;
     int i, nDupGates;
     // create the new network
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
+    if ( pIfMan->pPars->fUseBdds )
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    else
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
     // prepare the mapping manager
     If_ManCleanNodeCopy( pIfMan );
     If_ManCleanCutData( pIfMan );
@@ -221,75 +223,37 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
         Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
     // derive the function of this node
-//    pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pCutBest );
-    pNodeNew->pData = Abc_NodeIfToHop2( pNtkNew->pManFunc, pIfMan, pIfObj );
-    If_ObjSetCopy( pIfObj, pNodeNew );
-    return pNodeNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively derives the truth table for the cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Ptr_t * vVisited )
-{
-    Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
-    // if the cut is visited, return the result
-    if ( If_CutData(pCut) )
-        return If_CutData(pCut);
-    // compute the functions of the children
-    gFunc0 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut->pOne, vVisited );
-    gFunc1 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut->pTwo, vVisited );
-    // get the function of the cut
-    gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, pCut->fCompl0), Hop_NotCond(gFunc1, pCut->fCompl1) );  
-    gFunc  = Hop_NotCond( gFunc, pCut->Phase );
-    assert( If_CutData(pCut) == NULL );
-    If_CutSetData( pCut, gFunc );
-    // add this cut to the visited list
-    Vec_PtrPush( vVisited, pCut );
-    return gFunc;
-}
-
-/**Function*************************************************************
 
-  Synopsis    [Derives the truth table for one cut.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
+    if ( pIfMan->pPars->fTruth )
+    {
+        if ( pIfMan->pPars->fUseBdds )
+        { 
+            extern void Abc_NodeBddReorder( void * p, Abc_Obj_t * pNode );
+            extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
+            // transform truth table into the BDD 
+            pNodeNew->pData = Kit_TruthToBdd( pNtkNew->pManFunc, If_CutTruth(pCutBest), pCutBest->nLimit );
+            // reorder the fanins to minimize the BDD size
+            Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
+        }
+        else
+        {
+            typedef int Kit_Graph_t;
+            extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
+            extern Hop_Obj_t * Dec_GraphToNetworkAig( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+            // transform truth table into the decomposition tree
+            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit );
+            // derive the AIG for that tree
+            pNodeNew->pData = Dec_GraphToNetworkAig( pNtkNew->pManFunc, pGraph );
+            Kit_GraphFree( pGraph );
+        }
+    }
+    else
 
-***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t * pCut )
-{
-    Hop_Obj_t * gFunc;
-    If_Obj_t * pLeaf;
-    int i;
-    assert( pCut->nLeaves > 1 );
-    // set the leaf variables
-    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) );
-    // recursively compute the function while collecting visited cuts
-    Vec_PtrClear( pIfMan->vTemp );
-    gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pCut, pIfMan->vTemp ); 
-//    printf( "%d ", Vec_PtrSize(p->vTemp) );
-    // clean the cuts
-    If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
-        If_CutSetData( If_ObjCutTriv(pLeaf), NULL );
-    Vec_PtrForEachEntry( pIfMan->vTemp, pCut, i )
-        If_CutSetData( pCut, NULL );
-    return gFunc;
+        pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
+    If_ObjSetCopy( pIfObj, pNodeNew );
+    return pNodeNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Recursively derives the truth table for the cut.]
@@ -301,7 +265,7 @@ Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Cut_t *
   SeeAlso     []
 
 ***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
+Hop_Obj_t * Abc_NodeIfToHop_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Ptr_t * vVisited )
 {
     If_Cut_t * pCut;
     Hop_Obj_t * gFunc, * gFunc0, * gFunc1;
@@ -311,11 +275,10 @@ Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj
     if ( If_CutData(pCut) )
         return If_CutData(pCut);
     // compute the functions of the children
-    gFunc0 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj->pFanin0, vVisited );
-    gFunc1 = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj->pFanin1, vVisited );
+    gFunc0 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj->pFanin0, vVisited );
+    gFunc1 = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj->pFanin1, vVisited );
     // get the function of the cut
     gFunc  = Hop_And( pHopMan, Hop_NotCond(gFunc0, pIfObj->fCompl0), Hop_NotCond(gFunc1, pIfObj->fCompl1) );  
-    gFunc  = Hop_NotCond( gFunc, pCut->Phase );
     assert( If_CutData(pCut) == NULL );
     If_CutSetData( pCut, gFunc );
     // add this cut to the visited list
@@ -334,7 +297,7 @@ Hop_Obj_t * Abc_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj
   SeeAlso     []
 
 ***********************************************************************/
-Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
+Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj )
 {
     If_Cut_t * pCut;
     Hop_Obj_t * gFunc;
@@ -348,7 +311,7 @@ Hop_Obj_t * Abc_NodeIfToHop2( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t *
         If_CutSetData( If_ObjCutTriv(pLeaf), Hop_IthVar(pHopMan, i) );
     // recursively compute the function while collecting visited cuts
     Vec_PtrClear( pIfMan->vTemp );
-    gFunc = Abc_NodeIfToHop2_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
+    gFunc = Abc_NodeIfToHop_rec( pHopMan, pIfMan, pIfObj, pIfMan->vTemp ); 
 //    printf( "%d ", Vec_PtrSize(p->vTemp) );
     // clean the cuts
     If_CutForEachLeaf( pIfMan, pCut, pLeaf, i )
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index c4f9850a..d4d50923 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -469,6 +469,7 @@ Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
 {
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkNew, * pNtkNew2;
     Abc_Obj_t * pNode;
@@ -484,7 +485,7 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
 
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
-    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 );
+    pNtkNew  = Abc_NtkMulti( pNtkNew2, 0, 20, 0, 0, 1, 0 );
     if ( !Abc_NtkBddToSop( pNtkNew, 0 ) )
     {
         printf( "Abc_NtkFromMapSuperChoice(): Converting to SOPs has failed.\n" );
diff --git a/src/base/abci/abcMulti.c b/src/base/abci/abcMulti.c
new file mode 100644
index 00000000..e93360a0
--- /dev/null
+++ b/src/base/abci/abcMulti.c
@@ -0,0 +1,643 @@
+/**CFile****************************************************************
+
+  FileName    [abcMulti.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Procedures which transform an AIG into multi-input AND-graph.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcMulti.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static void        Abc_NtkMultiInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t * Abc_NtkMulti_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld );
+
+static DdNode *    Abc_NtkMultiDeriveBdd_rec( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFanins );
+static DdNode *    Abc_NtkMultiDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
+
+static void        Abc_NtkMultiSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax );
+static void        Abc_NtkMultiSetBoundsCnf( Abc_Ntk_t * pNtk );
+static void        Abc_NtkMultiSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh );
+static void        Abc_NtkMultiSetBoundsSimple( Abc_Ntk_t * pNtk );
+static void        Abc_NtkMultiSetBoundsFactor( Abc_Ntk_t * pNtk );
+static void        Abc_NtkMultiCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms the AIG into nodes.]
+
+  Description [Threhold is the max number of nodes duplicated at a node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor )
+{
+    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_NtkMultiSetBoundsCnf( pNtk );
+    else if ( fMulti )
+        Abc_NtkMultiSetBoundsMulti( pNtk, nThresh );
+    else if ( fSimple )
+        Abc_NtkMultiSetBoundsSimple( pNtk );
+    else if ( fFactor )
+        Abc_NtkMultiSetBoundsFactor( pNtk );
+    else
+        Abc_NtkMultiSetBounds( pNtk, nThresh, nFaninMax );
+
+    // perform renoding for this boundary
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    Abc_NtkMultiInt( 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 )
+    {
+//        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 );
+    }
+//printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
+
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkMulti: 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     []
+
+***********************************************************************/
+void Abc_NtkMultiInt( 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);
+    if ( Abc_ObjFanoutNum(pConst1) > 0 )
+    {
+        pNodeNew = Abc_NtkCreateNode( pNtkNew );  
+        pNodeNew->pData = Cudd_ReadOne( pNtkNew->pManFunc );   Cudd_Ref( pNodeNew->pData );
+        pConst1->pCopy = pNodeNew;
+    }
+
+    // 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_NtkMulti_rec( pNtkNew, Abc_ObjFanin0(pNode) );
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // clean the boundaries and data field in the old network
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        pNode->fMarkA = 0;
+        pNode->pData = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find the best multi-input node rooted at the given node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkMulti_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_AigNodeIsConst(pNodeOld) );
+    assert( pNodeOld->fMarkA );
+
+//printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) );
+
+    // collect the renoding cone
+    vCone = Vec_PtrAlloc( 10 );
+    Abc_NtkMultiCone( pNodeOld, vCone );
+
+    // create a new node 
+    pNodeNew = Abc_NtkCreateNode( pNtkNew ); 
+    for ( i = 0; i < vCone->nSize; i++ )
+        Abc_ObjAddFanin( pNodeNew, Abc_NtkMulti_rec(pNtkNew, vCone->pArray[i]) );
+
+    // derive the function of this node
+    pNodeNew->pData = Abc_NtkMultiDeriveBdd( 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_NtkMultiDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld )
+{
+    Abc_Obj_t * pFaninOld;
+    DdNode * bFunc;
+    int i;
+    assert( !Abc_AigNodeIsConst(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_NtkMultiDeriveBdd_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_NtkMultiDeriveBdd_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_NtkMultiDeriveBdd_rec( dd, Abc_ObjFanin(pNode,0), vFanins ); Cudd_Ref( bFunc0 );
+    bFunc1 = Abc_NtkMultiDeriveBdd_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;
+}
+
+
+
+/**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_NtkMultiLimit_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_NtkMultiLimit_rec( Abc_ObjFanin(pNode,0), vCone, nFaninMax, 0, 0 );
+        Abc_NtkMultiLimit_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_NtkMultiLimit_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_NtkMultiLimit_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_NtkMultiLimit_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_NtkMultiLimit_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_NtkMultiLimit( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax )
+{
+    vCone->nSize = 0;
+    return Abc_NtkMultiLimit_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_NtkMultiSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
+{
+    Vec_Ptr_t * vCone = Vec_PtrAlloc(10);
+    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 until it meets the fanin limit
+        while ( Abc_NtkMultiLimit(pNode, vCone, nFaninMax) );
+        assert( vCone->nSize <= nFaninMax );  
+    }
+    Vec_PtrFree(vCone);
+/*
+    // 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_NtkMultiCone( 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_NtkMultiSetBoundsCnf( 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 []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
+{
+    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    [Sets a simple boundary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBoundsSimple( Abc_Ntk_t * pNtk )
+{
+    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    [Sets a factor-cut boundary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiSetBoundsFactor( Abc_Ntk_t * pNtk )
+{
+    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 = (pNode->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pNode));
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the fanins of a large node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
+{
+    assert( !Abc_ObjIsComplement(pNode) );
+    if ( pNode->fMarkA || !Abc_ObjIsNode(pNode) )
+    {
+        Vec_PtrPushUnique( vCone, pNode );
+        return;
+    }
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,0), vCone );
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,1), vCone );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the fanins of a large node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMultiCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
+{
+    assert( !Abc_ObjIsComplement(pNode) );
+    assert( Abc_ObjIsNode(pNode) );
+    vCone->nSize = 0;
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,0), vCone );
+    Abc_NtkMultiCone_rec( Abc_ObjFanin(pNode,1), vCone );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index fd5a38e1..8793ce53 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -536,73 +536,6 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
 
 
 
-#include "reo.h"
-
-/**Function*************************************************************
-
-  Synopsis    [Reorders BDD of the local function of the node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
-{
-    Abc_Obj_t * pFanin;
-    DdNode * bFunc;
-    int * pOrder, i;
-    // create the temporary array for the variable order
-    pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) );
-    for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
-        pOrder[i] = -1;
-    // reorder the BDD
-    bFunc = Extra_Reorder( p, pNode->pNtk->pManFunc, pNode->pData, pOrder ); Cudd_Ref( bFunc );
-    Cudd_RecursiveDeref( pNode->pNtk->pManFunc, pNode->pData );
-    pNode->pData = bFunc;
-    // update the fanin order
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ];
-    Abc_ObjForEachFanin( pNode, pFanin, i )
-        pNode->vFanins.pArray[i] = pOrder[i];
-    free( pOrder );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reorders BDDs of the local functions.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
-{
-    reo_man * p;
-    Abc_Obj_t * pNode;
-    int i;
-    p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
-    Abc_NtkForEachNode( pNtk, pNode, i )
-    {
-        if ( Abc_ObjFaninNum(pNode) < 3 )
-            continue;
-        if ( fVerbose )
-            fprintf( stdout, "%10s: ", Abc_ObjName(pNode) );
-        if ( fVerbose )
-            fprintf( stdout, "Before = %5d  BDD nodes.  ", Cudd_DagSize(pNode->pData) );
-        Abc_NodeBddReorder( p, pNode );
-        if ( fVerbose )
-            fprintf( stdout, "After = %5d  BDD nodes.\n", Cudd_DagSize(pNode->pData) );
-    }
-    Extra_ReorderQuit( p );
-}
-
-
 
 /**Function*************************************************************
 
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 2e448ce5..a3360953 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,22 +19,22 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "reo.h"
+#include "if.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_NtkRenodeEvalBdd( unsigned * pTruth, int nVars );
+static int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars );
 
-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 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_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk );
-static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
+typedef int Kit_Graph_t;
+extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
+extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -42,165 +42,70 @@ static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 
 /**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, int fFactor )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, 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 if ( fFactor )
-        Abc_NtkRenodeSetBoundsFactor( pNtk );
-    else
-        Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax );
-
-    // perform renoding for this boundary
-    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_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 )
-    {
-//        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 );
-    }
-//printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
-
-    if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-    // make sure everything is okay
-    if ( !Abc_NtkCheck( pNtkNew ) )
-    {
-        printf( "Abc_NtkRenode: The network check has failed.\n" );
-        Abc_NtkDelete( pNtkNew );
-        return NULL;
+    // set defaults
+    memset( pPars, 0, sizeof(If_Par_t) );
+    // user-controlable paramters
+    pPars->Mode        =  0;
+    pPars->nLutSize    =  nFaninMax;
+    pPars->nCutsMax    = 10;
+    pPars->DelayTarget = -1;
+    pPars->fPreprocess =  1;
+    pPars->fArea       =  0;
+    pPars->fFancy      =  0;
+    pPars->fExpRed     =  0; //
+    pPars->fLatchPaths =  0;
+    pPars->fSeq        =  0;
+    pPars->fVerbose    =  0;
+    // internal parameters
+    pPars->fTruth      =  1;
+    pPars->nLatches    =  0;
+    pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
+    pPars->pTimesArr   =  NULL; 
+    pPars->pTimesArr   =  NULL;   
+    pPars->pFuncCost   =  fUseBdds? Abc_NtkRenodeEvalBdd : Abc_NtkRenodeEvalSop;   
+
+    // start the manager
+    if ( fUseBdds )
+    {
+        assert( s_pReo == NULL );
+        s_pDd  = Cudd_Init( nFaninMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+        s_pReo = Extra_ReorderInit( nFaninMax, 100 );
+        pPars->fUseBdds = 1;
+        pPars->pReoMan  = s_pReo;
+    }
+
+    // perform mapping/renoding
+    pNtkNew = Abc_NtkIf( pNtk, pPars );
+
+    // start the manager
+    if ( fUseBdds )
+    {
+        Extra_StopManager( s_pDd );
+        Extra_ReorderQuit( s_pReo );
+        s_pReo = NULL;
+        s_pDd = NULL;
     }
     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);
-    if ( Abc_ObjFanoutNum(pConst1) > 0 )
-    {
-        pNodeNew = Abc_NtkCreateNode( pNtkNew );  
-        pNodeNew->pData = Cudd_ReadOne( pNtkNew->pManFunc );   Cudd_Ref( pNodeNew->pData );
-        pConst1->pCopy = pNodeNew;
-    }
-
-    // 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 );
-
-    // clean the boundaries and data field in the old network
-    Abc_NtkForEachObj( pNtk, pNode, i )
-    {
-        pNode->fMarkA = 0;
-        pNode->pData = 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_AigNodeIsConst(pNodeOld) );
-    assert( pNodeOld->fMarkA );
-
-//printf( "%d ", Abc_NodeMffcSizeSupp(pNodeOld) );
-
-    // 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.]
+  Synopsis    [Derives the BDD after reordering.]
 
   Description []
                
@@ -209,415 +114,22 @@ Abc_Obj_t * Abc_NtkRenode_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld )
+int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
 {
-    Abc_Obj_t * pFaninOld;
-    DdNode * bFunc;
-    int i;
-    assert( !Abc_AigNodeIsConst(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 )
-{
-    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;
-}
-
-
-
-/**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 = Vec_PtrAlloc(10);
-    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 until it meets the fanin limit
-        while ( Abc_NtkRenodeLimit(pNode, vCone, nFaninMax) );
-        assert( vCone->nSize <= nFaninMax );  
-    }
-    Vec_PtrFree(vCone);
-/*
-    // 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 )
-    {
-        // 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 []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh )
-{
-    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    [Sets a simple boundary.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk )
-{
-    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    [Sets a factor-cut boundary.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk )
-{
-    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 = (pNode->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pNode));
-    // mark the PO drivers
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        Abc_ObjFanin0(pNode)->fMarkA = 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the fanins of a large node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkRenodeCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone )
-{
-    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 );
+    DdNode * bFunc, * bFuncNew;
+    int nNodes, nSupport;
+    bFunc = Kit_TruthToBdd( s_pDd, pTruth, nVars );           Cudd_Ref( bFunc );
+    bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, NULL );   Cudd_Ref( bFuncNew );
+    nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
+    nNodes = Cudd_DagSize( bFuncNew );
+    Cudd_RecursiveDeref( s_pDd, bFuncNew );
+    Cudd_RecursiveDeref( s_pDd, bFunc );
+    return (nSupport << 16) | nNodes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collects the fanins of a large node.]
+  Synopsis    [Derives the BDD after reordering.]
 
   Description []
                
@@ -626,13 +138,15 @@ 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_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
 {
-    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 );
+    Kit_Graph_t * pGraph;
+    int nNodes, nDepth;
+    pGraph = Kit_TruthToGraph( pTruth, nVars );
+    nNodes = Kit_GraphNodeNum( pGraph );
+    nDepth = Kit_GraphLevelNum( pGraph );
+    Kit_GraphFree( pGraph );
+    return (nDepth << 16) | nNodes;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
new file mode 100644
index 00000000..d6dee49b
--- /dev/null
+++ b/src/base/abci/abcReorder.c
@@ -0,0 +1,100 @@
+/**CFile****************************************************************
+
+  FileName    [abcReorder.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Reordering local BDDs of the nodes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcReorder.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "reo.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDD of the local function of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    DdNode * bFunc;
+    int * pOrder, i;
+    // create the temporary array for the variable order
+    pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) );
+    for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+        pOrder[i] = -1;
+    // reorder the BDD
+    bFunc = Extra_Reorder( p, pNode->pNtk->pManFunc, pNode->pData, pOrder ); Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( pNode->pNtk->pManFunc, pNode->pData );
+    pNode->pData = bFunc;
+    // update the fanin order
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ];
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pNode->vFanins.pArray[i] = pOrder[i];
+    free( pOrder );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDDs of the local functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    reo_man * p;
+    Abc_Obj_t * pNode;
+    int i;
+    p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_ObjFaninNum(pNode) < 3 )
+            continue;
+        if ( fVerbose )
+            fprintf( stdout, "%10s: ", Abc_ObjName(pNode) );
+        if ( fVerbose )
+            fprintf( stdout, "Before = %5d  BDD nodes.  ", Cudd_DagSize(pNode->pData) );
+        Abc_NodeBddReorder( p, pNode );
+        if ( fVerbose )
+            fprintf( stdout, "After = %5d  BDD nodes.\n", Cudd_DagSize(pNode->pData) );
+    }
+    Extra_ReorderQuit( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index ad58e35c..f4717eda 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -46,6 +46,7 @@ static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2,
 ***********************************************************************/
 void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit )
 {
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pCnf;
     int RetValue;
@@ -76,7 +77,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0, 0 );
+    pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pMiter );
     if ( pCnf == NULL )
     {
@@ -207,6 +208,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
 ***********************************************************************/
 void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames )
 {
+    extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pFrames;
     Abc_Ntk_t * pCnf;
@@ -256,7 +258,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0, 0 );
+    pCnf = Abc_NtkMulti( pFrames, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pFrames );
     if ( pCnf == NULL )
     {
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 04ed07a7..7e674fbe 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -21,6 +21,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMini.c \
     src/base/abci/abcMiter.c \
+    src/base/abci/abcMulti.c \
     src/base/abci/abcNtbdd.c \
     src/base/abci/abcOrder.c \
     src/base/abci/abcPrint.c \
@@ -28,6 +29,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \
+    src/base/abci/abcReorder.c \
     src/base/abci/abcRestruct.c \
     src/base/abci/abcResub.c \
     src/base/abci/abcRewrite.c \