Version abc60614

10 files changed, 1067 insertions, 106 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 29a95e46..15d3aa06 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -515,6 +515,7 @@ extern Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fIni
 /*=== abcObj.c ==========================================================*/
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
 extern void               Abc_NtkDeleteObj( Abc_Obj_t * pObj );
+extern void               Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj );
 extern Abc_Obj_t *        Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName );
@@ -598,6 +599,7 @@ extern int                Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pParams
 extern Abc_ManCut_t *     Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop );
 extern void               Abc_NtkManCutStop( Abc_ManCut_t * p );
 extern Vec_Ptr_t *        Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p );
+extern Vec_Ptr_t *        Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p );
 extern Vec_Ptr_t *        Abc_NtkManCutReadVisited( Abc_ManCut_t * p );
 extern Vec_Ptr_t *        Abc_NodeFindCut( Abc_ManCut_t * p, Abc_Obj_t * pRoot, bool fContain );
 extern void               Abc_NodeConeCollect( Abc_Obj_t ** ppRoots, int nRoots, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited, int fIncludeFanins );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 53886161..d993ca65 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -264,8 +264,33 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     Abc_ObjRecycle( pObj );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Deletes the node and MFFC of the node.]
 
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj )
+{
+    Abc_Ntk_t * pNtk = pObj->pNtk;
+    Vec_Ptr_t * vNodes;
+    int i;
+    assert( !Abc_ObjIsComplement(pObj) );
+    assert( Abc_ObjFanoutNum(pObj) == 0 );
+    // delete fanins and fanouts
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NodeCollectFanins( pObj, vNodes );
+    Abc_NtkDeleteObj( pObj );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        if ( Abc_ObjIsNode(pObj) && Abc_ObjFanoutNum(pObj) == 0 )
+            Abc_NtkDeleteObj_rec( pObj );
+    Vec_PtrFree( vNodes );
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 175b17f7..afa91c45 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -915,7 +915,7 @@ void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 
 /**Function*************************************************************
 
-  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+  Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]
 
   Description []
                
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 075c64ee..64ee4596 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31,96 +31,97 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Abc_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintExdc    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintLatch   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintLevel   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSymms   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintUnate   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintAuto    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintKMap    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintGates   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPrintSharing ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowAig      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShowNtk      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-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_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 );
-static int Abc_CommandFastExtract  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDisjoint     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandRewrite      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRefactor     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRestructure  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRr           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDemiter      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOrPos        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandReorder      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandMuxes        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneOutput    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandOneNode      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcFree     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandEspresso     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandGen          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXyz          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigStore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigClean   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandFraigSweep   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandMap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnmap        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPga          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandScut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandInit         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPipe         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqFpga      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqMap       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSeqCleanup   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandProve        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Abc_CommandTraceStart   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandTraceCheck   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintStats     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintExdc      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintIo        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintLatch     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFanio     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFactor    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintLevel     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSupport   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSymms     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintUnate     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintAuto      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintKMap      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintGates     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintSharing   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandShowBdd        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowCut        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowAig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowNtk        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+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_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 );
+static int Abc_CommandFastExtract    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDisjoint       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandRewrite        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRefactor       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRestructure    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandResubstitute   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRr             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandLogic          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMiter          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDemiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOrPos          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFrames         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBdd            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandReorder        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMuxes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExtSeqDcs      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneOutput      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandOneNode        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShortNames     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcFree       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcGet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcSet        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCut            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEspresso       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGen            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXyz            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTest           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFraig          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigTrust     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigStore     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigRestore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigClean     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigSweep     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandMap            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnmap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAttach         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoice    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoiceLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFpga           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPga            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandInit           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPipe           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeq            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnseq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRetime         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandCec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSec            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSat            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -209,6 +210,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Abc_CommandUnmap,            1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Abc_CommandAttach,           1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Abc_CommandSuperChoice,      1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "scl",           Abc_CommandSuperChoiceLut,   1 );
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "pga",           Abc_CommandPga,              1 );
@@ -5494,15 +5496,121 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandSuperChoiceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nLutSize;
+    int nCutSizeMax;
+    int fVerbose;
+    extern int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 1;
+    nLutSize = 4;
+    nCutSizeMax = 10;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KNh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nCutSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCutSizeMax < 0 ) 
+                goto usage;
+            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, "Superchoicing works only for the AIG representation (run \"strash\").\n" );
+        return 1;
+    }
+
+    // convert the network into the SOP network
+    pNtkRes = Abc_NtkAigToLogicSop( pNtk );
+
+    // get the new network
+    if ( !Abc_NtkSuperChoiceLut( pNtkRes, nLutSize, nCutSizeMax, fVerbose ) )
+    {
+        Abc_NtkDelete( pNtkRes );
+        fprintf( pErr, "Superchoicing has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: scl [-K num] [-N num] [-vh]\n" );
+    fprintf( pErr, "\t        performs superchoicing for K-LUTs\n" );
+    fprintf( pErr, "\t        (accumulate: \"r file.blif; b; scl; f -ac; wb file_sc.blif\")\n" );
+    fprintf( pErr, "\t        (FPGA map: \"r file_sc.blif; ft; read_lut lutlibK; fpga\")\n" );
+    fprintf( pErr, "\t-K num : the number of LUT inputs [default = %d]\n", nLutSize );
+    fprintf( pErr, "\t-N num : the max size of the cut [default = %d]\n", nCutSizeMax );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char Buffer[100];
+    char LutSize[100];
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int fRecovery;
     int fSwitching;
     int fVerbose;
+    int nLutSize;
     float DelayTarget;
 
     extern Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, float DelayTarget, int fRecovery, int fSwitching, int fVerbose );
@@ -5516,8 +5624,9 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     fSwitching  = 0;
     fVerbose    = 0;
     DelayTarget =-1;
+    nLutSize    =-1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "apvhD" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "apvhDK" ) ) != EOF )
     {
         switch ( c )
         {
@@ -5543,6 +5652,17 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( DelayTarget <= 0.0 ) 
                 goto usage;
             break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nLutSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutSize < 0 ) 
+                goto usage;
+            break;
         default:
             goto usage;
         }
@@ -5560,6 +5680,10 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    // create the new LUT library
+    if ( nLutSize >= 3 && nLutSize <= 6 )
+        Fpga_SetSimpleLutLib( nLutSize );
+
     if ( !Abc_NtkIsStrash(pNtk) )
     {
         // strash and balance the network
@@ -5606,13 +5730,18 @@ usage:
         sprintf( Buffer, "not used" );
     else
         sprintf( Buffer, "%.2f", DelayTarget );
-    fprintf( pErr, "usage: fpga [-D float] [-apvh]\n" );
-    fprintf( pErr, "\t        performs FPGA mapping of the current network\n" );
-    fprintf( pErr, "\t-a    : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
-    fprintf( pErr, "\t-p    : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
-    fprintf( pErr, "\t-D    : sets the required time for the mapping [default = %s]\n", Buffer );  
-    fprintf( pErr, "\t-v    : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h    : prints the command usage\n");
+    if ( nLutSize == -1 ) 
+        sprintf( LutSize, "library" );
+    else
+        sprintf( LutSize, "%d", nLutSize );
+    fprintf( pErr, "usage: fpga [-D float] [-K num] [-apvh]\n" );
+    fprintf( pErr, "\t           performs FPGA mapping of the current network\n" );
+    fprintf( pErr, "\t-a       : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
+    fprintf( pErr, "\t-p       : optimizes power by minimizing switching activity [default = %s]\n", fSwitching? "yes": "no" );
+    fprintf( pErr, "\t-D float : sets the required time for the mapping [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-K num   : the number of LUT inputs [default = %s]%s\n", LutSize, (nLutSize == -1 ? " (type \"print_lut\")" : "") );
+    fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h       : prints the command usage\n");
     return 1;
 }
 
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 2752dc69..f5fe2629 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -314,7 +314,7 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree )
 {
     Abc_Obj_t * pFanin;
     int fDagNode, fTriv, TreeCode = 0;
-    assert( Abc_NtkIsStrash(pObj->pNtk) );
+//    assert( Abc_NtkIsStrash(pObj->pNtk) );
     assert( Abc_ObjFaninNum(pObj) == 2 );
     // check if the node is a DAG node
     fDagNode = (Abc_ObjFanoutNum(pObj) > 1 && !Abc_NodeIsMuxControlType(pObj));
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 0108b520..a04f3d9c 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -85,7 +85,9 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 
 //    Ivy_MffcTest( pMan );
     Ivy_ManPrintStats( pMan );
-    Ivy_ManSeqRewrite( pMan, 0, 0 );
+//    Ivy_ManSeqRewrite( pMan, 0, 0 );
+//    Ivy_ManTestCutsAlg( pMan );
+    Ivy_ManTestCutsBool( pMan );
     Ivy_ManPrintStats( pMan );
 
     // convert from the AIG manager
diff --git a/src/base/abci/abcLut.c b/src/base/abci/abcLut.c
new file mode 100644
index 00000000..165d84c5
--- /dev/null
+++ b/src/base/abci/abcLut.c
@@ -0,0 +1,786 @@
+/**CFile****************************************************************
+
+  FileName    [abcLut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Superchoicing for K-LUTs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+#define SCL_LUT_MAX          6   // the maximum LUT size
+#define SCL_VARS_MAX        15   // the maximum number of variables
+#define SCL_NODE_MAX      1000   // the maximum number of nodes
+
+typedef struct Abc_ManScl_t_ Abc_ManScl_t;
+struct Abc_ManScl_t_
+{
+    // paramers
+    int                nLutSize;    // the LUT size
+    int                nCutSizeMax; // the max number of leaves of the cone
+    int                nNodesMax;   // the max number of divisors in the cone
+    int                nWords;      // the number of machine words in sim info
+    // structural representation of the cone
+    Vec_Ptr_t *        vLeaves;     // leaves of the cut
+    Vec_Ptr_t *        vVolume;     // volume of the cut
+    int                pBSet[SCL_VARS_MAX]; // bound set
+    // functional representation of the cone
+    unsigned *         uTruth;      // truth table of the cone
+    // representation of truth tables
+    unsigned **        uVars;       // elementary truth tables
+    unsigned **        uSims;       // truth tables of the nodes
+    unsigned **        uCofs;       // truth tables of the cofactors
+};
+
+static Vec_Ptr_t * s_pLeaves = NULL;
+
+static Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize );
+static Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax );
+static void Abc_ManSclStop( Abc_ManScl_t * p );
+static void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj );
+
+static Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * pManScl, Abc_Obj_t * pObj );
+static int Abc_NodeDecomposeStep( Abc_ManScl_t * pManScl );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for K-LUTs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkSuperChoiceLut( Abc_Ntk_t * pNtk, int nLutSize, int nCutSizeMax, int fVerbose )
+{
+    ProgressBar * pProgress;
+    Abc_ManCut_t * pManCut;
+    Abc_ManScl_t * pManScl;
+    Cut_Man_t * pManCuts;
+    Abc_Obj_t * pObj, * pFanin, * pObjTop;
+    int i, LevelMax, nNodes;
+    int nNodesTried, nNodesDec, nNodesExist, nNodesUsed;
+
+    assert( Abc_NtkIsSopLogic(pNtk) );
+    if ( nLutSize < 3 || nLutSize > SCL_LUT_MAX )
+    {
+        printf( "LUT size (%d) does not belong to the interval: 3 <= LUT size <= %d\n", nLutSize, SCL_LUT_MAX );
+        return 0;
+    }
+    if ( nCutSizeMax <= nLutSize || nCutSizeMax > SCL_VARS_MAX )
+    {
+        printf( "Cut size (%d) does not belong to the interval: LUT size (%d) < Cut size <= %d\n", nCutSizeMax, nLutSize, SCL_VARS_MAX );
+        return 0;
+    }
+
+    assert( nLutSize <= SCL_LUT_MAX );
+    assert( nCutSizeMax <= SCL_VARS_MAX );
+    nNodesTried = nNodesDec = nNodesExist = nNodesUsed = 0;
+
+    // set the delays of the CIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->Level = 0;
+
+//Abc_NtkGetLevelNum( pNtk );
+ 
+    // start the managers
+    pManScl = Abc_ManSclStart( nLutSize, nCutSizeMax, 1000 );
+    pManCuts = Abc_NtkStartCutManForScl( pNtk, nLutSize );
+    pManCut = Abc_NtkManCutStart( nCutSizeMax, 100000, 100000, 100000 );
+    s_pLeaves = Abc_NtkManCutReadCutSmall( pManCut );
+    pManScl->vVolume = Abc_NtkManCutReadVisited( pManCut );
+
+    // process each internal node (assuming topological order of nodes!!!)
+    nNodes = Abc_NtkObjNumMax(pNtk);
+    pProgress = Extra_ProgressBarStart( stdout, nNodes );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+//        if ( i != nNodes-1 )
+//            continue;
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( i >= nNodes )
+            break;
+        if ( Abc_ObjFaninNum(pObj) != 2 )
+            continue;
+        nNodesTried++;
+
+        // map this node using regular cuts
+//        pObj->Level = 0;
+        Abc_NodeLutMap( pManCuts, pObj );
+        // compute the cut
+        pManScl->vLeaves = Abc_NodeFindCut( pManCut, pObj, 0 );
+        if ( Vec_PtrSize(pManScl->vLeaves) <= nLutSize )
+            continue;
+        // get the volume of the cut
+        if ( Vec_PtrSize(pManScl->vVolume) > SCL_NODE_MAX )
+            continue;
+        nNodesDec++;
+
+        // decompose the cut
+        pObjTop = Abc_NodeSuperChoiceLut( pManScl, pObj );
+        if ( pObjTop == NULL )
+            continue;
+        nNodesExist++;
+
+        // if there is no delay improvement, skip; otherwise, update level
+        if ( pObjTop->Level >= pObj->Level )
+        {
+            Abc_NtkDeleteObj_rec( pObjTop );
+            continue;
+        }
+        pObj->Level = pObjTop->Level;
+        nNodesUsed++;
+    }
+    Extra_ProgressBarStop( pProgress );
+
+    // delete the managers
+    Abc_ManSclStop( pManScl );
+    Abc_NtkManCutStop( pManCut );
+    Cut_ManStop( pManCuts );
+
+    // get the largest arrival time
+    LevelMax = 0;
+    Abc_NtkForEachCo( pNtk, pObj, i )
+    {
+        pFanin = Abc_ObjFanin0( pObj );
+        // skip inv/buf
+        if ( Abc_ObjFaninNum(pFanin) == 1 )
+            pFanin = Abc_ObjFanin0( pFanin );
+        // get the new level
+        LevelMax = ABC_MAX( LevelMax, (int)pFanin->Level );
+    }
+
+    if ( fVerbose )
+    printf( "Try = %d. Dec = %d. Exist = %d. Use = %d. SUPER = %d levels of %d-LUTs.\n", 
+        nNodesTried, nNodesDec, nNodesExist, nNodesUsed, LevelMax, nLutSize );
+//    if ( fVerbose )
+//    printf( "The network is superchoiced for %d levels of %d-LUTs.\n", LevelMax, nLutSize );
+
+    // clean the data field
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pNext = NULL;
+
+    // check
+    if ( !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkSuperChoiceLut: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs LUT mapping of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeLutMap( Cut_Man_t * pManCuts, Abc_Obj_t * pObj )
+{
+    Cut_Cut_t * pCut;
+    Abc_Obj_t * pFanin;
+    int i, DelayMax;
+    pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCuts, pObj, 0, 0 );
+    assert( pCut != NULL );
+    assert( pObj->Level == 0 );
+    // go through the cuts
+    pObj->Level = ABC_INFINITY;
+    for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
+    {
+        DelayMax = 0;
+        for ( i = 0; i < (int)pCut->nLeaves; i++ )
+        {
+            pFanin = Abc_NtkObj( pObj->pNtk, pCut->pLeaves[i] );
+//            assert( Abc_ObjIsCi(pFanin) || pFanin->Level > 0 ); // should hold if node ordering is topological
+            if ( DelayMax < (int)pFanin->Level )
+                DelayMax = pFanin->Level;
+        }
+        if ( (int)pObj->Level > DelayMax )
+            pObj->Level = DelayMax;
+    }
+    assert( pObj->Level < ABC_INFINITY );
+    pObj->Level++;
+//    printf( "%d(%d) ", pObj->Id, pObj->Level );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut manager for rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkStartCutManForScl( Abc_Ntk_t * pNtk, int nLutSize )
+{
+    static Cut_Params_t Params, * pParams = &Params;
+    Cut_Man_t * pManCut;
+    Abc_Obj_t * pObj;
+    int i;
+    // start the cut manager
+    memset( pParams, 0, sizeof(Cut_Params_t) );
+    pParams->nVarsMax  = nLutSize; // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 500;   // the max number of cuts kept at a node
+    pParams->fTruth    = 0;     // compute truth tables
+    pParams->fFilter   = 1;     // filter dominated cuts
+    pParams->fSeq      = 0;     // compute sequential cuts
+    pParams->fDrop     = 0;     // drop cuts on the fly
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    pParams->nIdsMax   = Abc_NtkObjNumMax( pNtk );
+    pManCut = Cut_ManStart( pParams );
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( pManCut, pObj->Id );
+    return pManCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManScl_t * Abc_ManSclStart( int nLutSize, int nCutSizeMax, int nNodesMax )
+{
+    Abc_ManScl_t * p;
+    int i, k;
+    assert( sizeof(unsigned) == 4 );
+    p = ALLOC( Abc_ManScl_t, 1 );
+    memset( p, 0, sizeof(Abc_ManScl_t) );
+    p->nLutSize    = nLutSize;
+    p->nCutSizeMax = nCutSizeMax;
+    p->nNodesMax   = nNodesMax;
+    p->nWords      = Extra_TruthWordNum(nCutSizeMax);
+    // allocate simulation info
+    p->uVars = (unsigned **)Extra_ArrayAlloc( nCutSizeMax, p->nWords, 4 );
+    p->uSims = (unsigned **)Extra_ArrayAlloc( nNodesMax, p->nWords, 4 );
+    p->uCofs = (unsigned **)Extra_ArrayAlloc( 2 << nLutSize, p->nWords, 4 );
+    memset( p->uVars[0], 0, nCutSizeMax * p->nWords * 4 );
+    // assign elementary truth tables
+    for ( k = 0; k < p->nCutSizeMax; k++ )
+        for ( i = 0; i < p->nWords * 32; i++ )
+            if ( i & (1 << k) )
+                p->uVars[k][i>>5] |= (1 << (i&31));
+    // other data structures
+//    p->vBound = Vec_IntAlloc( nCutSizeMax );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManSclStop( Abc_ManScl_t * p )
+{
+//    Vec_IntFree( p->vBound );
+    free( p->uVars );
+    free( p->uSims );
+    free( p->uCofs );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Abc_NodeSuperChoiceTruth( Abc_ManScl_t * pManScl )
+{
+    Abc_Obj_t * pObj;
+    unsigned * puData0, * puData1, * puData;
+    char * pSop;
+    int i, k;
+    // set elementary truth tables
+    Vec_PtrForEachEntry( pManScl->vLeaves, pObj, i )
+        pObj->pNext = (Abc_Obj_t *)pManScl->uVars[i];
+    // compute truth tables for internal nodes
+    Vec_PtrForEachEntry( pManScl->vVolume, pObj, i )
+    {
+        // set storage for the node's simulation info
+        pObj->pNext = (Abc_Obj_t *)pManScl->uSims[i];
+        // get pointer to the simulation info
+        puData  = (unsigned *)pObj->pNext;
+        puData0 = (unsigned *)Abc_ObjFanin0(pObj)->pNext;
+        puData1 = (unsigned *)Abc_ObjFanin1(pObj)->pNext;
+        // simulate
+        pSop = pObj->pData;
+        if ( pSop[0] == '0' && pSop[1] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = ~puData0[k] & ~puData1[k];
+        else if ( pSop[0] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = ~puData0[k] & puData1[k];
+        else if ( pSop[1] == '0' )
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = puData0[k] & ~puData1[k];
+        else 
+            for ( k = 0; k < pManScl->nWords; k++ )
+                puData[k] = puData0[k] & puData1[k];
+    }
+    return puData;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vVolume )
+{
+    if ( pObj->fMarkC )
+        return;
+    pObj->fMarkC = 1;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin0(pObj), vVolume );
+    Abc_NodeSuperChoiceCollect2_rec( Abc_ObjFanin1(pObj), vVolume );
+    Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect2( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 1;
+    Vec_PtrClear( vVolume );
+    Abc_NodeSuperChoiceCollect2_rec( pRoot, vVolume );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 0;
+    Vec_PtrForEachEntry( vVolume, pObj, i )
+        pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    if ( pObj->fMarkB )
+    {
+        Vec_PtrPush( vLeaves, pObj );
+        pObj->fMarkB = 0;
+    }
+    if ( pObj->fMarkC )
+        return;
+    pObj->fMarkC = 1;
+    assert( Abc_ObjFaninNum(pObj) == 2 );
+    Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin0(pObj), vLeaves, vVolume );
+    Abc_NodeSuperChoiceCollect_rec( Abc_ObjFanin1(pObj), vLeaves, vVolume );
+    Vec_PtrPush( vVolume, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description [Orders the leaves topologically.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoiceCollect( Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVolume )
+{
+    Abc_Obj_t * pObj;
+    int i, nLeaves;
+    nLeaves = Vec_PtrSize(vLeaves);
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkB = pObj->fMarkC = 1;
+    Vec_PtrClear( vVolume );
+    Vec_PtrClear( vLeaves );
+    Abc_NodeSuperChoiceCollect_rec( pRoot, vLeaves, vVolume );
+    assert( Vec_PtrSize(vLeaves) == nLeaves );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+        pObj->fMarkC = 0;
+    Vec_PtrForEachEntry( vVolume, pObj, i )
+        pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeLeavesRemove( Vec_Ptr_t * vLeaves, unsigned uPhase, int nVars )
+{
+    int i;
+    for ( i = nVars - 1; i >= 0; i-- )
+        if ( uPhase & (1 << i) )
+            Vec_PtrRemove( vLeaves, Vec_PtrEntry(vLeaves, i) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeGetLevel( Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i, Level;
+    Level = 0;
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Level = ABC_MAX( Level, (int)pFanin->Level );
+    return Level + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeSuperChoiceLut( Abc_ManScl_t * p, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin, * pObjNew;
+    int i, nVars, uSupport, nSuppVars;
+    // collect the cone using DFS (excluding leaves)
+    Abc_NodeSuperChoiceCollect2( pObj, p->vLeaves, p->vVolume );
+    assert( Vec_PtrEntryLast(p->vVolume) == pObj );  
+    // compute the truth table
+    p->uTruth = Abc_NodeSuperChoiceTruth( p );
+    // get the support of this truth table
+    nVars = Vec_PtrSize(p->vLeaves);
+    uSupport = Extra_TruthSupport(p->uTruth, nVars);
+    nSuppVars = Extra_WordCountOnes(uSupport);
+    assert( nSuppVars <= nVars );
+    if ( nSuppVars == 0 )
+    {
+        pObj->Level = 0;
+        return NULL;
+    }
+    if ( nSuppVars == 1 )
+    {
+        // find the variable
+        for ( i = 0; i < nVars; i++ )
+            if ( uSupport & (1 << i) )
+                break;
+        assert( i < nVars );
+        pFanin = Vec_PtrEntry( p->vLeaves, i );
+        pObj->Level = pFanin->Level;
+        return NULL;
+    }
+    // support-minimize the truth table
+    if ( nSuppVars != nVars )
+    {
+        Extra_TruthShrink( p->uCofs[0], p->uTruth, nSuppVars, nVars, uSupport );
+        Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+        Abc_NodeLeavesRemove( p->vLeaves, ((1 << nVars) - 1) & ~uSupport, nVars );
+    }
+//    return NULL;
+    // decompose the truth table recursively
+    while ( Vec_PtrSize(p->vLeaves) > p->nLutSize )
+        if ( !Abc_NodeDecomposeStep( p ) )
+        {
+            Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+                if ( Abc_ObjIsNode(pFanin) && Abc_ObjFanoutNum(pFanin) == 0 )
+                    Abc_NtkDeleteObj_rec( pFanin );
+            return NULL;
+        }
+    // create the topmost node
+    pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pFanin, i )
+        Abc_ObjAddFanin( pObjNew, pFanin );
+    // create the function
+    pObjNew->pData = Abc_SopCreateFromTruth( pObj->pNtk->pManFunc, Vec_PtrSize(p->vLeaves), p->uTruth ); // need ISOP
+    pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in increasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeCompareLevelsInc( int * pp1, int * pp2 )
+{
+    Abc_Obj_t * pNode1, * pNode2;
+    pNode1 = Vec_PtrEntry(s_pLeaves, *pp1);
+    pNode2 = Vec_PtrEntry(s_pLeaves, *pp2);
+    if ( pNode1->Level < pNode2->Level )
+        return -1;
+    if ( pNode1->Level > pNode2->Level ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Selects the earliest arriving nodes from the array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeDecomposeSort( Abc_Obj_t ** pLeaves, int nVars, int * pBSet, int nLutSize )
+{
+    Abc_Obj_t * pTemp[SCL_VARS_MAX];
+    int i, k, kBest, LevelMin;
+    assert( nLutSize < nVars );
+    assert( nVars <= SCL_VARS_MAX );
+    // copy nodes into the internal storage
+//    printf( "(" );
+    for ( i = 0; i < nVars; i++ )
+    {
+        pTemp[i] = pLeaves[i];
+//        printf( " %d", pLeaves[i]->Level );
+    }
+//    printf( " )\n" );
+    // choose one node at a time
+    for ( i = 0; i < nLutSize; i++ )
+    {
+        kBest = -1;
+        LevelMin = ABC_INFINITY;
+        for ( k = 0; k < nVars; k++ )
+            if ( pTemp[k] && LevelMin > (int)pTemp[k]->Level )
+            {
+                LevelMin = pTemp[k]->Level;
+                kBest = k;
+            }
+        pBSet[i] = kBest;
+        pTemp[kBest] = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs superchoicing for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeDecomposeStep( Abc_ManScl_t * p )
+{
+    static char pCofClasses[1<<SCL_LUT_MAX][1<<SCL_LUT_MAX];
+    static char nCofClasses[1<<SCL_LUT_MAX];
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObjNew, * pFanin, * pNodesNew[SCL_LUT_MAX];
+    unsigned * pTruthCof, * pTruthClass, * pTruth, uPhase;
+    int i, k, c, v, w, nVars, nVarsNew, nClasses, nCofs;
+    // set the network
+    pNtk = ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, 0))->pNtk;
+    // find the earliest nodes
+    nVars = Vec_PtrSize(p->vLeaves);
+    assert( nVars > p->nLutSize );
+/*
+    for ( v = 0; v < nVars; v++ )
+        p->pBSet[v] = v;
+    qsort( (void *)p->pBSet, nVars, sizeof(int), 
+            (int (*)(const void *, const void *)) Abc_NodeCompareLevelsInc );
+*/
+    Abc_NodeDecomposeSort( (Abc_Obj_t **)Vec_PtrArray(p->vLeaves), Vec_PtrSize(p->vLeaves), p->pBSet, p->nLutSize );
+    assert( ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[0]))->Level <=
+        ((Abc_Obj_t *)Vec_PtrEntry(p->vLeaves, p->pBSet[1]))->Level );
+    // cofactor w.r.t. the selected variables
+    Extra_TruthCopy( p->uCofs[1], p->uTruth, nVars );
+    c = 2;
+    for ( v = 0; v < p->nLutSize; v++ )
+        for ( k = 0; k < (1<<v); k++ )
+        {
+            Extra_TruthCopy( p->uCofs[c], p->uCofs[c/2], nVars );
+            Extra_TruthCopy( p->uCofs[c+1], p->uCofs[c/2], nVars );
+            Extra_TruthCofactor0( p->uCofs[c], nVars, p->pBSet[v] );
+            Extra_TruthCofactor1( p->uCofs[c+1], nVars, p->pBSet[v] );
+            c += 2;
+        }
+    assert( c == (2 << p->nLutSize) );
+    // count unique cofactors
+    nClasses = 0;
+    nCofs = (1 << p->nLutSize);
+    for ( i = 0; i < nCofs; i++ )
+    {
+        pTruthCof = p->uCofs[ nCofs + i ];
+        for ( k = 0; k < nClasses; k++ )
+        {
+            pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+            if ( Extra_TruthIsEqual( pTruthCof, pTruthClass, nVars ) )
+            {
+                pCofClasses[k][ nCofClasses[k]++ ] = i;
+                break;
+            }
+        }
+        if ( k != nClasses )
+            continue;
+        // not found
+        pCofClasses[nClasses][0] = i;
+        nCofClasses[nClasses] = 1;
+        nClasses++;
+        if ( nClasses > nCofs/2 )
+            return 0;
+    }
+    // the number of cofactors is acceptable
+    nVarsNew = Extra_Base2Log( nClasses );
+    assert( nVarsNew < p->nLutSize );
+    // create the remainder truth table
+    // for each class of cofactors, multiply cofactor truth table by its code
+    Extra_TruthClear( p->uTruth, nVars );
+    for ( k = 0; k < nClasses; k++ )
+    {
+        pTruthClass = p->uCofs[ nCofs + pCofClasses[k][0] ];
+        for ( v = 0; v < nVarsNew; v++ )
+            if ( k & (1 << v) )
+                Extra_TruthAnd( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+            else
+                Extra_TruthSharp( pTruthClass, pTruthClass, p->uVars[p->pBSet[v]], nVars );
+        Extra_TruthOr( p->uTruth, p->uTruth, pTruthClass, nVars );
+    }
+    // create nodes
+    pTruth = p->uCofs[0];
+    for ( v = 0; v < nVarsNew; v++ )
+    {
+        Extra_TruthClear( pTruth, p->nLutSize );
+        for ( k = 0; k < nClasses; k++ )
+            if ( k & (1 << v) )
+                for ( i = 0; i < nCofClasses[k]; i++ )
+                {
+                    pTruthCof = p->uCofs[1];
+                    Extra_TruthFill( pTruthCof, p->nLutSize );
+                    for ( w = 0; w < p->nLutSize; w++ )
+                        if ( pCofClasses[k][i] & (1 << (p->nLutSize-1-w)) )
+                            Extra_TruthAnd( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+                        else
+                            Extra_TruthSharp( pTruthCof, pTruthCof, p->uVars[w], p->nLutSize );
+                    Extra_TruthOr( pTruth, pTruth, pTruthCof, p->nLutSize );
+                }
+        // implement the node
+        pObjNew = Abc_NtkCreateNode( pNtk );
+        for ( i = 0; i < p->nLutSize; i++ )
+        {
+            pFanin = Vec_PtrEntry( p->vLeaves, p->pBSet[i] );
+            Abc_ObjAddFanin( pObjNew, pFanin );
+        }
+        // create the function
+        pObjNew->pData = Abc_SopCreateFromTruth( pNtk->pManFunc, p->nLutSize, pTruth ); // need ISOP
+        pObjNew->Level = Abc_NodeGetLevel( pObjNew );
+        pNodesNew[v] = pObjNew;
+    }
+    // put the new nodes back into the list
+    for ( v = 0; v < nVarsNew; v++ )
+        Vec_PtrWriteEntry( p->vLeaves, p->pBSet[v], pNodesNew[v] );
+    // compute the variables that should be removed
+    uPhase = 0;
+    for ( v = nVarsNew; v < p->nLutSize; v++ )
+        uPhase |= (1 << p->pBSet[v]);
+    // remove entries from the array
+    Abc_NodeLeavesRemove( p->vLeaves, uPhase, nVars );
+    // update truth table
+    Extra_TruthShrink( p->uCofs[0], p->uTruth, nVars - p->nLutSize + nVarsNew, nVars, ((1 << nVars) - 1) & ~uPhase );
+    Extra_TruthCopy( p->uTruth, p->uCofs[0], nVars );
+    assert( !Extra_TruthVarInSupport( p->uTruth, nVars, nVars - p->nLutSize + nVarsNew ) );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index f95591ab..48b9eeda 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -135,18 +135,18 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
     }
 */
 
-/*
+
     // print the statistic into a file
     {
         FILE * pTable;
-        pTable = fopen( "stats.txt", "a+" );
+        pTable = fopen( "fpga_stats.txt", "a+" );
         fprintf( pTable, "%s ",  pNtk->pName );
         fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) );
         fprintf( pTable, "%d ", Abc_AigGetLevelNum(pNtk) );
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
-*/
+
 /*
     // print the statistic into a file
     {
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index e5b9e024..10400129 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -321,7 +321,8 @@ int Abc_NodeBuildCutLevelOne_int( Vec_Ptr_t * vVisited, Vec_Ptr_t * vLeaves, int
     {
         CostCur = Abc_NodeGetLeafCostOne( pNode, nFaninLimit );
 //printf( "    Fanin %s has cost %d.\n", Abc_ObjName(pNode), CostCur );
-        if ( CostBest > CostCur )
+        if ( CostBest > CostCur ||
+             (CostBest == CostCur && pNode->Level > pFaninBest->Level) )
         {
             CostBest   = CostCur;
             pFaninBest = pNode;
@@ -643,6 +644,22 @@ Vec_Ptr_t * Abc_NtkManCutReadCutLarge( Abc_ManCut_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Ptr_t * Abc_NtkManCutReadCutSmall( Abc_ManCut_t * p )
+{
+    return p->vNodeLeaves;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the leaves of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Ptr_t * Abc_NtkManCutReadVisited( Abc_ManCut_t * p )
 {
     return p->vVisited;
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index c297180d..5d35678d 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -11,7 +11,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
         src/base/abci/abcGen.c \
-    src/base/abci/abcIvy.c \
+    src/base/abci/abcLut.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \