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

  FileName    [simSupp.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Simulation to determine functional support.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "base/abc/abc.h"
#include "proof/fraig/fraig.h"
#include "sim.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////
 
static int    Sim_ComputeSuppRound( Sim_Man_t * p, int  fUseTargets );
static int    Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, int  fUseTargets );
static void   Sim_ComputeSuppSetTargets( Sim_Man_t * p );

static void   Sim_UtilAssignRandom( Sim_Man_t * p );
static void   Sim_UtilAssignFromFifo( Sim_Man_t * p );
static void   Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters );
static int    Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output );

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

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

  Synopsis    [Computes structural supports.]

  Description [Supports are returned as an array of bit strings, one
  for each CO.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Sim_ComputeStrSupp( Abc_Ntk_t * pNtk )
{
    Vec_Ptr_t * vSuppStr;
    Abc_Obj_t * pNode;
    unsigned * pSimmNode, * pSimmNode1, * pSimmNode2;
    int nSuppWords, i, k;
    // allocate room for structural supports
    nSuppWords = SIM_NUM_WORDS( Abc_NtkCiNum(pNtk) );
    vSuppStr   = Sim_UtilInfoAlloc( Abc_NtkObjNumMax(pNtk), nSuppWords, 1 );
    // assign the structural support to the PIs
    Abc_NtkForEachCi( pNtk, pNode, i )
        Sim_SuppStrSetVar( vSuppStr, pNode, i );
    // derive the structural supports of the internal nodes
    Abc_NtkForEachNode( pNtk, pNode, i )
    {
//        if ( Abc_NodeIsConst(pNode) )
//            continue;
        pSimmNode  = (unsigned *)vSuppStr->pArray[ pNode->Id ];
        pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
        pSimmNode2 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId1(pNode) ];
        for ( k = 0; k < nSuppWords; k++ )
            pSimmNode[k] = pSimmNode1[k] | pSimmNode2[k];
    }
    // set the structural supports of the PO nodes
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        pSimmNode  = (unsigned *)vSuppStr->pArray[ pNode->Id ];
        pSimmNode1 = (unsigned *)vSuppStr->pArray[ Abc_ObjFaninId0(pNode) ];
        for ( k = 0; k < nSuppWords; k++ )
            pSimmNode[k] = pSimmNode1[k];
    }
    return vSuppStr;
}

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

  Synopsis    [Compute functional supports.]

  Description [Supports are returned as an array of bit strings, one
  for each CO.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose )
{
    Sim_Man_t * p;
    Vec_Ptr_t * vResult;
    int nSolved, i;
    abctime clk = Abc_Clock();

    srand( 0xABC );

    // start the simulation manager
    p = Sim_ManStart( pNtk, 0 );

    // compute functional support using one round of random simulation
    Sim_UtilAssignRandom( p );
    Sim_ComputeSuppRound( p, 0 );

    // set the support targets 
    Sim_ComputeSuppSetTargets( p );
if ( fVerbose )
    printf( "Number of support targets after simulation = %5d.\n", Vec_VecSizeSize(p->vSuppTargs) );
    if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
        goto exit;

    for ( i = 0; i < 1; i++ )
    {
        // compute patterns using one round of random simulation
        Sim_UtilAssignRandom( p );
        nSolved = Sim_ComputeSuppRound( p, 1 );
        if ( Vec_VecSizeSize(p->vSuppTargs) == 0 )
            goto exit;

if ( fVerbose )
    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.\n", 
       Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo) );
    }

    // try to solve the support targets
    while ( Vec_VecSizeSize(p->vSuppTargs) > 0 )
    {
        // solve targets until the first disproved one (which gives counter-example)
        Sim_SolveTargetsUsingSat( p, p->nSimWords/p->nSuppWords );
        // compute additional functional support
        Sim_UtilAssignFromFifo( p );
        nSolved = Sim_ComputeSuppRound( p, 1 );

if ( fVerbose )
    printf( "Targets = %5d.   Solved = %5d.  Fifo = %5d.  SAT runs = %3d.\n", 
            Vec_VecSizeSize(p->vSuppTargs), nSolved, Vec_PtrSize(p->vFifo), p->nSatRuns );
    }

exit:
p->timeTotal = Abc_Clock() - clk;
    vResult = p->vSuppFun;  
    //  p->vSuppFun = NULL;
    Sim_ManStop( p );
    return vResult;
}

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

  Synopsis    [Computes functional support using one round of simulation.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Sim_ComputeSuppRound( Sim_Man_t * p, int  fUseTargets )
{
    Vec_Ptr_t * vTargets;
    int i, Counter = 0;
    abctime clk;
    // perform one round of random simulation
clk = Abc_Clock();
    Sim_UtilSimulate( p, 0 );
p->timeSim += Abc_Clock() - clk;
    // iterate through the CIs and detect COs that depend on them
    for ( i = p->iInput; i < p->nInputs; i++ )
    {
        vTargets = (Vec_Ptr_t *)p->vSuppTargs->pArray[i];
        if ( fUseTargets && vTargets->nSize == 0 )
            continue;
        Counter += Sim_ComputeSuppRoundNode( p, i, fUseTargets );
    }
    return Counter;
}

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

  Synopsis    [Computes functional support for one node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Sim_ComputeSuppRoundNode( Sim_Man_t * p, int iNumCi, int  fUseTargets )
{
    int fVerbose = 0;
    Sim_Pat_t * pPat;
    Vec_Ptr_t * vTargets;
    Vec_Vec_t * vNodesByLevel;
    Abc_Obj_t * pNodeCi, * pNode;
    int i, k, v, Output, LuckyPat, fType0, fType1;
    int Counter = 0;
    int fFirst = 1;
    abctime clk;
    // collect nodes by level in the TFO of the CI 
    // this procedure does not collect the CIs and COs
    // but it increments TravId of the collected nodes and CIs/COs
clk = Abc_Clock();
    pNodeCi       = Abc_NtkCi( p->pNtk, iNumCi );
    vNodesByLevel = Abc_DfsLevelized( pNodeCi, 0 );
p->timeTrav += Abc_Clock() - clk;
    // complement the simulation info of the selected CI
    Sim_UtilInfoFlip( p, pNodeCi );
    // simulate the levelized structure of nodes
    Vec_VecForEachEntry( Abc_Obj_t *, vNodesByLevel, pNode, i, k )
    {
        fType0 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin0(pNode) );
        fType1 = Abc_NodeIsTravIdCurrent( Abc_ObjFanin1(pNode) );
clk = Abc_Clock();
        Sim_UtilSimulateNode( p, pNode, 1, fType0, fType1 );
p->timeSim += Abc_Clock() - clk;
    }
    // set the simulation info of the affected COs
    if ( fUseTargets )
    {
        vTargets = (Vec_Ptr_t *)p->vSuppTargs->pArray[iNumCi];
        for ( i = vTargets->nSize - 1; i >= 0; i-- )
        {
            // get the target output
            Output = (int)(ABC_PTRUINT_T)vTargets->pArray[i];
            // get the target node
            pNode  = Abc_ObjFanin0( Abc_NtkCo(p->pNtk, Output) );
            // the output should be in the cone
            assert( Abc_NodeIsTravIdCurrent(pNode) );

            // skip if the simulation info is equal
            if ( Sim_UtilInfoCompare( p, pNode ) )
                continue;

            // otherwise, we solved a new target
            Vec_PtrRemove( vTargets, vTargets->pArray[i] );
if ( fVerbose )
    printf( "(%d,%d) ", iNumCi, Output );
            Counter++;
            // make sure this variable is not yet detected
            assert( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) );
            // set this variable
            Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
            
            // detect the differences in the simulation info
            Sim_UtilInfoDetectDiffs( (unsigned *)p->vSim0->pArray[pNode->Id], (unsigned *)p->vSim1->pArray[pNode->Id], p->nSimWords, p->vDiffs );
            // create new patterns
            if ( !fFirst && p->vFifo->nSize > 1000 )
                continue;

            Vec_IntForEachEntry( p->vDiffs, LuckyPat, k )
            {
                // set the new pattern
                pPat = Sim_ManPatAlloc( p );
                pPat->Input  = iNumCi;
                pPat->Output = Output;
                Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
                    if ( Sim_SimInfoHasVar( p->vSim0, pNodeCi, LuckyPat ) )
                        Sim_SetBit( pPat->pData, v );
                Vec_PtrPush( p->vFifo, pPat );

                fFirst = 0;
                break;
            }
        }
if ( fVerbose && Counter )
printf( "\n" );
    }
    else
    {
        Abc_NtkForEachCo( p->pNtk, pNode, Output )
        {
            if ( !Abc_NodeIsTravIdCurrent( pNode ) )
                continue;
            if ( !Sim_UtilInfoCompare( p, Abc_ObjFanin0(pNode) ) )
            {
                if ( !Sim_SuppFunHasVar(p->vSuppFun, Output, iNumCi) )
                {
                    Counter++;
                    Sim_SuppFunSetVar( p->vSuppFun, Output, iNumCi );
                }
            }
        }
    }
    Vec_VecFree( vNodesByLevel );
    return Counter;
}

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

  Synopsis    [Sets the simulation targets.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Sim_ComputeSuppSetTargets( Sim_Man_t * p )
{
    Abc_Obj_t * pNode;
    unsigned * pSuppStr, * pSuppFun;
    int i, k, Num;
    Abc_NtkForEachCo( p->pNtk, pNode, i )
    {
        pSuppStr = (unsigned *)p->vSuppStr->pArray[pNode->Id];
        pSuppFun = (unsigned *)p->vSuppFun->pArray[i];
        // find vars in the structural support that are not in the functional support
        Sim_UtilInfoDetectNews( pSuppFun, pSuppStr, p->nSuppWords, p->vDiffs );
        Vec_IntForEachEntry( p->vDiffs, Num, k )
            Vec_VecPush( p->vSuppTargs, Num, (void *)(ABC_PTRUINT_T)i );
    }
}

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

  Synopsis    [Assigns random simulation info to the PIs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Sim_UtilAssignRandom( Sim_Man_t * p )
{
    Abc_Obj_t * pNode;
    unsigned * pSimInfo;
    int i, k;
    // assign the random/systematic simulation info to the PIs
    Abc_NtkForEachCi( p->pNtk, pNode, i )
    {
        pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id];
        for ( k = 0; k < p->nSimWords; k++ )
            pSimInfo[k] = SIM_RANDOM_UNSIGNED;
    }
}

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

  Synopsis    [Sets the new patterns from fifo.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Sim_UtilAssignFromFifo( Sim_Man_t * p )
{
    int fUseOneWord = 0;
    Abc_Obj_t * pNode;
    Sim_Pat_t * pPat;
    unsigned * pSimInfo;
    int nWordsNew, iWord, iWordLim, i, w;
    int iBeg, iEnd;
    int Counter = 0;
    // go through the patterns and fill in the dist-1 minterms for each
    for ( iWord = 0; p->vFifo->nSize > 0; iWord = iWordLim )
    {
        ++Counter;
        // get the pattern
        pPat = (Sim_Pat_t *)Vec_PtrPop( p->vFifo );
        if ( fUseOneWord )
        {
            // get the first word of the next series
            iWordLim = iWord + 1; 
            // set the pattern for all PIs from iBit to iWord + p->nInputs
            iBeg = p->iInput;
            iEnd = Abc_MinInt( iBeg + 32, p->nInputs );
//            for ( i = iBeg; i < iEnd; i++ )
            Abc_NtkForEachCi( p->pNtk, pNode, i )
            {
                pNode = Abc_NtkCi(p->pNtk,i);
                pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id];
                if ( Sim_HasBit(pPat->pData, i) )
                    pSimInfo[iWord] = SIM_MASK_FULL;
                else
                    pSimInfo[iWord] = 0;
                // flip one bit
                if ( i >= iBeg && i < iEnd )
                    Sim_XorBit( pSimInfo + iWord, i-iBeg );
            }
        }
        else
        {
            // get the number of words for the remaining inputs
            nWordsNew = p->nSuppWords;
//            nWordsNew = SIM_NUM_WORDS( p->nInputs - p->iInput );
            // get the first word of the next series
            iWordLim = (iWord + nWordsNew < p->nSimWords)? iWord + nWordsNew : p->nSimWords; 
            // set the pattern for all CIs from iWord to iWord + nWordsNew
            Abc_NtkForEachCi( p->pNtk, pNode, i )
            {
                pSimInfo = (unsigned *)p->vSim0->pArray[pNode->Id];
                if ( Sim_HasBit(pPat->pData, i) )
                {
                    for ( w = iWord; w < iWordLim; w++ )
                        pSimInfo[w] = SIM_MASK_FULL;
                }
                else
                {
                    for ( w = iWord; w < iWordLim; w++ )
                        pSimInfo[w] = 0;
                }
                Sim_XorBit( pSimInfo + iWord, i );
                // flip one bit
//                if ( i >= p->iInput )
//                    Sim_XorBit( pSimInfo + iWord, i-p->iInput );
            }
        }
        Sim_ManPatFree( p, pPat );
        // stop if we ran out of room for patterns
        if ( iWordLim == p->nSimWords )
            break;
//        if ( Counter == 1 )
//            break;
    }
}

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

  Synopsis    [Get the given number of counter-examples using SAT.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
{
    Fraig_Params_t Params;
    Fraig_Man_t * pMan;
    Abc_Obj_t * pNodeCi;
    Abc_Ntk_t * pMiter;
    Sim_Pat_t * pPat;
    void * pEntry;
    int * pModel;
    int RetValue, Output, Input, k, v;
    int Counter = 0;
    abctime clk;

    p->nSatRuns = 0;
    // put targets into one array
    Vec_VecForEachEntryReverse( void *, p->vSuppTargs, pEntry, Input, k )
    {
        p->nSatRuns++;
        Output = (int)(ABC_PTRUINT_T)pEntry;

        // set up the miter for the two cofactors of this output w.r.t. this input
        pMiter = Abc_NtkMiterForCofactors( p->pNtk, Output, Input, -1 );

        // transform the miter into a fraig
        Fraig_ParamsSetDefault( &Params );
        Params.nSeconds = ABC_INFINITY;
        Params.fInternal = 1;
clk = Abc_Clock();
        pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
p->timeFraig += Abc_Clock() - clk;
clk = Abc_Clock();
        Fraig_ManProveMiter( pMan );
p->timeSat += Abc_Clock() - clk;

        // analyze the result
        RetValue = Fraig_ManCheckMiter( pMan );
        assert( RetValue >= 0 );
        if ( RetValue == 1 ) // unsat
        {
            p->nSatRunsUnsat++;
            pModel = NULL;
            Vec_PtrRemove( (Vec_Ptr_t *)p->vSuppTargs->pArray[Input], pEntry );
        }
        else // sat
        {
            p->nSatRunsSat++;
            pModel = Fraig_ManReadModel( pMan );
            assert( pModel != NULL );
            assert( Sim_SolveSuppModelVerify( p->pNtk, pModel, Input, Output ) );

//printf( "Solved by SAT (%d,%d).\n", Input, Output );
            // set the new pattern
            pPat = Sim_ManPatAlloc( p );
            pPat->Input  = Input;
            pPat->Output = Output;
            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
                if ( pModel[v] )
                    Sim_SetBit( pPat->pData, v );
            Vec_PtrPush( p->vFifo, pPat );
/*
            // set the new pattern
            pPat = Sim_ManPatAlloc( p );
            pPat->Input  = Input;
            pPat->Output = Output;
            Abc_NtkForEachCi( p->pNtk, pNodeCi, v )
                if ( pModel[v] )
                    Sim_SetBit( pPat->pData, v );
            Sim_XorBit( pPat->pData, Input );  // add this bit in the opposite polarity
            Vec_PtrPush( p->vFifo, pPat );
*/
            Counter++;
        }
        // delete the fraig manager
        Fraig_ManFree( pMan );
        // delete the miter
        Abc_NtkDelete( pMiter );

        // makr the input, which we are processing
        p->iInput = Input;

        // stop when we found enough patterns
//        if ( Counter == Limit )
        if ( Counter == 1 )
            return;
    }
}


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

  Synopsis    [Saves the counter example.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Sim_NtkSimTwoPats_rec( Abc_Obj_t * pNode )
{
    int Value0, Value1;
    if ( Abc_NodeIsTravIdCurrent( pNode ) )
        return (int)(ABC_PTRUINT_T)pNode->pCopy;
    Abc_NodeSetTravIdCurrent( pNode );
    Value0 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin0(pNode) );
    Value1 = Sim_NtkSimTwoPats_rec( Abc_ObjFanin1(pNode) );
    if ( Abc_ObjFaninC0(pNode) )
        Value0 = ~Value0;
    if ( Abc_ObjFaninC1(pNode) )
        Value1 = ~Value1;
    pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)(Value0 & Value1);
    return Value0 & Value1;
}

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

  Synopsis    [Verifies that pModel proves the presence of Input in the support of Output.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output )
{
    Abc_Obj_t * pNode;
    int RetValue, i;
    // set the PI values
    Abc_NtkIncrementTravId( pNtk );
    Abc_NtkForEachCi( pNtk, pNode, i )
    {
        Abc_NodeSetTravIdCurrent( pNode );
        if ( pNode == Abc_NtkCi(pNtk,Input) )
            pNode->pCopy = (Abc_Obj_t *)1;
        else if ( pModel[i] == 1 )
            pNode->pCopy = (Abc_Obj_t *)3;
        else
            pNode->pCopy = NULL;
    }
    // perform the traversal
    RetValue = 3 & Sim_NtkSimTwoPats_rec( Abc_ObjFanin0( Abc_NtkCo(pNtk,Output) ) );
//    assert( RetValue == 1 || RetValue == 2 ); 
    return RetValue == 1 || RetValue == 2;
}

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


ABC_NAMESPACE_IMPL_END