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

  FileName    [pdrTsim.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Property driven reachability.]

  Synopsis    [Ternary simulation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - November 20, 2010.]

  Revision    [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]

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

#include "pdrInt.h"

ABC_NAMESPACE_IMPL_START

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

#define PDR_ZER 1
#define PDR_ONE 2
#define PDR_UND 3

static inline int Pdr_ManSimInfoNot( int Value )
{
    if ( Value == PDR_ZER )
        return PDR_ONE;
    if ( Value == PDR_ONE )
        return PDR_ZER;
    return PDR_UND;
}

static inline int Pdr_ManSimInfoAnd( int Value0, int Value1 )
{
    if ( Value0 == PDR_ZER || Value1 == PDR_ZER )
        return PDR_ZER;
    if ( Value0 == PDR_ONE && Value1 == PDR_ONE )
        return PDR_ONE;
    return PDR_UND;
}

static inline int Pdr_ManSimInfoGet( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
}

static inline void Pdr_ManSimInfoSet( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
{
    assert( Value >= PDR_ZER && Value <= PDR_UND );
    Value ^= Pdr_ManSimInfoGet( p, pObj );
    p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
}

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

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

  Synopsis    [Marks the TFI cone and collects CIs and nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
{
    assert( !Aig_IsComplement(pObj) );
    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
        return;
    Aig_ObjSetTravIdCurrent(pAig, pObj);
    if ( Aig_ObjIsCi(pObj) )
    {
        Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
        return;
    }
    Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
    if ( Aig_ObjIsCo(pObj) )
        return;
    Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
    Vec_IntPush( vNodes, Aig_ObjId(pObj) );
}

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

  Synopsis    [Marks the TFI cone and collects CIs and nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
{
    Aig_Obj_t * pObj;
    int i;
    Vec_IntClear( vCiObjs );
    Vec_IntClear( vNodes );
    Aig_ManIncrementTravId( pAig );
    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
        Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
}

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

  Synopsis    [Performs ternary simulation for one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
{
    int Value0, Value1, Value;
    Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
    if ( Aig_ObjFaninC0(pObj) )
        Value0 = Pdr_ManSimInfoNot( Value0 );
    if ( Aig_ObjIsCo(pObj) )
    {
        Pdr_ManSimInfoSet( pAig, pObj, Value0 );
        return Value0;
    }
    assert( Aig_ObjIsNode(pObj) );
    Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) );
    if ( Aig_ObjFaninC1(pObj) )
        Value1 = Pdr_ManSimInfoNot( Value1 );
    Value = Pdr_ManSimInfoAnd( Value0, Value1 );
    Pdr_ManSimInfoSet( pAig, pObj, Value );
    return Value;
}

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

  Synopsis    [Performs ternary simulation for one design.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManSimDataInit( Aig_Man_t * pAig,
    Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
    Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
{
    Aig_Obj_t * pObj;
    int i;
    // set the CI values
    Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
        Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
    // set the FOs to remove
    if ( vCi2Rem != NULL )
    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
        Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
    // perform ternary simulation
    Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
        Pdr_ManExtendOneEval( pAig, pObj );
    // transfer results to the output
    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
        Pdr_ManExtendOneEval( pAig, pObj );
    // check the results
    Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
        if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
            return 0;
    return 1;
}

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

  Synopsis    [Tries to assign ternary value to one of the CIs.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis )
{
    Aig_Obj_t * pFanout;
    int i, k, iFanout = -1, Value, Value2;
    assert( Saig_ObjIsLo(pAig, pObj) );
    assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
    // save original value
    Value = Pdr_ManSimInfoGet( pAig, pObj );
    assert( Value == PDR_ZER || Value == PDR_ONE );
    Vec_IntPush( vUndo, Aig_ObjId(pObj) );
    Vec_IntPush( vUndo, Value );
    // update original value
    Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
    // traverse
    Vec_IntClear( vVis );
    Vec_IntPush( vVis, Aig_ObjId(pObj) );
    Aig_ManForEachObjVec( vVis, pAig, pObj, i )
    {
        Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
        {
            if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
                continue;
            assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
            Value = Pdr_ManSimInfoGet( pAig, pFanout );
            if ( Value == PDR_UND )
                continue;
            Value2 = Pdr_ManExtendOneEval( pAig, pFanout );
            if ( Value2 == Value )
                continue;
            assert( Value2 == PDR_UND );
            Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
            Vec_IntPush( vUndo, Value );
            if ( Aig_ObjIsCo(pFanout) )
                return 0;
            assert( Aig_ObjIsNode(pFanout) );
            Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
        }
    }
    return 1;
}

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

  Synopsis    [Undoes the partial results of ternary simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
{
    Aig_Obj_t * pObj;
    int i, Value;
    Aig_ManForEachObjVec( vUndo, pAig, pObj, i )
    {
        Value  = Vec_IntEntry(vUndo, ++i);
        assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
        Pdr_ManSimInfoSet( pAig, pObj, Value );
    }
}

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

  Synopsis    [Derives the resulting cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem, Vec_Int_t * vRes, Vec_Int_t * vPiLits )
{
    Aig_Obj_t * pObj;
    int i, Lit;
    // mark removed flop outputs
    Aig_ManIncrementTravId( pAig );
    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
    {
        assert( Saig_ObjIsLo( pAig, pObj ) );
        Aig_ObjSetTravIdCurrent(pAig, pObj);
    }
    // collect flop outputs that are not marked
    Vec_IntClear( vRes );
    Vec_IntClear( vPiLits );
    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
    {
        if ( Saig_ObjIsPi(pAig, pObj) )
        {
            Lit = Abc_Var2Lit( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
            Vec_IntPush( vPiLits, Lit );
            continue;
        }
        assert( Saig_ObjIsLo(pAig, pObj) );
        if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
            continue;
        Lit = Abc_Var2Lit( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
        Vec_IntPush( vRes, Lit );
    }
    if ( Vec_IntSize(vRes) == 0 )
        Vec_IntPush(vRes, 0);
}

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

  Synopsis    [Derives the resulting cube.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem )
{
    Aig_Obj_t * pObj;
    int i;
    char * pBuff = ABC_ALLOC( char, Aig_ManCiNum(pAig)+1 );
    for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
        pBuff[i] = '-';
    pBuff[i] = 0;
    Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
        pBuff[Aig_ObjCioId(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
    if ( vCi2Rem )
    Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
        pBuff[Aig_ObjCioId(pObj)] = 'x';
    Abc_Print( 1, "%s\n", pBuff );
    ABC_FREE( pBuff );
}

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

  Synopsis    [Shrinks values using ternary simulation.]

  Description [The cube contains the set of flop index literals which,
  when converted into a clause and applied to the combinational outputs, 
  led to a satisfiable SAT run in frame k (values stored in the SAT solver).
  If the cube is NULL, it is assumed that the first property output was
  asserted and failed.
  The resulting array is a set of flop index literals that asserts the COs.
  Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
{
    Pdr_Set_t * pRes;
    Vec_Int_t * vPrio   = p->vPrio;    // priority flops (flop indices)
    Vec_Int_t * vPiLits = p->vLits;    // array of literals (0/1 PI values)
    Vec_Int_t * vCiObjs = p->vCiObjs;  // cone leaves (CI obj IDs)
    Vec_Int_t * vCoObjs = p->vCoObjs;  // cone roots (CO obj IDs)
    Vec_Int_t * vCiVals = p->vCiVals;  // cone leaf values (0/1 CI values)
    Vec_Int_t * vCoVals = p->vCoVals;  // cone root values (0/1 CO values)
    Vec_Int_t * vNodes  = p->vNodes;   // cone nodes (node obj IDs)
    Vec_Int_t * vUndo   = p->vUndo;    // cone undos (node obj IDs)
    Vec_Int_t * vVisits = p->vVisits;  // intermediate (obj IDs)
    Vec_Int_t * vCi2Rem = p->vCi2Rem;  // CIs to be removed (CI obj IDs)
    Vec_Int_t * vRes    = p->vRes;     // final result (flop literals)
    Aig_Obj_t * pObj;
    int i, Entry, RetValue;
    //abctime clk = Abc_Clock();

    // collect CO objects
    Vec_IntClear( vCoObjs );
    if ( pCube == NULL ) // the target is the property output
    {
//        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, p->iOutCur)) );
    }
    else // the target is the cube
    {
        for ( i = 0; i < pCube->nLits; i++ )
        {
            if ( pCube->Lits[i] == -1 )
                continue;
            pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
            Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
        }
    }
if ( p->pPars->fVeryVerbose )
{
Abc_Print( 1, "Trying to justify cube " );
if ( pCube )
    Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
else
    Abc_Print( 1, "<prop=fail>" );
Abc_Print( 1, " in frame %d.\n", k );
}

    // collect CI objects
    Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
    // collect values
    Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
    Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
    // simulate for the first time
if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
    assert( RetValue );

    // iteratively remove flops
    if ( p->pPars->fFlopPrio )
    {
        // collect flops and sort them by priority
        Vec_IntClear( vRes );
        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
        {
            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                continue;
            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
            Vec_IntPush( vRes, Entry );
        }
        Vec_IntSelectSortCost( Vec_IntArray(vRes), Vec_IntSize(vRes), vPrio );

        // try removing flops starting from low-priority to high-priority
        Vec_IntClear( vCi2Rem );
        Vec_IntForEachEntry( vRes, Entry, i )
        {
            pObj = Aig_ManCi( p->pAig, Saig_ManPiNum(p->pAig) + Entry );
            assert( Saig_ObjIsLo( p->pAig, pObj ) );
            Vec_IntClear( vUndo );
            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
            else
                Pdr_ManExtendUndo( p->pAig, vUndo );
        }
    }
    else
    {
        // try removing low-priority flops first
        Vec_IntClear( vCi2Rem );
        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
        {
            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                continue;
            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
            if ( Vec_IntEntry(vPrio, Entry) )
                continue;
            Vec_IntClear( vUndo );
            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
            else
                Pdr_ManExtendUndo( p->pAig, vUndo );
        }
        // try removing high-priority flops next
        Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
        {
            if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                continue;
            Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
            if ( !Vec_IntEntry(vPrio, Entry) )
                continue;
            Vec_IntClear( vUndo );
            if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
                Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
            else
                Pdr_ManExtendUndo( p->pAig, vUndo );
        }
    }

if ( p->pPars->fVeryVerbose )
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
    RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
    assert( RetValue );

    // derive the set of resulting registers
    Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
    assert( Vec_IntSize(vRes) > 0 );
    //p->tTsim += Abc_Clock() - clk;

    // move abstracted literals from flops to inputs
    if ( p->pPars->fUseAbs && p->vAbsFlops )
    {
        int i, iLit, k = 0;
        Vec_IntForEachEntry( vRes, iLit, i )
        {
            if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
                Vec_IntWriteEntry( vRes, k++, iLit );
            else
                Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit );
        }
        Vec_IntShrink( vRes, k );
    }
    pRes = Pdr_SetCreate( vRes, vPiLits );
    //ZH: Disabled assertion because this invariant doesn't hold with down
    //because of the join operation which can bring in initial states
    //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
    return pRes;
}

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


ABC_NAMESPACE_IMPL_END