path: root/src/proof/abs/absOldCex.c

/**CFile****************************************************************

  FileName    [saigAbsCba.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [CEX-based abstraction.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: saigAbsCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "abs.h"
#include "sat/bmc/bmc.h"

ABC_NAMESPACE_IMPL_START

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

// local manager
typedef struct Saig_ManCba_t_ Saig_ManCba_t;
struct Saig_ManCba_t_
{
    // user data
    Aig_Man_t * pAig;       // user's AIG
    Abc_Cex_t * pCex;       // user's CEX
    int         nInputs;    // the number of first inputs to skip
    int         fVerbose;   // verbose flag
    // unrolling
    Aig_Man_t * pFrames;    // unrolled timeframes
    Vec_Int_t * vMapPiF2A;  // mapping of frame PIs into real PIs
    // additional information
    Vec_Vec_t * vReg2Frame; // register to frame mapping
    Vec_Vec_t * vReg2Value; // register to value mapping
};

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////


/**Function*************************************************************

  Synopsis    [Selects the best flops from the given array.]

  Description [Selects the best 'nFfsToSelect' flops among the array 
  'vAbsFfsToAdd' of flops that should be added to the abstraction.
  To this end, this procedure simulates the original AIG (pAig) using
  the given CEX (pAbsCex), which was detected for the abstraction.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect )
{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    Vec_Int_t * vMapEntries, * vFlopCosts, * vFlopAddCosts, * vFfsToAddBest;
    int i, k, f, Entry, iBit, * pPerm;
    assert( Aig_ManRegNum(pAig) == Vec_IntSize(vFlopClasses) );
    assert( Vec_IntSize(vAbsFfsToAdd) > nFfsToSelect );
    // map previously abstracted flops into their original numbers
    vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
    Vec_IntForEachEntry( vFlopClasses, Entry, i )
        if ( Entry == 0 )
            Vec_IntPush( vMapEntries, i );
    // simulate one frame at a time
    assert( Saig_ManPiNum(pAig) + Vec_IntSize(vMapEntries) == pAbsCex->nPis );
    vFlopCosts = Vec_IntStart( Vec_IntSize(vMapEntries) );
    // initialize the flops
    Aig_ManCleanMarkB(pAig);
    Aig_ManConst1(pAig)->fMarkB = 1;
    Saig_ManForEachLo( pAig, pObj, i )
        pObj->fMarkB = 0;
    for ( f = 0; f < pAbsCex->iFrame; f++ )
    {
        // override the flop values according to the cex
        iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig);
        Vec_IntForEachEntry( vMapEntries, Entry, k )
            Saig_ManLo(pAig, Entry)->fMarkB = Abc_InfoHasBit(pAbsCex->pData, iBit + k);
        // simulate
        Aig_ManForEachNode( pAig, pObj, k )
            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
        Aig_ManForEachCo( pAig, pObj, k )
            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
        // transfer
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
            pObjRo->fMarkB = pObjRi->fMarkB;
        // compare
        iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig);
        Vec_IntForEachEntry( vMapEntries, Entry, k )
            if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Abc_InfoHasBit(pAbsCex->pData, iBit + k) )
                Vec_IntAddToEntry( vFlopCosts, k, 1 );
    }
//    Vec_IntForEachEntry( vFlopCosts, Entry, i )
//        printf( "%d ", Entry );
//    printf( "\n" );
    // remap the cost
    vFlopAddCosts = Vec_IntAlloc( Vec_IntSize(vAbsFfsToAdd) );
    Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
        Vec_IntPush( vFlopAddCosts, -Vec_IntEntry(vFlopCosts, Entry) );
    // sort the flops
    pPerm = Abc_MergeSortCost( Vec_IntArray(vFlopAddCosts), Vec_IntSize(vFlopAddCosts) );
    // shrink the array
    vFfsToAddBest = Vec_IntAlloc( nFfsToSelect );
    for ( i = 0; i < nFfsToSelect; i++ )
    {
//        printf( "%d ", Vec_IntEntry(vFlopAddCosts, pPerm[i]) );
        Vec_IntPush( vFfsToAddBest, Vec_IntEntry(vAbsFfsToAdd, pPerm[i]) );
    }
//    printf( "\n" );
    // cleanup
    ABC_FREE( pPerm );
    Vec_IntFree( vMapEntries );
    Vec_IntFree( vFlopCosts );
    Vec_IntFree( vFlopAddCosts );
    Aig_ManCleanMarkB(pAig);
    // return the computed flops
    return vFfsToAddBest;
}


/**Function*************************************************************

  Synopsis    [Duplicate with literals.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManDupWithCubes( 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) );
    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
    // create variables for PIs
    Aig_ManForEachCi( pAig, pObj, i )
        pObj->pData = Aig_ObjCreateCi( 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 )
    {
        pMiter = Aig_ManConst1( pAigNew );
        Vec_IntForEachEntry( vLevel, Lit, k )
        {
            pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
            pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
        }
        Aig_ObjCreateCo( pAigNew, pMiter );
    }
    // transfer to register outputs
    Saig_ManForEachLi( pAig, pObj, i )
        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
    // finalize
    Aig_ManCleanup( pAigNew );
    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
    return pAigNew;
}

/**Function*************************************************************

  Synopsis    [Maps array of frame PI IDs into array of additional PI IDs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_ManCbaReason2Inputs( Saig_ManCba_t * p, Vec_Int_t * vReasons )
{
    Vec_Int_t * vOriginal, * vVisited;
    int i, Entry;
    vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) ); 
    vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
    Vec_IntForEachEntry( vReasons, Entry, i )
    {
        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
        assert( iInput >= p->nInputs && iInput < Aig_ManCiNum(p->pAig) );
        if ( Vec_IntEntry(vVisited, iInput) == 0 )
            Vec_IntPush( vOriginal, iInput - p->nInputs );
        Vec_IntAddToEntry( vVisited, iInput, 1 );
    }
    Vec_IntFree( vVisited );
    return vOriginal;
}

/**Function*************************************************************

  Synopsis    [Creates the counter-example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Saig_ManCbaReason2Cex( Saig_ManCba_t * p, Vec_Int_t * vReasons )
{
    Abc_Cex_t * pCare;
    int i, Entry, iInput, iFrame;
    pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
    memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
    Vec_IntForEachEntry( vReasons, Entry, i )
    {
        assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) );
        iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
        iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
        Abc_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 +=  Abc_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i);
        printf( "%d ", Count );
    }
printf( "\n" );
*/
    return pCare;
}

/**Function*************************************************************

  Synopsis    [Returns reasons for the property to fail.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons )
{
    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(p, pObj);
    if ( Aig_ObjIsConst1(pObj) )
        return;
    if ( Aig_ObjIsCi(pObj) )
    {
        Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    if ( pObj->fPhase )
    {
        Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
        Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
    }
    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_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
        else if ( fPhase0 && !fPhase1 )
            Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
        else 
        {
            int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
            int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
            if ( iPrio0 <= iPrio1 )
                Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
            else
                Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
        }
    }
}

/**Function*************************************************************

  Synopsis    [Returns reasons for the property to fail.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
{
    Aig_Obj_t * pObj;
    Vec_Int_t * vPrios, * vReasons;
    int i;

    // set PI values according to CEX
    vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
    Aig_ManConst1(p->pFrames)->fPhase = 1;
    Aig_ManForEachCi( p->pFrames, pObj, i )
    {
        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
        int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
        pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
        Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
    }

    // traverse and set the priority
    Aig_ManForEachNode( p->pFrames, pObj, i )
    {
        int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
        int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
        int iPrio0  = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
        int iPrio1  = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
        pObj->fPhase = fPhase0 && fPhase1;
        if ( fPhase0 && fPhase1 ) // both are one
            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(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_MinInt(iPrio0, iPrio1) );
    }
    // check the property output
    pObj = Aig_ManCo( p->pFrames, 0 );
    pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
    assert( !pObj->fPhase );

    // select the reason
    vReasons = Vec_IntAlloc( 100 );
    Aig_ManIncrementTravId( p->pFrames );
    Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
    Vec_IntFree( vPrios );
//    assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
    return vReasons;
}


/**Function*************************************************************

  Synopsis    [Collect nodes in the unrolled timeframes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManCbaUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots )
{
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
    if ( Aig_ObjIsCo(pObj) )
        Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
    else if ( Aig_ObjIsNode(pObj) )
    {
        Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
        Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
    }
    if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
        Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
    Vec_IntPush( vObjs, Aig_ObjId(pObj) );
}

/**Function*************************************************************

  Synopsis    [Derive unrolled timeframes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A, Vec_Vec_t ** pvReg2Frame )
{
    Aig_Man_t * pFrames;     // unrolled timeframes
    Vec_Vec_t * vFrameCos;   // the list of COs per frame
    Vec_Vec_t * vFrameObjs;  // the list of objects per frame
    Vec_Int_t * vRoots, * vObjs;
    Aig_Obj_t * pObj;
    int i, f;
    // sanity checks
    assert( Saig_ManPiNum(pAig) == pCex->nPis );
//    assert( Saig_ManRegNum(pAig) == pCex->nRegs );
    assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );

    // map PIs of the unrolled frames into PIs of the original design
    *pvMapPiF2A = Vec_IntAlloc( 1000 );

    // collect COs and Objs visited in each frame
    vFrameCos  = Vec_VecStart( pCex->iFrame+1 );
    vFrameObjs = Vec_VecStart( pCex->iFrame+1 );
    // initialized the topmost frame
    pObj = Aig_ManCo( pAig, pCex->iPo );
    Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) );
    for ( f = pCex->iFrame; f >= 0; f-- )
    {
        // collect nodes starting from the roots
        Aig_ManIncrementTravId( pAig );
        vRoots = Vec_VecEntryInt( vFrameCos, f );
        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
            Saig_ManCbaUnrollCollect_rec( pAig, pObj, 
                Vec_VecEntryInt(vFrameObjs, f),
                (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
    }

    // derive unrolled timeframes
    pFrames = Aig_ManStart( 10000 );
    pFrames->pName = Abc_UtilStrsav( pAig->pName );
    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
    // initialize the flops 
    if ( Saig_ManRegNum(pAig) == pCex->nRegs )
    {
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) );
    }
    else // this is the case when synthesis was applied, assume all-0 init state
    {
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), 1 );
    }
    // iterate through the frames
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        // construct
        vObjs = Vec_VecEntryInt( vFrameObjs, f );
        Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
        {
            if ( Aig_ObjIsNode(pObj) )
                pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
            else if ( Aig_ObjIsCo(pObj) )
                pObj->pData = Aig_ObjChild0Copy(pObj);
            else if ( Aig_ObjIsConst1(pObj) )
                pObj->pData = Aig_ManConst1(pFrames);
            else if ( Saig_ObjIsPi(pAig, pObj) )
            {
                if ( Aig_ObjCioId(pObj) < nInputs )
                {
                    int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
                    pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
                }
                else
                {
                    pObj->pData = Aig_ObjCreateCi( pFrames );
                    Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
                    Vec_IntPush( *pvMapPiF2A, f );
                }
            }
        }
        if ( f == pCex->iFrame )
            break;
        // transfer
        vRoots = Vec_VecEntryInt( vFrameCos, f );
        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
        {
            Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
            if ( *pvReg2Frame )
            {
                Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjId(pObj) );             // record LO
                Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjToLit((Aig_Obj_t *)pObj->pData) ); // record its literal
            }
        }
    }
    // create output
    pObj = Aig_ManCo( pAig, pCex->iPo );
    Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
    Aig_ManSetRegNum( pFrames, 0 );
    // cleanup
    Vec_VecFree( vFrameCos );
    Vec_VecFree( vFrameObjs );
    // finallize
    Aig_ManCleanup( pFrames );
    // return
    return pFrames;
}

/**Function*************************************************************

  Synopsis    [Creates refinement manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Saig_ManCba_t * Saig_ManCbaStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
{
    Saig_ManCba_t * p;
    p = ABC_CALLOC( Saig_ManCba_t, 1 );
    p->pAig = pAig;
    p->pCex = pCex;
    p->nInputs = nInputs;
    p->fVerbose = fVerbose;
    return p;
}

/**Function*************************************************************

  Synopsis    [Destroys refinement manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManCbaStop( Saig_ManCba_t * p )
{
    Vec_VecFreeP( &p->vReg2Frame );
    Vec_VecFreeP( &p->vReg2Value );
    Aig_ManStopP( &p->pFrames );
    Vec_IntFreeP( &p->vMapPiF2A );
    ABC_FREE( p );
}

/**Function*************************************************************

  Synopsis    [Destroys refinement manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManCbaShrink( Saig_ManCba_t * p )
{
    Aig_Man_t * pManNew;
    Aig_Obj_t * pObjLi, * pObjFrame;
    Vec_Int_t * vLevel, * vLevel2;
    int f, k, ObjId, Lit;
    // assuming that important objects are labeled in Saig_ManCbaFindReason()
    Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, f )
    {
        Vec_IntForEachEntryDouble( vLevel, ObjId, Lit, k )
        {
            pObjFrame = Aig_ManObj( p->pFrames, Abc_Lit2Var(Lit) );
            if ( pObjFrame == NULL || (!Aig_ObjIsConst1(pObjFrame) && !Aig_ObjIsTravIdCurrent(p->pFrames, pObjFrame)) )
                continue;
            pObjLi = Aig_ManObj( p->pAig, ObjId );
            assert( Saig_ObjIsLi(p->pAig, pObjLi) );
            Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjCioId(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) );
        }
    }
    // print statistics
    Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, k )
    {
        vLevel2 = Vec_VecEntryInt( p->vReg2Value, k );
        printf( "Level = %4d   StateBits = %4d (%6.2f %%)  CareBits = %4d (%6.2f %%)\n", k, 
            Vec_IntSize(vLevel)/2, 100.0 * (Vec_IntSize(vLevel)/2) / Aig_ManRegNum(p->pAig),
            Vec_IntSize(vLevel2),  100.0 * Vec_IntSize(vLevel2) / Aig_ManRegNum(p->pAig) );
    }
    // try reducing the frames
    pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value );
//    Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 );
    Aig_ManStop( pManNew );
}

static inline void Saig_ObjCexMinSet0( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; pObj->fMarkB = 0;    }
static inline void Saig_ObjCexMinSet1( Aig_Obj_t * pObj ) { pObj->fMarkA = 0; pObj->fMarkB = 1;    }
static inline void Saig_ObjCexMinSetX( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; pObj->fMarkB = 1;    }

static inline int  Saig_ObjCexMinGet0( Aig_Obj_t * pObj ) { return  pObj->fMarkA && !pObj->fMarkB; }
static inline int  Saig_ObjCexMinGet1( Aig_Obj_t * pObj ) { return !pObj->fMarkA &&  pObj->fMarkB; }
static inline int  Saig_ObjCexMinGetX( Aig_Obj_t * pObj ) { return  pObj->fMarkA &&  pObj->fMarkB; }

static inline int  Saig_ObjCexMinGet0Fanin0( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }
static inline int  Saig_ObjCexMinGet1Fanin0( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }

static inline int  Saig_ObjCexMinGet0Fanin1( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }
static inline int  Saig_ObjCexMinGet1Fanin1( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }

static inline void Saig_ObjCexMinSim( Aig_Obj_t * pObj )
{
    if ( Aig_ObjIsAnd(pObj) )
    {
        if ( Saig_ObjCexMinGet0Fanin0(pObj) || Saig_ObjCexMinGet0Fanin1(pObj) )
            Saig_ObjCexMinSet0( pObj );
        else if ( Saig_ObjCexMinGet1Fanin0(pObj) && Saig_ObjCexMinGet1Fanin1(pObj) )
            Saig_ObjCexMinSet1( pObj );
        else 
            Saig_ObjCexMinSetX( pObj );
    }
    else if ( Aig_ObjIsCo(pObj) )
    {
        if ( Saig_ObjCexMinGet0Fanin0(pObj) )
            Saig_ObjCexMinSet0( pObj );
        else if ( Saig_ObjCexMinGet1Fanin0(pObj) )
            Saig_ObjCexMinSet1( pObj );
        else 
            Saig_ObjCexMinSetX( pObj );
    }
    else assert( 0 );
}

static inline void Saig_ObjCexMinPrint( Aig_Obj_t * pObj )
{
    if ( Saig_ObjCexMinGet0(pObj) )
        printf( "0" );
    else if ( Saig_ObjCexMinGet1(pObj) )
        printf( "1" );
    else if ( Saig_ObjCexMinGetX(pObj) )
        printf( "X" );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManCexVerifyUsingTernary( Aig_Man_t * pAig, Abc_Cex_t * pCex, Abc_Cex_t * pCare )
{
    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
    int i, f, iBit = 0;
    assert( pCex->iFrame == pCare->iFrame );
    assert( pCex->nBits  == pCare->nBits );
    assert( pCex->iPo < Saig_ManPoNum(pAig) );
    Saig_ObjCexMinSet1( Aig_ManConst1(pAig) );
    // set flops to the init state
    Saig_ManForEachLo( pAig, pObj, i )
    {
        assert( !Abc_InfoHasBit(pCex->pData, iBit) );
        assert( !Abc_InfoHasBit(pCare->pData, iBit) );
//        if ( Abc_InfoHasBit(pCare->pData, iBit++) )
            Saig_ObjCexMinSet0( pObj );
//        else
//            Saig_ObjCexMinSetX( pObj );
    }
    iBit = pCex->nRegs;
    for ( f = 0; f <= pCex->iFrame; f++ )
    {
        // init inputs
        Saig_ManForEachPi( pAig, pObj, i )
        {
            if ( Abc_InfoHasBit(pCare->pData, iBit++) )
            {
                if ( Abc_InfoHasBit(pCex->pData, iBit-1) )
                    Saig_ObjCexMinSet1( pObj );
                else
                    Saig_ObjCexMinSet0( pObj );
            }
            else
                Saig_ObjCexMinSetX( pObj );
        }
        // simulate internal nodes
        Aig_ManForEachNode( pAig, pObj, i )
            Saig_ObjCexMinSim( pObj );
        // simulate COs
        Aig_ManForEachCo( pAig, pObj, i )
            Saig_ObjCexMinSim( pObj );
/*
        Aig_ManForEachObj( pAig, pObj, i )
        {
            Aig_ObjPrint(pAig, pObj);
            printf( "  Value = " );
            Saig_ObjCexMinPrint( pObj );
            printf( "\n" );
        }
*/
        // transfer
        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
            pObjRo->fMarkA = pObjRi->fMarkA,
            pObjRo->fMarkB = pObjRi->fMarkB;
    }
    assert( iBit == pCex->nBits );
    return Saig_ObjCexMinGet1( Aig_ManCo( pAig, pCex->iPo ) );
}

/**Function*************************************************************

  Synopsis    [SAT-based refinement of the counter-example.]

  Description [The first parameter (nInputs) indicates how many first 
  primary inputs to skip without considering as care candidates.]
               

  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
{
    Saig_ManCba_t * p;
    Vec_Int_t * vReasons;
    Abc_Cex_t * pCare;
    abctime clk = Abc_Clock();

    clk = Abc_Clock();
    p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );

//    p->vReg2Frame = Vec_VecStart( pCex->iFrame );
//    p->vReg2Value = Vec_VecStart( pCex->iFrame );
    p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A, &p->vReg2Frame );
    vReasons = Saig_ManCbaFindReason( p );
    if ( p->vReg2Frame )
        Saig_ManCbaShrink( p );


//if ( fVerbose )
//Aig_ManPrintStats( p->pFrames );

    if ( fVerbose )
    {
        Vec_Int_t * vRes = Saig_ManCbaReason2Inputs( p, vReasons );
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
        Vec_IntFree( vRes );
ABC_PRT( "Time", Abc_Clock() - clk );
    }

    pCare = Saig_ManCbaReason2Cex( p, vReasons );
    Vec_IntFree( vReasons );
    Saig_ManCbaStop( p );

if ( fVerbose )
{
printf( "Real " );
Abc_CexPrintStats( pCex );
}
if ( fVerbose )
{
printf( "Care " );
Abc_CexPrintStats( pCare );
}
/*
    // verify the reduced counter-example using ternary simulation
    if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
        printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
    else if ( fVerbose )
        printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
*/
    Aig_ManCleanMarkAB( pAig );
    return pCare;
}

/**Function*************************************************************

  Synopsis    [Returns the array of PIs for flops that should not be absracted.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
{
    Saig_ManCba_t * p;
    Vec_Int_t * vRes, * vReasons;
    abctime clk;
    if ( Saig_ManPiNum(pAig) != pCex->nPis )
    {
        printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
            Aig_ManCiNum(pAig), pCex->nPis );
        return NULL;
    }

clk = Abc_Clock();
    p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose );
    p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame );
    vReasons = Saig_ManCbaFindReason( p );
    vRes = Saig_ManCbaReason2Inputs( p, vReasons );
    if ( fVerbose )
    {
        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
            Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), 
            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
ABC_PRT( "Time", Abc_Clock() - clk );
    }

    Vec_IntFree( vReasons );
    Saig_ManCbaStop( p );
    return vRes;
}




/**Function*************************************************************

  Synopsis    [Checks the abstracted model for a counter-example.]

  Description [Returns the array of abstracted flops that should be added
  to the abstraction.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars )
{
    Vec_Int_t * vAbsFfsToAdd;
    int RetValue;
    abctime clk = Abc_Clock();
//    assert( pAbs->nRegs > 0 );
    // perform BMC
    RetValue = Saig_ManBmcScalable( pAbs, pPars );
    if ( RetValue == -1 ) // time out - nothing to add
    {
        printf( "Resource limit is reached during BMC.\n" );
        assert( pAbs->pSeqModel == NULL );
        return Vec_IntAlloc( 0 );
    }
    if ( pAbs->pSeqModel == NULL )
    {
        printf( "BMC did not detect a CEX with the given depth.\n" );
        return Vec_IntAlloc( 0 );
    }
    if ( pPars->fVerbose )
        Abc_CexPrintStats( pAbs->pSeqModel );
    // CEX is detected - refine the flops
    vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAbs, nInputs, pAbs->pSeqModel, pPars->fVerbose );
    if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
    {
        Vec_IntFree( vAbsFfsToAdd );
        return NULL;
    }
    if ( pPars->fVerbose )
    {
        printf( "Adding %d registers to the abstraction (total = %d).  ", 
            Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    }
    return vAbsFfsToAdd;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_IMPL_END