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

  FileName    [giaCCof.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    [Backward reachability using circuit cofactoring.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "gia.h"
#include "sat/bsat/satSolver.h"

ABC_NAMESPACE_IMPL_START


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

typedef struct Ccf_Man_t_ Ccf_Man_t; // manager
struct Ccf_Man_t_
{
    // user data
    Gia_Man_t *  pGia;       // single-output AIG manager
    int          nFrameMax;  // maximum number of frames
    int          nConfMax;   // maximum number of conflicts
    int          nTimeMax;   // maximum runtime in seconds
    int          fVerbose;   // verbose flag
    // internal data
    void *       pUnr;       // unrolling manager
    Gia_Man_t *  pFrames;    // unrolled timeframes
    Vec_Int_t *  vCopies;    // copy pointers of the AIG
    sat_solver * pSat;       // SAT solver
};

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

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

  Synopsis    [Create manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Ccf_Man_t * Ccf_ManStart( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose )
{
    static Gia_ParFra_t Pars, * pPars = &Pars;
    Ccf_Man_t * p;
    assert( nFrameMax > 0 );
    p = ABC_CALLOC( Ccf_Man_t, 1 );
    p->pGia      = pGia;
    p->nFrameMax = nFrameMax;    
    p->nConfMax  = nConfMax;
    p->nTimeMax  = nTimeMax;
    p->fVerbose  = fVerbose;
    // create unrolling manager
    memset( pPars, 0, sizeof(Gia_ParFra_t) );
    pPars->fVerbose     = fVerbose;
    pPars->nFrames      = nFrameMax;
    pPars->fSaveLastLit = 1;
    p->pUnr = Gia_ManUnrollStart( pGia, pPars );
    p->vCopies = Vec_IntAlloc( 1000 );
    // internal data
    p->pSat = sat_solver_new();
//    sat_solver_setnvars( p->pSat, 10000 );
    return p;
}

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

  Synopsis    [Delete manager.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Ccf_ManStop( Ccf_Man_t * p )
{
    Vec_IntFree( p->vCopies );
    Gia_ManUnrollStop( p->pUnr );
    sat_solver_delete( p->pSat );
    Gia_ManStopP( &p->pFrames );
    ABC_FREE( p );
}


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

  Synopsis    [Extends the solver.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManCofExtendSolver( Ccf_Man_t * p )
{
    Gia_Obj_t * pObj;
    int i;
    // add SAT clauses
    for ( i = sat_solver_nvars(p->pSat); i < Gia_ManObjNum(p->pFrames); i++ )
    {
        pObj = Gia_ManObj( p->pFrames, i );
        if ( Gia_ObjIsAnd(pObj) )
            sat_solver_add_and( p->pSat, i, 
                Gia_ObjFaninId0(pObj, i), 
                Gia_ObjFaninId1(pObj, i), 
                Gia_ObjFaninC0(pObj), 
                Gia_ObjFaninC1(pObj), 0 ); 
    }
    sat_solver_setnvars( p->pSat, Gia_ManObjNum(p->pFrames) );
}

static inline int Gia_Obj0Copy( Vec_Int_t * vCopies, int Fan0, int fCompl0 )  
{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); }

static inline int Gia_Obj1Copy( Vec_Int_t * vCopies, int Fan1, int fCompl1 )  
{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); }
 
/**Function*************************************************************

  Synopsis    [Cofactor the circuit w.r.t. the given assignment.]

  Description [Assumes that the solver has just returned SAT.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Gia_ManCofOneDerive_rec( Ccf_Man_t * p, int Id )
{
    Gia_Obj_t * pObj;
    int Res;
    if ( Vec_IntEntry(p->vCopies, Id) != -1 )
        return;
    pObj = Gia_ManObj(p->pFrames, Id);
    assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
    if ( Gia_ObjIsAnd(pObj) )
    {
        int fCompl0 = Gia_ObjFaninC0(pObj);
        int fCompl1 = Gia_ObjFaninC1(pObj);
        int Fan0 = Gia_ObjFaninId0p(p->pFrames, pObj);
        int Fan1 = Gia_ObjFaninId1p(p->pFrames, pObj);
        Gia_ManCofOneDerive_rec( p, Fan0 );
        Gia_ManCofOneDerive_rec( p, Fan1 );
        Res = Gia_ManHashAnd( p->pFrames, 
            Gia_Obj0Copy(p->vCopies, Fan0, fCompl0), 
            Gia_Obj1Copy(p->vCopies, Fan1, fCompl1) );
    }
    else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI
        Res = sat_solver_var_value( p->pSat, Id );
    else
        Res = Abc_Var2Lit( Id, 0 );
    Vec_IntWriteEntry( p->vCopies, Id, Res );
}

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

  Synopsis    [Cofactor the circuit w.r.t. the given assignment.]

  Description [Assumes that the solver has just returned SAT.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
{
    int LitOut;
    // derive the cofactor of the property node
    Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 );
    Gia_ManCofOneDerive_rec( p, Abc_Lit2Var(LitProp) );
    LitOut = Vec_IntEntry( p->vCopies, Abc_Lit2Var(LitProp) );
    LitOut = Abc_LitNotCond( LitOut, Abc_LitIsCompl(LitProp) );
    // add new PO for the cofactor
    Gia_ManAppendCo( p->pFrames, LitOut );
    // add SAT clauses
    Gia_ManCofExtendSolver( p );
    // return negative literal of the cofactor
    return Abc_LitNot(LitOut);
} 

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

  Synopsis    [Enumerates backward reachable states.]

  Description [Return -1 if resource limit is reached. Returns 1 
  if computation converged (there is no more reachable states).
  Returns 0 if no more states to enumerate.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
{
    int ObjPrev = 0, ConfPrev = 0;
    int Count = 0, LitOut, RetValue;
    abctime clk;
    // try solving for the first time and quit if converged
    RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
    if ( RetValue == l_False )
        return 1;
    // iterate circuit cofactoring
    while ( RetValue == l_True )
    {
        clk = Abc_Clock();
        // derive cofactor
        LitOut = Gia_ManCofOneDerive( p, Lit );
        // add the blocking clause
        RetValue = sat_solver_addclause( p->pSat, &LitOut, &LitOut + 1 );
        assert( RetValue );
        // try solving again
        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
        // derive cofactors
        if ( p->fVerbose ) 
        {
            printf( "%3d : AIG =%7d  Conf =%7d.  ", Count++, 
                Gia_ManObjNum(p->pFrames) - ObjPrev, sat_solver_nconflicts(p->pSat) - ConfPrev );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            ObjPrev = Gia_ManObjNum(p->pFrames);
            ConfPrev = sat_solver_nconflicts(p->pSat);
        }
    }
    if ( RetValue == l_Undef )
        return -1;
    return 0;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose )
{ 
    Gia_Man_t * pNew;
    Ccf_Man_t * p;
    Gia_Obj_t * pObj;
    int f, i, Lit, RetValue = -1, fFailed = 0;
    abctime nTimeToStop = Abc_Clock() + nTimeMax * CLOCKS_PER_SEC;
    abctime clk = Abc_Clock();
    assert( Gia_ManPoNum(pGia) == 1 );

    // create reachability manager
    p = Ccf_ManStart( pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );

    // set runtime limit
    if ( nTimeMax )
        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );

    // perform backward image computation
    for ( f = 0; f < nFrameMax; f++ )
    {
        if ( fVerbose ) 
            printf( "ITER %3d :\n", f );
        // add to the mapping of nodes
        p->pFrames = (Gia_Man_t *)Gia_ManUnrollAdd( p->pUnr, f+1 );
        // add SAT clauses
        Gia_ManCofExtendSolver( p );
        // return output literal
        Lit = Gia_ManUnrollLastLit( p->pUnr );
        // derives cofactors of the property literal till all states are blocked
        RetValue = Gia_ManCofGetReachable( p, Lit );
        if ( RetValue )
            break;

        // check the property output
        Gia_ManSetPhase( p->pFrames );
        Gia_ManForEachPo( p->pFrames, pObj, i )
            if ( pObj->fPhase )
            {
                printf( "Property failed in frame %d.\n", f );
                fFailed = 1;
                break;
            }
        if ( i < Gia_ManPoNum(p->pFrames) )
            break;
    }

    // report the result
    if ( nTimeToStop && Abc_Clock() > nTimeToStop )
        printf( "Runtime limit (%d sec) is reached after %d frames.  ", nTimeMax, f );
    else if ( f == nFrameMax )
        printf( "Completed %d frames without converging.  ", f );
    else if ( RetValue == 1 )
        printf( "Backward reachability converged after %d iterations.  ", f-1 );
    else if ( RetValue == -1 )
        printf( "Conflict limit or timeout is reached after %d frames.  ", f-1 );
    Abc_PrintTime( 1, "Runtime", Abc_Clock() - clk );

    if ( !fFailed && RetValue == 1 )
        printf( "Property holds.\n" );
    else if ( !fFailed )
        printf( "Property is undecided.\n" );

    // get the resulting AIG manager
    Gia_ManHashStop( p->pFrames );
    pNew = p->pFrames;  p->pFrames = NULL;
    Ccf_ManStop( p );

    // cleanup
//    if ( fVerbose )
//        Gia_ManPrintStats( pNew, 0 );
    pNew = Gia_ManCleanup( pGia = pNew );
    Gia_ManStop( pGia );
//    if ( fVerbose )
//        Gia_ManPrintStats( pNew, 0 );
    return pNew;   
}

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


ABC_NAMESPACE_IMPL_END