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

  FileName    [int2Core.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Interpolation engine.]

  Synopsis    [Core procedures.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - Dec 1, 2013.]

  Revision    [$Id: int2Core.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]

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

#include "int2Int.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    [This procedure sets default values of interpolation parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Int2_ManSetDefaultParams( Int2_ManPars_t * p )
{ 
    memset( p, 0, sizeof(Int2_ManPars_t) );
    p->nBTLimit      =  0;     // limit on the number of conflicts
    p->nFramesS      =  1;     // the starting number timeframes
    p->nFramesMax    =  0;     // the max number timeframes to unroll
    p->nSecLimit     =  0;     // time limit in seconds
    p->nFramesK      =  1;     // the number of timeframes to use in induction
    p->fRewrite      =  0;     // use additional rewriting to simplify timeframes
    p->fTransLoop    =  0;     // add transition into the init state under new PI var
    p->fDropInvar    =  0;     // dump inductive invariant into file
    p->fVerbose      =  0;     // print verbose statistics
    p->iFrameMax     = -1;
}
/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Gia_Man_t * Int2_ManUnroll( Gia_Man_t * p, int nFrames )
{
    Gia_Man_t * pFrames, * pTemp;
    Gia_Obj_t * pObj;
    int i, f;
    assert( Gia_ManRegNum(pAig) > 0 );
    pFrames = Gia_ManStart( Gia_ManObjNum(pAig) );
    pFrames->pName = Abc_UtilStrsav( pAig->pName );
    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
    Gia_ManHashAlloc( pFrames );
    Gia_ManConst0(pAig)->Value = 0;
    for ( f = 0; f < nFrames; f++ )
    {
        Gia_ManForEachRo( pAig, pObj, i )
            pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0;
        Gia_ManForEachPi( pAig, pObj, i )
            pObj->Value = Gia_ManAppendCi( pFrames );
        Gia_ManForEachAnd( pAig, pObj, i )
            pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
        Gia_ManForEachRi( pAig, pObj, i )
            pObj->Value = Gia_ObjFanin0Copy(pObj);
    }
    Gia_ManForEachRi( pAig, pObj, i )
        Gia_ManAppendCo( pFrames, pObj->Value );
    Gia_ManHashStop( pFrames );
    pFrames = Gia_ManCleanup( pTemp = pFrames );
    Gia_ManStop( pTemp );
    return pFrames;
}
sat_solver * Int2_ManPreparePrefix( Gia_Man_t * p, int f, Vec_Int_t ** pvCiMap )
{
    Gia_Man_t * pPref, * pNew;
    sat_solver * pSat;
    // create subset of the timeframe
    pPref = Int2_ManUnroll( p, f );
    // create SAT solver
    pNew = Jf_ManDeriveCnf( pPref, 0 );  
    pCnf = (Cnf_Dat_t *)pPref->pData; pPref->pData = NULL;
    Gia_ManStop( pPref );
    // derive the SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // collect indexes of CO variables
    *pvCiMap = Vec_IntAlloc( 100 );
    Gia_ManForEachPo( pNew, pObj, i )     
        Vec_IntPush( *pvCiMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
    // cleanup
    Cnf_DataFree( pCnf );
    Gia_ManStop( pNew );
    return pSat;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
sat_solver * Int2_ManPrepareSuffix( Gia_Man_t * p, Vec_Int_t * vImageOne, Vec_Int_t * vImagesAll, Vec_Int_t ** pvCoMap, Gia_Man_t ** ppSuff )
{
    Gia_Man_t * pSuff, * pNew;
    Gia_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Vec_Int_t * vLits;
    int i, Lit, Limit;
    // create subset of the timeframe
    pSuff = Int2_ManProbToGia( p, vImageOne );
    assert( Gia_ManPiNum(pSuff) == Gia_ManCiNum(p) );
    // create SAT solver
    pNew = Jf_ManDeriveCnf( pSuff, 0 );  
    pCnf = (Cnf_Dat_t *)pSuff->pData; pSuff->pData = NULL;
    Gia_ManStop( pSuff );
    // derive the SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    // create new constraints
    vLits = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntryStart( vImagesAll, Limit, i, 1 )
    {
        Vec_IntClear( vLits );
        for ( k = 0; k < Limit; k++ )
        {
            i++;
            Lit = Vec_IntEntry( vSop, i + k );
            Vec_IntPush( vLits, Abc_LitNot(Lit) );
        }
        if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) )  )  // UNSAT
        {
            Vec_IntFree( vLits );
            Cnf_DataFree( pCnf );
            Gia_ManStop( pNew );
            *pvCoMap = NULL;
            return NULL;
        }
    }
    Vec_IntFree( vLits );
    // collect indexes of CO variables
    *pvCoMap = Vec_IntAlloc( 100 );
    Gia_ManForEachRo( p, pObj, i )     
    {
        pObj = Gia_ManPi( pNew, i + Gia_ManPiNum(p) );
        Vec_IntPush( *pvCoMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
    }
    // cleanup
    Cnf_DataFree( pCnf );
    if ( ppSuff )
        *ppSuff = pNew;
    else
        Gia_ManStop( pNew );
    return pSat;
}

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

  Synopsis    [Returns the cube cover and status.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Int2_ManComputePreimage( Gia_Man_t * pSuff, sat_solver * pSatPref, sat_solver * pSatSuff, Vec_Int_t * vCiMap, Vec_Int_t * vCoMap, Vec_Int_t * vPrio )
{
    int i, iVar, status;
    Vec_IntClear( p->vImage );
    while ( 1 )
    {
        // run suffix solver
        status = sat_solver_solve( p->pSatSuff, NULL, NULL, 0, 0, 0, 0 );
        if ( status == l_Undef )
            return NULL; // timeout
        if ( status == l_False )
            return INT2_COMPUTED;
        assert( status == l_True );
        // collect assignment
        Vec_IntClear( p->vAssign );
        Vec_IntForEachEntry( p->vCiMap, iVar, i )
            Vec_IntPush( p->vAssign, sat_solver_var_value(p->pSatSuff, iVar) );
        // derive initial cube
        vCube = Int2_ManRefineCube( p->pSuff, p->vAssign, p->vPrio );
        // expend the cube using prefix
        status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
        if ( status == l_False )
        {
            int k, nCoreLits, * pCoreLits;
            nCoreLits = sat_solver_final( p->pSatPref, &pCoreLits );
            // create cube
            Vec_IntClear( vCube );
            Vec_IntPush( vImage, nCoreLits );
            for ( k = 0; k < nCoreLits; k++ )
            {
                Vec_IntPush( vCube, pCoreLits[k] );
                Vec_IntPush( vImage, pCoreLits[k] );
            }
            // add cube to the solver
            if ( !sat_solver_addclause( p->pSatSuff, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube) ) )
            {
                Vec_IntFree( vCube );
                return INT2_COMPUTED;
            }
        }
        Vec_IntFree( vCube );
        if ( status == l_Undef )
            return INT2_TIME_OUT;
        if ( status == l_True )
            return INT2_FALSE_NEG;
        assert( status == l_False );
        continue;
    }
    return p->vImage;
}

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

  Synopsis    [Interpolates while the number of conflicts is not exceeded.]

  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
               
  SideEffects [Does not check the property in 0-th frame.]

  SeeAlso     []

***********************************************************************/
int Int2_ManPerformInterpolation( Gia_Man_t * pInit, Int2_ManPars_t * pPars )
{
    Int2_Man_t * p;
    int f, i, RetValue = -1;
    abctime clk, clkTotal = Abc_Clock(), timeTemp = 0;
    abctime nTimeToStop = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;

    // sanity checks
    assert( Gia_ManPiNum(pInit) > 0 );
    assert( Gia_ManPoNum(pInit) > 0 );
    assert( Gia_ManRegNum(pInit) > 0 );

    // create manager
    p = Int2_ManCreate( pInit, pPars );

    // create SAT solver
    p->pSatPref = sat_solver_new();
    sat_solver_setnvars( p->pSatPref, 1000 );
    sat_solver_set_runtime_limit( p->pSatPref, nTimeToStop );

    // check outputs in the first frame
    for ( i = 0; i < Gia_ManPoNum(pInit); i++ )
        Vec_IntPush( p->vPrefCos, i );
    Int2_ManCreateFrames( p, 0, p->vPrefCos );
    RetValue = Int2_ManCheckBmc( p, NULL );
    if ( RetValue != 1 )
        return RetValue;

    // create original image
    for ( f = pPars->nFramesS; f < p->nFramesMax; f++ )
    {
        for ( i = 0; i < p->nFramesMax; i++ )
        {
            p->pSatSuff = Int2_ManPrepareSuffix( p, vImageOne. vImagesAll, &vCoMap, &pGiaSuff );
            sat_solver_set_runtime_limit( p->pSatSuff, nTimeToStop );
            Vec_IntFreeP( &vImageOne );
            vImageOne = Int2_ManComputePreimage( pGiaSuff, p->pSatPref, p->pSatSuff, vCiMap, vCoMap );
            Vec_IntFree( vCoMap );
            Gia_ManStop( pGiaSuff );
            if ( nTimeToStop && Abc_Clock() > nTimeToStop )
                return -1;
            if ( vImageOne == NULL )
            {
                if ( i == 0 )
                {
                    printf( "Satisfiable in frame %d.\n", f );
                    Vec_IntFree( vCiMap );
                    sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
                    return 0;
                }
                f += i;
                break;
            }
            Vec_IntAppend( vImagesAll, vImageOne );
            sat_solver_delete( p->pSatSuff ); p->pSatSuff = NULL;
        }
        Vec_IntFree( vCiMap );
        sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
    }
    Abc_PrintTime( "Time", Abc_Clock() - clk );


p->timeSatPref += Abc_Clock() - clk;

    Int2_ManStop( p );
    return RetValue;
}



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


ABC_NAMESPACE_IMPL_END