Version abc50822

10 files changed, 373 insertions, 93 deletions

diff --git a/src/base/abc/abc.c b/src/base/abc/abc.c
index dfe2f4d4..7f4ee12f 100644
--- a/src/base/abc/abc.c
+++ b/src/base/abc/abc.c
@@ -23,6 +23,7 @@
 #include "ft.h"
 #include "fraig.h"
 #include "fxu.h"
+#include "cut.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -58,6 +59,7 @@ static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSplit        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCut         ( 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 );
@@ -126,6 +128,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "split",         Abc_CommandSplit,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
+    Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
@@ -149,6 +152,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Ft_FactorStartMan();
 //    Rwt_Man4ExploreStart();
+//    Map_Var3Print();
+//    Map_Var4Test();
 }
 
 /**Function*************************************************************
@@ -929,14 +934,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     fMulti    =  0;
     fSimple   =  0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "tfmcsh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "TFmcsh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 't':
+        case 'T':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-t\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
                 goto usage;
             }
             nThresh = atoi(argv[util_optind]);
@@ -944,10 +949,10 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nThresh < 0 ) 
                 goto usage;
             break;
-        case 'f':
+        case 'F':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-f\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFaninMax = atoi(argv[util_optind]);
@@ -994,10 +999,10 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-t num] [-f num] [-cmsh]\n" );
+    fprintf( pErr, "usage: renode [-T num] [-F num] [-cmsh]\n" );
     fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
-    fprintf( pErr, "\t-t num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
-    fprintf( pErr, "\t-f num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
+    fprintf( pErr, "\t-T num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
+    fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
     fprintf( pErr, "\t-c      : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" );
     fprintf( pErr, "\t-m      : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" );
     fprintf( pErr, "\t-s      : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" );
@@ -1099,14 +1104,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     p->fUseCompl = 1;
     p->fVerbose  = 0;
     util_getopt_reset();
-    while ( (c = util_getopt(argc, argv, "lnsdzcvh")) != EOF ) 
+    while ( (c = util_getopt(argc, argv, "LNsdzcvh")) != EOF ) 
     {
         switch (c) 
         {
-            case 'l':
+            case 'L':
                 if ( util_optind >= argc )
                 {
-                    fprintf( pErr, "Command line switch \"-l\" should be followed by an integer.\n" );
+                    fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
                     goto usage;
                 }
                 p->nPairsMax = atoi(argv[util_optind]);
@@ -1114,10 +1119,10 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
                 if ( p->nPairsMax < 0 ) 
                     goto usage;
                 break;
-            case 'n':
+            case 'N':
                 if ( util_optind >= argc )
                 {
-                    fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
+                    fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
                     goto usage;
                 }
                 p->nNodesExt = atoi(argv[util_optind]);
@@ -1168,10 +1173,10 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fx [-n num] [-l num] [-sdzcvh]\n");
+    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-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" );  
@@ -1423,14 +1428,14 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     fUseDcs      =  0;
     fVerbose     =  0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "ncdvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "NCdvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'n':
+        case 'N':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
                 goto usage;
             }
             nNodeSizeMax = atoi(argv[util_optind]);
@@ -1438,10 +1443,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nNodeSizeMax < 0 ) 
                 goto usage;
             break;
-        case 'c':
+        case 'C':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
             nConeSizeMax = atoi(argv[util_optind]);
@@ -1487,10 +1492,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: refactor [-n num] [-c num] [-dvh]\n" );
+    fprintf( pErr, "usage: refactor [-N num] [-C num] [-dvh]\n" );
     fprintf( pErr, "\t         performs technology-independent refactoring of the AIG\n" );
-    fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );  
-    fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", nConeSizeMax );  
+    fprintf( pErr, "\t-N num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );  
+    fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax );  
     fprintf( pErr, "\t-d     : toggle use of don't-cares [default = %s]\n", fUseDcs? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -1663,14 +1668,14 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     fInitial = 0;
     nFrames  = 5;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "fih" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Fih" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'f':
+        case 'F':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFrames = atoi(argv[util_optind]);
@@ -1713,9 +1718,9 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: frames [-f num] [-ih]\n" );
+    fprintf( pErr, "usage: frames [-F num] [-ih]\n" );
     fprintf( pErr, "\t         unrolls the network for a number of time frames\n" );
-    fprintf( pErr, "\t-f num : the number of frames to unroll [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames );
     fprintf( pErr, "\t-i     : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -2015,14 +2020,14 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
     fUseAllCis = 0;
     Output = -1;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "oah" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Oah" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'o':
+        case 'O':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-o\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" );
                 goto usage;
             }
             Output = atoi(argv[util_optind]);
@@ -2092,11 +2097,11 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: split [-o num] [-ah] <name>\n" );
+    fprintf( pErr, "usage: split [-O num] [-ah] <name>\n" );
     fprintf( pErr, "\t         replaces the current network by the logic cone of one output\n" );
     fprintf( pErr, "\t-a     : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
     fprintf( pErr, "\t-h     : print the command usage\n");
-    fprintf( pErr, "\t-o num : (optional) the 0-based number of the output\n");
+    fprintf( pErr, "\t-O num : (optional) the 0-based number of the output\n");
     fprintf( pErr, "\tname   : (optional) the name of the output\n");
     return 1;
 }
@@ -2151,6 +2156,121 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Cut_Params_t Params, * pParams = &Params;
+    Cut_Man_t * pCutMan;
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    pParams->nVarsMax  = 5;     // the max cut size ("k" of the k-feasible cuts)
+    pParams->nKeepMax  = 250;   // the max number of cuts kept at a node
+    pParams->fTruth    = 1;     // compute truth tables
+    pParams->fHash     = 0;     // hash cuts to detect unique
+    pParams->fFilter   = 0;     // filter dominated cuts
+    pParams->fSeq      = 0;     // compute sequential cuts
+    pParams->fDrop     = 0;     // drop cuts on the fly
+    pParams->fVerbose  = 0;     // the verbosiness flag
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "KMtrfsdvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'K':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nVarsMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( pParams->nVarsMax < 0 ) 
+                goto usage;
+            break;
+        case 'M':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nKeepMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( pParams->nKeepMax < 0 ) 
+                goto usage;
+            break;
+        case 't':
+            pParams->fTruth ^= 1;
+            break;
+        case 'r':
+            pParams->fHash ^= 1;
+            break;
+        case 'f':
+            pParams->fFilter ^= 1;
+            break;
+        case 's':
+            pParams->fSeq ^= 1;
+            break;
+        case 'd':
+            pParams->fDrop ^= 1;
+            break;
+        case 'v':
+            pParams->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "Cut computation is available only for AIGs.\n" );
+        return 1;
+    }
+    pCutMan = Abc_NtkCuts( pNtk, pParams );
+    Cut_ManPrintStats( pCutMan );
+    Cut_ManStop( pCutMan );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: cut [-K num] [-M num] [-trfsdvh]\n" );
+    fprintf( pErr, "\t         computes k-feasible cuts for the AIG\n" );
+    fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n",    pParams->nVarsMax );
+    fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n",     pParams->nKeepMax );
+    fprintf( pErr, "\t-t     : toggle truth table computation [default = %s]\n",          pParams->fTruth? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle reduction by hashing [default = %s]\n",             pParams->fHash? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle filtering by dominance [default = %s]\n",           pParams->fFilter? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle sequential cut computation [default = %s]\n",       pParams->fSeq? "yes": "no" );
+    fprintf( pErr, "\t-d     : toggle dropping when fanouts are done [default = %s]\n",   pParams->fDrop? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n",     pParams->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 
@@ -2168,7 +2288,7 @@ usage:
 int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char Buffer[100];
-    Fraig_Params_t Params;
+    Fraig_Params_t Params, * pParams = &Params;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int fAllNodes;
@@ -2180,17 +2300,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // 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
-    Params.fFuncRed   =  1;   // performs only one level hashing
-    Params.fFeedBack  =  1;   // enables solver feedback
-    Params.fDist1Pats =  1;   // enables distance-1 patterns
-    Params.fDoSparse  =  0;   // performs equiv tests for sparse functions 
-    Params.fChoicing  =  0;   // enables recording structural choices
-    Params.fTryProve  =  0;   // tries to solve the final miter
-    Params.fVerbose   =  0;   // the verbosiness flag
-    Params.fVerboseP  =  0;   // the verbosiness flag
+    pParams->nPatsRand  = 2048; // the number of words of random simulation info
+    pParams->nPatsDyna  = 2048; // the number of words of dynamic simulation info
+    pParams->nBTLimit   = 99;   // the max number of backtracks to perform
+    pParams->fFuncRed   =  1;   // performs only one level hashing
+    pParams->fFeedBack  =  1;   // enables solver feedback
+    pParams->fDist1Pats =  1;   // enables distance-1 patterns
+    pParams->fDoSparse  =  0;   // performs equiv tests for sparse functions 
+    pParams->fChoicing  =  0;   // enables recording structural choices
+    pParams->fTryProve  =  0;   // tries to solve the final miter
+    pParams->fVerbose   =  0;   // the verbosiness flag
+    pParams->fVerboseP  =  0;   // the verbosiness flag
     util_getopt_reset();
     while ( ( c = util_getopt( argc, argv, "RDBrscpvah" ) ) != EOF )
     {
@@ -2200,51 +2320,51 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'R':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-r\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
                 goto usage;
             }
-            Params.nPatsRand = atoi(argv[util_optind]);
+            pParams->nPatsRand = atoi(argv[util_optind]);
             util_optind++;
-            if ( Params.nPatsRand < 0 ) 
+            if ( pParams->nPatsRand < 0 ) 
                 goto usage;
             break;
         case 'D':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-d\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
                 goto usage;
             }
-            Params.nPatsDyna = atoi(argv[util_optind]);
+            pParams->nPatsDyna = atoi(argv[util_optind]);
             util_optind++;
-            if ( Params.nPatsDyna < 0 ) 
+            if ( pParams->nPatsDyna < 0 ) 
                 goto usage;
             break;
         case 'B':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-b\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
                 goto usage;
             }
-            Params.nBTLimit = atoi(argv[util_optind]);
+            pParams->nBTLimit = atoi(argv[util_optind]);
             util_optind++;
-            if ( Params.nBTLimit < 0 ) 
+            if ( pParams->nBTLimit < 0 ) 
                 goto usage;
             break;
 
         case 'r':
-            Params.fFuncRed ^= 1;
+            pParams->fFuncRed ^= 1;
             break;
         case 's':
-            Params.fDoSparse ^= 1;
+            pParams->fDoSparse ^= 1;
             break;
         case 'c':
-            Params.fChoicing ^= 1;
+            pParams->fChoicing ^= 1;
             break;
         case 'p':
-            Params.fTryProve ^= 1;
+            pParams->fTryProve ^= 1;
             break;
         case 'v':
-            Params.fVerbose ^= 1;
+            pParams->fVerbose ^= 1;
             break;
         case 'a':
             fAllNodes ^= 1;
@@ -2268,7 +2388,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // report the proof
-    Params.fVerboseP = Params.fTryProve;
+    pParams->fVerboseP = pParams->fTryProve;
 
     // get the new network
     if ( Abc_NtkIsAig(pNtk) )
@@ -2285,7 +2405,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    if ( Params.fTryProve ) // report the result
+    if ( pParams->fTryProve ) // report the result
         Abc_NtkMiterReport( pNtkRes );
 
     // replace the current network
@@ -2293,17 +2413,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    sprintf( Buffer, "%d", Params.nBTLimit );
+    sprintf( Buffer, "%d", pParams->nBTLimit );
     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 );
-    fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n",    Params.nBTLimit==-1? "infinity" : Buffer );
-    fprintf( pErr, "\t-r     : toggle functional reduction [default = %s]\n",                 Params.fFuncRed? "yes": "no" );
-    fprintf( pErr, "\t-s     : toggle considering sparse functions [default = %s]\n",         Params.fDoSparse? "yes": "no" );
-    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-R num : number of random patterns (127 < num < 32769) [default = %d]\n",     pParams->nPatsRand );
+    fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
+    fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n",    pParams->nBTLimit==-1? "infinity" : Buffer );
+    fprintf( pErr, "\t-r     : toggle functional reduction [default = %s]\n",                 pParams->fFuncRed? "yes": "no" );
+    fprintf( pErr, "\t-s     : toggle considering sparse functions [default = %s]\n",         pParams->fDoSparse? "yes": "no" );
+    fprintf( pErr, "\t-c     : toggle accumulation of choices [default = %s]\n",              pParams->fChoicing? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle proving the final miter [default = %s]\n",              pParams->fTryProve? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n",                       pParams->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;
@@ -2657,14 +2777,14 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     fSweep      = 1;
     fVerbose    = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "dasvh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Dasvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'd':
+        case 'D':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-d\" should be followed by a floating point number.\n" );
+                fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
                 goto usage;
             }
             DelayTarget = (float)atof(argv[util_optind]);
@@ -2743,9 +2863,9 @@ usage:
         sprintf( Buffer, "not used" );
     else
         sprintf( Buffer, "%.3f", DelayTarget );
-    fprintf( pErr, "usage: map [-d num] [-asvh]\n" );
+    fprintf( pErr, "usage: map [-D num] [-asvh]\n" );
     fprintf( pErr, "\t         performs standard cell mapping of the current network\n" );
-    fprintf( pErr, "\t-d num : sets the global required times [default = %s]\n", Buffer );  
+    fprintf( pErr, "\t-D num : sets the global required times [default = %s]\n", Buffer );  
     fprintf( pErr, "\t-a     : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
     fprintf( pErr, "\t-s     : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -3299,14 +3419,14 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     nFrames = 3;
     fSat    = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "fsh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "Fsh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'f':
+        case 'F':
             if ( util_optind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-t\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFrames = atoi(argv[util_optind]);
@@ -3338,11 +3458,11 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sec [-sh] [-f num] <file1> <file2>\n" );
+    fprintf( pErr, "usage: sec [-sh] [-F num] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs bounded sequential equivalence checking\n" );
     fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
     fprintf( pErr, "\t-h     : print the command usage\n");
-    fprintf( pErr, "\t-f num : the number of time frames to use [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
     fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
     fprintf( pErr, "\t         if no files are given, uses the current network and its spec\n");
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 18923f26..3bf419c5 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -426,7 +426,7 @@ extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
 extern Vec_Ptr_t *        Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
 extern Vec_Ptr_t *        Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
-extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll );
+extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
 extern Vec_Vec_t *        Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
 extern int                Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 25237868..b7bcde83 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -156,7 +156,7 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
     Abc_NtkForEachLatch( pMan->pNtkAig, pObj, i )
         pObj->pCopy = Abc_NtkLatch( pManNew->pNtkAig, i );
     // copy internal nodes
-    vNodes = Abc_AigDfs( pMan->pNtkAig, 1 );
+    vNodes = Abc_AigDfs( pMan->pNtkAig, 1, 0 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
     {
         if ( !Abc_NodeIsAigAnd(pObj) )
diff --git a/src/base/abc/abcCut.c b/src/base/abc/abcCut.c
new file mode 100644
index 00000000..424d7561
--- /dev/null
+++ b/src/base/abc/abcCut.c
@@ -0,0 +1,157 @@
+/**CFile****************************************************************
+
+  FileName    [abcCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Interface to cut computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "cut.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
+{
+    Cut_Man_t *  p;
+    Abc_Obj_t * pObj, * pDriver, * pNode;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vChoices;
+    int i;
+    int clk = clock();
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // start the manager
+    pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
+    p = Cut_ManStart( pParams );
+    if ( pParams->fDrop )
+        Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
+    // set cuts for PIs
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        if ( Abc_ObjFanoutNum(pObj) > 0 )
+            Cut_NodeSetTriv( p, pObj->Id );
+    // compute cuts for internal nodes
+    vNodes = Abc_AigDfs( pNtk, 0, 1 );
+    vChoices = Vec_IntAlloc( 100 );
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+    {
+        // when we reached a CO, it is time to deallocate the cuts
+        if ( Abc_ObjIsCo(pObj) )
+        {
+            if ( pParams->fDrop )
+                Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
+            continue;
+        }
+        // skip constant node, it has no cuts
+        if ( Abc_NodeIsConst(pObj) )
+            continue;
+        // compute the cuts to the internal node
+        Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),  
+            Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );  
+        // add cuts due to choices
+        if ( Abc_NodeIsAigChoice(pObj) )
+        {
+            Vec_IntClear( vChoices );
+            for ( pNode = pObj; pNode; pNode = pNode->pData )
+                Vec_IntPush( vChoices, pNode->Id );
+            Cut_NodeUnionCuts( p, vChoices );
+        }
+    }
+    if ( !pParams->fSeq )
+    {
+        Vec_PtrFree( vNodes );
+        Vec_IntFree( vChoices );
+PRT( "Total", clock() - clk );
+        return p;
+    }
+    assert( 0 );
+
+    // compute sequential cuts
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        pDriver = Abc_ObjFanin0(pObj);
+        if ( !Abc_ObjIsNode(pDriver) )
+            continue;
+        if ( Abc_NodeIsTravIdCurrent(pDriver) )
+            continue;
+        Abc_NodeSetTravIdCurrent(pDriver);
+        Cut_NodeSetComputedAsNew( p, pDriver->Id );
+    }
+    // compute as long as new cuts appear
+
+
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the array of fanout counters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vFanNums;
+    Abc_Obj_t * pObj;//, * pFanout;
+    int i;//, k, nFanouts;
+    vFanNums = Vec_IntAlloc( 0 );
+    Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) )
+        {
+            Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
+/*
+            // get the number of non-CO fanouts
+            nFanouts = 0;
+            Abc_ObjForEachFanout( pObj, pFanout, k )
+                if ( !Abc_ObjIsCo(pFanout) )
+                    nFanouts++;
+            Vec_IntWriteEntry( vFanNums, i, nFanouts );
+*/
+        }
+    return vFanNums;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 40fbf799..e5f1bde9 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -141,8 +141,8 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 
   Synopsis    [Returns the reverse DFS ordered array of logic nodes.]
 
-  Description [Collects only the internal nodes, leaving CIs and CO.
-  However it marks with the current TravId both CIs and COs.]
+  Description [Collects only the internal nodes, leaving out CIs/COs.
+  However it marks both CIs and COs with the current TravId.]
                
   SideEffects []
 
@@ -210,15 +210,15 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
 
   Synopsis    [Returns the DFS ordered array of logic nodes.]
 
-  Description [Collects only the internal nodes, leaving CIs and CO.
-  However it marks with the current TravId both CIs and COs.]
+  Description [Collects only the internal nodes, leaving out CIs/COs.
+  However it marks both CIs and COs with the current TravId.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll )
+Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos )
 {
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pNode;
@@ -231,8 +231,10 @@ Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll )
     // go through the PO nodes and call for each of them
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        Abc_NodeSetTravIdCurrent( pNode );
         Abc_AigDfs_rec( Abc_ObjFanin0(pNode), vNodes );
+        Abc_NodeSetTravIdCurrent( pNode );
+        if ( fCollectCos )
+            Vec_PtrPush( vNodes, pNode );
     }
     // collect dangling nodes if asked to
     if ( fCollectAll )
diff --git a/src/base/abc/abcFpga.c b/src/base/abc/abcFpga.c
index 1ced34d2..b83c376a 100644
--- a/src/base/abc/abcFpga.c
+++ b/src/base/abc/abcFpga.c
@@ -121,7 +121,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
         pNode->pCopy = (Abc_Obj_t *)Fpga_ManReadInputs(pMan)[i];
 
     // load the AIG into the mapper
-    vNodes = Abc_AigDfs( pNtk, 0 );
+    vNodes = Abc_AigDfs( pNtk, 0, 0 );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
diff --git a/src/base/abc/abcFraig.c b/src/base/abc/abcFraig.c
index 3f5304a7..c0eb1c0a 100644
--- a/src/base/abc/abcFraig.c
+++ b/src/base/abc/abcFraig.c
@@ -104,7 +104,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
     pConst1 = Abc_AigConst1( pNtk->pManFunc );
 
     // perform strashing
-    vNodes = Abc_AigDfs( pNtk, fAllNodes );
+    vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
diff --git a/src/base/abc/abcMap.c b/src/base/abc/abcMap.c
index 78f2faaa..15e5c6af 100644
--- a/src/base/abc/abcMap.c
+++ b/src/base/abc/abcMap.c
@@ -147,7 +147,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
         pNode->pCopy = (Abc_Obj_t *)Map_ManReadInputs(pMan)[i];
 
     // load the AIG into the mapper
-    vNodes = Abc_AigDfs( pNtk, 0 );
+    vNodes = Abc_AigDfs( pNtk, 0, 0 );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
diff --git a/src/base/abc/abcSeq.c b/src/base/abc/abcSeq.c
index e0685bf7..2fcbf670 100644
--- a/src/base/abc/abcSeq.c
+++ b/src/base/abc/abcSeq.c
@@ -87,7 +87,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
     }
 
     // copy internal nodes
-    vNodes = Abc_AigDfs( pNtk, 1 );
+    vNodes = Abc_AigDfs( pNtk, 1, 0 );
     Vec_PtrForEachEntry( vNodes, pObj, i )
         if ( Abc_ObjFaninNum(pObj) == 2 )
             pObj->pCopy = Abc_AigAnd( pManNew, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
diff --git a/src/base/abc/module.make b/src/base/abc/module.make
index b05cf03b..bd390002 100644
--- a/src/base/abc/module.make
+++ b/src/base/abc/module.make
@@ -4,6 +4,7 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcCheck.c \
     src/base/abc/abcCollapse.c \
     src/base/abc/abcCreate.c \
+    src/base/abc/abcCut.c \
     src/base/abc/abcDfs.c \
     src/base/abc/abcDsd.c \
     src/base/abc/abcFanio.c \