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

  FileName    [sscCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [SAT sweeping under constraints.]

  Synopsis    [The core procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 29, 2008.]

  Revision    [$Id: sscCore.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]

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

#include "sscInt.h"
#include "proof/cec/cec.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [This procedure sets default parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssc_ManSetDefaultParams( Ssc_Pars_t * p )
{
    memset( p, 0, sizeof(Ssc_Pars_t) );
    p->nWords         =     1;  // the number of simulation words
    p->nBTLimit       =  1000;  // conflict limit at a node
    p->nSatVarMax     =  5000;  // the max number of SAT variables
    p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
    p->fVerbose       =     0;  // verbose stats
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ssc_ManStop( Ssc_Man_t * p )
{
    Vec_IntFreeP( &p->vFront );
    Vec_IntFreeP( &p->vFanins );
    Vec_IntFreeP( &p->vPattern );
    Vec_IntFreeP( &p->vDisPairs );
    Vec_IntFreeP( &p->vPivot );
    Vec_IntFreeP( &p->vId2Var );
    Vec_IntFreeP( &p->vVar2Id );
    if ( p->pSat ) sat_solver_delete( p->pSat );
    Gia_ManStopP( &p->pFraig );
    ABC_FREE( p );
}
Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
{
    Ssc_Man_t * p;
    p = ABC_CALLOC( Ssc_Man_t, 1 );
    p->pPars  = pPars;
    p->pAig   = pAig;
    p->pCare  = pCare;
    p->pFraig = Gia_ManDupDfs( p->pCare );
    assert( p->pFraig->pHTable == NULL );
    assert( !Gia_ManHasDangling(p->pFraig) );
    Gia_ManInvertPos( p->pFraig );
    Ssc_ManStartSolver( p );
    if ( p->pSat == NULL )
    {
        printf( "Constraints are UNSAT after propagation.\n" );
        Ssc_ManStop( p );
        return (Ssc_Man_t *)(ABC_PTRINT_T)1;
    }
//    p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
//    Vec_IntFreeP( &p->vPivot  );
    p->vPivot = Ssc_ManFindPivotSat( p );
    if ( p->vPivot == (Vec_Int_t *)(ABC_PTRINT_T)1 )
    {
        printf( "Constraints are UNSAT.\n" );
        Ssc_ManStop( p );
        return (Ssc_Man_t *)(ABC_PTRINT_T)1;
    }
    if ( p->vPivot == NULL )
    {
        printf( "Conflict limit is reached while trying to find one SAT assignment.\n" );
        Ssc_ManStop( p );
        return NULL;
    }
    sat_solver_bookmark( p->pSat );
//    Vec_IntPrint( p->vPivot );
    Gia_ManSetPhasePattern( p->pAig, p->vPivot );
    Gia_ManSetPhasePattern( p->pCare, p->vPivot );
    if ( Gia_ManCheckCoPhase(p->pCare) )
    {
        printf( "Computed reference pattern violates %d constraints (this is a bug!).\n", Gia_ManCheckCoPhase(p->pCare) );
        Ssc_ManStop( p );
        return NULL;
    }
    // other things
    p->vDisPairs = Vec_IntAlloc( 100 );
    p->vPattern = Vec_IntAlloc( 100 );
    p->vFanins = Vec_IntAlloc( 100 );
    p->vFront = Vec_IntAlloc( 100 );
    Ssc_GiaClassesInit( pAig );
    // now it is ready for refinement using simulation 
    return p;
}
void Ssc_ManPrintStats( Ssc_Man_t * p )
{
    Abc_Print( 1, "Parameters: SimWords = %d. SatConfs = %d. SatVarMax = %d. CallsRec = %d. Verbose = %d.\n",
        p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax, p->pPars->nCallsRecycle, p->pPars->fVerbose );
    Abc_Print( 1, "SAT calls : Total = %d. Proof = %d. Cex = %d. Undec = %d.\n",
        p->nSatCalls, p->nSatCallsUnsat, p->nSatCallsSat, p->nSatCallsUndec );
    Abc_Print( 1, "SAT solver: Vars = %d. Clauses = %d. Recycles = %d. Sim rounds = %d.\n",
        sat_solver_nvars(p->pSat), sat_solver_nclauses(p->pSat), p->nRecycles, p->nSimRounds );

    p->timeOther = p->timeTotal - p->timeSimInit - p->timeSimSat - p->timeCnfGen - p->timeSatSat - p->timeSatUnsat - p->timeSatUndec;
    ABC_PRTP( "Initialization ", p->timeSimInit,            p->timeTotal );
    ABC_PRTP( "SAT simulation ", p->timeSimSat,             p->timeTotal );
    ABC_PRTP( "CNF generation ", p->timeSimSat,             p->timeTotal );
    ABC_PRTP( "SAT solving    ", p->timeSat-p->timeCnfGen,  p->timeTotal );
    ABC_PRTP( "  unsat        ", p->timeSatUnsat,           p->timeTotal );
    ABC_PRTP( "  sat          ", p->timeSatSat,             p->timeTotal );
    ABC_PRTP( "  undecided    ", p->timeSatUndec,           p->timeTotal );
    ABC_PRTP( "Other          ", p->timeOther,              p->timeTotal );
    ABC_PRTP( "TOTAL          ", p->timeTotal,              p->timeTotal );
}

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

  Synopsis    [Refine one class by resimulating one pattern.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssc_GiaSimulatePatternFraig_rec( Ssc_Man_t * p, int iFraigObj )
{
    Gia_Obj_t * pObj;
    int Res0, Res1;
    if ( Ssc_ObjSatVar(p, iFraigObj) )
        return sat_solver_var_value( p->pSat, Ssc_ObjSatVar(p, iFraigObj) );
    pObj = Gia_ManObj( p->pFraig, iFraigObj );
    assert( Gia_ObjIsAnd(pObj) );
    Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId0(pObj, iFraigObj) );
    Res1 = Ssc_GiaSimulatePatternFraig_rec( p, Gia_ObjFaninId1(pObj, iFraigObj) );
    pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
    return pObj->fMark0;
}
int Ssc_GiaSimulatePattern_rec( Ssc_Man_t * p, Gia_Obj_t * pObj )
{
    int Res0, Res1;
    if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
        return pObj->fMark0;
    Gia_ObjSetTravIdCurrent(p->pAig, pObj);
    if ( ~pObj->Value )  // mapping into FRAIG exists - simulate FRAIG
    { 
        Res0 = Ssc_GiaSimulatePatternFraig_rec( p, Abc_Lit2Var(pObj->Value) );
        pObj->fMark0 = Res0 ^ Abc_LitIsCompl(pObj->Value);
    }
    else // mapping into FRAIG does not exist - simulate AIG
    {
        Res0 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin0(pObj) );
        Res1 = Ssc_GiaSimulatePattern_rec( p, Gia_ObjFanin1(pObj) );
        pObj->fMark0 = (Res0 ^ Gia_ObjFaninC0(pObj)) & (Res1 ^ Gia_ObjFaninC1(pObj));
    }
    return pObj->fMark0;
}
int Ssc_GiaResimulateOneClass( Ssc_Man_t * p, int iRepr, int iObj )
{
    int Ent, RetValue;
    assert( iRepr == Gia_ObjRepr(p->pAig, iObj) );
    assert( Gia_ObjIsHead( p->pAig, iRepr ) );
    // set bit-values at the nodes according to the counter-example
    Gia_ManIncrementTravId( p->pAig );
    Gia_ClassForEachObj( p->pAig, iRepr, Ent )
        Ssc_GiaSimulatePattern_rec( p, Gia_ManObj(p->pAig, Ent) );
    // refine one class using these bit-values
    RetValue = Ssc_GiaSimClassRefineOneBit( p->pAig, iRepr );
    // check that the candidate equivalence is indeed refined
    assert( iRepr != Gia_ObjRepr(p->pAig, iObj) );
    return RetValue;
}

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

  Synopsis    [Perform verification of conditional sweeping.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Ssc_PerformVerification( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
{
    int Status;
    Cec_ParCec_t ParsCec, * pPars = &ParsCec;
    // derive the OR of constraint outputs
    Gia_Man_t * pCond = Gia_ManDupAndOr( pC, Gia_ManPoNum(p0), 1, 0 );
    // derive F = F & !OR(c0, c1, c2, ...)
    Gia_Man_t * p0c = Gia_ManMiter( p0, pCond, 0, 0, 0, 1, 0 );
    // derive F = F & !OR(c0, c1, c2, ...)
    Gia_Man_t * p1c = Gia_ManMiter( p1, pCond, 0, 0, 0, 1, 0 );
    // derive dual-output miter
    Gia_Man_t * pMiter = Gia_ManMiter( p0c, p1c, 0, 1, 0, 0, 0 );
    Gia_ManStop( p0c );
    Gia_ManStop( p1c );
    Gia_ManStop( pCond );
    // run equivalence checking
    Cec_ManCecSetDefaultParams( pPars );
    Status = Cec_ManVerify( pMiter, pPars );
    Gia_ManStop( pMiter );
    // report the results
    if ( Status == 1 )
        printf( "Verification succeeded.\n" );
    else if ( Status == 0 )
        printf( "Verification failed.\n" );
    else if ( Status == -1 )
        printf( "Verification undecided.\n" );
    else assert( 0 );
    return Status;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Ssc_PerformSweepingInt( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
{
    Ssc_Man_t * p;
    Gia_Man_t * pResult, * pTemp;
    Gia_Obj_t * pObj, * pRepr;
    abctime clk, clkTotal = Abc_Clock();
    int i, fCompl, nRefined, status;
clk = Abc_Clock();
    assert( Gia_ManRegNum(pCare) == 0 );
    assert( Gia_ManCiNum(pAig) == Gia_ManCiNum(pCare) );
    assert( Gia_ManIsNormalized(pAig) );
    assert( Gia_ManIsNormalized(pCare) );
    // reset random numbers
    Gia_ManRandom( 1 );
    // sweeping manager
    p = Ssc_ManStart( pAig, pCare, pPars );
    if ( p == (Ssc_Man_t *)(ABC_PTRINT_T)1 ) // UNSAT
        return Gia_ManDupZero( pAig );
    if ( p == NULL ) // timeout
        return Gia_ManDup( pAig );
    if ( p->pPars->fVerbose )
        printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 );
    // perform simulation 
    while ( 1 ) 
    {
        // simulate care set
        Ssc_GiaRandomPiPattern( p->pFraig, 5, NULL );
        Ssc_GiaSimRound( p->pFraig );
        // transfer care patterns to user's AIG
        if ( !Ssc_GiaTransferPiPattern( pAig, p->pFraig, p->vPivot ) )
            break;
        // simulate the main AIG
        Ssc_GiaSimRound( pAig );
        nRefined = Ssc_GiaClassesRefine( pAig );
        if ( pPars->fVerbose ) 
            Gia_ManEquivPrintClasses( pAig, 0, 0 );
        if ( nRefined <= Gia_ManCandNum(pAig) / 100 )
            break;
    }
p->timeSimInit += Abc_Clock() - clk;

    // prepare user's AIG
    Gia_ManFillValue(pAig);
    Gia_ManConst0(pAig)->Value = 0;
    Gia_ManForEachCi( pAig, pObj, i )
        pObj->Value = Gia_Obj2Lit( p->pFraig, Gia_ManCi(p->pFraig, i) );
//    Gia_ManLevelNum(pAig);
    // prepare swept AIG (should be done after starting SAT solver in Ssc_ManStart)
    Gia_ManHashStart( p->pFraig );
    // perform sweeping
    Ssc_GiaResetPiPattern( pAig, pPars->nWords );
    Ssc_GiaSavePiPattern( pAig, p->vPivot );
    Gia_ManForEachCand( pAig, pObj, i )
    {
        if ( pAig->iPatsPi == 64 * pPars->nWords )
        {
clk = Abc_Clock();
            Ssc_GiaSimRound( pAig );
            Ssc_GiaClassesRefine( pAig );
            if ( pPars->fVerbose ) 
                Gia_ManEquivPrintClasses( pAig, 0, 0 );
            Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
            Vec_IntClear( p->vDisPairs );
            // prepare next patterns
            Ssc_GiaResetPiPattern( pAig, pPars->nWords );
            Ssc_GiaSavePiPattern( pAig, p->vPivot );
p->timeSimSat += Abc_Clock() - clk;
//printf( "\n" );
        }
        if ( Gia_ObjIsAnd(pObj) )
            pObj->Value = Gia_ManHashAnd( p->pFraig, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        if ( !Gia_ObjHasRepr(pAig, i) )
            continue;
        pRepr = Gia_ObjReprObj(pAig, i);
        if ( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase ) )
        {
            Gia_ObjSetProved( pAig, i );
            continue;
        }
        assert( Abc_Lit2Var(pRepr->Value) != Abc_Lit2Var(pObj->Value) );
        fCompl = pRepr->fPhase ^ pObj->fPhase ^ Abc_LitIsCompl(pRepr->Value) ^ Abc_LitIsCompl(pObj->Value);

        // perform SAT call
clk = Abc_Clock();
        p->nSatCalls++;
        status = Ssc_ManCheckEquivalence( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl );
        if ( status == l_False )
        {
            p->nSatCallsUnsat++;
            pObj->Value = Abc_LitNotCond( pRepr->Value, pRepr->fPhase ^ pObj->fPhase );
            Gia_ObjSetProved( pAig, i );
        }
        else if ( status == l_True )
        {
            p->nSatCallsSat++;
            Ssc_GiaSavePiPattern( pAig, p->vPattern );
            Vec_IntPush( p->vDisPairs, Gia_ObjRepr(p->pAig, i) );
            Vec_IntPush( p->vDisPairs, i );
//            printf( "Try %2d and %2d: ", Gia_ObjRepr(p->pAig, i), i );
//            Vec_IntPrint( p->vPattern );
            if ( Gia_ObjRepr(p->pAig, i) > 0 )
                Ssc_GiaResimulateOneClass( p, Gia_ObjRepr(p->pAig, i), i );
        }
        else if ( status == l_Undef )
            p->nSatCallsUndec++;
        else assert( 0 );
p->timeSat += Abc_Clock() - clk;
    }
    if ( pAig->iPatsPi > 1 )
    {
clk = Abc_Clock();
        while ( pAig->iPatsPi < 64 * pPars->nWords )
            Ssc_GiaSavePiPattern( pAig, p->vPivot );
        Ssc_GiaSimRound( pAig );
        Ssc_GiaClassesRefine( pAig );
        if ( pPars->fVerbose ) 
            Gia_ManEquivPrintClasses( pAig, 0, 0 );
        Ssc_GiaClassesCheckPairs( pAig, p->vDisPairs );
        Vec_IntClear( p->vDisPairs );
p->timeSimSat += Abc_Clock() - clk;
    }
//    Gia_ManEquivPrintClasses( pAig, 1, 0 );
//    Gia_ManPrint( pAig );

    // generate the resulting AIG
    pResult = Gia_ManEquivReduce( pAig, 0, 0, 1, 0 );
    if ( pResult == NULL )
    {
        printf( "There is no equivalences.\n" );
        ABC_FREE( pAig->pReprs );
        ABC_FREE( pAig->pNexts );
        pResult = Gia_ManDup( pAig );
    }
    pResult = Gia_ManCleanup( pTemp = pResult );
    Gia_ManStop( pTemp );
    p->timeTotal = Abc_Clock() - clkTotal;
    if ( pPars->fVerbose )
        Ssc_ManPrintStats( p );
    Ssc_ManStop( p );
    // count the number of representatives
    if ( pPars->fVerbose ) 
    {
        Abc_Print( 1, "Reduction in AIG nodes:%8d  ->%8d (%6.2f %%).  ", 
            Gia_ManAndNum(pAig), Gia_ManAndNum(pResult), 
            100.0 - 100.0 * Gia_ManAndNum(pResult) / Gia_ManAndNum(pAig) );
        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
    }
    return pResult;
}
Gia_Man_t * Ssc_PerformSweeping( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPars )
{
    Gia_Man_t * pResult = Ssc_PerformSweepingInt( pAig, pCare, pPars );
    if ( pPars->fVerify )
        Ssc_PerformVerification( pAig, pResult, pCare );
    return pResult;
}
Gia_Man_t * Ssc_PerformSweepingConstr( Gia_Man_t * p, Ssc_Pars_t * pPars )
{
    Gia_Man_t * pAig, * pCare, * pResult;
    int i;
    if ( pPars->fVerbose )
        Abc_Print( 0, "SAT sweeping AIG with %d constraints.\n", p->nConstrs );
    if ( p->nConstrs == 0 )
    {
        pAig = Gia_ManDup( p );
        pCare = Gia_ManStart( Gia_ManCiNum(p) + 2 );
        pCare->pName = Abc_UtilStrsav( "care" );
        for ( i = 0; i < Gia_ManCiNum(p); i++ )
            Gia_ManAppendCi( pCare );
        Gia_ManAppendCo( pCare, 0 );
    }
    else
    {
        Vec_Int_t * vOuts = Vec_IntStartNatural( Gia_ManPoNum(p) );
        pAig = Gia_ManDupCones( p, Vec_IntArray(vOuts), Gia_ManPoNum(p) - p->nConstrs, 0 );
        pCare = Gia_ManDupCones( p, Vec_IntArray(vOuts) + Gia_ManPoNum(p) - p->nConstrs, p->nConstrs, 0 );
        Vec_IntFree( vOuts );
    }
    if ( pPars->fVerbose )
    {
        printf( "User AIG: " );
        Gia_ManPrintStats( pAig, NULL );
        printf( "Care AIG: " );
        Gia_ManPrintStats( pCare, NULL );
    }

    pAig = Gia_ManDupLevelized( pResult = pAig );
    Gia_ManStop( pResult );
    pResult = Ssc_PerformSweeping( pAig, pCare, pPars );
    if ( pPars->fAppend )
    {
        Gia_ManDupAppendShare( pResult, pCare );
        pResult->nConstrs = Gia_ManPoNum(pCare);
    }
    Gia_ManStop( pAig );
    Gia_ManStop( pCare );
    return pResult;
}

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


ABC_NAMESPACE_IMPL_END