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

  FileName    [bmcMulti.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [SAT-based bounded model checking.]

  Synopsis    [Proving multi-output properties.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "bmc.h"
#include "proof/ssw/ssw.h"
#include "misc/extra/extra.h"
#include "aig/gia/giaAig.h"
#include "aig/ioa/ioa.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [Divides outputs into solved and unsolved.]

  Description [Return array of unsolved outputs to extract into a new AIG.
  Updates the resulting CEXes (vCexesOut) and current output map (vOutMap).]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut, Vec_Int_t * vOutMap )
{
    Abc_Cex_t * pCex; 
    Vec_Int_t * vLeftOver;
    int i, iOut;
    assert( Vec_PtrSize(vCexesIn) == Vec_IntSize(vOutMap) );
    vLeftOver = Vec_IntAlloc( Vec_PtrSize(vCexesIn) );
    Vec_IntForEachEntry( vOutMap, iOut, i )
    {
        assert( Vec_PtrEntry(vCexesOut, iOut) == NULL );
        pCex = (Abc_Cex_t *)Vec_PtrEntry( vCexesIn, i );
        if ( pCex ) // found a CEX for output iOut
        {
            Vec_PtrWriteEntry( vCexesIn, i, NULL );
            Vec_PtrWriteEntry( vCexesOut, iOut, pCex );
        }
        else // still unsolved
        {
            Vec_IntWriteEntry( vOutMap, Vec_IntSize(vLeftOver), iOut );
            Vec_IntPush( vLeftOver, i );
        }
    }
    Vec_IntShrink( vOutMap, Vec_IntSize(vLeftOver) );
    return vLeftOver;
}

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

  Synopsis    [Counts the number of constant 0 POs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCountConst0PosGia( Gia_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i, Counter = 0;
    Gia_ManForEachPo( p, pObj, i )
        Counter += (Gia_ObjFaninLit0p(p, pObj) == 0);
    return Counter;
}
int Gia_ManCountConst0Pos( Aig_Man_t * p )
{
    Aig_Obj_t * pObj;
    int i, Counter = 0;
    Saig_ManForEachPo( p, pObj, i )
        Counter += (Aig_ObjChild0(pObj) == Aig_ManConst0(p));
    return Counter;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManMultiReport( Aig_Man_t * p, char * pStr, int nTotalPo, int nTotalSize, abctime clkStart )
{
    printf( "%3s : ", pStr );
    printf( "PI =%6d  ", Saig_ManPiNum(p) );
    printf( "PO =%6d  ", Saig_ManPoNum(p) );
    printf( "FF =%7d  ", Saig_ManRegNum(p) );
    printf( "ND =%7d  ", Aig_ManNodeNum(p) );
    printf( "Solved =%7d (%5.1f %%)  ", nTotalPo-Saig_ManPoNum(p), 100.0*(nTotalPo-Saig_ManPoNum(p))/Abc_MaxInt(1, nTotalPo) );
    printf( "Size   =%7d (%5.1f %%)  ", Aig_ManObjNum(p),          100.0*Aig_ManObjNum(p)/Abc_MaxInt(1, nTotalSize) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
{
    Aig_Man_t * pAig;
    Gia_Man_t * pGia, * pTemp;
    pGia = Gia_ManFromAig( p );
    pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0, 0 );
    Gia_ManStop( pTemp );
    pAig = Gia_ManToAig( pGia, 0 );
    Gia_ManStop( pGia );
    return pAig;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, Bmc_MulPar_t * pPars )
{
    Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
    Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
    Vec_Int_t * vOutMap, * vLeftOver;
    Vec_Ptr_t * vCexes;
    Aig_Man_t * pTemp;
    abctime clkStart = Abc_Clock();
    abctime nTimeToStop = pPars->TimeOutGlo ? Abc_Clock() + pPars->TimeOutGlo * CLOCKS_PER_SEC : 0;
    int nTotalPo     = Saig_ManPoNum(p);
    int nTotalSize   = Aig_ManObjNum(p);
    int TimeOutLoc   = pPars->TimeOutLoc;
    int i, RetValue  = -1;
    if ( pPars->fVerbose )
        printf( "MultiProve parameters: Global timeout = %d sec.  Local timeout = %d sec.  Time increase = %d %%.\n", 
            pPars->TimeOutGlo, pPars->TimeOutLoc, pPars->TimeOutInc );
    if ( pPars->fVerbose )
        printf( "Gap timout = %d sec. Per-output timeout = %d msec. Use synthesis = %d. Dump final = %d. Verbose = %d.\n", 
            pPars->TimeOutGap, pPars->TimePerOut, pPars->fUseSyn, pPars->fDumpFinal, pPars->fVerbose );
    // create output map
    vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
    vCexes  = Vec_PtrStart( Saig_ManPoNum(p) );        // maps solved outputs into their CEXes (or markers)
    for ( i = 0; i < 1000; i++ )
    {
        int nSolved = Vec_PtrCountZero(vCexes);
        // perform SIM3
        Ssw_RarSetDefaultParams( pParsSim );
        pParsSim->fSolveAll = 1;
        pParsSim->fNotVerbose = 1;
        pParsSim->fSilent = !pPars->fVeryVerbose;
        pParsSim->TimeOut = TimeOutLoc;
        pParsSim->nRandSeed = (i * 17) % 500;
        pParsSim->nWords = 5;
        RetValue *= Ssw_RarSimulate( p, pParsSim );
        // sort outputs
        if ( p->vSeqModelVec )
        {
            vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
            if ( Vec_IntSize(vLeftOver) == 0 )
                break;
            // remove solved        
            p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
            Vec_IntFree( vLeftOver );
            Aig_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
            Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );

        // check timeout
        if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
        {
            printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
            break;
        }

        // perform BMC
        Saig_ParBmcSetDefaultParams( pParsBmc );
        pParsBmc->fSolveAll = 1;
        pParsBmc->fNotVerbose = 1;
        pParsBmc->fSilent = !pPars->fVeryVerbose;
        pParsBmc->nTimeOut = TimeOutLoc;
        pParsBmc->nTimeOutOne = pPars->TimePerOut;
        RetValue *= Saig_ManBmcScalable( p, pParsBmc );
        if ( pPars->fVeryVerbose )
            Abc_Print( 1, "Some outputs are SAT (%d out of %d) after %d frames.\n", 
                Saig_ManPoNum(p) - Vec_PtrCountZero(p->vSeqModelVec), Saig_ManPoNum(p), pParsBmc->iFrame );
        // sort outputs
        if ( p->vSeqModelVec )
        {
            vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
            if ( Vec_IntSize(vLeftOver) == 0 )
                break;
            // remove solved        
            p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
            Vec_IntFree( vLeftOver );
            Aig_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
            Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );

        // check timeout
        if ( nTimeToStop && Abc_Clock() + TimeOutLoc * CLOCKS_PER_SEC > nTimeToStop )
        {
            printf( "Global timeout (%d sec) is reached.\n", pPars->TimeOutGlo );
            break;
        }

        // check gap timeout
        if ( pPars->TimeOutGap && pPars->TimeOutGap <= TimeOutLoc && nSolved == Vec_PtrCountZero(vCexes) )
        {
            printf( "Gap timeout (%d sec) is reached.\n", pPars->TimeOutGap );
            break;
        }

        // synthesize
        if ( pPars->fUseSyn )
        {
            p = Gia_ManMultiProveSyn( pTemp = p, pPars->fVerbose, pPars->fVeryVerbose );
            Aig_ManStop( pTemp );
            if ( pPars->fVerbose )
                Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
        }

        // increase timeout
        TimeOutLoc += TimeOutLoc * pPars->TimeOutInc / 100;
    }
    Vec_IntFree( vOutMap );
    if ( pPars->fVerbose )
        printf( "The number of POs proved UNSAT by synthesis = %d.\n", Gia_ManCountConst0Pos(p) );
    if ( pPars->fDumpFinal )
    {
        char * pFileName = Extra_FileNameGenericAppend( p->pName, "_out.aig" );
        Ioa_WriteAiger( p, pFileName, 0, 0 );
        printf( "Final AIG was dumped into file \"%s\".\n", pFileName );
    }
    Aig_ManStop( p );
    return vCexes;
}
int Gia_ManMultiProve( Gia_Man_t * p, Bmc_MulPar_t * pPars )
{
    Aig_Man_t * pAig;
    if ( p->vSeqModelVec )
        Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
    pAig = Gia_ManToAig( p, 0 );
    p->vSeqModelVec = Gia_ManMultiProveAig( pAig, pPars ); // deletes pAig
    assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
    return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
}

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


ABC_NAMESPACE_IMPL_END