Changes to enable CEX minimization.

4 files changed, 533 insertions, 78 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 3ad6caa4..e0b214a3 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -2421,6 +2421,10 @@ SOURCE=.\src\misc\util\utilMem.h
 
 SOURCE=.\src\misc\util\utilSignal.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\utilSort.c
+# End Source File
 # End Group
 # Begin Group "nm"
 
@@ -3511,6 +3515,10 @@ SOURCE=.\src\aig\saig\saigBmc3.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\saig\saigCexMin.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\saig\saigCone.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 9766768d..b84bc0a1 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -144,6 +144,8 @@ extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFra
 /*=== saigBmc3.c ==========================================================*/
 extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
+/*=== saigCexMin.c ==========================================================*/
+extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
 /*=== saigConstr.c ==========================================================*/
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
new file mode 100644
index 00000000..a2ad3e59
--- /dev/null
+++ b/src/aig/saig/saigCexMin.c
@@ -0,0 +1,330 @@
+/**CFile****************************************************************
+
+  FileName    [saigCexMin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [CEX minimization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigCexMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns reasons for the property to fail.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCexMinFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasonPis, Vec_Int_t * vReasonLis )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Saig_ObjIsPi(p, pObj) )
+    {
+        Vec_IntPush( vReasonPis, Aig_ObjPioNum(pObj) );
+        return;
+    }
+    if ( Saig_ObjIsLo(p, pObj) )
+    {
+        Vec_IntPush( vReasonLis, Aig_ObjPioNum(pObj) - Aig_ManRegNum(p) );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    if ( pObj->fPhase )
+    {
+        Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasonPis, vReasonLis );
+        Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasonPis, vReasonLis );
+    }
+    else
+    {
+        int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
+        int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
+        assert( !fPhase0 || !fPhase1 );
+        if ( !fPhase0 && fPhase1 )
+            Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasonPis, vReasonLis );
+        else if ( fPhase0 && !fPhase1 )
+            Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasonPis, vReasonLis );
+        else 
+        {
+            int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
+            int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
+            if ( iPrio0 >= iPrio1 )
+                Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasonPis, vReasonLis );
+            else
+                Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasonPis, vReasonLis );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively sets phase and priority.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCexMinComputePrio_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vPrios )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        Saig_ManCexMinComputePrio_rec( pAig, Aig_ObjFanin0(pObj), vPrios );
+        pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
+        Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) ) );
+    }
+    else if ( Aig_ObjIsNode(pObj) )
+    {
+        int fPhase0, fPhase1, iPrio0, iPrio1;
+        Saig_ManCexMinComputePrio_rec( pAig, Aig_ObjFanin0(pObj), vPrios );
+        Saig_ManCexMinComputePrio_rec( pAig, Aig_ObjFanin1(pObj), vPrios );
+        fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
+        fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
+        iPrio0  = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
+        iPrio1  = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
+        pObj->fPhase = fPhase0 && fPhase1;
+        if ( fPhase0 && fPhase1 ) // both are one
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
+        else if ( !fPhase0 && fPhase1 ) 
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
+        else if ( fPhase0 && !fPhase1 )
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
+        else // both are zero
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect nodes in the unrolled timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vFramePis, Vec_Int_t * vFrameLis )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsPo(pObj) )
+        Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFramePis, vFrameLis );
+    else if ( Aig_ObjIsNode(pObj) )
+    {
+        Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFramePis, vFrameLis );
+        Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFramePis, vFrameLis );
+    }
+    if ( Saig_ObjIsPi( pAig, pObj ) )
+        Vec_IntPush( vFramePis, Aig_ObjId(pObj) );
+    if ( vFrameLis && Saig_ObjIsLo( pAig, pObj ) )
+        Vec_IntPush( vFrameLis, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive unrolled timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFramePis, Vec_Vec_t * vFrameLis )
+{
+    Aig_Obj_t * pObj;
+    int i, f, Entry;
+    // sanity checks
+    assert( Saig_ManPiNum(pAig) == pCex->nPis );
+    assert( Saig_ManRegNum(pAig) == pCex->nRegs );
+    assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
+    // initialized the topmost frame
+    pObj = Aig_ManPo( pAig, pCex->iPo );
+    Vec_VecPushInt( vFrameLis, pCex->iFrame, Aig_ObjId(pObj) );
+    for ( f = pCex->iFrame; f >= 0; f-- )
+    {
+        // collect nodes starting from the roots
+        Aig_ManIncrementTravId( pAig );
+        Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
+            Saig_ManCollectFrameTerms_rec( pAig, Aig_ManObj(pAig, Entry),
+                (Vec_Int_t *)Vec_VecEntry( vFramePis, f ),
+                (Vec_Int_t *)(f ? Vec_VecEntry( vFrameLis, f-1 ) : NULL) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCexMinPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f, 
+    Vec_Vec_t * vFramePis, Vec_Vec_t * vFrameLis, Vec_Vec_t * vPrioPis, Vec_Vec_t * vPrioLis, Vec_Vec_t * vPhaseLis, Vec_Int_t * vPrios )
+{
+    Aig_Obj_t * pObj;
+    int i, Entry;
+    // set PI priority for this frame
+    Vec_VecForEachEntryIntLevel( vFramePis, Entry, i, f )
+    {
+        pObj = Aig_ManObj( pAig, Entry );
+        pObj->fPhase = Aig_InfoHasBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
+        Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_VecEntryEntryInt(vPrioPis, f, i) );
+    }
+    // set LO priority for this frame
+    if ( f == 0 ) 
+    {
+        int nPiPrioStart = Vec_VecSizeSize(vFramePis);
+        Saig_ManForEachLo( pAig, pObj, i )
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), nPiPrioStart + i );
+    }
+    else
+    {
+        Vec_Int_t * vPrioLiOne  = Vec_VecEntryInt( vPrioLis, f-1 );
+        Vec_Int_t * vPhaseLiOne = Vec_VecEntryInt( vPhaseLis, f-1 );
+        Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f-1 )
+        {
+            pObj = Saig_ObjLiToLo( pAig, Aig_ManObj(pAig, Entry) );
+            pObj->fPhase = Vec_IntEntry( vPhaseLiOne, i );
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPrioLiOne, i) );
+        }
+    }
+    // traverse, set phase and priority for internal nodes
+    Aig_ManIncrementTravId( pAig );
+    Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
+        Saig_ManCexMinComputePrio_rec( pAig, Aig_ManObj(pAig, Entry), vPrios );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
+{
+    Abc_Cex_t * pCexMin = NULL;
+    Aig_Obj_t * pObj;
+    Vec_Vec_t * vFramePis, * vFrameLis, * vPrioPis, * vPrioLis, * vPhaseLis, * vReasonPis, * vReasonLis;
+    Vec_Int_t * vPrios;
+    int f, i, Entry, nPiPrioStart;
+
+    // collect PIs and LOs visited in each frame
+    vFramePis = Vec_VecStart( pCex->iFrame+1 );
+    vFrameLis = Vec_VecStart( pCex->iFrame+1 );
+    Saig_ManCollectFrameTerms( pAig, pCex, vFramePis, vFrameLis );
+
+    // set priority for the PIs
+    nPiPrioStart = 0;
+    vPrioPis  = Vec_VecStart( pCex->iFrame+1 );
+    Vec_VecForEachEntryInt( vFramePis, Entry, f, i )
+        Vec_VecPushInt( vPrioPis, f, nPiPrioStart++ );
+    assert( nPiPrioStart == Vec_VecSizeSize(vFramePis) );
+
+    // storage for priorities
+    vPrios = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
+    Vec_IntWriteEntry( vPrios, Aig_ObjId(Aig_ManConst1(pAig)), Vec_VecSizeSize(vFramePis) + Aig_ManRegNum(pAig) );
+
+    // compute LO priority and phase
+    vPrioLis  = Vec_VecStart( pCex->iFrame+1 );
+    vPhaseLis = Vec_VecStart( pCex->iFrame+1 );
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        // set phase and polarity
+        Saig_ManCexMinPhasePriority( pAig, pCex, f, vFramePis, vFrameLis, vPrioPis, vPrioLis, vPhaseLis, vPrios );
+        // save phase and priority
+        Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
+        {
+            pObj = Aig_ManObj( pAig, Entry );
+            Vec_VecPushInt( vPrioLis, f, Vec_IntEntry(vPrios, Aig_ObjId(pObj)) );
+            Vec_VecPushInt( vPhaseLis, f, pObj->fPhase );
+        }
+    }
+    // check the property output
+    pObj = Aig_ManPo( pAig, pCex->iPo );
+    assert( pObj->fPhase );
+
+    // select reason for the property to fail
+    vReasonPis = Vec_VecStart( pCex->iFrame+1 );
+    vReasonLis = Vec_VecStart( pCex->iFrame+1 );
+    for ( f = pCex->iFrame; f >= 0; f-- )
+    {
+        // set phase and polarity
+        Saig_ManCexMinPhasePriority( pAig, pCex, f, vFramePis, vFrameLis, vPrioPis, vPrioLis, vPhaseLis, vPrios );
+        // select reasons
+        Aig_ManIncrementTravId( pAig );
+        Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
+            Saig_ManCexMinFindReason_rec( pAig, Aig_ManObj(pAig, Entry), vPrios, 
+                (Vec_Int_t *)Vec_VecEntry( vReasonPis, f ),
+                (Vec_Int_t *)(f ? Vec_VecEntry( vReasonLis, f-1 ) : NULL) );
+    }
+
+    // here are computes the reasons
+    printf( "Total number of reason PIs = %d.\n", Vec_VecSizeSize(vReasonPis) );
+
+    // clean up
+    Vec_VecFree( vFramePis );
+    Vec_VecFree( vFrameLis );
+    Vec_VecFree( vPrioPis );
+    Vec_VecFree( vPrioLis );
+    Vec_VecFree( vPhaseLis );
+    Vec_VecFree( vReasonPis );
+    Vec_VecFree( vReasonLis );
+    Vec_IntFree( vPrios );
+    return pCexMin;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ce571aec..54f6a1ff 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -252,6 +252,8 @@ static int Abc_CommandSynch                  ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandClockGate              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtWin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInsWin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPermute                ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnpermute              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandCec                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDCec                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -278,8 +280,7 @@ static int Abc_CommandBm                     ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandTestCex                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPdr                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReconcile              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandPermute                ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandUnpermute              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCexMin                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandTraceStart             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -674,6 +675,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "clockgate",     Abc_CommandClockGate,        1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "extwin",        Abc_CommandExtWin,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "inswin",        Abc_CommandInsWin,           1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "permute",       Abc_CommandPermute,          1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "unpermute",     Abc_CommandUnpermute,        1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dcec",          Abc_CommandDCec,             0 );
@@ -705,8 +708,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "testcex",       Abc_CommandTestCex,          0 );
     Cmd_CommandAdd( pAbc, "Verification", "pdr",           Abc_CommandPdr,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "reconcile",     Abc_CommandReconcile,        1 );
-    Cmd_CommandAdd( pAbc, "Verification", "permute",       Abc_CommandPermute,          1 );
-    Cmd_CommandAdd( pAbc, "Verification", "unpermute",     Abc_CommandUnpermute,        1 );
+    Cmd_CommandAdd( pAbc, "Verification", "cexmin",        Abc_CommandCexMin,           0 );
 
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*r",            Abc_CommandAbc8Read,         0 );
@@ -16520,6 +16522,120 @@ usage:
     return 1;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
+{    
+    Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
+    int fInputs = 1;
+    int fOutputs = 1;
+    int c, fFlops = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "iofh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'i':
+            fInputs ^= 1;
+            break;
+        case 'o':
+            fOutputs ^= 1;
+            break;
+        case 'f':
+            fFlops ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDup( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        Abc_Print( -1, "Command \"permute\" has failed.\n" );
+        return 1;
+    }
+    Abc_NtkPermute( pNtkRes, fInputs, fOutputs, fFlops );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: permute [-iofh]\n" );
+    Abc_Print( -2, "\t        performs random permutation of inputs/outputs/flops\n" );
+    Abc_Print( -2, "\t-i    : toggle permuting primary inputs [default = %s]\n", fInputs? "yes": "no" );
+    Abc_Print( -2, "\t-o    : toggle permuting primary outputs [default = %s]\n", fOutputs? "yes": "no" );
+    Abc_Print( -2, "\t-f    : toggle permuting flip-flops [default = %s]\n", fFlops? "yes": "no" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandUnpermute( Abc_Frame_t * pAbc, int argc, char ** argv )
+{    
+    Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            Abc_Print( -2, "Unknown switch.\n");
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        Abc_Print( -1, "Empty network.\n" );
+        return 1;
+    }
+    pNtkRes = Abc_NtkDup( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        Abc_Print( -1, "Command \"unpermute\" has failed.\n" );
+        return 1;
+    }
+    Abc_NtkUnpermute( pNtkRes );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: unpermute [-h]\n" );
+    Abc_Print( -2, "\t        restores inputs/outputs/flops before the last permutation\n" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -20503,25 +20619,43 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
 {    
-    Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
-    int fInputs = 1;
-    int fOutputs = 1;
-    int c, fFlops = 1;
+     Abc_Ntk_t * pNtk;
+    Abc_Cex_t * vCexNew = NULL;
+    int c;
+    int nConfLimit = 1000;
+    int nRounds    =    1;
+    int fVerbose   =    0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "iofh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CRvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'i':
-            fInputs ^= 1;
+        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 'o':
-            fOutputs ^= 1;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRounds = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRounds < 0 ) 
+                goto usage;
             break;
-        case 'f':
-            fFlops ^= 1;
+        case 'v':
+            fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -20530,77 +20664,58 @@ int Abc_CommandPermute( Abc_Frame_t * pAbc, int argc, char ** argv )
             goto usage;
         }
     }
-    if ( pNtk == NULL )
-    {
-        Abc_Print( -1, "Empty network.\n" );
-        return 1;
-    }
-    pNtkRes = Abc_NtkDup( pNtk );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command \"permute\" has failed.\n" );
-        return 1;
-    }
-    Abc_NtkPermute( pNtkRes, fInputs, fOutputs, fFlops );
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    return 0;
-
-usage:
-    Abc_Print( -2, "usage: permute [-iofh]\n" );
-    Abc_Print( -2, "\t        performs random permutation of inputs/outputs/flops\n" );
-    Abc_Print( -2, "\t-i    : toggle permuting primary inputs [default = %s]\n", fInputs? "yes": "no" );
-    Abc_Print( -2, "\t-o    : toggle permuting primary outputs [default = %s]\n", fOutputs? "yes": "no" );
-    Abc_Print( -2, "\t-f    : toggle permuting flip-flops [default = %s]\n", fFlops? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
 
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandUnpermute( Abc_Frame_t * pAbc, int argc, char ** argv )
-{    
-    Abc_Ntk_t * pNtk = pAbc->pNtkCur, * pNtkRes = NULL;
-    int c;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    if ( pAbc->pCex == NULL )
     {
-        switch ( c )
-        {
-        case 'h':
-            goto usage;
-        default:
-            Abc_Print( -2, "Unknown switch.\n");
-            goto usage;
-        }
+        Abc_Print( 1, "There is no current cex.\n");
+        return 0;
     }
+
+    // check the main AIG
+    pNtk = Abc_FrameReadNtk(pAbc);
     if ( pNtk == NULL )
+        Abc_Print( 1, "Main AIG: There is no current network.\n");
+    else if ( !Abc_NtkIsStrash(pNtk) )
+        Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
+    else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
+        Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
+//        else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
+//            Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
+//        else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
+//            Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
+    else 
     {
-        Abc_Print( -1, "Empty network.\n" );
-        return 1;
-    }
-    pNtkRes = Abc_NtkDup( pNtk );
-    if ( pNtkRes == NULL )
-    {
-        Abc_Print( -1, "Command \"unpermute\" has failed.\n" );
-        return 1;
+        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+        Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
+//        if ( !Gia_ManVerifyCex( pGia, pAbc->pCex, 0 ) )
+        int iPoOld = pAbc->pCex->iPo;
+        pAbc->pCex->iPo = Gia_ManFindFailedPoCex( pGia, pAbc->pCex, 0 );
+        Gia_ManStop( pGia );
+        if ( pAbc->pCex->iPo == -1 )
+        {
+            pAbc->pCex->iPo = iPoOld;
+            Abc_Print( -1, "Main AIG: The cex does not fail any outputs.\n" );
+            return 0;
+        }
+        else if ( iPoOld != pAbc->pCex->iPo )
+            Abc_Print( 0, "Main AIG: The cex refined PO %d instead of PO %d.\n", pAbc->pCex->iPo, iPoOld );
+        // perform minimization
+//        vCexNew = Saig_ManCexMinPerform( pAig, pAbc->pCex );
+        Aig_ManStop( pAig );
+//        Abc_FrameReplaceCex( pAbc, &vCexNew );
+
+        printf( "Implementation of this command is not finished.\n" );
     }
-    Abc_NtkUnpermute( pNtkRes );
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: unpermute [-h]\n" );
-    Abc_Print( -2, "\t        restores inputs/outputs/flops before the last permutation\n" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "usage: cexmin [-CR num] [-vh]\n" );
+    Abc_Print( -2, "\t         reduces the length of the counter-example\n" );
+    Abc_Print( -2, "\t-C num : the maximum number of conflicts [default = %d]\n", nConfLimit );
+    Abc_Print( -2, "\t-R num : the number of minimization rounds [default = %d]\n", nRounds );
+    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;
 }