Merged alanmi/abc into default

16 files changed, 1270 insertions, 56 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 6c0d96d1..fad0b804 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -825,6 +825,7 @@ extern ABC_DLL void               Abc_NtkDontCareFree( Odc_Man_t * p );
 extern ABC_DLL int                Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth );
 /*=== abcPrint.c ==========================================================*/
 extern ABC_DLL float              Abc_NtkMfsTotalSwitching( Abc_Ntk_t * pNtk );
+extern ABC_DLL float              Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose );
 extern ABC_DLL void               Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes, int fPower, int fGlitch, int fSkipBuf, int fSkipSmall, int fPrintMem );
 extern ABC_DLL void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk, int fPrintFlops );
 extern ABC_DLL void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 466af66a..7fc45f48 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -61,6 +61,7 @@
 #include "bool/rpo/rpo.h"
 #include "map/mpm/mpm.h"
 #include "opt/fret/fretime.h"
+#include "opt/nwk/nwkMerge.h"
 
 #ifndef _WIN32
 #include <unistd.h>
@@ -121,10 +122,11 @@ static int Abc_CommandMfs                    ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandMfs2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMfs3                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTrace                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandGlitch                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSpeedup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPowerdown              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAddBuffs               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestDec                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestNpn                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestRPO                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -315,6 +317,7 @@ static int Abc_CommandPSat                   ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandProve                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEco                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc3                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -771,10 +774,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs2",          Abc_CommandMfs2,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "mfs3",          Abc_CommandMfs3,             1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "trace",         Abc_CommandTrace,            0 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "glitch",        Abc_CommandGlitch,           0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "powerdown",     Abc_CommandPowerdown,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "addbuffs",      Abc_CommandAddBuffs,         1 );
-//    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testdec",       Abc_CommandTestDec,          0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testnpn",       Abc_CommandTestNpn,          0 );
     Cmd_CommandAdd( pAbc, "LogiCS",       "testrpo",       Abc_CommandTestRPO,          0 );
@@ -965,6 +969,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
+    Cmd_CommandAdd( pAbc, "Verification", "eco",           Abc_CommandEco,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc",           Abc_CommandBmc,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc2",          Abc_CommandBmc2,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc3",          Abc_CommandBmc3,             1 );
@@ -1000,12 +1005,14 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&save",         Abc_CommandAbc9Save,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&load",         Abc_CommandAbc9Load,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&r",            Abc_CommandAbc9Read,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&read",         Abc_CommandAbc9Read,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_blif",    Abc_CommandAbc9ReadBlif,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_cblif",   Abc_CommandAbc9ReadCBlif,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_stg",     Abc_CommandAbc9ReadStg,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&read_ver",     Abc_CommandAbc9ReadVer,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&write_ver",    Abc_CommandAbc9WriteVer,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&w",            Abc_CommandAbc9Write,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&write",        Abc_CommandAbc9Write,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&wlut",         Abc_CommandAbc9WriteLut,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&ps",           Abc_CommandAbc9Ps,           0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&pfan",         Abc_CommandAbc9PFan,         0 );
@@ -5715,6 +5722,88 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandGlitch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    int nPats    = 4000;
+    int Prob     =    8;
+    int fVerbose =    1;
+    int c;
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NPvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPats = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPats < 1 )
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Prob = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Prob < 1 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsLogic(pNtk) )
+    {
+        Abc_Print( -1, "This command can only be applied to a mapped logic network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsMappedLogic(pNtk) || Abc_NtkGetFaninMax(pNtk) <= 6 )
+        Abc_Print( 1, "Glitching adds %7.2f %% of signal transitions, compared to switching.\n", Abc_NtkMfsTotalGlitching(pNtk, nPats, Prob, fVerbose) );
+    else
+        printf( "Currently computes glitching only for K-LUT networks with K <= 6.\n" );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: glitch [-NP <num>] [-vh]\n" );
+    Abc_Print( -2, "\t           comparing glitching activity to switching activity\n" );
+    Abc_Print( -2, "\t-N <num> : the number of random patterns to use (0 < num < 1000000) [default = %d]\n", nPats );
+    Abc_Print( -2, "\t-P <num> : once in how many cycles an input changes its value [default = %d]\n", Prob );
+    Abc_Print( -2, "\t-v       : toggle printing optimization summary [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_CommandSpeedup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -6009,7 +6098,7 @@ usage:
     return 1;
 }
 
-#if 0
+//#if 0
 /**Function*************************************************************
 
   Synopsis    []
@@ -6142,7 +6231,7 @@ usage:
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
 }
-#endif
+//#endif
 
 
 
@@ -23862,6 +23951,50 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandEco( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Abc_NtkEco( char * pFileNames[3] );
+    char * pFileNames[3] = {NULL};  int c;
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( globalUtilOptind + 3 != argc )
+    {
+        Abc_Print( -1, "Expecting three file names on the command line.\n" );
+        return 1;
+    }
+    for ( c = 0; c < 3; c++ )
+        pFileNames[c] = argv[globalUtilOptind+c];
+    Abc_NtkEco( pFileNames );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: eco [-h]\n" );
+    Abc_Print( -2, "\t        performs experimental ECO computation\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
@@ -42428,7 +42561,7 @@ usage:
     Abc_Print( -2, "\t-Q num  : stop when abstraction size exceeds num %% during refinement (0<=num<=100) [default = %d]\n", pPars->nRatioMin2 );
     Abc_Print( -2, "\t-P num  : maximum percentage of added objects before a restart (0<=num<=100) [default = %d]\n", pPars->nRatioMax );
     Abc_Print( -2, "\t-B num  : the number of stable frames to call prover or dump abstraction [default = %d]\n", pPars->nFramesNoChangeLim );
-    Abc_Print( -2, "\t-A file : file name for dumping abstrated model [default = \"glabs.aig\"]\n" );
+    Abc_Print( -2, "\t-A file : file name for dumping abstrated model (&gla -d) or abstraction map (&gla -m)\n" );
     Abc_Print( -2, "\t-f      : toggle propagating fanout implications [default = %s]\n", pPars->fPropFanout? "yes": "no" );
     Abc_Print( -2, "\t-a      : toggle refinement by adding one layers of gates [default = %s]\n", pPars->fAddLayer? "yes": "no" );
     Abc_Print( -2, "\t-r      : toggle using improved refinement heuristics [default = %s]\n", pPars->fNewRefine? "yes": "no" );
diff --git a/src/base/abci/abcEco.c b/src/base/abci/abcEco.c
new file mode 100644
index 00000000..70a76729
--- /dev/null
+++ b/src/base/abci/abcEco.c
@@ -0,0 +1,58 @@
+/**CFile****************************************************************
+
+  FileName    [abcEco.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Experimental procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcEco.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "base/main/main.h"
+#include "map/mio/mio.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkEco( char * pFileNames[3] )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 4e588e2d..f758d0f0 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -923,9 +923,9 @@ void Abc_NtkPrintMiniMapping( int * pArray )
   SeeAlso     []
 
 ***********************************************************************/
-int * Abc_NtkOutputMiniMapping( void * pAbc0 )
+int * Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     Vec_Int_t * vMapping;
     int * pArray;
@@ -977,9 +977,9 @@ void Abc_NtkTestMiniMapping( Abc_Ntk_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
+void Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     if ( pAbc == NULL )
@@ -1001,9 +1001,9 @@ void Abc_NtkSetCiArrivalTime( void * pAbc0, int iCi, float Rise, float Fall )
     pNode = Abc_NtkCi( pNtk, iCi );
     Abc_NtkTimeSetArrival( pNtk, Abc_ObjId(pNode), Rise, Fall );
 }
-void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
+void Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     Abc_Obj_t * pNode;
     if ( pAbc == NULL )\
@@ -1037,9 +1037,9 @@ void Abc_NtkSetCoRequiredTime( void * pAbc0, int iCo, float Rise, float Fall )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSetAndGateDelay( void * pAbc0, float Delay )
+void Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay )
 {
-    Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
+    //Abc_Frame_t * pAbc = (Abc_Frame_t *)pAbc0;
     Abc_Ntk_t * pNtk;
     if ( pAbc == NULL )
     {
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2129782f..ea91619c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -351,9 +351,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
         Abc_Print( 1,"  power =%7.2f", Abc_NtkMfsTotalSwitching(pNtk) );
     if ( fGlitch )
     {
-        extern float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk );
         if ( Abc_NtkIsLogic(pNtk) && Abc_NtkGetFaninMax(pNtk) <= 6 )
-            Abc_Print( 1,"  glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk) );
+            Abc_Print( 1,"  glitch =%7.2f %%", Abc_NtkMfsTotalGlitching(pNtk, 4000, 8, 0) );
         else
             printf( "\nCurrently computes glitching only for K-LUT networks with K <= 6." );
     }
@@ -1744,7 +1743,7 @@ extern Gli_Man_t * Gli_ManAlloc( int nObjs, int nRegs, int nFanioPairs );
 extern void        Gli_ManStop( Gli_Man_t * p );
 extern int         Gli_ManCreateCi( Gli_Man_t * p, int nFanouts );
 extern int         Gli_ManCreateCo( Gli_Man_t * p, int iFanin );
-extern int         Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, unsigned * puTruth );
+extern int         Gli_ManCreateNode( Gli_Man_t * p, Vec_Int_t * vFanins, int nFanouts, word * pGateTruth );
 
 extern void        Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb, int fVerbose );
 extern int         Gli_ObjNumSwitches( Gli_Man_t * p, int iNode );
@@ -1761,13 +1760,14 @@ extern int         Gli_ObjNumGlitches( Gli_Man_t * p, int iNode );
   SeeAlso     []
 
 ***********************************************************************/
-float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
+float Abc_NtkMfsTotalGlitchingLut( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
 {
     int nSwitches, nGlitches;
     Gli_Man_t * p;
     Vec_Ptr_t * vNodes;
     Vec_Int_t * vFanins, * vTruth;
     Abc_Obj_t * pObj, * pFanin;
+    Vec_Wrd_t * vTruths; word * pTruth;
     unsigned * puTruth;
     int i, k;
     assert( Abc_NtkIsLogic(pNtk) );
@@ -1781,6 +1781,7 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
     vNodes = Abc_NtkDfs( pNtk, 0 );
     vFanins = Vec_IntAlloc( 6 );
     vTruth = Vec_IntAlloc( 1 << 12 );
+    vTruths = Vec_WrdStart( Abc_NtkObjNumMax(pNtk) );
 
     // derive network for glitch computation
     p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
@@ -1795,7 +1796,9 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
         Abc_ObjForEachFanin( pObj, pFanin, k )
             Vec_IntPush( vFanins, pFanin->iTemp );
         puTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pObj->pData, Abc_ObjFaninNum(pObj), vTruth, 0 );
-        pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), puTruth );
+        pTruth = Vec_WrdEntryP( vTruths, Abc_ObjId(pObj) );
+        *pTruth = ((word)puTruth[Abc_ObjFaninNum(pObj) == 6] << 32) | (word)puTruth[0];
+        pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), pTruth );
     }
     Abc_NtkForEachCo( pNtk, pObj, i )
         Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
@@ -1816,6 +1819,72 @@ float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk )
     Vec_PtrFree( vNodes );
     Vec_IntFree( vTruth );
     Vec_IntFree( vFanins );
+    Vec_WrdFree( vTruths );
+    return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the percentable of increased power due to glitching.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Abc_NtkMfsTotalGlitching( Abc_Ntk_t * pNtk, int nPats, int Prob, int fVerbose )
+{
+    int nSwitches, nGlitches;
+    Gli_Man_t * p;
+    Vec_Ptr_t * vNodes;
+    Vec_Int_t * vFanins;
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nFaninMax = Abc_NtkGetFaninMax(pNtk);
+    if ( !Abc_NtkIsMappedLogic(pNtk) )
+        return Abc_NtkMfsTotalGlitchingLut( pNtk, nPats, Prob, fVerbose );
+    assert( Abc_NtkIsMappedLogic(pNtk) );
+    if ( nFaninMax > 16 )
+    {
+        printf( "Abc_NtkMfsTotalGlitching() This procedure works only for mapped networks with LUTs size up to 6 inputs.\n" );
+        return -1.0;
+    }
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    vFanins = Vec_IntAlloc( 6 );
+
+    // derive network for glitch computation
+    p = Gli_ManAlloc( Vec_PtrSize(vNodes) + Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk),
+        Abc_NtkLatchNum(pNtk), Abc_NtkGetTotalFanins(pNtk) + Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->iTemp = -1;
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->iTemp = Gli_ManCreateCi( p, Abc_ObjFanoutNum(pObj) );
+    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+    {
+        Vec_IntClear( vFanins );
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+            Vec_IntPush( vFanins, pFanin->iTemp );
+        pObj->iTemp = Gli_ManCreateNode( p, vFanins, Abc_ObjFanoutNum(pObj), Mio_GateReadTruthP((Mio_Gate_t *)pObj->pData) );
+    }
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Gli_ManCreateCo( p, Abc_ObjFanin0(pObj)->iTemp );
+
+    // compute glitching
+    Gli_ManSwitchesAndGlitches( p, nPats, 1.0/Prob, fVerbose );
+
+    // compute the ratio
+    nSwitches = nGlitches = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        if ( pObj->iTemp >= 0 )
+        {
+            nSwitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumSwitches(p, pObj->iTemp);
+            nGlitches += Abc_ObjFanoutNum(pObj) * Gli_ObjNumGlitches(p, pObj->iTemp);
+        }
+
+    Gli_ManStop( p );
+    Vec_PtrFree( vNodes );
+    Vec_IntFree( vFanins );
     return nSwitches ? 100.0*(nGlitches-nSwitches)/nSwitches : 0.0;
 }
 
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index b97f526f..abf56716 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -17,6 +17,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDress2.c \
     src/base/abci/abcDress3.c \
     src/base/abci/abcDsd.c \
+    src/base/abci/abcEco.c \
     src/base/abci/abcExact.c \
     src/base/abci/abcExtract.c \
     src/base/abci/abcFraig.c \
diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c
index d1ff0a9d..36e546a7 100644
--- a/src/base/cmd/cmdHist.c
+++ b/src/base/cmd/cmdHist.c
@@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define ABC_USE_HISTORY 1
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -99,7 +101,7 @@ void Cmd_HistoryAddCommand(    Abc_Frame_t * p, const char * command )
 ***********************************************************************/
 void Cmd_HistoryRead( Abc_Frame_t * p )
 {
-#if defined(WIN32) 
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
     char Buffer[ABC_MAX_STR];
     FILE * pFile;
     assert( Vec_PtrSize(p->aHistory) == 0 );
@@ -130,7 +132,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p )
 ***********************************************************************/
 void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
 {
-#if defined(WIN32) 
+#if defined(WIN32) && defined(ABC_USE_HISTORY)
     FILE * pFile;
     char * pStr; 
     int i;
@@ -160,7 +162,7 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
 ***********************************************************************/
 void Cmd_HistoryPrint( Abc_Frame_t * p, int Limit )
 {
-#if defined(WIN32) 
+#if defined(WIN32) && defined(ABC_USE_HISTORY) 
     char * pStr; 
     int i;
     Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
new file mode 100644
index 00000000..3445a00f
--- /dev/null
+++ b/src/base/main/abcapis.h
@@ -0,0 +1,102 @@
+/**CFile****************************************************************
+
+  FileName    [abcapis.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Include this file in the external code calling ABC.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 29, 2012.]
+
+  Revision    [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef MINI_AIG__abc_apis_h
+#define MINI_AIG__abc_apis_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_Frame_t_      Abc_Frame_t;
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+#ifdef WIN32
+  #ifdef WIN32_NO_DLL
+    #define ABC_DLLEXPORT
+    #define ABC_DLLIMPORT
+  #else
+    #define ABC_DLLEXPORT __declspec(dllexport)
+    #define ABC_DLLIMPORT __declspec(dllimport)
+  #endif
+#else  /* defined(WIN32) */
+#define ABC_DLLIMPORT
+#endif /* defined(WIN32) */
+
+#ifndef ABC_DLL
+#define ABC_DLL ABC_DLLIMPORT
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// procedures to start and stop the ABC framework
+extern ABC_DLL void   Abc_Start();
+extern ABC_DLL void   Abc_Stop();
+
+// procedures to get the ABC framework (pAbc) and execute commands in it
+extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame();
+extern ABC_DLL int   Cmd_CommandExecute( Abc_Frame_t * pAbc, const char * pCommandLine );
+
+// procedures to input/output 'mini AIG'
+extern ABC_DLL void   Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * pMiniAig );
+extern ABC_DLL void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void   Abc_FrameGiaInputMiniAig( Abc_Frame_t * pAbc, void * p );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniAig( Abc_Frame_t * pAbc );
+extern ABC_DLL void   Abc_NtkSetFlopNum( Abc_Frame_t * pAbc, int nFlops );
+
+// procedures to input/output 'mini LUT'
+extern ABC_DLL void   Abc_FrameGiaInputMiniLut( Abc_Frame_t * pAbc, void * pMiniLut );
+extern ABC_DLL void * Abc_FrameGiaOutputMiniLut( Abc_Frame_t * pAbc );
+
+// procedures to set CI/CO arrival/required times
+extern ABC_DLL void   Abc_NtkSetCiArrivalTime( Abc_Frame_t * pAbc, int iCi, float Rise, float Fall );
+extern ABC_DLL void   Abc_NtkSetCoRequiredTime( Abc_Frame_t * pAbc, int iCo, float Rise, float Fall );
+
+// procedure to set AND-gate delay to tech-independent synthesis and mapping
+extern ABC_DLL void   Abc_NtkSetAndGateDelay( Abc_Frame_t * pAbc, float Delay );
+
+// procedures to return the mapped network
+extern ABC_DLL int *  Abc_NtkOutputMiniMapping( Abc_Frame_t * pAbc );
+extern ABC_DLL void   Abc_NtkPrintMiniMapping( int * pArray );
+
+// procedures to access verifization status and a counter-example
+extern ABC_DLL int    Abc_FrameReadProbStatus( Abc_Frame_t * pAbc );   
+extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * pAbc );    
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/main/abcapis_old.h b/src/base/main/abcapis_old.h
new file mode 100644
index 00000000..b2703bea
--- /dev/null
+++ b/src/base/main/abcapis_old.h
@@ -0,0 +1,84 @@
+/**CFile****************************************************************
+
+  FileName    [abcapis.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Include this file in the external code calling ABC.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 29, 2012.]
+
+  Revision    [$Id: abcapis.h,v 1.00 2012/09/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef MINI_AIG__abc_apis_old_h
+#define MINI_AIG__abc_apis_old_h
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+// procedures to start and stop the ABC framework
+extern void   Abc_Start();
+extern void   Abc_Stop();
+
+// procedures to get the ABC framework (pAbc) and execute commands in it
+extern void * Abc_FrameGetGlobalFrame();
+extern int    Cmd_CommandExecute( void * pAbc, char * pCommandLine );
+
+// procedures to input/output 'mini AIG'
+extern void   Abc_NtkInputMiniAig( void * pAbc, void * pMiniAig );
+extern void * Abc_NtkOutputMiniAig( void * pAbc );
+extern void   Abc_FrameGiaInputMiniAig( void * pAbc, void * p );
+extern void * Abc_FrameGiaOutputMiniAig( void * pAbc );
+extern void   Abc_NtkSetFlopNum( void * pAbc, int nFlops );
+
+// procedures to input/output 'mini LUT'
+extern void   Abc_FrameGiaInputMiniLut( void * pAbc, void * pMiniLut );
+extern void * Abc_FrameGiaOutputMiniLut( void * pAbc );
+
+// procedures to set CI/CO arrival/required times
+extern void   Abc_NtkSetCiArrivalTime( void * pAbc, int iCi, float Rise, float Fall );
+extern void   Abc_NtkSetCoRequiredTime( void * pAbc, int iCo, float Rise, float Fall );
+
+// procedure to set AND-gate delay to tech-independent synthesis and mapping
+extern void   Abc_NtkSetAndGateDelay( void * pAbc, float Delay );
+
+// procedures to return the mapped network
+extern int *  Abc_NtkOutputMiniMapping( void * pAbc );
+extern void   Abc_NtkPrintMiniMapping( int * pArray );
+
+// procedures to access verifization status and a counter-example
+extern int    Abc_FrameReadProbStatus( void * pAbc );   
+extern void * Abc_FrameReadCex( void * pAbc );    
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 89353fa6..a59a9a40 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -34,10 +34,8 @@
 #include "misc/vec/vec.h"
 #include "misc/st/st.h"
 
-ABC_NAMESPACE_HEADER_START
-// the framework containing all data
-typedef struct Abc_Frame_t_      Abc_Frame_t;
-ABC_NAMESPACE_HEADER_END
+// the framework containing all data is defined here
+#include "abcapis.h"
 
 #include "base/cmd/cmd.h"
 #include "base/io/ioAbc.h"
@@ -116,7 +114,7 @@ extern ABC_DLL void            Abc_FrameSetBridgeMode();
 
 extern ABC_DLL int             Abc_FrameReadBmcFrames( Abc_Frame_t * p );              
 extern ABC_DLL int             Abc_FrameReadProbStatus( Abc_Frame_t * p );              
-extern ABC_DLL Abc_Cex_t *     Abc_FrameReadCex( Abc_Frame_t * p );              
+extern ABC_DLL void *          Abc_FrameReadCex( Abc_Frame_t * p );              
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadCexVec( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Int_t *     Abc_FrameReadStatusVec( Abc_Frame_t * p );  
 extern ABC_DLL Vec_Ptr_t *     Abc_FrameReadPoEquivs( Abc_Frame_t * p );  
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 9647d020..cd4ff2c7 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -69,7 +69,7 @@ char *      Abc_FrameReadFlag( char * pFlag )                { return Cmd_FlagRe
 
 int         Abc_FrameReadBmcFrames( Abc_Frame_t * p )        { return s_GlobalFrame->nFrames;      }               
 int         Abc_FrameReadProbStatus( Abc_Frame_t * p )       { return s_GlobalFrame->Status;       }               
-Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * p )              { return s_GlobalFrame->pCex;         }        
+void *      Abc_FrameReadCex( Abc_Frame_t * p )              { return s_GlobalFrame->pCex;         }        
 Vec_Ptr_t * Abc_FrameReadCexVec( Abc_Frame_t * p )           { return s_GlobalFrame->vCexVec;      }        
 Vec_Int_t * Abc_FrameReadStatusVec( Abc_Frame_t * p )        { return s_GlobalFrame->vStatuses;    }        
 Vec_Ptr_t * Abc_FrameReadPoEquivs( Abc_Frame_t * p )         { return s_GlobalFrame->vPoEquivs;    }        
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 686d9f00..f5dbba42 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -169,9 +169,14 @@ struct Wlc_Par_t_
     int                    nBitsMux;           // MUX bit-width
     int                    nBitsFlop;          // flop bit-width
     int                    nIterMax;           // the max number of iterations
+    int                    nLimit;             // the max number of signals
     int                    fXorOutput;         // XOR outputs of word-level miter
-    int                    fCheckClauses;      // Check clauses in the reloaded trace                    
-    int                    fPushClauses;       // Push clauses in the reloaded trace                    
+    int                    fCheckClauses;      // Check clauses in the reloaded trace
+    int                    fPushClauses;       // Push clauses in the reloaded trace
+    int                    fMFFC;              // Refine the entire MFFC of a PPI
+    int                    fPdra;              // Use pdr -nct
+    int                    fProofRefine;       // Use proof-based refinement
+    int                    fHybrid;            // Use a hybrid of CBR and PBR
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
@@ -309,6 +314,7 @@ extern void           Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
 extern char *         Wlc_NtkNewName( Wlc_Ntk_t * p, int iCoId, int fSeq );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq );
 extern Wlc_Ntk_t *    Wlc_NtkDupDfsAbs( Wlc_Ntk_t * p, Vec_Int_t * vPisOld, Vec_Int_t * vPisNew, Vec_Int_t * vFlops );
+extern Wlc_Ntk_t *    Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p );
 extern void           Wlc_NtkCleanMarks( Wlc_Ntk_t * p );
 extern void           Wlc_NtkMarkCone( Wlc_Ntk_t * p, int iCoId, int Range, int fSeq, int fAllPis );
 extern void           Wlc_NtkProfileCones( Wlc_Ntk_t * p );
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index e33424f7..ad6c6642 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -34,10 +34,616 @@ extern Vec_Vec_t *   IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
 extern int           IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
 extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
 
+typedef struct Int_Pair_t_       Int_Pair_t;
+struct Int_Pair_t_
+{
+    int first;
+    int second;
+};
+
+int IntPairPtrCompare ( Int_Pair_t ** a, Int_Pair_t ** b )
+{
+    return (*a)->second < (*b)->second; 
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+int Wlc_NtkNumPiBits( Wlc_Ntk_t * pNtk ) 
+{
+    int num = 0;
+    int i;
+    Wlc_Obj_t * pObj;
+    Wlc_NtkForEachPi(pNtk, pObj, i) {
+        num += Wlc_ObjRange(pObj);
+    }
+    return num;
+}
+
+static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, Vec_Bit_t * vMark, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars ) 
+{
+    Vec_Int_t * vCores = NULL;
+    Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames );
+    Cnf_Dat_t * pCnf = Cnf_Derive(pAigFrames, Aig_ManCoNum(pAigFrames));
+    sat_solver * pSat = sat_solver_new();
+    int i;
+
+    sat_solver_setnvars(pSat, pCnf->nVars);
+
+    for (i = 0; i < pCnf->nClauses; i++) 
+    {
+        if (!sat_solver_addclause(pSat, pCnf->pClauses[i], pCnf->pClauses[i + 1]))
+            assert(false);
+    }
+    // add PO clauses
+    {
+        Vec_Int_t* vLits = Vec_IntAlloc(100);
+        Aig_Obj_t* pObj;
+        int i, ret;
+        Aig_ManForEachCo( pAigFrames, pObj, i )
+        {
+            assert(pCnf->pVarNums[pObj->Id] >= 0);
+            Vec_IntPush(vLits, toLitCond(pCnf->pVarNums[pObj->Id], 0));
+        }
+        ret = sat_solver_addclause(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits));
+        if (!ret) 
+            Abc_Print( 1, "UNSAT after adding PO clauses.\n" );
+
+        Vec_IntFree(vLits);
+    }
+    // main procedure
+    {
+        int status;
+        Vec_Int_t* vLits = Vec_IntAlloc(100);
+        Vec_Int_t* vMapVar2Sel = Vec_IntStart( pCnf->nVars );
+        int first_sel_pi = sel_pi_first ? 0 : num_other_pis;
+        for ( i = 0; i < num_sel_pis; ++i ) 
+        {
+            int cur_pi = first_sel_pi + i;
+            int var = pCnf->pVarNums[Aig_ManCi(pAigFrames, cur_pi)->Id];
+            int Lit;
+            assert(var >= 0);
+            Vec_IntWriteEntry( vMapVar2Sel, var, i );
+            Lit = toLitCond( var, 0 );
+            if ( Vec_BitEntry( vMark, i ) )
+                Vec_IntPush(vLits, Lit);
+            else
+                sat_solver_addclause( pSat, &Lit, &Lit+1 );
+        }
+        /*
+            int i, Entry;
+            Abc_Print( 1, "#vLits = %d; vLits = ", Vec_IntSize(vLits) );
+            Vec_IntForEachEntry(vLits, Entry, i)
+                Abc_Print( 1, "%d ", Entry);
+            Abc_Print( 1, "\n");
+        */
+        status = sat_solver_solve(pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)(nConfLimit), (ABC_INT64_T)(0), (ABC_INT64_T)(0), (ABC_INT64_T)(0));
+        if (status == l_False) {
+            int nCoreLits, *pCoreLits;
+            Abc_Print( 1, "UNSAT.\n" );
+            nCoreLits = sat_solver_final(pSat, &pCoreLits);
+            vCores = Vec_IntAlloc( nCoreLits );
+            for (i = 0; i < nCoreLits; i++) 
+            {
+                Vec_IntPush( vCores, Vec_IntEntry( vMapVar2Sel, lit_var( pCoreLits[i] ) ) );
+            }
+        } else if (status == l_True) {
+            Abc_Print( 1, "SAT.\n" );
+        } else {
+            Abc_Print( 1, "UNKNOWN.\n" );
+        }
+
+        Vec_IntFree(vLits);
+        Vec_IntFree(vMapVar2Sel);
+    }
+    Cnf_ManFree();
+    sat_solver_delete(pSat);
+    Aig_ManStop(pAigFrames);
+
+    return vCores;
+}
+
+static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first) 
+{
+    Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0 );
+    int nbits_new_pis = Wlc_NtkNumPiBits( pChoice );
+    int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis;
+    int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis;
+    Gia_Man_t * pFrames = NULL;
+    Gia_Obj_t * pObj, * pObjRi;
+    int f, i;
+    int is_sel_pi;
+    Gia_Man_t * pGia;
+    *p_num_ppis = num_ppis;
+
+    Abc_Print( 1, "#orig_pis = %d, #ppis = %d, #sel_pis = %d, #undc_pis = %d\n", nbits_old_pis, num_ppis, num_sel_pis, num_undc_pis );
+    assert(Gia_ManPiNum(pGiaChoice)==nbits_old_pis+num_ppis+num_sel_pis+num_undc_pis);
+    assert(Gia_ManPiNum(pGiaChoice)==pCex->nPis+num_sel_pis);
+
+    pFrames = Gia_ManStart( 10000 );
+    pFrames->pName = Abc_UtilStrsav( pGiaChoice->pName );
+    Gia_ManHashAlloc( pFrames );
+    Gia_ManConst0(pGiaChoice)->Value = 0;
+    Gia_ManForEachRi( pGiaChoice, pObj, i )
+        pObj->Value = 0;
+
+    for ( f = 0; f <= pCex->iFrame; f++ ) 
+    {
+        for( i = 0; i < Gia_ManPiNum(pGiaChoice); i++ ) 
+        {
+            if ( i >= nbits_old_pis && i < nbits_old_pis + num_ppis + num_sel_pis ) 
+            {
+                is_sel_pi = sel_pi_first ? (i < nbits_old_pis + num_sel_pis) : (i >= nbits_old_pis + num_ppis);
+                if(f == 0 || !is_sel_pi)
+                    Gia_ManPi(pGiaChoice, i)->Value = Gia_ManAppendCi(pFrames);
+            } 
+            else if (i < nbits_old_pis) 
+            {
+                Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i);
+            } 
+            else if (i >= nbits_old_pis + num_ppis + num_sel_pis) 
+            {
+                Gia_ManPi(pGiaChoice, i)->Value = Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i - num_sel_pis - num_ppis);
+            }
+        }
+        Gia_ManForEachRiRo( pGiaChoice, pObjRi, pObj, i )
+            pObj->Value = pObjRi->Value;
+        Gia_ManForEachAnd( pGiaChoice, pObj, i )
+            pObj->Value = Gia_ManHashAnd(pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj));
+        Gia_ManForEachCo( pGiaChoice, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+        Gia_ManForEachPo( pGiaChoice, pObj, i )
+            Gia_ManAppendCo(pFrames, pObj->Value);
+    }
+    Gia_ManHashStop (pFrames);
+    Gia_ManSetRegNum(pFrames, 0);
+    pFrames = Gia_ManCleanup(pGia = pFrames);
+    Gia_ManStop(pGia);
+    Gia_ManStop(pGiaChoice);
+
+    return pFrames;
+}
+
+Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks )
+{
+    //if ( vBlacks== NULL ) return NULL;
+    Vec_Int_t * vNodes = Vec_IntDup( vBlacks );
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    int i, k, iObj, iFanin;
+    Vec_Int_t * vFanins = Vec_IntAlloc( 3 );
+    Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+    Vec_Int_t * vMapNode2Sel = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+    int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
+    Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
+
+    Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) 
+    {
+        // TODO : fix FOs here
+        Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
+    }
+
+    // Vec_IntPrint(vNodes);
+    Wlc_NtkCleanCopy( p );
+
+    // mark nodes
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        pObj->Mark = 1;
+        // add fresh PI with the same number of bits
+        Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
+    }
+
+    // add sel PI
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
+    {
+        iObj = Wlc_ObjId( p, pObj );
+        Vec_IntWriteEntry( vMapNode2Sel, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, 0, 0, 0 ) );
+    }
+
+    // iterate through the nodes in the DFS order
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        int isSigned, range;
+        if ( i == nOrigObjNum ) 
+        {
+            // cout << "break at " << i << endl;
+            break;
+        }
+        if ( pObj->Mark ) 
+        {
+            // clean
+            pObj->Mark = 0;
+
+            isSigned = Wlc_ObjIsSigned(pObj);
+            range = Wlc_ObjRange(pObj);
+            Vec_IntClear(vFanins);
+            Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Sel, i) );
+            Vec_IntPush(vFanins, Vec_IntEntry( vMapNode2Pi, i ) );
+            Vec_IntPush(vFanins, i);
+            iObj = Wlc_ObjCreate(p, WLC_OBJ_MUX, isSigned, range - 1, 0, vFanins);
+        }
+        else 
+        {
+            // update fanins
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+            // node to remain
+            iObj = i;
+        }
+        Wlc_ObjSetCopy( p, i, iObj );
+    }
+
+    Wlc_NtkForEachCo( p, pObj, i )
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        if (iObj != Wlc_ObjCopy(p, iObj)) 
+        {
+            if (pObj->fIsFi)
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1;
+            else
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1;
+
+            Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj));
+        }
+    }
+
+    // DumpWlcNtk(p);
+    pNew = Wlc_NtkDupDfsSimple( p );
+
+    Vec_IntFree( vFanins );
+    Vec_IntFree( vMapNode2Pi );
+    Vec_IntFree( vMapNode2Sel );
+    Vec_IntFree( vNodes );
+    Wlc_NtkFree( p );
+
+    return pNew;
+}
+
+static Wlc_Ntk_t * Wlc_NtkAbs2( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_Int_t ** pvFlops )
+{
+    Vec_Int_t * vFlops  = Vec_IntAlloc( 100 );
+    Vec_Int_t * vNodes  = Vec_IntDup( vBlacks );
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    int i, k, iObj, iFanin;
+    Vec_Int_t * vMapNode2Pi = Vec_IntStart( Wlc_NtkObjNumMax(pNtk) );
+    int nOrigObjNum = Wlc_NtkObjNumMax( pNtk );
+    Wlc_Ntk_t * p = Wlc_NtkDupDfsSimple( pNtk );
+
+    Wlc_NtkForEachCi( pNtk, pObj, i )
+    {
+        if ( !Wlc_ObjIsPi( pObj ) )
+            Vec_IntPush( vFlops, Wlc_ObjId( pNtk, pObj ) ); 
+    }
+
+    Wlc_NtkForEachObjVec( vNodes, pNtk, pObj, i ) 
+        Vec_IntWriteEntry(vNodes, i, Wlc_ObjCopy(pNtk, Wlc_ObjId(pNtk, pObj)));
+
+    // mark nodes
+    Wlc_NtkForEachObjVec( vNodes, p, pObj, i ) 
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        pObj->Mark = 1;
+        // add fresh PI with the same number of bits
+        Vec_IntWriteEntry( vMapNode2Pi, iObj, Wlc_ObjAlloc( p, WLC_OBJ_PI, Wlc_ObjIsSigned(pObj), Wlc_ObjRange(pObj) - 1, 0 ) );
+    }
+
+    Wlc_NtkCleanCopy( p );
+
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( i == nOrigObjNum ) 
+            break;
+
+        if ( pObj->Mark ) {
+            // clean
+            pObj->Mark = 0;
+            iObj = Vec_IntEntry( vMapNode2Pi, i );
+        }
+        else {
+            // update fanins
+            Wlc_ObjForEachFanin( pObj, iFanin, k )
+                Wlc_ObjFanins(pObj)[k] = Wlc_ObjCopy(p, iFanin);
+            // node to remain
+            iObj = i;
+        }
+        Wlc_ObjSetCopy( p, i, iObj );
+    }
+
+    Wlc_NtkForEachCo( p, pObj, i )
+    {
+        iObj = Wlc_ObjId(p, pObj);
+        if (iObj != Wlc_ObjCopy(p, iObj)) 
+        {
+            if (pObj->fIsFi)
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsFi = 1;
+            else
+                Wlc_NtkObj(p, Wlc_ObjCopy(p, iObj))->fIsPo = 1;
+
+
+            Vec_IntWriteEntry(&p->vCos, i, Wlc_ObjCopy(p, iObj));
+        }
+    }
+
+    pNew = Wlc_NtkDupDfsSimple( p );
+    Vec_IntFree( vMapNode2Pi );
+    Vec_IntFree( vNodes );
+    Wlc_NtkFree( p );
+
+    if ( pvFlops )
+        *pvFlops = vFlops;
+    else
+        Vec_IntFree( vFlops );
+
+    return pNew;
+}
+
+static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCex, Vec_Int_t * vBlacks, Vec_Int_t ** pvRefine )
+{
+    Gia_Man_t * pGiaFrames;
+    Vec_Int_t * vRefine = NULL;
+    Vec_Bit_t * vUnmark;
+    Vec_Bit_t * vChoiceMark; 
+    Wlc_Ntk_t * pNtkWithChoices = NULL; 
+    Vec_Int_t * vCoreSels;
+    int num_ppis = -1;
+    int Entry, i;
+
+    if ( *pvRefine == NULL )
+        return 0;
+
+    vUnmark = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
+    vChoiceMark = Vec_BitStart( Vec_IntSize( vBlacks ) );      
+
+    Vec_IntForEachEntry( *pvRefine, Entry, i )
+        Vec_BitWriteEntry( vUnmark, Entry, 1 );
+
+    Vec_IntForEachEntry( vBlacks, Entry, i )
+    {
+        if ( Vec_BitEntry( vUnmark, Entry ) )
+            Vec_BitWriteEntry( vChoiceMark, i, 1 );
+    }
+
+    pNtkWithChoices = vBlacks ? Wlc_NtkIntroduceChoices( p, vBlacks ) : NULL;
+    pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0 );
+    vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars );
+    Wlc_NtkFree( pNtkWithChoices );
+    Gia_ManStop( pGiaFrames );
+    Vec_BitFree( vUnmark );
+    Vec_BitFree( vChoiceMark );
+ 
+    assert( Vec_IntSize( vCoreSels ) );
+
+    vRefine = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vCoreSels, Entry, i )
+        Vec_IntPush( vRefine, Vec_IntEntry( vBlacks, Entry ) );
+
+    Vec_IntFree( vCoreSels );
+
+    if ( pPars->fVerbose )
+        Abc_Print( 1, "Proof-based refinement reduces %d (out of %d) white boxes\n", Vec_IntSize( *pvRefine ) - Vec_IntSize( vRefine ), Vec_IntSize( *pvRefine ) );
+
+    Vec_IntFree( *pvRefine );
+    *pvRefine = vRefine;
+
+    return 0;
+}
+
+static int Wlc_NtkUpdateBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Int_t ** pvBlacks, Vec_Bit_t * vUnmark )
+{
+    int Entry, i;
+    Wlc_Obj_t * pObj; int Count[4] = {0};
+    Vec_Int_t * vBlacks = Vec_IntAlloc( 100 );
+
+    assert( *pvBlacks );
+
+    Vec_IntForEachEntry( *pvBlacks, Entry, i )
+    {
+        if ( Vec_BitEntry( vUnmark, Entry) )
+            continue;
+        Vec_IntPush( vBlacks, Entry );
+
+        pObj = Wlc_NtkObj( p, Entry );
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+            Count[0]++;
+        else if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+            Count[1]++;
+        else if ( pObj->Type == WLC_OBJ_MUX )
+            Count[2]++;
+        else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+            Count[3]++;
+    }
+    
+    Vec_IntFree( *pvBlacks );
+    *pvBlacks = vBlacks;
+
+    if ( pPars->fVerbose )
+        printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Vec_IntSize( vBlacks ) - Count[0] - Count[1] - Count[2] );
+
+    return 0;
+}
+
+static Vec_Bit_t * Wlc_NtkMarkLimit( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    Vec_Bit_t * vMarks = NULL;
+    Vec_Ptr_t * vAdds  = Vec_PtrAlloc( 1000 );
+    Vec_Ptr_t * vMuxes = Vec_PtrAlloc( 1000 );
+    Vec_Ptr_t * vMults = Vec_PtrAlloc( 1000 );
+    Vec_Ptr_t * vFlops = Vec_PtrAlloc( 1000 );
+    Wlc_Obj_t * pObj; int i;
+    Int_Pair_t * pPair;
+
+    if ( pPars->nLimit == ABC_INFINITY )
+        return NULL;
+
+    vMarks = Vec_BitStart( Wlc_NtkObjNumMax( p ) );
+
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vAdds, pPair );
+            }
+        }
+        else if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vMults, pPair );
+            }
+        }
+        else if ( pObj->Type == WLC_OBJ_MUX ) 
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vMuxes, pPair );
+            }
+        }
+        else if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+            {
+                pPair = ABC_ALLOC( Int_Pair_t, 1 );
+                pPair->first = i;
+                pPair->second = Wlc_ObjRange( pObj );
+                Vec_PtrPush( vFlops, pPair );
+            }
+        }
+    }
+
+    Vec_PtrSort( vAdds,  (int (*)(void))IntPairPtrCompare ) ;
+    Vec_PtrSort( vMults, (int (*)(void))IntPairPtrCompare ) ;
+    Vec_PtrSort( vMuxes, (int (*)(void))IntPairPtrCompare ) ;
+    Vec_PtrSort( vFlops, (int (*)(void))IntPairPtrCompare ) ;
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vAdds, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break;
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th ADD has width = %d\n", i, pPair->second );
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break;
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUL has width = %d\n", i, pPair->second );
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break; 
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th MUX has width = %d\n", i, pPair->second );
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i )
+    {
+        if ( i >= pPars->nLimit ) break;
+        Vec_BitWriteEntry( vMarks, pPair->first, 1 ); 
+    }
+    if ( i && pPars->fVerbose ) Abc_Print( 1, "%%PDRA: %d-th FF has width = %d\n", i, pPair->second );
+
+
+    Vec_PtrForEachEntry( Int_Pair_t *, vAdds,  pPair, i ) ABC_FREE( pPair );
+    Vec_PtrForEachEntry( Int_Pair_t *, vMults, pPair, i ) ABC_FREE( pPair );
+    Vec_PtrForEachEntry( Int_Pair_t *, vMuxes, pPair, i ) ABC_FREE( pPair );
+    Vec_PtrForEachEntry( Int_Pair_t *, vFlops, pPair, i ) ABC_FREE( pPair );
+    Vec_PtrFree( vAdds );
+    Vec_PtrFree( vMults );
+    Vec_PtrFree( vMuxes );
+    Vec_PtrFree( vFlops );
+
+    return vMarks;
+}
+
+static void Wlc_NtkSetUnmark( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark )
+{
+    int Entry, i;
+    Vec_Bit_t * vMarks = Wlc_NtkMarkLimit( p, pPars );
+
+    Vec_BitForEachEntry( vMarks, Entry, i )
+        Vec_BitWriteEntry( vUnmark, i, Entry^1 );
+
+    Vec_BitFree( vMarks );
+}
+
+static Vec_Int_t * Wlc_NtkGetBlacks( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    Vec_Int_t * vBlacks = Vec_IntAlloc( 100 ) ;
+    Wlc_Obj_t * pObj; int i, Count[4] = {0};
+    Vec_Bit_t * vMarks = NULL;
+
+    vMarks = Wlc_NtkMarkLimit( p, pPars ) ; 
+
+    Wlc_NtkForEachObj( p, pObj, i )
+    {
+        if ( pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB || pObj->Type == WLC_OBJ_ARI_MINUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsAdd )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[0]++;
+            }
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_DIVIDE || pObj->Type == WLC_OBJ_ARI_REM || pObj->Type == WLC_OBJ_ARI_MODULUS )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMul )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[1]++;
+            }
+            continue;
+        }
+        if ( pObj->Type == WLC_OBJ_MUX )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsMux )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId(p, pObj) ), Count[2]++;
+            }
+            continue;
+        }
+        if ( Wlc_ObjIsCi(pObj) && !Wlc_ObjIsPi(pObj) )
+        {
+            if ( Wlc_ObjRange(pObj) >= pPars->nBitsFlop )
+            {
+                if ( vMarks == NULL )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++;
+                else if ( Vec_BitEntry( vMarks, i ) )
+                    Vec_IntPushUniqueOrder( vBlacks, Wlc_ObjId( p, Wlc_ObjFo2Fi( p, pObj ) ) ), Count[3]++;
+            }
+            continue;
+        }
+    }
+    if ( vMarks )
+        Vec_BitFree( vMarks );
+    if ( pPars->fVerbose )
+        printf( "Abstraction engine marked %d adds/subs, %d muls/divs, %d muxes, and %d flops to be abstracted away.\n", Count[0], Count[1], Count[2], Count[3] );
+    return vBlacks;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Mark operators that meet the abstraction criteria.]
@@ -51,6 +657,7 @@ extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPu
   SeeAlso     []
 
 ***********************************************************************/
+
 static Vec_Bit_t * Wlc_NtkAbsMarkOpers( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Vec_Bit_t * vUnmark, int fVerbose )
 {
     Vec_Bit_t * vLeaves = Vec_BitStart( Wlc_NtkObjNumMax(p) );
@@ -302,6 +909,17 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
     return nNodes;
 }
 
+static int Wlc_NtkUnmarkRefinement( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec_Bit_t * vUnmark )
+{
+    Wlc_Obj_t * pObj; int i, nNodes = 0;
+    Wlc_NtkForEachObjVec( vRefine, p, pObj, i )
+    {
+        Vec_BitWriteEntry( vUnmark, Wlc_ObjId(p, pObj), 1 );
+        ++nNodes;
+    }
+    return nNodes;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Computes the map for remapping flop IDs used in the clauses.]
@@ -365,10 +983,12 @@ Vec_Int_t * Wlc_NtkFlopsRemap( Wlc_Ntk_t * p, Vec_Int_t * vFfOld, Vec_Int_t * vF
 int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
 {
     abctime clk = Abc_Clock();
-    abctime pdrClk;
+    abctime clk2;
+    abctime tPdr = 0, tCbr = 0, tPbr = 0, tTotal = 0;
     Pdr_Man_t * pPdr;
     Vec_Vec_t * vClauses = NULL;
     Vec_Int_t * vFfOld = NULL, * vFfNew = NULL, * vMap = NULL;
+    Vec_Int_t * vBlacks = NULL;
     int nIters, nNodes, nDcFlops, RetValue = -1, nGiaFfNumOld = -1;
     // start the bitmap to mark objects that cannot be abstracted because of refinement
     // currently, this bitmap is empty because abstraction begins without refinement
@@ -379,12 +999,21 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
     pPdrPars->fVerbose   = pPars->fPdrVerbose;
     pPdrPars->fVeryVerbose = 0;
     
+    if ( pPars->fPdra )
+    {
+        pPdrPars->fUseAbs    = 1;   // use 'pdr -t'  (on-the-fly abstraction)
+        pPdrPars->fCtgs      = 1;   // use 'pdr -nc' (improved generalization)
+        pPdrPars->fSkipDown  = 0;   // use 'pdr -nc' (improved generalization)
+        pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
+    } 
+
     // perform refinement iterations
     for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
     {
         Aig_Man_t * pAig;
         Abc_Cex_t * pCex;
-        Vec_Int_t * vPisNew, * vRefine;  
+        Vec_Int_t * vPisNew = NULL;  
+        Vec_Int_t * vRefine;  
         Gia_Man_t * pGia, * pTemp;
         Wlc_Ntk_t * pAbs;
 
@@ -392,7 +1021,22 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             printf( "\nIteration %d:\n", nIters );
 
         // get abstracted GIA and the set of pseudo-PIs (vPisNew)
-        pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
+        if ( pPars->fProofRefine )
+        {
+            if ( vBlacks == NULL )
+                vBlacks = Wlc_NtkGetBlacks( p, pPars );
+            else
+                Wlc_NtkUpdateBlacks( p, pPars, &vBlacks, vUnmark );
+            pAbs = Wlc_NtkAbs2( p, vBlacks, &vFfNew );
+            vPisNew = Vec_IntDup( vBlacks );
+        }
+        else
+        {
+            if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
+                Wlc_NtkSetUnmark( p, pPars, vUnmark );
+
+            pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, &vFfNew, pPars->fVerbose );
+        }
         pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
 
         // map old flops into new flops
@@ -438,7 +1082,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         pAig = Gia_ManToAigSimple( pGia );
 
         pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
-        pdrClk = Abc_Clock();
+        clk2 = Abc_Clock();
 
         if ( vClauses ) {
             assert( Vec_VecSize( vClauses) >= 2 ); 
@@ -447,7 +1091,8 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         Vec_IntFreeP( &vMap );
 
         RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
-        pPdr->tTotal += Abc_Clock() - pdrClk;
+        pPdr->tTotal += Abc_Clock() - clk2;
+        tPdr += pPdr->tTotal;
 
         pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
 
@@ -463,7 +1108,22 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         }
 
         // perform refinement
-        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+        if ( pPars->fHybrid || !pPars->fProofRefine )
+        {
+            clk2 = Abc_Clock();
+            vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+            tCbr += Abc_Clock() - clk2;
+        }
+        else // proof-based only
+        {
+            vRefine = Vec_IntDup( vPisNew );
+        }
+        if ( pPars->fProofRefine ) 
+        {
+            clk2 = Abc_Clock();
+            Wlc_NtkProofRefine( p, pPars, pCex, vPisNew, &vRefine );
+            tPbr += Abc_Clock() - clk2;
+        }
         Gia_ManStop( pGia );
         Vec_IntFree( vPisNew );
         if ( vRefine == NULL ) // real CEX
@@ -480,14 +1140,29 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
         Pdr_ManStop( pPdr );
 
         // update the set of objects to be un-abstracted
-        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
-        if ( pPars->fVerbose )
-            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+        clk2 = Abc_Clock();
+        if ( pPars->fMFFC )
+        {
+            nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
+            if ( pPars->fVerbose )
+                printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
+        }
+        else
+        {
+            nNodes = Wlc_NtkUnmarkRefinement( p, vRefine, vUnmark );
+            if ( pPars->fVerbose )
+                printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs.\n", pCex->iFrame, Vec_IntSize(vRefine) );
+
+        }
+        tCbr += Abc_Clock() - clk2;
+
         Vec_IntFree( vRefine );
         Abc_CexFree( pCex );
         Aig_ManStop( pAig );
     }
-
+    
+    if ( vBlacks )
+        Vec_IntFree( vBlacks );
     Vec_IntFreeP( &vFfOld );
     Vec_BitFree( vUnmark );
     // report the result
@@ -501,7 +1176,18 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
     else 
         printf( "timed out" );
     printf( " after %d iterations. ", nIters );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    tTotal = Abc_Clock() - clk;
+    Abc_PrintTime( 1, "Time", tTotal );
+
+    if ( pPars->fVerbose )
+    {
+        ABC_PRTP( "PDR          ", tPdr,                          tTotal );
+        ABC_PRTP( "CEX Refine   ", tCbr,                          tTotal );
+        ABC_PRTP( "Proof Refine ", tPbr,                          tTotal );
+        ABC_PRTP( "Misc.        ", tTotal - tPdr - tCbr - tPbr,   tTotal );
+        ABC_PRTP( "Total        ", tTotal,                        tTotal );
+    }
+    
     return RetValue;
 }
 
@@ -550,6 +1236,8 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             printf( "\nIteration %d:\n", nIters );
 
         // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+        if ( nIters == 1 && pPars->nLimit < ABC_INFINITY )
+            Wlc_NtkSetUnmark( p, pPars, vUnmark );
         pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose );
         pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
 
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index df736e70..38f919d4 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -521,6 +521,26 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nIterMax < 0 )
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLimit < 0 )
+                goto usage;
+            break;
+        case 'a':
+            pPars->fPdra ^= 1;
+            break;
+        case 'b':
+            pPars->fProofRefine ^= 1;
+            break;
+        case 'r':
+            pPars->fHybrid ^= 1;
+            break;
         case 'x':
             pPars->fXorOutput ^= 1;
             break;
@@ -530,6 +550,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             pPars->fPushClauses ^= 1;
             break;
+        case 'm':
+            pPars->fMFFC ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -550,16 +573,21 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkPdrAbs( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
     Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n",      pPars->nBitsMux );
     Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
     Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",                   pPars->nIterMax );
+    Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n",               pPars->nLimit );
     Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle running pdr with -nct [default = %s]\n",                         pPars->fPdra? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle using proof-based refinement [default = %s]\n",                  pPars->fProofRefine? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle using both cex-based and proof-based refinement [default = %s]\n",                  pPars->fHybrid? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle checking clauses in the reloaded trace [default = %s]\n",        pPars->fCheckClauses? "yes": "no" );
-    Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",        pPars->fPushClauses? "yes": "no" );
+    Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",         pPars->fPushClauses? "yes": "no" );
+    Abc_Print( -2, "\t-m     : toggle refining the whole MFFC of a PPI [default = %s]\n",              pPars->fMFFC? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",                   pPars->fPdrVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
@@ -585,7 +613,7 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -644,6 +672,17 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nIterMax < 0 )
                 goto usage;
             break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nLimit < 0 )
+                goto usage;
+            break;
         case 'x':
             pPars->fXorOutput ^= 1;
             break;
@@ -667,13 +706,14 @@ int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkAbsCore( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" );
+    Abc_Print( -2, "usage: %%abs [-AMXFIL num] [-xvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
     Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n",      pPars->nBitsMux );
     Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n",         pPars->nBitsFlop );
     Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n",                   pPars->nIterMax );
+    Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n",               pPars->nLimit );
     Abc_Print( -2, "\t-x     : toggle XORing outputs of word-level miter [default = %s]\n",            pPars->fXorOutput? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing verbose PDR output [default = %s]\n",                   pPars->fPdrVerbose? "yes": "no" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index c8fc15a7..89699949 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -108,16 +108,21 @@ char * Wlc_ObjTypeName( Wlc_Obj_t * p ) { return Wlc_Names[p->Type]; }
 void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Wlc_Par_t) );
-    pPars->nBitsAdd    = ABC_INFINITY;   // adder bit-width
-    pPars->nBitsMul    = ABC_INFINITY;   // multiplier bit-widht 
-    pPars->nBitsMux    = ABC_INFINITY;   // MUX bit-width
-    pPars->nBitsFlop   = ABC_INFINITY;   // flop bit-width
-    pPars->nIterMax    =         1000;   // the max number of iterations
-    pPars->fXorOutput  =            1;   // XOR outputs of word-level miter
-    pPars->fCheckClauses =          1;   // Check clauses in the reloaded trace                    
-    pPars->fPushClauses =           0;   // Push clauses in the reloaded trace                    
-    pPars->fVerbose    =            0;   // verbose output`
-    pPars->fPdrVerbose =            0;   // show verbose PDR output
+    pPars->nBitsAdd      = ABC_INFINITY;   // adder bit-width
+    pPars->nBitsMul      = ABC_INFINITY;   // multiplier bit-widht 
+    pPars->nBitsMux      = ABC_INFINITY;   // MUX bit-width
+    pPars->nBitsFlop     = ABC_INFINITY;   // flop bit-width
+    pPars->nIterMax      =         1000;   // the max number of iterations
+    pPars->nLimit        = ABC_INFINITY;   // the max number of signals
+    pPars->fXorOutput    =            1;   // XOR outputs of word-level miter
+    pPars->fCheckClauses =            1;   // Check clauses in the reloaded trace                    
+    pPars->fPushClauses  =            0;   // Push clauses in the reloaded trace                    
+    pPars->fMFFC         =            1;   // Refine the entire MFFC of a PPI 
+    pPars->fPdra         =            0;   // Use pdr -nct 
+    pPars->fProofRefine  =            0;   // Use proof-based refinement
+    pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
+    pPars->fVerbose      =            0;   // verbose output`
+    pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }
 
 /**Function*************************************************************
@@ -830,6 +835,33 @@ void Wlc_NtkDupDfs_rec( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p, int iObj, Vec_Int_t * v
         Wlc_NtkDupDfs_rec( pNew, p, iFanin, vFanins );
     Wlc_ObjDup( pNew, p, iObj, vFanins );
 }
+
+Wlc_Ntk_t * Wlc_NtkDupDfsSimple( Wlc_Ntk_t * p )
+{
+    Wlc_Ntk_t * pNew;
+    Wlc_Obj_t * pObj;
+    Vec_Int_t * vFanins;
+    int i;
+    Wlc_NtkCleanCopy( p );
+    vFanins = Vec_IntAlloc( 100 );
+    pNew = Wlc_NtkAlloc( p->pName, p->nObjsAlloc );
+    pNew->fSmtLib = p->fSmtLib;
+    Wlc_NtkForEachCi( p, pObj, i )
+        Wlc_ObjDup( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_NtkDupDfs_rec( pNew, p, Wlc_ObjId(p, pObj), vFanins );
+    Wlc_NtkForEachCo( p, pObj, i )
+        Wlc_ObjSetCo( pNew, Wlc_ObjCopyObj(pNew, p, pObj), pObj->fIsFi );
+    if ( p->vInits )
+    pNew->vInits = Vec_IntDup( p->vInits );
+    if ( p->pInits )
+    pNew->pInits = Abc_UtilStrsav( p->pInits );
+    Vec_IntFree( vFanins );
+    if ( p->pSpec )
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    return pNew;
+}
+
 Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p, int fMarked, int fSeq )
 {
     Wlc_Ntk_t * pNew;
diff --git a/src/base/wlc/wlcStdin.c b/src/base/wlc/wlcStdin.c
index 49c25ad0..3b747cc5 100644
--- a/src/base/wlc/wlcStdin.c
+++ b/src/base/wlc/wlcStdin.c
@@ -239,7 +239,7 @@ int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd )
             return 0;
         }
         // report value of this variable
-        Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, Abc_FrameReadCex(pAbc), pName, 16 );
+        Wlc_NtkReport( (Wlc_Ntk_t *)pAbc->pAbcWlc, (Abc_Cex_t *)Abc_FrameReadCex(pAbc), pName, 16 );
         Vec_StrFree( vInput );
         fflush( stdout );
     }