Version abc50806

13 files changed, 840 insertions, 10 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index f9bcde33..1179e400 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -22,6 +22,7 @@
 #include "mainInt.h"
 #include "ft.h"
 #include "fraig.h"
+#include "fxu.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -37,6 +38,7 @@ static int Ntk_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Ntk_CommandBalance      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Ntk_CommandRenode       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Ntk_CommandCleanup      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Ntk_CommandFx           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Ntk_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Ntk_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -55,6 +57,7 @@ static int Ntk_CommandFraigSweep   ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Ntk_CommandMap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Ntk_CommandUnmap        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Ntk_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Ntk_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Ntk_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -88,6 +91,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Ntk_CommandBalance,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Ntk_CommandRenode,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Ntk_CommandCleanup,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Ntk_CommandFx,               1 );
 
     Cmd_CommandAdd( pAbc, "Various",      "logic",         Ntk_CommandLogic,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Ntk_CommandMiter,            1 );
@@ -106,6 +110,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Ntk_CommandMap,              1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Ntk_CommandUnmap,            1 );
     Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Ntk_CommandAttach,           1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Ntk_CommandSuperChoice,      1 );
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Ntk_CommandFpga,             1 );
 
@@ -750,6 +755,127 @@ usage:
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_CommandFx( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    FILE * pOut, * pErr;
+    Fxu_Data_t * p = NULL;
+    int c;
+    extern bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
+    extern void Abc_NtkFxuFreeInfo( Fxu_Data_t * p );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // allocate the structure
+    p = ALLOC( Fxu_Data_t, 1 );
+    memset( p, 0, sizeof(Fxu_Data_t) );
+    // set the defaults
+    p->nPairsMax = 30000;
+    p->nNodesExt = 10000;
+    p->fOnlyS    = 0;
+    p->fOnlyD    = 0;
+    p->fUse0     = 0;
+    p->fUseCompl = 1;
+    p->fVerbose  = 0;
+    util_getopt_reset();
+    while ( (c = util_getopt(argc, argv, "lnsdzcvh")) != EOF ) 
+    {
+        switch (c) 
+        {
+            case 'l':
+                if ( util_optind >= argc )
+                {
+                    fprintf( pErr, "Command line switch \"-l\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                p->nPairsMax = atoi(argv[util_optind]);
+                util_optind++;
+                if ( p->nPairsMax < 0 ) 
+                    goto usage;
+                break;
+            case 'n':
+                if ( util_optind >= argc )
+                {
+                    fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
+                    goto usage;
+                }
+                p->nNodesExt = atoi(argv[util_optind]);
+                util_optind++;
+                if ( p->nNodesExt < 0 ) 
+                    goto usage;
+                break;
+            case 's':
+                p->fOnlyS ^= 1;
+                break;
+            case 'd':
+                p->fOnlyD ^= 1;
+                break;
+            case 'z':
+                p->fUse0 ^= 1;
+                break;
+            case 'c':
+                p->fUseCompl ^= 1;
+                break;
+            case 'v':
+                p->fVerbose ^= 1;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        Abc_NtkFxuFreeInfo( p );
+        return 1;
+    }
+
+    if ( Abc_NtkNodeNum(pNtk) == 0 )
+    {
+        fprintf( pErr, "The network does not have internal nodes.\n" );
+        Abc_NtkFxuFreeInfo( p );
+        return 1;
+    }
+
+    // the nodes to be merged are linked into the special linked list
+    Abc_NtkFastExtract( pNtk, p );
+    Abc_NtkFxuFreeInfo( p );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: fx [-n num] [-l num] [-sdzcvh]\n");
+    fprintf( pErr, "\t         performs unate fast extract on the current network\n");
+    fprintf( pErr, "\t-n num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );  
+    fprintf( pErr, "\t-l num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax );  
+    fprintf( pErr, "\t-s     : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" );  
+    fprintf( pErr, "\t-d     : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );  
+    fprintf( pErr, "\t-z     : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );  
+    fprintf( pErr, "\t-c     : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" );  
+    fprintf( pErr, "\t-v     : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" ); 
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    Abc_NtkFxuFreeInfo( p );
+    return 1;       
+}
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1189,6 +1315,7 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Fraig_Params_t Params;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
+    int fAllNodes;
     int c;
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -1196,6 +1323,7 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fAllNodes = 0;
     Params.nPatsRand  = 2048; // the number of words of random simulation info
     Params.nPatsDyna  = 2048; // the number of words of dynamic simulation info
     Params.nBTLimit   = 99;   // the max number of backtracks to perform
@@ -1208,7 +1336,7 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Params.fVerbose   =  0;   // the verbosiness flag
     Params.fVerboseP  =  0;   // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "RDBrscpvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "RDBrscpvah" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1262,7 +1390,9 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             Params.fVerbose ^= 1;
             break;
-
+        case 'a':
+            fAllNodes ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -1286,11 +1416,11 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsAig(pNtk) )
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, 0 );
+        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
     else
     {
         pNtk = Abc_NtkStrash( pNtk );
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, 0 );
+        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -1308,7 +1438,7 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     sprintf( Buffer, "%d", Params.nBTLimit );
-    fprintf( pErr, "usage: fraig [-R num] [-D num] [-B num] [-rscpvh]\n" );
+    fprintf( pErr, "usage: fraig [-R num] [-D num] [-B num] [-rscpvah]\n" );
     fprintf( pErr, "\t         transforms a logic network into a functionally reduced AIG\n" );
     fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n",     Params.nPatsRand );
     fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", Params.nPatsDyna );
@@ -1318,6 +1448,7 @@ usage:
     fprintf( pErr, "\t-c     : toggle accumulation of choices [default = %s]\n",              Params.fChoicing? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle proving the final miter [default = %s]\n",              Params.fTryProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n",                       Params.fVerbose?  "yes": "no" );
+    fprintf( pErr, "\t-a     : toggle between all nodes and DFS nodes [default = %s]\n",      fAllNodes? "all": "dfs" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -1890,6 +2021,72 @@ usage:
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntk_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "Works only for the AIG representation.\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkSuperChoice( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Superchoicing has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: sc [-h]\n" );
+    fprintf( pErr, "\t        performs superchoicing\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index d918cbc2..35fa85e9 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -480,6 +480,7 @@ extern bool               Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose );
 extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
+extern char *             Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars );
 extern int                Abc_SopGetCubeNum( char * pSop );
 extern int                Abc_SopGetLitNum( char * pSop );
 extern int                Abc_SopGetVarNum( char * pSop );
diff --git a/src/base/abc/abcAttach.c b/src/base/abc/abcAttach.c
index 9d9c378f..950ecc1d 100644
--- a/src/base/abc/abcAttach.c
+++ b/src/base/abc/abcAttach.c
@@ -267,6 +267,8 @@ void Abc_AttachComputeTruth( char * pSop, unsigned uTruthsIn[][2], unsigned * uT
             }
             uTruthRes[0] |= uSignCube[0];
         }
+        if ( Abc_SopGetPhase(pSop) == 0 )
+            uTruthRes[0] = ~uTruthRes[0];
         if ( nInputs < 5 )
             uTruthRes[0] &= ATTACH_MASK(1<<nInputs);
     }
@@ -295,6 +297,13 @@ void Abc_AttachComputeTruth( char * pSop, unsigned uTruthsIn[][2], unsigned * uT
             uTruthRes[0] |= uSignCube[0];
             uTruthRes[1] |= uSignCube[1];
         }
+
+        // complement if the SOP is complemented
+        if ( Abc_SopGetPhase(pSop) == 0 )
+        {
+            uTruthRes[0] = ~uTruthRes[0];
+            uTruthRes[1] = ~uTruthRes[1];
+        }
     }
 }
 
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 7b330b95..5c75a94c 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -223,9 +223,12 @@ int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk )
     }
     else
     {
-        Abc_NtkForEachCo( pNtk, pNode, i )
+//        Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_NtkForEachNode( pNtk, pNode, i )
         {
-            pDriver = Abc_ObjFanin0( pNode );
+//            pDriver = Abc_ObjFanin0( pNode );
+            pDriver = pNode;
+
             Abc_NtkGetLevelNum_rec( pDriver );
             if ( LevelsMax < pDriver->Level )
                 LevelsMax = pDriver->Level;
diff --git a/src/base/abc/abcFxu.c b/src/base/abc/abcFxu.c
new file mode 100644
index 00000000..99f37dfc
--- /dev/null
+++ b/src/base/abc/abcFxu.c
@@ -0,0 +1,262 @@
+/**CFile****************************************************************
+
+  FileName    [abcFxu.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface with the fast extract package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcFxu.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fxu.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static bool Abc_NtkFxuCheck( Abc_Ntk_t * pNtk );
+static void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
+static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast_extract on the current network.]
+
+  Description [Takes the network and the maximum number of nodes to extract.
+  Uses the concurrent double-cube and single cube divisor extraction procedure.
+  Modifies the network in the end, after extracting all nodes. Note that 
+  Ntk_NetworkSweep() may increase the performance of this procedure because 
+  the single-literal nodes will not be created in the sparse matrix. Returns 1 
+  if the network has been changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
+{
+    assert( Abc_NtkIsLogicBdd(pNtk) || Abc_NtkIsLogicSop(pNtk) );
+    // convert nodes to SOPs
+    if ( Abc_NtkIsLogicBdd(pNtk) )
+        Abc_NtkBddToSop(pNtk);
+    else
+    { // to make sure the SOPs are SCC-free
+//        Abc_NtkSopToBdd(pNtk);
+//        Abc_NtkBddToSop(pNtk);
+    }
+    // check if the network meets the requirements
+    if ( !Abc_NtkFxuCheck(pNtk) )
+    {
+        printf( "Abc_NtkFastExtract: Nodes have duplicated or complemented fanins. FXU is not performed.\n" );
+        return 0;
+    }
+    // sweep removes useless nodes
+    Abc_NtkCleanup( pNtk, 0 );
+    // collect information about the covers
+    // make sure all covers are SCC free
+    // allocate literal array for each cover
+    Abc_NtkFxuCollectInfo( pNtk, p );
+    // call the fast extract procedure
+    // returns the number of divisor extracted
+    if ( Fxu_FastExtract(p) > 0 )
+    {
+        // update the network
+        Abc_NtkFxuReconstruct( pNtk, p );
+        // make sure everything is okay
+        if ( !Abc_NtkCheck( pNtk ) )
+            printf( "Abc_NtkFastExtract: The network check has failed.\n" );
+        return 1;
+    }
+    return 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Makes sure the nodes do not have complemented and duplicated fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+bool Abc_NtkFxuCheck( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode, * pFanin1, * pFanin2;
+    int n, i, k;
+    Abc_NtkForEachNode( pNtk, pNode, n )
+    {
+        Abc_ObjForEachFanin( pNode, pFanin1, i )
+        {
+            if ( Abc_ObjFaninC(pNode, i) )
+                return 0;
+            Abc_ObjForEachFanin( pNode, pFanin2, k )
+            {
+                if ( i == k )
+                    continue;
+                if ( pFanin1 == pFanin2 )
+                    return 0;
+            }
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect information about the network for fast_extract.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFxuCollectInfo( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // add information to the manager
+    p->pManSop    = pNtk->pManFunc;
+    p->vSops      = Vec_PtrAlloc(0);
+    p->vFanins    = Vec_PtrAlloc(0);
+    p->vSopsNew   = Vec_PtrAlloc(0);
+    p->vFaninsNew = Vec_PtrAlloc(0);
+    Vec_PtrFill( p->vSops,      pNtk->vObjs->nSize, NULL );
+    Vec_PtrFill( p->vFanins,    pNtk->vObjs->nSize, NULL );
+    Vec_PtrFill( p->vSopsNew,   pNtk->vObjs->nSize + p->nNodesExt, NULL );
+    Vec_PtrFill( p->vFaninsNew, pNtk->vObjs->nSize + p->nNodesExt, NULL );
+    // add SOPs and fanin array
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_SopGetVarNum(pNode->pData) < 2 )
+            continue;
+        if ( Abc_SopGetCubeNum(pNode->pData) < 1 )
+            continue;
+        p->vSops->pArray[i]   = pNode->pData;
+        p->vFanins->pArray[i] = &pNode->vFanins;
+    }
+    p->nNodesOld = pNtk->vObjs->nSize;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
+{
+    int i;
+    // free the arrays of new fanins
+    if ( p->vFaninsNew )
+        for ( i = 0; i < p->vFaninsNew->nSize; i++ )
+            if ( p->vFaninsNew->pArray[i] )
+                Vec_IntFree( p->vFaninsNew->pArray[i] );
+    // free the arrays
+    if ( p->vSops      ) Vec_PtrFree( p->vSops      );
+    if ( p->vSopsNew   ) Vec_PtrFree( p->vSopsNew   );
+    if ( p->vFanins    ) Vec_PtrFree( p->vFanins    );
+    if ( p->vFaninsNew ) Vec_PtrFree( p->vFaninsNew );
+    FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recostructs the network after FX.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
+{
+    Vec_Fan_t * vFaninsOld;
+    Vec_Int_t * vFanins;
+    Abc_Obj_t * pNode, * pFanin;
+    int i, k;
+
+    assert( p->vFanins->nSize < p->vFaninsNew->nSize );
+    // create the new nodes
+    for ( i = p->vFanins->nSize; i < p->vFanins->nSize + p->nNodesNew; i++ )
+    {
+        // start the node
+        pNode = Abc_NtkCreateNode( pNtk );
+        assert( i == (int)pNode->Id );
+    }
+    // update the old nodes
+    for ( i = 0; i < p->vFanins->nSize; i++ )
+    {
+        // the new array of fanins
+        vFanins = p->vFaninsNew->pArray[i];
+        if ( vFanins == NULL )
+            continue;
+        // remove old fanins
+        pNode = Abc_NtkObj( pNtk, i );
+        vFaninsOld = &pNode->vFanins;
+        for ( k = vFaninsOld->nSize - 1; k >= 0; k-- )
+        {
+            pFanin = Abc_NtkObj( pNtk, vFaninsOld->pArray[k].iFan );
+            Abc_ObjDeleteFanin( pNode, pFanin );
+        }
+        // add new fanins
+        vFanins = p->vFaninsNew->pArray[i];
+        for ( k = 0; k < vFanins->nSize; k++ )
+        {
+            pFanin = Abc_NtkObj( pNtk, vFanins->pArray[k] );
+            Abc_ObjAddFanin( pNode, pFanin );
+        }
+        pNode->pData = p->vSopsNew->pArray[i];
+        assert( pNode->pData != NULL );
+    }
+    // set up the new nodes
+    for ( i = p->vFanins->nSize; i < p->vFanins->nSize + p->nNodesNew; i++ )
+    {
+        // get the new node
+        pNode = Abc_NtkObj( pNtk, i );
+        // add the fanins
+        vFanins = p->vFaninsNew->pArray[i];
+        for ( k = 0; k < vFanins->nSize; k++ )
+        {
+            pFanin = Abc_NtkObj( pNtk, vFanins->pArray[k] );
+            Abc_ObjAddFanin( pNode, pFanin );
+        }
+        pNode->pData = p->vSopsNew->pArray[i];
+        assert( pNode->pData != NULL );
+    }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c
index ca326ea1..7289b47b 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abc/abcMap.c
@@ -33,6 +33,12 @@ static Abc_Obj_t *  Abc_NodeFromMap_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNode
 static Abc_Obj_t *  Abc_NodeFromMapPhase_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, int fPhase );
 static Abc_Obj_t *  Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap, Map_Super_t * pSuper, Abc_Obj_t * pNodePis[], int nNodePis );
 static Abc_Obj_t *  Abc_NtkFixCiDriver( Abc_Obj_t * pNode );
+
+static Abc_Ntk_t *  Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk );
+static void         Abc_NodeSuperChoice( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
+static void         Abc_NodeFromMapCutPhase( Abc_Ntk_t * pNtkNew, Map_Cut_t * pCut, int fPhase );
+static Abc_Obj_t *  Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * pSuper, Abc_Obj_t * pNodePis[], int nNodePis );
+
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -53,8 +59,8 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkNew;
-
     Map_Man_t * pMan;
+    int clk;
 
     assert( Abc_NtkIsAig(pNtk) );
 
@@ -81,11 +87,13 @@ Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int
     pMan = Abc_NtkToMap( pNtk, DelayTarget, fRecovery, fVerbose );
     if ( pMan == NULL )
         return NULL;
+clk = clock();
     if ( !Map_Mapping( pMan ) )
     {
         Map_ManFree( pMan );
         return NULL;
     }
+    Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk );
 
     // reconstruct the network after mapping
     pNtkNew = Abc_NtkFromMap( pMan, pNtk );
@@ -432,6 +440,265 @@ Abc_Obj_t * Abc_NtkFixCiDriver( Abc_Obj_t * pNode )
 
 
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Interface with the mapping package.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkSuperChoice( Abc_Ntk_t * pNtk )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew;
+
+    Map_Man_t * pMan;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // check that the library is available
+    if ( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) == NULL )
+    {
+        printf( "The current library is not available.\n" );
+        return 0;
+    }
+
+    // derive the supergate library
+    if ( Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame()) == NULL && Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) )
+    {
+        printf( "A simple supergate library is derived from gate library \"%s\".\n", 
+            Mio_LibraryReadName(Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame())) );
+        Map_SuperLibDeriveFromGenlib( Abc_FrameReadLibGen(Abc_FrameGetGlobalFrame()) );
+    }
+
+    // print a warning about choice nodes
+    if ( Abc_NtkCountChoiceNodes( pNtk ) )
+        printf( "Performing mapping with choices.\n" );
+
+    // perform the mapping
+    pMan = Abc_NtkToMap( pNtk, -1, 1, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( !Map_Mapping( pMan ) )
+    {
+        Map_ManFree( pMan );
+        return NULL;
+    }
+
+    // reconstruct the network after mapping
+    pNtkNew = Abc_NtkFromMapSuperChoice( pMan, pNtk );
+    if ( pNtkNew == NULL )
+        return NULL;
+    Map_ManFree( pMan );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkMap: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkNew, * pNtkNew2;
+    Abc_Obj_t * pNode;
+    int i;
+
+    // save the pointer to the mapped nodes
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pNext = pNode->pCopy;
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        pNode->pNext = pNode->pCopy;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->pNext = pNode->pCopy;
+
+    // duplicate the network
+    pNtkNew2 = Abc_NtkDup( pNtk );
+    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1 );
+    Abc_NtkBddToSop( pNtkNew );
+
+    // set the old network to point to the new network
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = pNode->pCopy->pCopy;
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        pNode->pCopy = pNode->pCopy->pCopy;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->pCopy = pNode->pCopy->pCopy;
+    Abc_NtkDelete( pNtkNew2 );
+
+    // set the pointers from the mapper to the new nodes
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( Map_ManReadInputs(pMan)[i], 1, (char *)pNode->pCopy );
+    }
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 0, (char *)Abc_NodeCreateInv(pNtkNew,pNode->pCopy) );
+        Map_NodeSetData( (Map_Node_t *)pNode->pNext, 1, (char *)pNode->pCopy );
+    }
+
+    // assign the mapping of the required phase to the POs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_NodeIsConst(pNode) )
+            continue;
+        Abc_NodeSuperChoice( pNtkNew, pNode );
+    }
+    Extra_ProgressBarStop( pProgress );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the mapped network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeSuperChoice( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
+{
+    Map_Node_t * pMapNode = (Map_Node_t *)pNode->pNext;
+    Map_Cut_t * pCuts, * pTemp;
+
+    pCuts = Map_NodeReadCuts(pMapNode);
+    for ( pTemp = Map_CutReadNext(pCuts); pTemp; pTemp = Map_CutReadNext(pTemp) )
+    {
+        Abc_NodeFromMapCutPhase( pNtkNew, pTemp, 0 );
+        Abc_NodeFromMapCutPhase( pNtkNew, pTemp, 1 );
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the nodes corrresponding to one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFromMapCutPhase( Abc_Ntk_t * pNtkNew, Map_Cut_t * pCut, int fPhase )
+{
+    Abc_Obj_t * pNodePIs[10];
+    Map_Node_t ** ppLeaves;
+    Map_Super_t * pSuperBest;
+    unsigned uPhaseBest;
+    int i, fInvPin, nLeaves;
+
+    pSuperBest = Map_CutReadSuperBest( pCut, fPhase );
+    if ( pSuperBest == NULL )
+        return;
+
+    // get the information about the best cut 
+    uPhaseBest = Map_CutReadPhaseBest( pCut, fPhase );
+    nLeaves    = Map_CutReadLeavesNum( pCut );
+    ppLeaves   = Map_CutReadLeaves( pCut );
+
+    // collect the PI nodes
+    for ( i = 0; i < nLeaves; i++ )
+    {
+        fInvPin = ((uPhaseBest & (1 << i)) > 0);
+        pNodePIs[i] = (Abc_Obj_t *)Map_NodeReadData( ppLeaves[i], !fInvPin );
+        assert( pNodePIs[i] != NULL );
+    }
+
+    // implement the supergate
+    Abc_NodeFromMapSuperChoice_rec( pNtkNew, pSuperBest, pNodePIs, nLeaves );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the nodes corrresponding to one supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeFromMapSuperChoice_rec( Abc_Ntk_t * pNtkNew, Map_Super_t * pSuper, Abc_Obj_t * pNodePis[], int nNodePis )
+{
+    Mio_Gate_t * pRoot;
+    Map_Super_t ** ppFanins;
+    Abc_Obj_t * pNodeNew, * pNodeFanin;
+    int nFanins, Number, i;
+
+    // get the parameters of the supergate
+    pRoot = Map_SuperReadRoot(pSuper);
+    if ( pRoot == NULL )
+    {
+        Number = Map_SuperReadNum(pSuper);
+        if ( Number < nNodePis )  
+        {
+            return pNodePis[Number];
+        }
+        else
+        {  
+//            assert( 0 );
+            /* It might happen that a super gate with 5 inputs is constructed that
+             * actually depends only on the first four variables; i.e the fifth is a
+             * don't care -- in that case we connect constant node for the fifth
+             * (since the cut only has 4 variables). An interesting question is what
+             * if the first variable (and not the fifth one is the redundant one;
+             * can that happen?) */
+            return Abc_NodeCreateConst0(pNtkNew);
+        }
+    }
+
+    // get information about the fanins of the supergate
+    nFanins  = Map_SuperReadFaninNum( pSuper );
+    ppFanins = Map_SuperReadFanins( pSuper );
+    // create a new node with these fanins
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    for ( i = 0; i < nFanins; i++ )
+    {
+        pNodeFanin = Abc_NodeFromMapSuperChoice_rec( pNtkNew, ppFanins[i], pNodePis, nNodePis );
+        Abc_ObjAddFanin( pNodeNew, pNodeFanin );
+    }
+    pNodeNew->pData = Abc_SopRegister( pNtkNew->pManFunc, Mio_GateReadSop(pRoot) );
+    return pNodeNew;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 671fa9bc..0b7b44a0 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -67,7 +67,12 @@ Abc_Ntk_t * Abc_NtkLogic( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
     // create and connect the POs
     Abc_NtkForEachPo( pNtk, pObj, i )
-        Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), Abc_ObjFanin0(pObj)->pCopy );
+    {
+        if ( Abc_ObjFaninNum(pObj) == 0 )
+            Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), pObj->pCopy );
+        else
+            Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), Abc_ObjFanin0(pObj)->pCopy );
+    }
     // connect the latches
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
diff --git a/src/base/abc/abcPrint.c b/src/base/abc/abcPrint.c
index 0c3a2b5e..49b6db72 100644
--- a/src/base/abc/abcPrint.c
+++ b/src/base/abc/abcPrint.c
@@ -59,7 +59,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
     if ( Abc_NtkIsLogicSop(pNtk) )   
     {
         fprintf( pFile, "  cube = %5d",  Abc_NtkGetCubeNum(pNtk) );
-//        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
+        fprintf( pFile, "  lit(sop) = %5d",  Abc_NtkGetLitNum(pNtk) );
         fprintf( pFile, "  lit(fac) = %5d",  Abc_NtkGetLitFactNum(pNtk) );
     }
     else if ( Abc_NtkIsLogicBdd(pNtk) )
diff --git a/src/base/abc/abcRenode.c b/src/base/abc/abcRenode.c
index 6a24ab80..ab1a09c3 100644
--- a/src/base/abc/abcRenode.c
+++ b/src/base/abc/abcRenode.c
@@ -130,6 +130,8 @@ void Abc_NtkRenodeInt( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
+        if ( Abc_ObjIsTerm(Abc_ObjFanin0(pNode)) )
+            continue;
         Abc_NtkRenode_rec( pNtkNew, Abc_ObjFanin0(pNode) );
     }
     Extra_ProgressBarStop( pProgress );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 9862ea8e..aabc2660 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -61,6 +61,37 @@ char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Starts the constant 1 cover with the given number of variables and cubes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopStart( Extra_MmFlex_t * pMan, int nCubes, int nVars )
+{
+    char * pSopCover;
+    char * pCube;
+    int i, v;
+    pSopCover = Extra_MmFlexEntryFetch( pMan, nCubes * (nVars + 3) + 1 );
+    for ( i = 0; i < nCubes; i++ )
+    {
+        pCube = pSopCover + i * (nVars + 3);
+        for ( v = 0; v < nVars; v++ )
+            pCube[v] = '-';
+        pCube[nVars + 0] = ' ';
+        pCube[nVars + 1] = '1';
+        pCube[nVars + 2] = '\n';
+    }
+    pSopCover[nCubes * (nVars + 3)] = 0;
+    return pSopCover;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of cubes in the cover.]
 
   Description []
diff --git a/src/base/abc/abcStrash.c b/src/base/abc/abcStrash.c
index eb5b3df7..fcfeefda 100644
--- a/src/base/abc/abcStrash.c
+++ b/src/base/abc/abcStrash.c
@@ -107,6 +107,7 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
     // perform strashing
     vNodes = Abc_NtkDfs( pNtk );
+//    vNodes = Abc_AigCollectAll( pNtk );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     for ( i = 0; i < vNodes->nSize; i++ )
     {
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 1c826f95..e971ca18 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -768,6 +768,11 @@ Vec_Ptr_t * Abc_AigCollectAll( Abc_Ntk_t * pNtk )
     vNodes = Vec_PtrAlloc( 100 );
     Abc_NtkForEachNode( pNtk, pNode, i )
         Vec_PtrPush( vNodes, pNode );
+
+    // works only if the levels are set!!!
+    if ( !Abc_NtkIsAig(pNtk) )
+        Abc_NtkGetLevelNum(pNtk);
+
     Vec_PtrSort( vNodes, Abc_NodeCompareLevelsIncrease );
     return vNodes;
 }
diff --git a/src/base/abc/abc_.c b/src/base/abc/abc_.c
new file mode 100644
index 00000000..bef3836f
--- /dev/null
+++ b/src/base/abc/abc_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [abc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+