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

  FileName    [giaSatEdge.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Scalable AIG package.]

  Synopsis    []

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "gia.h"
#include "misc/tim/tim.h"
#include "sat/bsat/satStore.h"

ABC_NAMESPACE_IMPL_START


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

typedef struct Seg_Man_t_ Seg_Man_t;
struct Seg_Man_t_
{
    sat_solver *   pSat;         // SAT solver
    //Vec_Int_t *    vCardVars;    // candinality variables
    int            nVars;        // max vars (edge num)
    int            LogN;         // base-2 log of max vars
    int            Power2;       // power-2 of LogN
    int            FirstVar;     // first variable to be used
    // parameters
    int            nBTLimit;     // conflicts
    int            DelayMax;     // external delay
    int            nEdges;       // the number of edges
    int            fDelay;       // delay mode
    int            fReverse;     // reverse windowing
    int            fVerbose;     // verbose
    // window
    Gia_Man_t *    pGia;
    Vec_Int_t *    vPolars;      // polarity
    Vec_Int_t *    vToSkip;      // edges to skip
    Vec_Int_t *    vEdges;       // edges as fanin/fanout pairs 
    Vec_Int_t *    vFirsts;      // first SAT variable
    Vec_Int_t *    vNvars;       // number of SAT variables
    Vec_Int_t *    vLits;        // literals
    int *          pLevels;      // levels

    // statistics
    abctime        timeStart;
};

extern sat_solver * Sbm_AddCardinSolver( int LogN, Vec_Int_t ** pvVars );

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

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

  Synopsis    [Count the number of edges between internal nodes.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Seg_ManCountIntEdges( Gia_Man_t * p, Vec_Int_t * vPolars, Vec_Int_t * vToSkip, int nFanouts )
{
    int i, iLut, iFanin;
    Vec_Int_t * vEdges = Vec_IntAlloc( 1000 );
    assert( Gia_ManHasMapping(p) );
    Vec_IntClear( vPolars );
    Vec_IntClear( vToSkip );
    if ( nFanouts )
        Gia_ManSetLutRefs( p );
    Gia_ManForEachLut( p, iLut )
        Gia_LutForEachFanin( p, iLut, iFanin, i )
            if ( Gia_ObjIsAnd(Gia_ManObj(p, iFanin)) )
            {
                if ( p->vEdge1 && Gia_ObjCheckEdge(p, iFanin, iLut) )
                    Vec_IntPush( vPolars, Vec_IntSize(vEdges)/2 );
                if ( nFanouts && Gia_ObjLutRefNumId(p, iFanin) >= nFanouts )
                    Vec_IntPush( vToSkip, Vec_IntSize(vEdges)/2 );
                Vec_IntPushTwo( vEdges, iFanin, iLut );
            }
    if ( nFanouts )
        ABC_FREE( p->pLutRefs );
    return vEdges;
}
Vec_Wec_t * Seg_ManCollectObjEdges( Vec_Int_t * vEdges, int nObjs )
{
    int iFanin, iObj, i;
    Vec_Wec_t * vRes = Vec_WecStart( nObjs );
    Vec_IntForEachEntryDouble( vEdges, iFanin, iObj, i )
    {
        Vec_WecPush( vRes, iFanin, i/2 );
        Vec_WecPush( vRes, iObj, i/2 );
    }
    return vRes;
}
int Seg_ManCountIntLevels( Seg_Man_t * p, int iStartVar )
{
    Gia_Obj_t * pObj;
    int iLut, nVars;
    Vec_IntFill( p->vFirsts, Gia_ManObjNum(p->pGia), -1 );
    Vec_IntFill( p->vNvars,  Gia_ManObjNum(p->pGia), 0 );
    ABC_FREE( p->pLevels );
    if ( p->pGia->pManTime )
    {
        p->DelayMax = Gia_ManLutLevelWithBoxes( p->pGia );
        p->pLevels = Vec_IntReleaseArray( p->pGia->vLevels );
        Vec_IntFreeP( &p->pGia->vLevels );
    }
    else
        p->DelayMax = Gia_ManLutLevel( p->pGia, &p->pLevels );
    Gia_ManForEachObj1( p->pGia, pObj, iLut )
    {
        if ( Gia_ObjIsCo(pObj) )
            continue;
        if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsLut(p->pGia, iLut) )
            continue;
        assert( Gia_ObjIsCi(pObj) || Gia_ObjIsLut(p->pGia, iLut) );
        Vec_IntWriteEntry( p->vFirsts, iLut, iStartVar );
        //assert( p->pLevels[iLut] > 0 );
        nVars = p->pLevels[iLut] < 2 ? 0 : p->pLevels[iLut];
        Vec_IntWriteEntry( p->vNvars,  iLut, nVars );
        iStartVar += nVars;
    }
    return iStartVar;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Seg_Man_t * Seg_ManAlloc( Gia_Man_t * pGia, int nFanouts )
{
    int nVarsAll;
    Seg_Man_t * p = ABC_CALLOC( Seg_Man_t, 1 );
    p->vPolars    = Vec_IntAlloc( 1000 ); 
    p->vToSkip    = Vec_IntAlloc( 1000 ); 
    p->vEdges     = Seg_ManCountIntEdges( pGia, p->vPolars, p->vToSkip, nFanouts );
    p->nVars      = Vec_IntSize(p->vEdges)/2;
    p->LogN       = Abc_Base2Log(p->nVars);
    p->Power2     = 1 << p->LogN;
    //p->pSat       = Sbm_AddCardinSolver( p->LogN, &p->vCardVars );
    p->pSat       = sat_solver_new();
    sat_solver_setnvars( p->pSat, p->nVars );
    p->FirstVar   = sat_solver_nvars( p->pSat );
    sat_solver_bookmark( p->pSat );
    p->pGia       = pGia;
    // internal
    p->vFirsts    = Vec_IntAlloc( 0 ); 
    p->vNvars     = Vec_IntAlloc( 0 ); 
    p->vLits      = Vec_IntAlloc( 0 ); 
    nVarsAll      = Seg_ManCountIntLevels( p, p->FirstVar );
    sat_solver_setnvars( p->pSat, nVarsAll );
    // other
    Gia_ManFillValue( pGia );
    return p;
}
void Seg_ManClean( Seg_Man_t * p )
{
    p->timeStart = Abc_Clock();
    sat_solver_rollback( p->pSat );
    sat_solver_bookmark( p->pSat );
    // internal
    Vec_IntClear( p->vEdges );
    Vec_IntClear( p->vFirsts );
    Vec_IntClear( p->vNvars );
    Vec_IntClear( p->vLits );
    Vec_IntClear( p->vPolars );
    Vec_IntClear( p->vToSkip );
    // other
    Gia_ManFillValue( p->pGia );
}
void Seg_ManStop( Seg_Man_t * p )
{
    sat_solver_delete( p->pSat );
    //Vec_IntFree( p->vCardVars );
    // internal
    Vec_IntFree( p->vEdges );
    Vec_IntFree( p->vFirsts );
    Vec_IntFree( p->vNvars );
    Vec_IntFree( p->vLits );
    Vec_IntFree( p->vPolars );
    Vec_IntFree( p->vToSkip );
    ABC_FREE( p->pLevels );
    // other
    ABC_FREE( p );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Seg_ManCreateCnf( Seg_Man_t * p, int fTwo, int fVerbose )
{
    Tim_Man_t * pTim = (Tim_Man_t *)p->pGia->pManTime;
    Gia_Obj_t * pObj;
    Vec_Wec_t * vObjEdges;
    Vec_Int_t * vLevel;
    int iLut, iFanin, iFirst;
    int pLits[3], Count = 0;
    int i, k, nVars, Edge, value;
    abctime clk = Abc_Clock();
    // edge delay constraints
    int nConstr = sat_solver_nclauses(p->pSat);
    Gia_ManForEachObj( p->pGia, pObj, iLut )
    {
        int iFirstLut = Vec_IntEntry( p->vFirsts, iLut );
        int nVarsLut  = Vec_IntEntry( p->vNvars, iLut );
        if ( pTim && Gia_ObjIsCi(pObj) )
        {
            int iBox = Tim_ManBoxForCi( pTim, Gia_ObjCioId(pObj) );
            if ( nVarsLut > 0 && iBox >= 0 )
            {
                int iCiId = Tim_ManBoxOutputFirst( pTim, iBox );
                if ( iCiId == Gia_ObjCioId(pObj) ) // first input
                {
                    int nIns = Tim_ManBoxInputNum( pTim, iBox );
                    int iIn0 = Tim_ManBoxInputFirst( pTim, iBox );
                    for ( i = 0; i < nIns-1; i++ ) // skip carry-in pin
                    {
                        Gia_Obj_t * pOut = Gia_ManCo( p->pGia, iIn0+i );
                        int iDriverId = Gia_ObjFaninId0p( p->pGia, pOut );
                        int AddOn;

                        iFirst = Vec_IntEntry( p->vFirsts, iDriverId );
                        nVars  = Vec_IntEntry( p->vNvars, iDriverId );
                        assert( nVars < nVarsLut );
                        AddOn = (int)(nVars < nVarsLut);
                        for ( k = 0; k < nVars; k++ )
                        {
                            pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                            pLits[1] = Abc_Var2Lit( iFirstLut+k+AddOn, 0 );
                            value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                            assert( value );
                        }
                    }
                }
                else // intermediate input
                {
                    Gia_Obj_t * pIn = Gia_ManCi( p->pGia, iCiId );
                    int iObjId = Gia_ObjId( p->pGia, pIn );

                    iFirst = Vec_IntEntry( p->vFirsts, iObjId );
                    nVars  = Vec_IntEntry( p->vNvars, iObjId );
                    if ( nVars > 0 )
                    {
                        for ( k = 0; k < nVars; k++ )
                        {
                            pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                            pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
                            value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                            assert( value );
                        }
                    }
                }
            }
            continue;
        }
        if ( !Gia_ObjIsLut(p->pGia, iLut) )
            continue;
        Gia_LutForEachFanin( p->pGia, iLut, iFanin, i )
            if ( pTim && Gia_ObjIsCi(Gia_ManObj(p->pGia, iFanin)) )
            {
                iFirst = Vec_IntEntry( p->vFirsts, iFanin );
                nVars  = Vec_IntEntry( p->vNvars, iFanin );
                assert( nVars <= nVarsLut );
                if ( nVars > 0 )
                {
                    for ( k = 0; k < nVars; k++ )
                    {
                        pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                        pLits[1] = Abc_Var2Lit( iFirstLut+k, 0 );
                        value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                        assert( value );
                    }
                }
            }
            else if ( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) )
            {
                iFirst = Vec_IntEntry( p->vFirsts, iFanin );
                nVars  = Vec_IntEntry( p->vNvars, iFanin );
                assert( nVars != 1 && nVars < nVarsLut );
                // add initial
                if ( nVars == 0 )
                {
                    pLits[0] = Abc_Var2Lit( Count, 1 );
                    pLits[1] = Abc_Var2Lit( iFirstLut, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                    assert( value );

                    pLits[0] = Abc_Var2Lit( Count, 0 );
                    pLits[1] = Abc_Var2Lit( iFirstLut+1, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                    assert( value );
                }
                // add others
                for ( k = 0; k < nVars; k++ )
                {
                    pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                    pLits[1] = Abc_Var2Lit( Count, 1 );
                    pLits[2] = Abc_Var2Lit( iFirstLut+k, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
                    assert( value );

                    pLits[0] = Abc_Var2Lit( iFirst+k, 1 );
                    pLits[1] = Abc_Var2Lit( Count, 0 );
                    pLits[2] = Abc_Var2Lit( iFirstLut+k+1, 0 );
                    value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
                    assert( value );
                }
                Count++;
            }
    }
    assert( Count == p->nVars );
    if ( fVerbose )
    printf( "Delay constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
    nConstr = sat_solver_nclauses(p->pSat);
/*
    // delay relationship constraints
    Vec_IntForEachEntryTwo( p->vFirsts, p->vNvars, iFirst, nVars, iLut )
    {
        if ( nVars < 2 )
            continue;
        for ( i = 1; i < nVars; i++ )
        {
            pLits[0] = Abc_Var2Lit( iFirst + i - 1, 1 );
            pLits[1] = Abc_Var2Lit( iFirst + i,     0 );
            value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
            assert( value );
        }
    }
*/
    // edge compatibility constraint
    vObjEdges = Seg_ManCollectObjEdges( p->vEdges, Gia_ManObjNum(p->pGia) );
    Vec_WecForEachLevel( vObjEdges, vLevel, i )
    {
        int v1, v2, v3, Var1, Var2, Var3;
        if ( (!fTwo && Vec_IntSize(vLevel) >= 2) || (fTwo && Vec_IntSize(vLevel) > 10) )
        {
            Vec_IntForEachEntry( vLevel, Var1, v1 )
            Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 )
            {
                pLits[0] = Abc_Var2Lit( Var1, 1 );
                pLits[1] = Abc_Var2Lit( Var2, 1 );
                value = sat_solver_addclause( p->pSat, pLits, pLits+2 );
                assert( value );
            }
        }
        else if ( fTwo && Vec_IntSize(vLevel) >= 3 )
        {
            Vec_IntForEachEntry( vLevel, Var1, v1 )
            Vec_IntForEachEntryStart( vLevel, Var2, v2, v1 + 1 )
            Vec_IntForEachEntryStart( vLevel, Var3, v3, v2 + 1 )
            {
                pLits[0] = Abc_Var2Lit( Var1, 1 );
                pLits[1] = Abc_Var2Lit( Var2, 1 );
                pLits[2] = Abc_Var2Lit( Var3, 1 );
                value = sat_solver_addclause( p->pSat, pLits, pLits+3 );
                assert( value );
            }
        }
    }
    Vec_WecFree( vObjEdges );
    // block forbidden edges
    Vec_IntForEachEntry( p->vToSkip, Edge, i )
    {
        pLits[0] = Abc_Var2Lit( Edge, 1 );
        value = sat_solver_addclause( p->pSat, pLits, pLits+1 );
        assert( value );
    }
    if ( fVerbose )
    printf( "Edge constraints = %d. ", sat_solver_nclauses(p->pSat) - nConstr );
    if ( fVerbose )
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Seg_ManConvertResult( Seg_Man_t * p )
{
    int iFanin, iObj, i;
    Vec_Int_t * vEdges2 = Vec_IntAlloc( 1000 );
    Vec_IntForEachEntryDouble( p->vEdges, iFanin, iObj, i )
        if ( sat_solver_var_value(p->pSat, i/2) )
            Vec_IntPushTwo( vEdges2, iFanin, iObj );
    return vEdges2;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int nFanouts, int fTwo, int fVerbose )
{
    int nBTLimit = 0;
    int nTimeOut = 0;
    int fVeryVerbose = 0;

    Gia_Obj_t * pObj;
    abctime clk = Abc_Clock();
    Vec_Int_t * vEdges2 = NULL;
    int i, iLut, iFirst, nVars, status, Delay, nConfs;
    Seg_Man_t * p = Seg_ManAlloc( pGia, nFanouts );
    int DelayStart = DelayInit ? DelayInit : p->DelayMax;

    if ( fVerbose )
    printf( "Running SatEdge with starting delay %d and edge %d (edge vars %d, total vars %d)\n", 
        DelayStart, fTwo+1, p->FirstVar, sat_solver_nvars(p->pSat) );
    Seg_ManCreateCnf( p, fTwo, fVerbose );
    //Sat_SolverWriteDimacs( p->pSat, "test_edge.cnf", NULL, NULL, 0 );
    // set resource limits
    sat_solver_set_resource_limits( p->pSat, nBTLimit, 0, 0, 0 );
    sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
    sat_solver_set_random( p->pSat, 1 );
    sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolars), Vec_IntSize(p->vPolars) );
    //sat_solver_set_var_activity( p->pSat, NULL, p->nVars );
    // increment delay gradually
    for ( Delay = p->DelayMax; Delay >= 0; Delay-- )
    {
        // we constrain COs, although it would be fine to constrain only POs
        Gia_ManForEachCoDriver( p->pGia, pObj, i )
        {
            iLut   = Gia_ObjId( p->pGia, pObj );
            iFirst = Vec_IntEntry( p->vFirsts, iLut );
            nVars  = Vec_IntEntry( p->vNvars, iLut );
            if ( Delay < nVars && !sat_solver_push(p->pSat, Abc_Var2Lit(iFirst + Delay, 1)) )
                break;
        }
        if ( i < Gia_ManCoNum(p->pGia) )
        {
            printf( "Proved UNSAT for delay %d.  ", Delay );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            break;
        }
        if ( Delay > DelayStart )
            continue;
        // solve with assumptions
        //clk = Abc_Clock();
        nConfs = sat_solver_nconflicts( p->pSat );
        status = sat_solver_solve_internal( p->pSat );
        nConfs = sat_solver_nconflicts( p->pSat ) - nConfs;
        if ( status == l_True )
        {
            if ( fVerbose )
            {
                int Count = 0;
                for ( i = 0; i < p->nVars; i++ )
                    Count += sat_solver_var_value(p->pSat, i);
                printf( "Solution with delay %2d and %5d edges exists. Conf = %8d.  ", Delay, Count, nConfs );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            // save the result
            Vec_IntFreeP( &vEdges2 );
            vEdges2 = Seg_ManConvertResult( p );
            if ( fVeryVerbose )
            {
                for ( i = 0; i < p->nVars; i++ )
                    printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
                printf( "   " );

                for ( i = p->nVars; i < sat_solver_nvars(p->pSat); i++ )
                    printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
                printf( "\n" );
            }
        }
        else
        {
            if ( fVerbose )
            {
                if ( status == l_False )
                    printf( "Proved UNSAT for delay %d.  ", Delay );
                else
                    printf( "Resource limit reached for delay %d.  ", Delay );
                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
            }
            break;
        }
    }
    Gia_ManEdgeFromArray( p->pGia, vEdges2 );
    Vec_IntFreeP( &vEdges2 );
    Seg_ManStop( p );
}


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


ABC_NAMESPACE_IMPL_END