Cleaned 'abc.c' by removing useless procedures.

1 files changed, 939 insertions, 1689 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7ea474f7..c2b44921 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -51,9 +51,7 @@
 #include "base/cmd/cmd.h"
 #include "proof/abs/abs.h"
 
-#ifdef _WIN32
-//#include <io.h>
-#else
+#ifndef _WIN32
 #include <unistd.h>
 #endif
 
@@ -187,12 +185,10 @@ static int Abc_CommandIFraig                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandDFraig                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCSweep                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDProve                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandDProve2                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbSec                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSimSec                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMatch                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandHaig                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandMini                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandQbf                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -203,10 +199,6 @@ static int Abc_CommandFraigClean             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandFraigSweep             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFraigDress             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-//static int Abc_CommandHaigStart              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandHaigStop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandHaigUse                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
 static int Abc_CommandRecStart               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecStop                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRecAdd                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -269,7 +261,6 @@ static int Abc_CommandUnpermute              ( Abc_Frame_t * pAbc, int argc, cha
 
 static int Abc_CommandCec                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCec                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSec                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDSec                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSat                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDSat                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -351,34 +342,30 @@ static int Abc_CommandAbc9Trace              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Speedup            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Era                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Dch                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Reparam            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9BackReach          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Posplit            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ReachM             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ReachP             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ReachN             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ReachY             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Undo               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Iso                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9CexMin             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 static int Abc_CommandAbc9AbsDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandAbc9AbsCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandAbc9AbsPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaShrink          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandAbc9GlaCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandAbc9GlaPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Gla                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Vta                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Vta2Gla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Gla2Vta            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Fla2Gla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Gla2Fla            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Reparam            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9BackReach          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Posplit            ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9ReachM             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9ReachP             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9ReachN             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9ReachY             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Undo               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Iso                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9CexMin             ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
-static int Abc_CommandAbcTestNew             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 extern int Abc_CommandAbcLivenessToSafety    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -651,7 +638,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "dfraig",        Abc_CommandDFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "csweep",        Abc_CommandCSweep,           1 );
 //    Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
-//    Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "qbf",           Abc_CommandQbf,              0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -662,10 +648,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Abc_CommandFraigSweep,       1 );
     Cmd_CommandAdd( pAbc, "Fraiging",     "dress",         Abc_CommandFraigDress,       1 );
 
-//    Cmd_CommandAdd( pAbc, "Choicing",     "haig_start",    Abc_CommandHaigStart,        0 );
-//    Cmd_CommandAdd( pAbc, "Choicing",     "haig_stop",     Abc_CommandHaigStop,         0 );
-//    Cmd_CommandAdd( pAbc, "Choicing",     "haig_use",      Abc_CommandHaigUse,          1 );
-
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_start",     Abc_CommandRecStart,         0 );
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_stop",      Abc_CommandRecStop,          0 );
     Cmd_CommandAdd( pAbc, "Choicing",     "rec_add",       Abc_CommandRecAdd,           0 );
@@ -686,8 +668,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "SC mapping",   "amap",          Abc_CommandAmap,             1 );
     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, "SC mapping",   "superc",        Abc_CommandSuperChoice,      1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "supercl",       Abc_CommandSuperChoiceLut,   1 );
 
     Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
     Cmd_CommandAdd( pAbc, "FPGA mapping", "ffpga",         Abc_CommandFpgaFast,         1 );
@@ -726,10 +708,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dcec",          Abc_CommandDCec,             0 );
-//    Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsec",          Abc_CommandDSec,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "dprove",        Abc_CommandDProve,           0 );
-//    Cmd_CommandAdd( pAbc, "Verification", "dprove2",       Abc_CommandDProve2,          0 );
     Cmd_CommandAdd( pAbc, "Verification", "absec",         Abc_CommandAbSec,            0 );
     Cmd_CommandAdd( pAbc, "Verification", "simsec",        Abc_CommandSimSec,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "match",         Abc_CommandMatch,            0 );
@@ -810,21 +790,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&speedup",      Abc_CommandAbc9Speedup,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&era",          Abc_CommandAbc9Era,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&dch",          Abc_CommandAbc9Dch,          0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_derive",   Abc_CommandAbc9AbsDerive,    0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_refine",   Abc_CommandAbc9AbsRefine,    0 );
-//    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_cba",      Abc_CommandAbc9AbsCba,       0 );
-//    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_pba",      Abc_CommandAbc9AbsPba,       0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_refine",   Abc_CommandAbc9GlaRefine,    0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_shrink",   Abc_CommandAbc9GlaShrink,    0 );
-//    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_cba",      Abc_CommandAbc9GlaCba,       0 );
-//    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_pba",      Abc_CommandAbc9GlaPba,       0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&gla",          Abc_CommandAbc9Gla,          0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&vta",          Abc_CommandAbc9Vta,          0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&vta_gla",      Abc_CommandAbc9Vta2Gla,      0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_vta",      Abc_CommandAbc9Gla2Vta,      0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&fla_gla",      Abc_CommandAbc9Fla2Gla,      0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_fla",      Abc_CommandAbc9Gla2Fla,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reparam",      Abc_CommandAbc9Reparam,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&back_reach",   Abc_CommandAbc9BackReach,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&posplit",      Abc_CommandAbc9Posplit,      0 );
@@ -835,22 +800,28 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&undo",         Abc_CommandAbc9Undo,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&iso",          Abc_CommandAbc9Iso,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cexmin",       Abc_CommandAbc9CexMin,       0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,         0 );
 
-    Cmd_CommandAdd( pAbc, "Liveness",     "l2s",           Abc_CommandAbcLivenessToSafety,    0 );
-    Cmd_CommandAdd( pAbc, "Liveness",     "l2ssim",        Abc_CommandAbcLivenessToSafetySim, 0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_derive",   Abc_CommandAbc9AbsDerive,    0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&abs_refine",   Abc_CommandAbc9AbsRefine,    0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_refine",   Abc_CommandAbc9GlaRefine,    0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_shrink",   Abc_CommandAbc9GlaShrink,    0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla",          Abc_CommandAbc9Gla,          0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&vta",          Abc_CommandAbc9Vta,          0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&vta_gla",      Abc_CommandAbc9Vta2Gla,      0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_vta",      Abc_CommandAbc9Gla2Vta,      0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&fla_gla",      Abc_CommandAbc9Fla2Gla,      0 );
+    Cmd_CommandAdd( pAbc, "Abstraction",  "&gla_fla",      Abc_CommandAbc9Gla2Fla,      0 );
+
+    Cmd_CommandAdd( pAbc, "Liveness",     "l2s",           Abc_CommandAbcLivenessToSafety,           0 );
+    Cmd_CommandAdd( pAbc, "Liveness",     "l2ssim",        Abc_CommandAbcLivenessToSafetySim,        0 );
     Cmd_CommandAdd( pAbc, "Liveness",     "l3s",           Abc_CommandAbcLivenessToSafetyWithLTL,    0 );
 
-    Cmd_CommandAdd( pAbc, "Various",      "testnew",       Abc_CommandAbcTestNew,       0 );
-
+    Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,         0 );
     {
         extern void Dar_LibStart();
         Dar_LibStart();
     }
-    {
-//        extern void Extra_NpnTest();
-//        Extra_NpnTest();
-    }
 } 
 
 /**Function*************************************************************
@@ -11421,65 +11392,6 @@ usage:
     return 1;
 }
 */
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandMini( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
-    extern Abc_Ntk_t * Abc_NtkMiniBalance( Abc_Ntk_t * pNtk );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        Abc_Print( -1, "Empty network.\n" );
-        return 1;
-    }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "Only works for combinatinally strashed AIG networks.\n" );
-        return 1;
-    }
-
-    pNtkRes = Abc_NtkMiniBalance( pNtk );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command has failed.\n" );
-        return 0;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: mini [-h]\n" );
-    Abc_Print( -2, "\t         perform balancing using new package\n" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
  
 /**Function*************************************************************
 
@@ -12228,146 +12140,6 @@ usage:
     return 1;
 }
 
-#if 0
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandHaigStart( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "This command works only for AIGs; run strashing (\"st\").\n" );
-        return 0;
-    }
-    Abc_NtkHaigStart( pNtk );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: haig_start [-h]\n" );
-    Abc_Print( -2, "\t        starts constructive accumulation of combinational choices\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandHaigStop( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "This command works only for AIGs; run strashing (\"st\").\n" );
-        return 0;
-    }
-    Abc_NtkHaigStop( pNtk );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: haig_stop [-h]\n" );
-    Abc_Print( -2, "\t        cleans the internal storage for combinational choices\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandHaigUse( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "This command works only for AIGs; run strashing (\"st\").\n" );
-        return 0;
-    }
-    // get the new network
-    pNtkRes = Abc_NtkHaigUse( pNtk );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Transforming internal storage into AIG with choices has failed.\n" );
-        return 1;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: haig_use [-h]\n" );
-    Abc_Print( -2, "\t        transforms internal storage into an AIG with choices\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-#endif
-
 
 /**Function*************************************************************
 
@@ -13700,7 +13472,7 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sc [-h]\n" );
+    Abc_Print( -2, "usage: superc [-h]\n" );
     Abc_Print( -2, "\t      performs superchoicing\n" );
     Abc_Print( -2, "\t      (accumulate: \"r file.blif; rsup; b; sc; f -ac; wb file_sc.blif\")\n" );
     Abc_Print( -2, "\t      (map without supergate library: \"r file_sc.blif; ft; map\")\n" );
@@ -13797,7 +13569,7 @@ int Abc_CommandSuperChoiceLut( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: scl [-K num] [-N num] [-vh]\n" );
+    Abc_Print( -2, "usage: supercl [-K num] [-N num] [-vh]\n" );
     Abc_Print( -2, "\t        performs superchoicing for K-LUTs\n" );
     Abc_Print( -2, "\t        (accumulate: \"r file.blif; b; scl; f -ac; wb file_sc.blif\")\n" );
     Abc_Print( -2, "\t        (FPGA map: \"r file_sc.blif; ft; read_lut lutlibK; fpga\")\n" );
@@ -18482,152 +18254,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
-    int fDelete1, fDelete2;
-    char ** pArgvNew;
-    int nArgcNew;
-    int c;
-    int fRetime;
-    int fSat;
-    int fVerbose;
-    int nFrames;
-    int nSeconds;
-    int nConfLimit;
-    int nInsLimit;
-
-    extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames );
-    extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
-
-    Abc_Print( 0, "This command is no longer used.\n" );
-    return 0;
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    // set defaults
-    fRetime  =  0; // verification after retiming
-    fSat     =  0;
-    fVerbose =  0;
-    nFrames  =  5;
-    nSeconds = 20;
-    nConfLimit = 10000;   
-    nInsLimit  = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsrvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nFrames = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nFrames <= 0 ) 
-                goto usage;
-            break;
-        case 'T':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nSeconds = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nSeconds < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfLimit < 0 ) 
-                goto usage;
-            break;
-        case 'I':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nInsLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nInsLimit < 0 ) 
-                goto usage;
-            break;
-        case 'r':
-            fRetime ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 's':
-            fSat ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-
-    pArgvNew = argv + globalUtilOptind;
-    nArgcNew = argc - globalUtilOptind;
-    if ( !Abc_NtkPrepareTwoNtks( stdout, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) )
-        return 1;
-
-    if ( Abc_NtkLatchNum(pNtk1) == 0 || Abc_NtkLatchNum(pNtk2) == 0 )
-    {
-        if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
-        if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
-        Abc_Print( -1, "The network has no latches. Used combinational command \"cec\".\n" );
-        return 0;
-    }
-
-    // perform equivalence checking
-    if ( fSat )
-        Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames );
-    else
-        Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
-
-    if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
-    if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: sec [-F num] [-T num] [-C num] [-I num] [-srvh] <file1> <file2>\n" );
-    Abc_Print( -2, "\t         performs bounded sequential equivalence checking\n" );
-    Abc_Print( -2, "\t         (there is also an unbounded SEC commands, \"dsec\" and \"dprove\")\n" );
-    Abc_Print( -2, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
-    Abc_Print( -2, "\t-r     : toggles retiming verification [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    Abc_Print( -2, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
-    Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
-    Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-    Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
-    Abc_Print( -2, "\tfile1  : (optional) the file with the first network\n");
-    Abc_Print( -2, "\tfile2  : (optional) the file with the second network\n");
-    Abc_Print( -2, "\t         if no files are given, uses the current network and its spec\n");
-    Abc_Print( -2, "\t         if one file is given, uses the current network and the file\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Fra_Sec_t SecPar, * pSecPar = &SecPar;
@@ -19024,91 +18650,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandDProve2( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int nConfLast;
-    int fSeparate;
-    int fVeryVerbose;
-    int fVerbose;
-    int c;
-
-//    extern int Abc_NtkDProve2( Abc_Ntk_t * pNtk, int nConfLast, int fSeparate, int fVeryVerbose, int fVerbose );
-    // set defaults
-    nConfLast    = 75000;
-    fSeparate    = 0;
-    fVeryVerbose = 0;
-    fVerbose     = 1;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Ckwvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfLast = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfLast < 0 ) 
-                goto usage;
-            break;
-        case 'k':
-            fSeparate ^= 1;
-            break;
-        case 'w':
-            fVeryVerbose ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        Abc_Print( -1, "Empty network.\n" );
-        return 1;
-    }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "This command works only for structrally hashed networks. Run \"st\".\n" );
-        return 0;
-    }
-    if ( Abc_NtkLatchNum(pNtk) == 0 )
-    {
-        Abc_Print( -1, "This command works only for sequential networks.\n" );
-        return 0;
-    }
-    // perform verification
-//    Abc_NtkDProve2( pNtk, nConfLast, fSeparate, fVeryVerbose, fVerbose );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: dprove2 [-C num] [-kwvh]\n" );
-    Abc_Print( -2, "\t         improved integrated solver of sequential miters\n" );
-    Abc_Print( -2, "\t-C num : the conflict limit during final BMC [default = %d]\n", nConfLast );
-    Abc_Print( -2, "\t-k     : toggles solving each output separately [default = %s]\n", fSeparate? "yes": "no" );
-    Abc_Print( -2, "\t-w     : toggles very verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_CommandAbSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
@@ -22785,63 +22326,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbcTestNew( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    extern int Abc_NtkTestProcedure( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
-
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        Abc_Print( -1, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( !Abc_NtkIsStrash( pNtk) )
-    {
-        Abc_Print( -1, "The current network is not an AIG. Cannot continue.\n" );
-        return 1;
-    }
-
-//    Abc_NtkTestProcedure( pNtk, NULL );
-
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: testnew [-h]\n" );
-    Abc_Print( -2, "\t        new testing procedure\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pAig;
@@ -27220,7 +26704,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Dch(): There is no AIG.\n" );
         return 1;
     } 
     pTemp = Gia_ManPerformDch( pAbc->pGia, pPars );
@@ -27254,7 +26738,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
@@ -27274,26 +26758,16 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsDerive(): There is no AIG.\n" );
-        return 1;
-    } 
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
-    {
-        Abc_Print( -1, "The network is combinational.\n" );
-        return 0;
-    }
-    if ( pAbc->pGia->vFlopClasses == NULL )
-    {
-        Abc_Print( -1, "Abstraction flop map is missing.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Reparam(): There is no AIG.\n" );
         return 0;
-    }
-    pTemp = Gia_ManDupAbsFlops( pAbc->pGia, pAbc->pGia->vFlopClasses );
+    } 
+    pTemp = Gia_ManReparam( pAbc->pGia, fVerbose );
     Abc_CommandUpdate9( pAbc, pTemp );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_derive [-vh]\n" );
-    Abc_Print( -2, "\t        derives abstracted model using the pre-computed flop map\n" );
+    Abc_Print( -2, "usage: &reparam [-vh]\n" );
+    Abc_Print( -2, "\t        performs input trimming and reparameterization\n" );
     Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
@@ -27310,36 +26784,52 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9BackReach( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-//    Gia_Man_t * pTemp = NULL;
-    int c;
-    int nFfToAddMax = 0;
-    int fTryFour    = 1;
-    int fSensePath  = 0;
-    int fVerbose    = 0;
+    extern Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose );
 
+    Gia_Man_t * pTemp = NULL;
+    int c, fVerbose = 0;
+    int nFrameMax = 1000000;
+    int nConfMax  = 1000000;
+    int nTimeMax  =      10;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Mtsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCTvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'M':
+        case 'F':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFfToAddMax = atoi(argv[globalUtilOptind]);
+            nFrameMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFfToAddMax < 0 ) 
+            if ( nFrameMax < 0 ) 
                 goto usage;
             break;
-        case 't':
-            fTryFour ^= 1;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMax < 0 ) 
+                goto usage;
             break;
-        case 's':
-            fSensePath ^= 1;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeMax < 0 ) 
+                goto usage;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -27352,35 +26842,96 @@ int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9BackReach(): There is no AIG.\n" );
         return 1;
-    } 
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    }
+    if ( Gia_ManPoNum(pAbc->pGia) != 1 )
     {
-        Abc_Print( -1, "The network is combinational.\n" );
-        return 0;
+        Abc_Print( -1, "Abc_CommandAbc9BackReach(): The number of POs is different from 1.\n" );
+        return 1;
     }
-    if ( pAbc->pCex == NULL )
+    pTemp = Gia_ManCofTest( pAbc->pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
+    Abc_CommandUpdate9( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &back_reach [-FCT <num>] [-vh]\n" );
+    Abc_Print( -2, "\t         performs backward reachability by circuit cofactoring\n" );
+    Abc_Print( -2, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrameMax );
+    Abc_Print( -2, "\t-C num : the conflict limit at a node during induction [default = %d]\n", nConfMax );
+    Abc_Print( -2, "\t-T num : the timeout for property directed reachability [default = %d]\n", nTimeMax );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Posplit( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose );
+    Aig_Man_t * pMan, * pAux;
+    Gia_Man_t * pTemp = NULL;
+    int c, nVars = 5, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no counter-example.\n" );
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nVars = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nVars < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Posplit(): There is no AIG.\n" );
         return 1;
     } 
-    pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose );
-    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    pMan = Gia_ManToAigSimple( pAbc->pGia );
+    pMan = Aig_ManSplit( pAux = pMan, nVars, fVerbose );
+    Aig_ManStop( pAux );
+    if ( pMan != NULL )
+    {
+        pTemp = Gia_ManFromAigSimple( pMan );
+        Aig_ManStop( pMan );
+        Abc_CommandUpdate9( pAbc, pTemp );
+    }
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_refine [-M <num>] [-tsvh]\n" );
-    Abc_Print( -2, "\t         refines the pre-computed flop map using the counter-example\n" );
-    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", nFfToAddMax );
-    Abc_Print( -2, "\t-t     : toggle trying four abstractions instead of one [default = %s]\n", fTryFour? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle using the path sensitization algorithm [default = %s]\n", fSensePath? "yes": "no" );
+    Abc_Print( -2, "usage: &posplit [-N num] [-vh]\n" );
+    Abc_Print( -2, "\t         cofactors the property output w.r.t. a support subset\n" );
+    Abc_Print( -2, "\t         (the OR of new PO functions is equal to the original property)\n" );
+    Abc_Print( -2, "\t-N num : the number of random cofactoring variables [default = %d]\n", nVars );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
-} 
-
-#if 0
+}
 
 /**Function*************************************************************
 
@@ -27393,27 +26944,41 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Saig_ParBmc_t Pars, * pPars = &Pars;
+//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Gia_ParLlb_t Pars, * pPars = &Pars;
+    char * pLogFileName = NULL;
     int c;
-    Saig_ParBmcSetDefaultParams( pPars );
-    pPars->nStart     = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
-    pPars->nFramesMax = pPars->nStart + 10;
+    extern int Llb_ManModelCheckGia( Gia_Man_t * pGia, Gia_ParLlb_t * pPars );
+
+    // set defaults
+    Llb_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCMTvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TBFCHSLripcsyzvwh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'S':
+        case 'T':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nStart = atoi(argv[globalUtilOptind]);
+            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nStart < 0 ) 
+            if ( pPars->TimeLimit < 0 ) 
+                goto usage;
+            break;
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBddMax < 0 ) 
                 goto usage;
             break;
         case 'F':
@@ -27422,9 +26987,9 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nFramesMax = atoi(argv[globalUtilOptind]);
+            pPars->nIterMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nFramesMax < 0 ) 
+            if ( pPars->nIterMax < 0 ) 
                 goto usage;
             break;
         case 'C':
@@ -27433,20 +26998,178 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nConfLimit = atoi(argv[globalUtilOptind]);
+            pPars->nClusterMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nConfLimit < 0 ) 
+            if ( pPars->nClusterMax < 0 ) 
                 goto usage;
             break;
-        case 'M':
+        case 'H':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nHintDepth = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nHintDepth < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->HintFirst = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->HintFirst < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pLogFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'r':
+            pPars->fReorder ^= 1;
+            break;
+        case 'i':
+            pPars->fIndConstr ^= 1;
+            break;
+        case 'p':
+            pPars->fUsePivots ^= 1;
+            break;
+        case 'c':
+            pPars->fCluster ^= 1;
+            break;
+        case 's':
+            pPars->fSchedule ^= 1;
+            break;
+        case 'y':
+            pPars->fSkipOutCheck ^= 1;
+            break;
+        case 'z':
+            pPars->fSkipReach ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachM(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachM(): The current AIG has no latches.\n" );
+        return 0;
+    } 
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachM(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
+    pAbc->Status  = Llb_ManModelCheckGia( pAbc->pGia, pPars );
+    pAbc->nFrames = pPars->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    if ( pLogFileName )
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachm" );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &reachm [-TBFCHS num] [-L file] [-ripcsyzvwh]\n" );
+    Abc_Print( -2, "\t         model checking via BDD-based reachability (dependence-matrix-based)\n" );
+    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
+    Abc_Print( -2, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", pPars->nBddMax );
+    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
+    Abc_Print( -2, "\t-C num : max number of variables in a cluster [default = %d]\n", pPars->nClusterMax );
+    Abc_Print( -2, "\t-H num : max number of hints to use [default = %d]\n", pPars->nHintDepth );
+    Abc_Print( -2, "\t-S num : the number of the starting hint [default = %d]\n", pPars->HintFirst );
+    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
+    Abc_Print( -2, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );  
+    Abc_Print( -2, "\t-i     : enable extraction of inductive constraints [default = %s]\n", pPars->fIndConstr? "yes": "no" );  
+    Abc_Print( -2, "\t-p     : enable partitions for internal cut-points [default = %s]\n", pPars->fUsePivots? "yes": "no" );  
+    Abc_Print( -2, "\t-c     : enable clustering of partitions [default = %s]\n", pPars->fCluster? "yes": "no" );  
+    Abc_Print( -2, "\t-s     : enable scheduling of clusters [default = %s]\n", pPars->fSchedule? "yes": "no" );  
+    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
+    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
+    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
+    Abc_Print( -2, "\t-w     : prints dependency matrix [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Gia_ParLlb_t Pars, * pPars = &Pars;
+    Aig_Man_t * pMan;
+    char * pLogFileName = NULL;
+    int c;
+    extern int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
+
+    // set defaults
+    Llb_ManSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NBFTLrbyzdvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nFfToAddMax = atoi(argv[globalUtilOptind]);
+            pPars->nPartValue = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nFfToAddMax < 0 ) 
+            if ( pPars->nPartValue < 0 ) 
+                goto usage;
+            break;
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBddMax < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nIterMax < 0 ) 
                 goto usage;
             break;
         case 'T':
@@ -27455,14 +27178,41 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
                 goto usage;
             }
-            pPars->nTimeOut = atoi(argv[globalUtilOptind]);
+            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nTimeOut < 0 ) 
+            if ( pPars->TimeLimit < 0 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pLogFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'r':
+            pPars->fReorder ^= 1;
+            break;
+        case 'b':
+            pPars->fBackward ^= 1;
+            break;
+        case 'y':
+            pPars->fSkipOutCheck ^= 1;
+            break;
+        case 'z':
+            pPars->fSkipReach ^= 1;
+            break;
+        case 'd':
+            pPars->fDumpReached ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -27471,32 +27221,46 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9ReachP(): There is no AIG.\n" );
         return 1;
-    } 
+    }
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
-        Abc_Print( -1, "The network is combinational.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9ReachP(): The current AIG has no latches.\n" );
         return 0;
     }
-    pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars );
-    if ( pPars->nStart == 0 )
-        pAbc->nFrames = pPars->iFrame;
-    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachP(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
+    pMan          = Gia_ManToAigSimple( pAbc->pGia );
+    pAbc->Status  = Llb_ManReachMinCut( pMan, pPars );
+    pAbc->nFrames = pPars->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
+    if ( pLogFileName )
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachp" );
+    Aig_ManStop( pMan );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" );
-    Abc_Print( -2, "\t         refines abstracted flop map with CEX-based abstraction\n" );
-    Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
-    Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
-    Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
-//    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax );
-    Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "usage: &reachp [-NFT num] [-L file] [-rbyzdvwh]\n" );
+    Abc_Print( -2, "\t         model checking via BDD-based reachability (partitioning-based)\n" );
+    Abc_Print( -2, "\t-N num : partitioning value (MinVol=nANDs/N/2; MaxVol=nANDs/N) [default = %d]\n", pPars->nPartValue );
+//    Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax );
+    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
+    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
+    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
+    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
+    Abc_Print( -2, "\t-b     : perform backward reachability analysis [default = %s]\n", pPars->fBackward? "yes": "no" );  
+    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
+    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
+    Abc_Print( -2, "\t-d     : dump BDD of reached states into file \"reached.blif\" [default = %s]\n", pPars->fDumpReached? "yes": "no" );  
+    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
+    Abc_Print( -2, "\t-w     : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
-} 
+}
 
 /**Function*************************************************************
 
@@ -27509,30 +27273,31 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    int nStart     =        0;
-    int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
-    int nConfMax   = 10000000;
-    int nTimeLimit =        0;
-    int fVerbose   =        0;
-    int iFrame     =       -1;
+//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Gia_ParLlb_t Pars, * pPars = &Pars;
+    Aig_Man_t * pMan;
+    char * pLogFileName = NULL;
     int c;
+    extern int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
 
+    // set defaults
+    Llb_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLryzvwh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'S':
+        case 'B':
             if ( globalUtilOptind >= argc )
             {
-                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nStart = atoi(argv[globalUtilOptind]);
+            pPars->nBddMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nStart < 0 ) 
+            if ( pPars->nBddMax < 0 ) 
                 goto usage;
             break;
         case 'F':
@@ -27541,9 +27306,131 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFramesMax = atoi(argv[globalUtilOptind]);
+            pPars->nIterMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFramesMax < 0 ) 
+            if ( pPars->nIterMax < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->TimeLimit < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pLogFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'r':
+            pPars->fReorder ^= 1;
+            break;
+        case 'y':
+            pPars->fSkipOutCheck ^= 1;
+            break;
+        case 'z':
+            pPars->fSkipReach ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" );
+        return 0;
+    }
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
+    pMan          = Gia_ManToAigSimple( pAbc->pGia );
+    pAbc->Status  = Llb_NonlinCoreReach( pMan, pPars );
+    pAbc->nFrames = pPars->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
+    if ( pLogFileName )
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" );
+    Aig_ManStop( pMan );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &reachn [-BFT num] [-L file] [-ryzvh]\n" );
+    Abc_Print( -2, "\t         model checking via BDD-based reachability (non-linear-QS-based)\n" );
+    Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax );
+    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
+    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
+    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
+    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
+    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
+    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
+    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
+//    Abc_Print( -2, "\t-w     : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Gia_ParLlb_t Pars, * pPars = &Pars;
+    Aig_Man_t * pMan;
+    char * pLogFileName = NULL;
+    int c;
+
+    // set defaults
+    Llb_ManSetDefaultParams( pPars );
+    pPars->fCluster = 0;
+    pPars->fReorder = 0;
+    pPars->nBddMax     = 100;
+    pPars->nClusterMax = 500;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BCFTLbcryzvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBddMax < 0 ) 
                 goto usage;
             break;
         case 'C':
@@ -27552,9 +27439,20 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nConfMax = atoi(argv[globalUtilOptind]);
+            pPars->nClusterMax = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nConfMax < 0 ) 
+            if ( pPars->nClusterMax < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nIterMax < 0 ) 
                 goto usage;
             break;
         case 'T':
@@ -27563,11 +27461,162 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
                 Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nTimeLimit = atoi(argv[globalUtilOptind]);
+            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nTimeLimit < 0 ) 
+            if ( pPars->TimeLimit < 0 ) 
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pLogFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'b':
+            pPars->fBackward ^= 1;
+            break;
+        case 'c':
+            pPars->fCluster ^= 1;
+            break;
+        case 'r':
+            pPars->fReorder ^= 1;
+            break;
+        case 'y':
+            pPars->fSkipOutCheck ^= 1;
+            break;
+        case 'z':
+            pPars->fSkipReach ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" );
+        return 0;
+    }
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
+    pMan          = Gia_ManToAigSimple( pAbc->pGia );
+    pAbc->Status  = Llb_Nonlin4CoreReach( pMan, pPars );
+    pAbc->nFrames = pPars->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
+    if ( pLogFileName )
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachy" );
+    Aig_ManStop( pMan );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &reachy [-BCFT num] [-L file] [-bcryzvh]\n" );
+    Abc_Print( -2, "\t         model checking via BDD-based reachability (non-linear-QS-based)\n" );
+    Abc_Print( -2, "\t-B num : the max BDD size to introduce cut points [default = %d]\n", pPars->nBddMax );
+    Abc_Print( -2, "\t-C num : the max BDD size to reparameterize/cluster [default = %d]\n", pPars->nClusterMax );
+    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
+    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
+    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
+    Abc_Print( -2, "\t-b     : enable using backward enumeration [default = %s]\n", pPars->fBackward? "yes": "no" );  
+    Abc_Print( -2, "\t-c     : enable reparametrization clustering [default = %s]\n", pPars->fCluster? "yes": "no" );  
+    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
+    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
+    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
+    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
+//    Abc_Print( -2, "\t-w     : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Undo( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    int c;
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Undo(): There is no design.\n" );
+        return 1;
+    } 
+    if ( pAbc->pGia2 == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Undo(): There is no previously saved network.\n" );
+        return 1;
+    } 
+    Gia_ManStop( pAbc->pGia );
+    pAbc->pGia = pAbc->pGia2;
+    pAbc->pGia2 = NULL;
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &undo [-h]\n" );
+    Abc_Print( -2, "\t        reverses the previous AIG transformation\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pAig;
+    Vec_Ptr_t * vPosEquivs;
+    int c, fDualOut = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'd':
+            fDualOut ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -27579,7 +27628,162 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9Iso(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManPoNum(pAbc->pGia) == 1 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Iso(): The AIG has only one PO. Isomorphism detection is not performed.\n" );
+        return 1;
+    }
+    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, fDualOut, fVerbose );
+    if ( pAig == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Iso(): Transformation has failed.\n" );
+        return 1;
+    }
+    // update the internal storage of PO equivalences
+    Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
+    // update the AIG
+    Abc_CommandUpdate9( pAbc, pAig );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &iso [-dvh]\n" );
+    Abc_Print( -2, "\t         removes POs with isomorphic sequential COI\n" );
+    Abc_Print( -2, "\t-d     : treat the current AIG as a dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9CexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int nRealPis, int fJustMax, int fUseAll, int fVerbose );
+    Abc_Cex_t * pCexNew;
+    int iFrameStart = 0;
+    int nRealPis = -1;
+    int fJustMax = 1;
+    int fUseAll = 0;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FNjavh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            iFrameStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( iFrameStart < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRealPis = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRealPis < 0 ) 
+                goto usage;
+            break;
+        case 'j':
+            fJustMax ^= 1;
+            break;
+        case 'a':
+            fUseAll ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9CexMin(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9CexMin(): The network is combinational.\n" );
+        return 0;
+    }
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9CexMin(): There is no counter-example.\n" );
+        return 1;
+    } 
+    pCexNew = Gia_ManCexMin( pAbc->pGia, pAbc->pCex, iFrameStart, nRealPis, fJustMax, fUseAll, fVerbose );
+    if ( pCexNew )
+        Abc_FrameReplaceCex( pAbc, &pCexNew );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &cexmin [-FN num] [-javh]\n" );
+    Abc_Print( -2, "\t         minimizes a deep counter-example\n" );
+    Abc_Print( -2, "\t-F num : starting timeframe for minimization [default = %d]\n", iFrameStart );
+    Abc_Print( -2, "\t-N num : the number of real primary inputs [default = %d]\n", nRealPis );
+    Abc_Print( -2, "\t-j     : toggle computing all justifying assignments [default = %s]\n", fJustMax? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle using all terminal objects [default = %s]\n", fUseAll? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+} 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_Man_t * pTemp = NULL;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9AbsDerive(): There is no AIG.\n" );
         return 1;
     } 
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
@@ -27589,33 +27793,102 @@ int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia->vFlopClasses == NULL )
     {
-        Abc_Print( -1, "The flop map is not given.\n" );
+        Abc_Print( -1, "Abstraction flop map is missing.\n" );
         return 0;
     }
-    if ( nStart >= nFramesMax )
+    pTemp = Gia_ManDupAbsFlops( pAbc->pGia, pAbc->pGia->vFlopClasses );
+    Abc_CommandUpdate9( pAbc, pTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &abs_derive [-vh]\n" );
+    Abc_Print( -2, "\t        derives abstracted model using the pre-computed flop map\n" );
+    Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+//    Gia_Man_t * pTemp = NULL;
+    int c;
+    int nFfToAddMax = 0;
+    int fTryFour    = 1;
+    int fSensePath  = 0;
+    int fVerbose    = 0;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Mtsvh" ) ) != EOF )
     {
-        Abc_Print( -1, "The starting frame (%d) should be less than the total number of frames (%d).\n", nStart, nFramesMax );
+        switch ( c )
+        {
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFfToAddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFfToAddMax < 0 ) 
+                goto usage;
+            break;
+        case 't':
+            fTryFour ^= 1;
+            break;
+        case 's':
+            fSensePath ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-    Gia_ManPbaPerform( pAbc->pGia, nStart, nFramesMax, nConfMax, nTimeLimit, fVerbose, &iFrame );
-    if ( iFrame >= 0 )
-        pAbc->nFrames = iFrame;
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no counter-example.\n" );
+        return 1;
+    } 
+    pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, nFfToAddMax, fTryFour, fSensePath, fVerbose );
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_pba [-SFCT num] [-vh]\n" );
-    Abc_Print( -2, "\t         refines abstracted flop map with proof-based abstraction\n" );
-    Abc_Print( -2, "\t-S num : the starting timeframe for SAT check [default = %d]\n", nStart );
-    Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", nFramesMax );
-    Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", nConfMax );
-    Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", nTimeLimit );
+    Abc_Print( -2, "usage: &abs_refine [-M <num>] [-tsvh]\n" );
+    Abc_Print( -2, "\t         refines the pre-computed flop map using the counter-example\n" );
+    Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", nFfToAddMax );
+    Abc_Print( -2, "\t-t     : toggle trying four abstractions instead of one [default = %s]\n", fTryFour? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle using the path sensitization algorithm [default = %s]\n", fSensePath? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 } 
 
-#endif
 
 /**Function*************************************************************
 
@@ -28538,1029 +28811,6 @@ usage:
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9Reparam( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Gia_Man_t * pTemp = NULL;
-    int c, fVerbose = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Reparam(): There is no AIG.\n" );
-        return 0;
-    } 
-    pTemp = Gia_ManReparam( pAbc->pGia, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &reparam [-vh]\n" );
-    Abc_Print( -2, "\t        performs input trimming and reparameterization\n" );
-    Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9BackReach( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    extern Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose );
-
-    Gia_Man_t * pTemp = NULL;
-    int c, fVerbose = 0;
-    int nFrameMax = 1000000;
-    int nConfMax  = 1000000;
-    int nTimeMax  =      10;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCTvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nFrameMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nFrameMax < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfMax < 0 ) 
-                goto usage;
-            break;
-        case 'T':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nTimeMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nTimeMax < 0 ) 
-                goto usage;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9BackReach(): There is no AIG.\n" );
-        return 1;
-    }
-    if ( Gia_ManPoNum(pAbc->pGia) != 1 )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9BackReach(): The number of POs is different from 1.\n" );
-        return 1;
-    }
-    pTemp = Gia_ManCofTest( pAbc->pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
-    Abc_CommandUpdate9( pAbc, pTemp );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &back_reach [-FCT <num>] [-vh]\n" );
-    Abc_Print( -2, "\t         performs backward reachability by circuit cofactoring\n" );
-    Abc_Print( -2, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrameMax );
-    Abc_Print( -2, "\t-C num : the conflict limit at a node during induction [default = %d]\n", nConfMax );
-    Abc_Print( -2, "\t-T num : the timeout for property directed reachability [default = %d]\n", nTimeMax );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9Posplit( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    extern Aig_Man_t * Aig_ManSplit( Aig_Man_t * p, int nVars, int fVerbose );
-    Aig_Man_t * pMan, * pAux;
-    Gia_Man_t * pTemp = NULL;
-    int c, nVars = 5, fVerbose = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'N':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nVars = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nVars < 0 ) 
-                goto usage;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Posplit(): There is no AIG.\n" );
-        return 1;
-    } 
-    pMan = Gia_ManToAigSimple( pAbc->pGia );
-    pMan = Aig_ManSplit( pAux = pMan, nVars, fVerbose );
-    Aig_ManStop( pAux );
-    if ( pMan != NULL )
-    {
-        pTemp = Gia_ManFromAigSimple( pMan );
-        Aig_ManStop( pMan );
-        Abc_CommandUpdate9( pAbc, pTemp );
-    }
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &posplit [-N num] [-vh]\n" );
-    Abc_Print( -2, "\t         cofactors the property output w.r.t. a support subset\n" );
-    Abc_Print( -2, "\t         (the OR of new PO functions is equal to the original property)\n" );
-    Abc_Print( -2, "\t-N num : the number of random cofactoring variables [default = %d]\n", nVars );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9ReachM( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Gia_ParLlb_t Pars, * pPars = &Pars;
-    char * pLogFileName = NULL;
-    int c;
-    extern int Llb_ManModelCheckGia( Gia_Man_t * pGia, Gia_ParLlb_t * pPars );
-
-    // set defaults
-    Llb_ManSetDefaultParams( pPars );
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TBFCHSLripcsyzvwh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'T':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->TimeLimit < 0 ) 
-                goto usage;
-            break;
-        case 'B':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBddMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBddMax < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nIterMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nIterMax < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nClusterMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nClusterMax < 0 ) 
-                goto usage;
-            break;
-        case 'H':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nHintDepth = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nHintDepth < 0 ) 
-                goto usage;
-            break;
-        case 'S':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->HintFirst = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->HintFirst < 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
-                goto usage;
-            }
-            pLogFileName = argv[globalUtilOptind];
-            globalUtilOptind++;
-            break;
-        case 'r':
-            pPars->fReorder ^= 1;
-            break;
-        case 'i':
-            pPars->fIndConstr ^= 1;
-            break;
-        case 'p':
-            pPars->fUsePivots ^= 1;
-            break;
-        case 'c':
-            pPars->fCluster ^= 1;
-            break;
-        case 's':
-            pPars->fSchedule ^= 1;
-            break;
-        case 'y':
-            pPars->fSkipOutCheck ^= 1;
-            break;
-        case 'z':
-            pPars->fSkipReach ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'w':
-            pPars->fVeryVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachM(): There is no AIG.\n" );
-        return 1;
-    }
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachM(): The current AIG has no latches.\n" );
-        return 0;
-    } 
-    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachM(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
-        return 0;
-    }
-    pAbc->Status  = Llb_ManModelCheckGia( pAbc->pGia, pPars );
-    pAbc->nFrames = pPars->iFrame;
-    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
-    if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachm" );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &reachm [-TBFCHS num] [-L file] [-ripcsyzvwh]\n" );
-    Abc_Print( -2, "\t         model checking via BDD-based reachability (dependence-matrix-based)\n" );
-    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
-    Abc_Print( -2, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", pPars->nBddMax );
-    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
-    Abc_Print( -2, "\t-C num : max number of variables in a cluster [default = %d]\n", pPars->nClusterMax );
-    Abc_Print( -2, "\t-H num : max number of hints to use [default = %d]\n", pPars->nHintDepth );
-    Abc_Print( -2, "\t-S num : the number of the starting hint [default = %d]\n", pPars->HintFirst );
-    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
-    Abc_Print( -2, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", pPars->fReorder? "yes": "no" );  
-    Abc_Print( -2, "\t-i     : enable extraction of inductive constraints [default = %s]\n", pPars->fIndConstr? "yes": "no" );  
-    Abc_Print( -2, "\t-p     : enable partitions for internal cut-points [default = %s]\n", pPars->fUsePivots? "yes": "no" );  
-    Abc_Print( -2, "\t-c     : enable clustering of partitions [default = %s]\n", pPars->fCluster? "yes": "no" );  
-    Abc_Print( -2, "\t-s     : enable scheduling of clusters [default = %s]\n", pPars->fSchedule? "yes": "no" );  
-    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
-    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
-    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
-    Abc_Print( -2, "\t-w     : prints dependency matrix [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9ReachP( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Gia_ParLlb_t Pars, * pPars = &Pars;
-    Aig_Man_t * pMan;
-    char * pLogFileName = NULL;
-    int c;
-    extern int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
-
-    // set defaults
-    Llb_ManSetDefaultParams( pPars );
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NBFTLrbyzdvwh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'N':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nPartValue = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nPartValue < 0 ) 
-                goto usage;
-            break;
-        case 'B':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBddMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBddMax < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nIterMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nIterMax < 0 ) 
-                goto usage;
-            break;
-        case 'T':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->TimeLimit < 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
-                goto usage;
-            }
-            pLogFileName = argv[globalUtilOptind];
-            globalUtilOptind++;
-            break;
-        case 'r':
-            pPars->fReorder ^= 1;
-            break;
-        case 'b':
-            pPars->fBackward ^= 1;
-            break;
-        case 'y':
-            pPars->fSkipOutCheck ^= 1;
-            break;
-        case 'z':
-            pPars->fSkipReach ^= 1;
-            break;
-        case 'd':
-            pPars->fDumpReached ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'w':
-            pPars->fVeryVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachP(): There is no AIG.\n" );
-        return 1;
-    }
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachP(): The current AIG has no latches.\n" );
-        return 0;
-    }
-    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachP(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
-        return 0;
-    }
-    pMan          = Gia_ManToAigSimple( pAbc->pGia );
-    pAbc->Status  = Llb_ManReachMinCut( pMan, pPars );
-    pAbc->nFrames = pPars->iFrame;
-    Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
-    if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachp" );
-    Aig_ManStop( pMan );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &reachp [-NFT num] [-L file] [-rbyzdvwh]\n" );
-    Abc_Print( -2, "\t         model checking via BDD-based reachability (partitioning-based)\n" );
-    Abc_Print( -2, "\t-N num : partitioning value (MinVol=nANDs/N/2; MaxVol=nANDs/N) [default = %d]\n", pPars->nPartValue );
-//    Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax );
-    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
-    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
-    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
-    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
-    Abc_Print( -2, "\t-b     : perform backward reachability analysis [default = %s]\n", pPars->fBackward? "yes": "no" );  
-    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
-    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
-    Abc_Print( -2, "\t-d     : dump BDD of reached states into file \"reached.blif\" [default = %s]\n", pPars->fDumpReached? "yes": "no" );  
-    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
-    Abc_Print( -2, "\t-w     : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9ReachN( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Gia_ParLlb_t Pars, * pPars = &Pars;
-    Aig_Man_t * pMan;
-    char * pLogFileName = NULL;
-    int c;
-    extern int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
-
-    // set defaults
-    Llb_ManSetDefaultParams( pPars );
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLryzvwh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'B':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBddMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBddMax < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nIterMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nIterMax < 0 ) 
-                goto usage;
-            break;
-        case 'T':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->TimeLimit < 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
-                goto usage;
-            }
-            pLogFileName = argv[globalUtilOptind];
-            globalUtilOptind++;
-            break;
-        case 'r':
-            pPars->fReorder ^= 1;
-            break;
-        case 'y':
-            pPars->fSkipOutCheck ^= 1;
-            break;
-        case 'z':
-            pPars->fSkipReach ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'w':
-            pPars->fVeryVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachN(): There is no AIG.\n" );
-        return 1;
-    }
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" );
-        return 0;
-    }
-    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachN(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
-        return 0;
-    }
-    pMan          = Gia_ManToAigSimple( pAbc->pGia );
-    pAbc->Status  = Llb_NonlinCoreReach( pMan, pPars );
-    pAbc->nFrames = pPars->iFrame;
-    Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
-    if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" );
-    Aig_ManStop( pMan );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &reachn [-BFT num] [-L file] [-ryzvh]\n" );
-    Abc_Print( -2, "\t         model checking via BDD-based reachability (non-linear-QS-based)\n" );
-    Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax );
-    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
-    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
-    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
-    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
-    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
-    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
-    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
-//    Abc_Print( -2, "\t-w     : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-//    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Gia_ParLlb_t Pars, * pPars = &Pars;
-    Aig_Man_t * pMan;
-    char * pLogFileName = NULL;
-    int c;
-
-    // set defaults
-    Llb_ManSetDefaultParams( pPars );
-    pPars->fCluster = 0;
-    pPars->fReorder = 0;
-    pPars->nBddMax     = 100;
-    pPars->nClusterMax = 500;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BCFTLbcryzvwh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'B':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBddMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBddMax < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nClusterMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nClusterMax < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nIterMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nIterMax < 0 ) 
-                goto usage;
-            break;
-        case 'T':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->TimeLimit < 0 ) 
-                goto usage;
-            break;
-        case 'L':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
-                goto usage;
-            }
-            pLogFileName = argv[globalUtilOptind];
-            globalUtilOptind++;
-            break;
-        case 'b':
-            pPars->fBackward ^= 1;
-            break;
-        case 'c':
-            pPars->fCluster ^= 1;
-            break;
-        case 'r':
-            pPars->fReorder ^= 1;
-            break;
-        case 'y':
-            pPars->fSkipOutCheck ^= 1;
-            break;
-        case 'z':
-            pPars->fSkipReach ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'w':
-            pPars->fVeryVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachN(): There is no AIG.\n" );
-        return 1;
-    }
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" );
-        return 0;
-    }
-    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9ReachN(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
-        return 0;
-    }
-    pMan          = Gia_ManToAigSimple( pAbc->pGia );
-    pAbc->Status  = Llb_Nonlin4CoreReach( pMan, pPars );
-    pAbc->nFrames = pPars->iFrame;
-    Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
-    if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachy" );
-    Aig_ManStop( pMan );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &reachy [-BCFT num] [-L file] [-bcryzvh]\n" );
-    Abc_Print( -2, "\t         model checking via BDD-based reachability (non-linear-QS-based)\n" );
-    Abc_Print( -2, "\t-B num : the max BDD size to introduce cut points [default = %d]\n", pPars->nBddMax );
-    Abc_Print( -2, "\t-C num : the max BDD size to reparameterize/cluster [default = %d]\n", pPars->nClusterMax );
-    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
-    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
-    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
-    Abc_Print( -2, "\t-b     : enable using backward enumeration [default = %s]\n", pPars->fBackward? "yes": "no" );  
-    Abc_Print( -2, "\t-c     : enable reparametrization clustering [default = %s]\n", pPars->fCluster? "yes": "no" );  
-    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
-    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
-    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
-    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
-//    Abc_Print( -2, "\t-w     : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9Undo( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    int c;
-    // set defaults
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Undo(): There is no design.\n" );
-        return 1;
-    } 
-    if ( pAbc->pGia2 == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Undo(): There is no previously saved network.\n" );
-        return 1;
-    } 
-    Gia_ManStop( pAbc->pGia );
-    pAbc->pGia = pAbc->pGia2;
-    pAbc->pGia2 = NULL;
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &undo [-h]\n" );
-    Abc_Print( -2, "\t        reverses the previous AIG transformation\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Gia_Man_t * pAig;
-    Vec_Ptr_t * vPosEquivs;
-    int c, fDualOut = 0, fVerbose = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'd':
-            fDualOut ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Iso(): There is no AIG.\n" );
-        return 1;
-    }
-    if ( Gia_ManPoNum(pAbc->pGia) == 1 )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Iso(): The AIG has only one PO. Isomorphism detection is not performed.\n" );
-        return 1;
-    }
-    pAig = Gia_ManIsoReduce( pAbc->pGia, &vPosEquivs, fDualOut, fVerbose );
-    if ( pAig == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9Iso(): Transformation has failed.\n" );
-        return 1;
-    }
-    // update the internal storage of PO equivalences
-    Abc_FrameReplacePoEquivs( pAbc, &vPosEquivs );
-    // update the AIG
-    Abc_CommandUpdate9( pAbc, pAig );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &iso [-dvh]\n" );
-    Abc_Print( -2, "\t         removes POs with isomorphic sequential COI\n" );
-    Abc_Print( -2, "\t-d     : treat the current AIG as a dual-output miter [default = %s]\n", fDualOut? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandAbc9CexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    extern Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int nRealPis, int fJustMax, int fUseAll, int fVerbose );
-    Abc_Cex_t * pCexNew;
-    int iFrameStart = 0;
-    int nRealPis = -1;
-    int fJustMax = 1;
-    int fUseAll = 0;
-    int c, fVerbose = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FNjavh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            iFrameStart = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( iFrameStart < 0 ) 
-                goto usage;
-            break;
-        case 'N':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nRealPis = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nRealPis < 0 ) 
-                goto usage;
-            break;
-        case 'j':
-            fJustMax ^= 1;
-            break;
-        case 'a':
-            fUseAll ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pAbc->pGia == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9CexMin(): There is no AIG.\n" );
-        return 1;
-    } 
-    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9CexMin(): The network is combinational.\n" );
-        return 0;
-    }
-    if ( pAbc->pCex == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9CexMin(): There is no counter-example.\n" );
-        return 1;
-    } 
-    pCexNew = Gia_ManCexMin( pAbc->pGia, pAbc->pCex, iFrameStart, nRealPis, fJustMax, fUseAll, fVerbose );
-    if ( pCexNew )
-        Abc_FrameReplaceCex( pAbc, &pCexNew );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: &cexmin [-FN num] [-javh]\n" );
-    Abc_Print( -2, "\t         minimizes a deep counter-example\n" );
-    Abc_Print( -2, "\t-F num : starting timeframe for minimization [default = %d]\n", iFrameStart );
-    Abc_Print( -2, "\t-N num : the number of real primary inputs [default = %d]\n", nRealPis );
-    Abc_Print( -2, "\t-j     : toggle computing all justifying assignments [default = %s]\n", fJustMax? "yes": "no" );
-    Abc_Print( -2, "\t-a     : toggle using all terminal objects [default = %s]\n", fUseAll? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-} 
 
 /**Function*************************************************************