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

  FileName    [sswDyn.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Inductive prover with constraints.]

  Synopsis    [Dynamic loading of constraints.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - September 1, 2008.]

  Revision    [$Id: sswDyn.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]

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

#include "sswInt.h"
#include "misc/bar/bar.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Label PIs nodes of the frames corresponding to PIs of AIG.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
{
    Aig_Obj_t * pObj, * pObjFrames;
    int f, i;
    Aig_ManConst1( p->pFrames )->fMarkA = 1;
    Aig_ManConst1( p->pFrames )->fMarkB = 1;
    for ( f = 0; f < p->nFrames; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjFrames = Ssw_ObjFrame( p, pObj, f );
            assert( Aig_ObjIsCi(pObjFrames) );
            assert( pObjFrames->fMarkB == 0 );
            pObjFrames->fMarkA = 1;
            pObjFrames->fMarkB = 1;
        }
    }
}

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

  Synopsis    [Collects new POs in p->vNewPos.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
{
    assert( !Aig_IsComplement(pObj) );
    if ( pObj->fMarkA )
        return;
    pObj->fMarkA = 1;
    if ( Aig_ObjIsCi(pObj) )
    {
        Vec_PtrPush( vNewPis, pObj );
        return;
    }
    assert( Aig_ObjIsNode(pObj) );
    Ssw_ManCollectPis_rec( Aig_ObjFanin0(pObj), vNewPis );
    Ssw_ManCollectPis_rec( Aig_ObjFanin1(pObj), vNewPis );
}

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

  Synopsis    [Collects new POs in p->vNewPos.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos )
{
    Aig_Obj_t * pFanout;
    int iFanout = -1, i;
    assert( !Aig_IsComplement(pObj) );
    if ( pObj->fMarkB )
        return;
    pObj->fMarkB = 1;
    if ( pObj->Id > p->nSRMiterMaxId )
        return;
    if ( Aig_ObjIsCo(pObj) )
    {
        // skip if it is a register input PO
        if ( Aig_ObjCioId(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
            return;
        // add the number of this constraint
        Vec_IntPush( vNewPos, Aig_ObjCioId(pObj)/2 );
        return;
    }
    // visit the fanouts
    assert( p->pFrames->pFanData != NULL );
    Aig_ObjForEachFanout( p->pFrames, pObj, pFanout, iFanout, i )
        Ssw_ManCollectPos_rec( p, pFanout, vNewPos );
}

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

  Synopsis    [Loads logic cones and relevant constraints.]

  Description [Both pRepr and pObj are objects of the AIG.
  The result is the current SAT solver loaded with the logic cones
  for pRepr and pObj corresponding to them in the frames,
  as well as all the relevant constraints.]

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
{
    Aig_Obj_t * pObjFrames, * pReprFrames;
    Aig_Obj_t * pTemp, * pObj0, * pObj1;
    int i, iConstr, RetValue;

    assert( pRepr != pObj );
    // get the corresponding frames nodes
    pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
    pObjFrames  = Aig_Regular( Ssw_ObjFrame( p, pObj,  p->pPars->nFramesK ) );
    assert( pReprFrames != pObjFrames );
 /*
    // compute the AIG support
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
    Ssw_ManCollectPis_rec( pObj,  p->vNewLos );
    // add logic cones for register outputs
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
    {
        pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
        Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
    }
*/
    // add cones for the nodes
    Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
    Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );

    // compute the frames support
    Vec_PtrClear( p->vNewLos );
    Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
    Ssw_ManCollectPis_rec( pObjFrames,  p->vNewLos );
    // these nodes include both nodes corresponding to PIs and LOs
    // (the nodes corresponding to PIs should be labeled with fMarkB!)

    // collect the related constraint POs
    Vec_IntClear( p->vNewPos );
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
        Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
    // check if the corresponding pairs are added
    Vec_IntForEachEntry( p->vNewPos, iConstr, i )
    {
        pObj0 = Aig_ManCo( p->pFrames, 2*iConstr   );
        pObj1 = Aig_ManCo( p->pFrames, 2*iConstr+1 );
//        if ( pObj0->fMarkB && pObj1->fMarkB )
        if ( pObj0->fMarkB || pObj1->fMarkB )
        {
            pObj0->fMarkB = 1;
            pObj1->fMarkB = 1;
            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
        }
    }
    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
    {
        RetValue = sat_solver_simplify(p->pMSat->pSat);
        assert( RetValue != 0 );
    }
}

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

  Synopsis    [Tranfers simulation information from FRAIG to AIG.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
{
    Aig_Obj_t * pObj, * pObjFraig;
    unsigned * pInfo;
    int i, f, nFrames;

    // transfer simulation information
    Aig_ManForEachCi( p->pAig, pObj, i )
    {
        pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
        if ( pObjFraig == Aig_ManConst0(p->pFrames) )
        {
            Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
            continue;
        }
        assert( !Aig_IsComplement(pObjFraig) );
        assert( Aig_ObjIsCi(pObjFraig) );
        pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
        Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
    }
    // set random simulation info for the second frame
    for ( f = 1; f < p->nFrames; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
        {
            pObjFraig = Ssw_ObjFrame( p, pObj, f );
            assert( !Aig_IsComplement(pObjFraig) );
            assert( Aig_ObjIsCi(pObjFraig) );
            pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
            Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
        }
    }
    // create random info
    nFrames = Ssw_SmlNumFrames( p->pSml );
    for ( ; f < nFrames; f++ )
    {
        Saig_ManForEachPi( p->pAig, pObj, i )
            Ssw_SmlAssignRandomFrame( p->pSml, pObj, f );
    }
}

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

  Synopsis    [Performs one round of simulation with counter-examples.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
{
    int RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    // transfer PI simulation information from storage
//    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
    Ssw_ManSweepTransferDyn( p );
    // simulate internal nodes
//    Ssw_SmlSimulateOneFrame( p->pSml );
    Ssw_SmlSimulateOne( p->pSml );
    // check equivalence classes
    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
    // prepare simulation info for the next round
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
    p->nPatterns = 0;
    p->nSimRounds++;
p->timeSimSat += Abc_Clock() - clk;
    return RetValue1 > 0 || RetValue2 > 0;
}

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

  Synopsis    [Performs one round of simulation with counter-examples.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
{
    Aig_Obj_t * pObj, * pRepr, ** ppClass;
    int i, k, nSize, RetValue1, RetValue2;
    abctime clk = Abc_Clock();
    p->nSimRounds++;
    // transfer PI simulation information from storage
//    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
    Ssw_ManSweepTransferDyn( p );
    // determine const1 cands and classes to be simulated
    Vec_PtrClear( p->vResimConsts );
    Vec_PtrClear( p->vResimClasses );
    Aig_ManIncrementTravId( p->pAig );
    for ( i = p->iNodeStart; i < p->iNodeLast + p->pPars->nResimDelta; i++ )
    {
        if ( i >= Aig_ManObjNumMax( p->pAig ) )
            break;
        pObj = Aig_ManObj( p->pAig, i );
        if ( pObj == NULL )
            continue;
        if ( Ssw_ObjIsConst1Cand(p->pAig, pObj) )
        {
            Vec_PtrPush( p->vResimConsts, pObj );
            continue;
        }
        pRepr = Aig_ObjRepr(p->pAig, pObj);
        if ( pRepr == NULL )
            continue;
        if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
            continue;
        Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
        Vec_PtrPush( p->vResimClasses, pRepr );
    }
    // simulate internal nodes
//    Ssw_SmlSimulateOneFrame( p->pSml );
//    Ssw_SmlSimulateOne( p->pSml );
    // resimulate dynamically
//    Aig_ManIncrementTravId( p->pAig );
//    Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
    p->nVisCounter++;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimConsts, pObj, i )
        Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter );
    // resimulate the cone of influence of the cand classes
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
    {
        ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize );
        for ( k = 0; k < nSize; k++ )
            Ssw_SmlSimulateOneDyn_rec( p->pSml, ppClass[k], p->nFrames-1, p->pVisited, p->nVisCounter );
    }

    // check equivalence classes
//    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
//    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
    // refine these nodes
    RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 );
    RetValue2 = 0;
    Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
        RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 );

    // prepare simulation info for the next round
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
    p->nPatterns = 0;
    p->nSimRounds++;
p->timeSimSat += Abc_Clock() - clk;
    return RetValue1 > 0 || RetValue2 > 0;
}

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

  Synopsis    [Performs fraiging for the internal nodes.]

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssw_ManSweepDyn( Ssw_Man_t * p )
{
    Bar_Progress_t * pProgress = NULL;
    Aig_Obj_t * pObj, * pObjNew;
    int i, f;
    abctime clk;

    // perform speculative reduction
clk = Abc_Clock();
    // create timeframes
    p->pFrames = Ssw_FramesWithClasses( p );
    Aig_ManFanoutStart( p->pFrames );
    p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );

    // map constants and PIs of the last frame
    f = p->pPars->nFramesK;
    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
    Saig_ManForEachPi( p->pAig, pObj, i )
        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
    Aig_ManSetCioIds( p->pFrames );
    // label nodes corresponding to primary inputs
    Ssw_ManLabelPiNodes( p );
p->timeReduce += Abc_Clock() - clk;

    // prepare simulation info
    assert( p->vSimInfo == NULL );
    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 );
    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );

    // sweep internal nodes
    p->fRefined = 0;
    Ssw_ClassesClearRefined( p->ppClasses );
    if ( p->pPars->fVerbose )
        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
    p->iNodeStart = 0;
    Aig_ManForEachObj( p->pAig, pObj, i )
    {
        if ( p->iNodeStart == 0 )
            p->iNodeStart = i;
        if ( p->pPars->fVerbose )
            Bar_ProgressUpdate( pProgress, i, NULL );
        if ( Saig_ObjIsLo(p->pAig, pObj) )
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
        else if ( Aig_ObjIsNode(pObj) )
        {
            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
        }
        // check if it is time to recycle the solver
        if ( p->pMSat->pSat == NULL ||
            (p->pPars->nSatVarMax2 &&
             p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
             p->nRecycleCalls > p->pPars->nRecycleCalls2) )
        {
            // resimulate
            if ( p->nPatterns > 0 )
            {
                p->iNodeLast = i;
                if ( p->pPars->fLocalSim )
                    Ssw_ManSweepResimulateDynLocal( p, f );
                else
                    Ssw_ManSweepResimulateDyn( p, f );
                p->iNodeStart = i+1;
            }
//                Abc_Print( 1, "Recycling SAT solver with %d vars and %d calls.\n", 
//                    p->pMSat->nSatVars, p->nRecycleCalls );
//            Aig_ManCleanMarkAB( p->pAig );
            Aig_ManCleanMarkAB( p->pFrames );
            // label nodes corresponding to primary inputs
            Ssw_ManLabelPiNodes( p );
            // replace the solver
            if ( p->pMSat )
            {
                p->nVarsMax  = Abc_MaxInt( p->nVarsMax,  p->pMSat->nSatVars );
                p->nCallsMax = Abc_MaxInt( p->nCallsMax, p->pMSat->nSolverCalls );
                Ssw_SatStop( p->pMSat );
                p->nRecycles++;
                p->nRecyclesTotal++;
                p->nRecycleCalls = 0;
            }
            p->pMSat = Ssw_SatStart( 0 );
            assert( p->nPatterns == 0 );
        }
        // resimulate
        if ( p->nPatterns == 32 )
        {
            p->iNodeLast = i;
            if ( p->pPars->fLocalSim )
                Ssw_ManSweepResimulateDynLocal( p, f );
            else
                Ssw_ManSweepResimulateDyn( p, f );
            p->iNodeStart = i+1;
        }
    }
    // resimulate
    if ( p->nPatterns > 0 )
    {
        p->iNodeLast = i;
        if ( p->pPars->fLocalSim )
            Ssw_ManSweepResimulateDynLocal( p, f );
        else
            Ssw_ManSweepResimulateDyn( p, f );
    }
    // collect stats
    if ( p->pPars->fVerbose )
        Bar_ProgressStop( pProgress );

    // cleanup
//    Ssw_ClassesCheck( p->ppClasses );
    return p->fRefined;
}

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


ABC_NAMESPACE_IMPL_END