Changes to enable CEX minimization.

4 files changed, 370 insertions, 194 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index b84bc0a1..4437413f 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -105,6 +105,7 @@ static inline int          Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); }
 static inline Aig_Obj_t *  Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPiNum(p));   }
 static inline Aig_Obj_t *  Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPoNum(p));   }
+static inline int          Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj )   { if ( Saig_ObjIsLo(p, pObj) ) return Aig_ObjPioNum(pObj)-Saig_ManPiNum(p); if ( Saig_ObjIsLi(p, pObj) ) return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p); else assert(0);  return -1; }
 
 // iterator over the primary inputs/outputs
 #define Saig_ManForEachPi( p, pObj, i )                                           \
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
index 66cf5586..78a77ecb 100644
--- a/src/aig/saig/saigAbsCba.c
+++ b/src/aig/saig/saigAbsCba.c
@@ -151,6 +151,16 @@ Abc_Cex_t * Saig_ManCbaReason2Cex( Saig_ManCba_t * p, Vec_Int_t * vReasons )
         iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
         Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
     }
+/*
+    for ( iFrame = 0; iFrame <= pCare->iFrame; iFrame++ )
+    {
+        int Count = 0;
+        for ( i = 0; i < pCare->nPis; i++ )
+            Count +=  Aig_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i);
+        printf( "%d ", Count );
+    }
+printf( "\n" );
+*/
     return pCare;
 }
 
@@ -216,28 +226,19 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr
 Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
 {
     Aig_Obj_t * pObj;
-    Vec_Int_t * vPrios, * vPi2Prio, * vReasons;
-    int i, CountPrios;
-
-    vPi2Prio = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
-    vPrios   = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
+    Vec_Int_t * vPrios, * vReasons;
+    int i;
 
     // set PI values according to CEX
-    CountPrios = 0;
+    vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
     Aig_ManConst1(p->pFrames)->fPhase = 1;
     Aig_ManForEachPi( p->pFrames, pObj, i )
     {
         int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
         int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
         pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
-        // assign priority
-        if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 )
-            Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ );
-//        Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPi2Prio, iInput) );
         Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
     }
-//    printf( "Priority numbers = %d.\n", CountPrios );
-    Vec_IntFree( vPi2Prio );
 
     // traverse and set the priority
     Aig_ManForEachNode( p->pFrames, pObj, i )
@@ -341,7 +342,9 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI
             Saig_ManCbaUnrollCollect_rec( pAig, pObj, 
                 Vec_VecEntryInt(vFrameObjs, f),
                 (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
+//printf( "%d ", Vec_VecLevelSize(vFrameCos, f) );
     }
+//printf( "\n" );
 
     // derive unrolled timeframes
     pFrames = Aig_ManStart( 10000 );
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index 5dfcda01..dd88fb70 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "saig.h"
+#include "ioa.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -33,7 +34,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Returns reasons for the property to fail.]
+  Synopsis    [Find the roots to begin traversal.]
 
   Description []
                
@@ -42,48 +43,85 @@ ABC_NAMESPACE_IMPL_START
   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 )
+void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Int_t * vLeaves, Vec_Int_t * vRoots )
 {
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Saig_ObjIsPi(p, pObj) )
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_IntClear( vRoots );
+    if ( vLeaves == NULL )
     {
-        Vec_IntPush( vReasonPis, Aig_ObjPioNum(pObj) );
+        pObj = Aig_ManPo( pAig, pCex->iPo );
+        Vec_IntPush( vRoots, Aig_ObjId(pObj) );
         return;
     }
-    if ( Saig_ObjIsLo(p, pObj) )
-    {
-        Vec_IntPush( vReasonLis, Aig_ObjPioNum(pObj) - Aig_ManRegNum(p) );
+    Aig_ManForEachObjVec( vLeaves, pAig, pObj, i )
+        if ( Saig_ObjIsLo(pAig, pObj) )
+            Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects CI of the given timeframe.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCexMinCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vFrameCisOne )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
         return;
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    if ( pObj->fPhase )
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsPo(pObj) )
+        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
+    else if ( Aig_ObjIsNode(pObj) )
     {
-        Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasonPis, vReasonLis );
-        Saig_ManCexMinFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasonPis, vReasonLis );
+        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
+        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFrameCisOne );
     }
-    else
+    else if ( Aig_ObjIsPi(pObj) )
+        Vec_IntPush( vFrameCisOne, Aig_ObjId(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects CIs of all timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Saig_ManCexMinCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex )
+{
+    Vec_Vec_t * vFrameCis;
+    Vec_Int_t * vRoots, * vLeaves;
+    Aig_Obj_t * pObj;
+    int i, f;
+    // create terminals
+    vRoots = Vec_IntAlloc( 1000 );
+    vFrameCis = Vec_VecStart( pCex->iFrame+1 );
+    for ( f = pCex->iFrame; f >= 0; f-- )
     {
-        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 );
-        }
+        // create roots
+        vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
+        Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
+        // collect nodes starting from the roots
+        Aig_ManIncrementTravId( pAig );
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
+            Saig_ManCexMinCollectFrameTerms_rec( pAig, pObj, Vec_VecEntryInt(vFrameCis, f) );
     }
+    Vec_IntFree( vRoots );
+    return vFrameCis;
 }
 
+
+
 /**Function*************************************************************
 
   Synopsis    [Recursively sets phase and priority.]
@@ -95,41 +133,42 @@ void Saig_ManCexMinFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManCexMinComputePrio_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vPrios )
+void Saig_ManCexMinDerivePhasePriority_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj )
 {
     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) ) );
+        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
+        assert( Aig_ObjFanin0(pObj)->iData >= 0 );
+        pObj->iData = Aig_ObjFanin0(pObj)->iData ^ Aig_ObjFaninC0(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;
+        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
+        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin1(pObj) );
+        assert( Aig_ObjFanin0(pObj)->iData >= 0 );
+        assert( Aig_ObjFanin1(pObj)->iData >= 0 );
+        fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
+        fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
+        iPrio0  = Aig_Lit2Var( Aig_ObjFanin0(pObj)->iData );
+        iPrio1  = Aig_Lit2Var( Aig_ObjFanin1(pObj)->iData );
         if ( fPhase0 && fPhase1 ) // both are one
-            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
+            pObj->iData = Aig_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 );
         else if ( !fPhase0 && fPhase1 ) 
-            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
+            pObj->iData = Aig_Var2Lit( iPrio0, 0 );
         else if ( fPhase0 && !fPhase1 )
-            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
+            pObj->iData = Aig_Var2Lit( iPrio1, 0 );
         else // both are zero
-            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
+            pObj->iData = Aig_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 );
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collect nodes in the unrolled timeframes.]
+  Synopsis    [Verify phase.]
 
   Description []
                
@@ -138,27 +177,33 @@ void Saig_ManCexMinComputePrio_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vFramePis, Vec_Int_t * vFrameLis )
+void Saig_ManCexMinVerifyPhase( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f )
 {
-    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) )
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManConst1(pAig)->fPhase = 1;
+    Saig_ManForEachPi( pAig, pObj, i )
+        pObj->fPhase = Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i);
+    if ( f == 0 )
     {
-        Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFramePis, vFrameLis );
-        Saig_ManCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFramePis, vFrameLis );
+        Saig_ManForEachLo( pAig, pObj, i )
+            pObj->fPhase = 0;
     }
-    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) ) );
+    else
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+            pObj->fPhase = Saig_ObjLoToLi(pAig, pObj)->fPhase;
+    }
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase) & 
+                       (Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase);
+    Aig_ManForEachPo( pAig, pObj, i )
+        pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase);
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derive unrolled timeframes.]
+  Synopsis    [Collects phase and priority of all timeframes.]
 
   Description []
                
@@ -167,79 +212,162 @@ void Saig_ManCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFramePis, Vec_Vec_t * vFrameLis )
+void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int f, Vec_Int_t * vRoots )
 {
+    Vec_Int_t * vFramePPsOne, * vFrameCisOne, * vLeaves;
     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-- )
+    int i;
+    // set PP for the CIs
+    vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
+    vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
+    Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
     {
-        // collect nodes starting from the roots
-        Aig_ManIncrementTravId( pAig );
-        Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
-            Saig_ManCollectFrameTerms_rec( pAig, Aig_ManObj(pAig, Entry),
-                Vec_VecEntryInt( vFramePis, f ),
-                (Vec_Int_t *)(f ? Vec_VecEntry( vFrameLis, f-1 ) : NULL) );
+        pObj->iData = Vec_IntEntry( vFramePPsOne, i );
+        assert( pObj->iData >= 0 );
+    }
+//    if ( f == 0 )
+//        Saig_ManCexMinVerifyPhase( pAig, pCex, f );
+
+    // create roots
+    vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
+    Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
+    // derive for the nodes starting from the roots
+    Aig_ManIncrementTravId( pAig );
+    Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
+    {
+        Saig_ManCexMinDerivePhasePriority_rec( pAig, pObj );
+//        if ( f == 0 )
+//            assert( (pObj->iData & 1) == pObj->fPhase );
     }
 }
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Collects phase and priority of all timeframes.]
 
   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 )
+Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
 {
+    Vec_Vec_t * vFramePPs;
+    Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
     Aig_Obj_t * pObj;
-    int i, Entry;
-    // set PI priority for this frame
-    Vec_VecForEachEntryIntLevel( vFramePis, Entry, i, f )
+    int i, f, nPrioOffset;
+
+    // initialize phase and priority
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->iData = -1;
+
+    // set the constant node to higher priority than the flops
+    vFramePPs = Vec_VecStart( pCex->iFrame+1 );
+    nPrioOffset = (pCex->iFrame + 1) * pCex->nPis;
+    Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + pCex->nRegs, 1 );
+    vRoots = Vec_IntAlloc( 1000 );
+//printf( "Const1 = %d  Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset ); 
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        int nPiCount = 0;
+        // fill in PP for the CIs
+        vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
+        vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
+        assert( Vec_IntSize(vFramePPsOne) == 0 );
+        Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
+        {
+            assert( Aig_ObjIsPi(pObj) );
+            if ( Saig_ObjIsPi(pAig, pObj) )
+                Vec_IntPush( vFramePPsOne, Aig_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
+            else if ( f == 0 )
+                Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) );
+            else
+            {
+                Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
+                int Value = Saig_ObjLoToLi(pAig, pObj)->iData;
+                Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
+            }
+//printf( "%d ", Vec_IntEntryLast(vFramePPsOne) );
+        }
+//printf( "\n" );
+        // compute the PP info
+        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
+    }
+    Vec_IntFree( vRoots );
+    // check the output
+    pObj = Aig_ManPo( pAig, pCex->iPo );
+    assert( Aig_LitIsCompl(pObj->iData) );
+    return vFramePPs;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns reasons for the property to fail.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vReason, int fPiReason )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsPi(pObj) )
     {
-        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) );
+        if ( fPiReason && Saig_ObjIsPi(p, pObj) )
+            Vec_IntPush( vReason, Aig_Var2Lit( Aig_ObjPioNum(pObj), !Aig_LitIsCompl(pObj->iData) ) );
+        else if ( !fPiReason && Saig_ObjIsLo(p, pObj) )
+            Vec_IntPush( vReason, Aig_Var2Lit( Saig_ObjRegId(p, pObj), !Aig_LitIsCompl(pObj->iData) ) );
+        return;
     }
-    // set LO priority for this frame
-    if ( f == 0 ) 
+    if ( Aig_ObjIsPo(pObj) )
     {
-        int nPiPrioStart = Vec_VecSizeSize(vFramePis);
-        Saig_ManForEachLo( pAig, pObj, i )
-            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), nPiPrioStart + i );
+        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
+        return;
+    }
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    if ( Aig_LitIsCompl(pObj->iData) ) // value 1
+    {
+        int fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
+        int fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
+        assert( fPhase0 && fPhase1 );
+        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
+        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
     }
     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 )
+        int fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
+        int fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
+        assert( !fPhase0 || !fPhase1 );
+        if ( !fPhase0 && fPhase1 )
+            Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
+        else if ( fPhase0 && !fPhase1 )
+            Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
+        else 
         {
-            pObj = Saig_ObjLiToLo( pAig, Aig_ManObj(pAig, Entry) );
-            pObj->fPhase = Vec_IntEntry( vPhaseLiOne, i );
-            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPrioLiOne, i) );
+            int iPrio0 = Aig_Lit2Var( Aig_ObjFanin0(pObj)->iData );
+            int iPrio1 = Aig_Lit2Var( Aig_ObjFanin1(pObj)->iData );
+            if ( iPrio0 >= iPrio1 )
+                Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
+            else
+                Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
         }
     }
-    // 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    []
+  Synopsis    [Collects phase and priority of all timeframes.]
 
   Description []
                
@@ -248,77 +376,31 @@ void Saig_ManCexMinPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f,
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
+Vec_Vec_t * Saig_ManCexMinCollectReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int fPiReason )
 {
-    Abc_Cex_t * pCexMin = NULL;
+    Vec_Vec_t * vFrameReas;
+    Vec_Int_t * vRoots, * vLeaves;
     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 );
-
+    int i, f;
     // select reason for the property to fail
-    vReasonPis = Vec_VecStart( pCex->iFrame+1 );
-    vReasonLis = Vec_VecStart( pCex->iFrame+1 );
+    vFrameReas = Vec_VecStart( pCex->iFrame+1 );
+    vRoots = Vec_IntAlloc( 1000 );
     for ( f = pCex->iFrame; f >= 0; f-- )
     {
         // set phase and polarity
-        Saig_ManCexMinPhasePriority( pAig, pCex, f, vFramePis, vFrameLis, vPrioPis, vPrioLis, vPhaseLis, vPrios );
-        // select reasons
+        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
+        // create roots
+        vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
+        Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
+        // collect nodes starting from the roots
         Aig_ManIncrementTravId( pAig );
-        Vec_VecForEachEntryIntLevel( vFrameLis, Entry, i, f )
-            Saig_ManCexMinFindReason_rec( pAig, Aig_ManObj(pAig, Entry), vPrios, 
-                Vec_VecEntryInt( vReasonPis, f ),
-                (Vec_Int_t *)(f ? Vec_VecEntry( vReasonLis, f-1 ) : NULL) );
+        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
+            Saig_ManCexMinCollectReason_rec( pAig, pObj, Vec_VecEntryInt(vFrameReas, f), fPiReason );
+//printf( "%d(%d) ", Vec_VecLevelSize(vFrameCis, f), Vec_VecLevelSize(vFrameReas, f) ); 
     }
-
-    // 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;
+//printf( "\n" );
+    Vec_IntFree( vRoots );
+    return vFrameReas;
 }
 
 /**Function*************************************************************
@@ -332,25 +414,114 @@ Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, int f, Vec_Int_t * vTemp )
+Vec_Vec_t * Saig_ManCexMinComputeReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, int fPiReason )
 {
-    Vec_Int_t * vFrameCisOne;
-    Aig_Obj_t * pObj;
-    int i;
-    Vec_IntClear( vTemp );
-    if ( f == Vec_VecSize(vFrameCis) - 1 )
+    Vec_Vec_t * vFrameCis, * vFramePPs, * vFrameReas;
+    // sanity checks
+    assert( pCex->nPis == Saig_ManPiNum(pAig) );
+    assert( pCex->nRegs == Saig_ManRegNum(pAig) );
+    assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
+    // derive frame terms
+    vFrameCis = Saig_ManCexMinCollectFrameTerms( pAig, pCex );
+    // derive phase and priority
+    vFramePPs = Saig_ManCexMinCollectPhasePriority( pAig, pCex, vFrameCis );
+    // derive reasons for property failure
+    vFrameReas = Saig_ManCexMinCollectReason( pAig, pCex, vFrameCis, vFramePPs, fPiReason );
+    Vec_VecFree( vFramePPs );
+    Vec_VecFree( vFrameCis );
+    return vFrameReas;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicate with literals.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value )
+{
+    Vec_Int_t * vLevel;
+    Aig_Man_t * pAigNew;
+    Aig_Obj_t * pObj, * pMiter;
+    int i, k, Lit;
+    assert( pAig->nConstrs == 0 );
+    // start the new manager
+    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) + Vec_VecSize(vReg2Value) );
+    pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+    // create variables for PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pAigNew );
+    // add internal nodes of this frame
+    Aig_ManForEachNode( pAig, pObj, i )
+        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create POs for cubes
+    Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
     {
-        pObj = Aig_ManPo( pAig, pCex->iPo );
-        Vec_IntPush( vTemp, Aig_ObjId(pObj) );
-        return;
+        if ( i == 0 )
+            continue;
+        pMiter = Aig_ManConst1( pAigNew );
+        Vec_IntForEachEntry( vLevel, Lit, k )
+        {
+            assert( Lit >= 0 && Lit < 2 * Aig_ManRegNum(pAig) );
+            pObj = Saig_ManLi( pAig, Aig_Lit2Var(Lit) );
+            pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Aig_LitIsCompl(Lit)) );
+        }
+        Aig_ObjCreatePo( pAigNew, pMiter );
     }
-    vFrameCisOne = Vec_VecEntryInt( vFrameCis, f+1 );
-    Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
-        if ( Saig_ObjIsLo(pAig, pObj) )
-            Vec_IntPush( vTemp, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
+    // transfer to register outputs
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    // finalize
+    Aig_ManCleanup( pAigNew );
+    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+    return pAigNew;
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
+{
+    int fReasonPi = 0;
+
+    Abc_Cex_t * pCexMin = NULL;
+    Aig_Man_t * pManNew = NULL;
+    Vec_Vec_t * vFrameReas;
+    vFrameReas = Saig_ManCexMinComputeReason( pAig, pCex, fReasonPi );
+    printf( "Reason size = %d.  Ave = %d.\n", Vec_VecSizeSize(vFrameReas), Vec_VecSizeSize(vFrameReas)/(pCex->iFrame + 1) );
+
+    // try reducing the frames
+    if ( !fReasonPi )
+    {
+        char * pFileName = "aigcube.aig";
+        pManNew = Saig_ManCexMinDupWithCubes( pAig, vFrameReas );
+        Ioa_WriteAiger( pManNew, pFileName, 0, 0 );
+        Aig_ManStop( pManNew );
+        printf( "Intermediate AIG is written into file \"%s\".\n", pFileName );
+    }
+
+    // find reduced counter-example
+    Vec_VecFree( vFrameReas );
+    return pCexMin;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 54f6a1ff..5e9041b1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -20701,11 +20701,12 @@ int Abc_CommandCexMin( Abc_Frame_t * pAbc, int argc, char ** argv )
         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 );
+        vCexNew = Saig_ManCexMinPerform( pAig, pAbc->pCex );
         Aig_ManStop( pAig );
+        Abc_CexFree( vCexNew );
 //        Abc_FrameReplaceCex( pAbc, &vCexNew );
 
-        printf( "Implementation of this command is not finished.\n" );
+//        printf( "Implementation of this command is not finished.\n" );
     }
     return 0;