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

  FileName    [wlcAbc.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Verilog parser.]

  Synopsis    [Parses several flavors of word-level Verilog.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - August 22, 2014.]

  Revision    [$Id: wlcAbc.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]

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

#include "wlc.h"
#include "base/abc/abc.h"

ABC_NAMESPACE_IMPL_START

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

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

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

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vCounts, int fVerbose )
{
    Wlc_Obj_t * pObj;
    int i, k, nNum, nRange, nBits = 0;
    Wlc_NtkForEachCi( pNtk, pObj, i )
    {
        if ( pObj->Type != WLC_OBJ_FO )
            continue;
        nRange = Wlc_ObjRange(pObj);
        for ( k = 0; k < nRange; k++ )
        {
            nNum = Vec_IntEntry(vCounts, nBits + k);
            if ( nNum )
                break;
        }
        if ( k == nRange )
        {
            nBits += nRange;
            continue;
        }
        printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
        for ( k = 0; k < nRange; k++ )
        {
            nNum = Vec_IntEntry( vCounts, nBits + k );
            if ( nNum == 0 )
                continue;
            printf( "  [%d] -> %d", k, nNum );
        }
        printf( "\n");
        nBits += nRange;
    }
    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
    assert( Vec_IntSize(vCounts) == nBits );
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv )
{
    extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
    extern Vec_Str_t * Pdr_InvPrintStr( Vec_Int_t * vInv, Vec_Int_t * vCounts );

    Vec_Int_t * vCounts = Pdr_InvCounts( vInv );
    Vec_Str_t * vSop = Pdr_InvPrintStr( vInv, vCounts );

    Wlc_Obj_t * pObj;
    int i, k, nNum, nRange, nBits = 0;
    Abc_Ntk_t * pMainNtk = NULL;
    Abc_Obj_t * pMainObj, * pMainTemp;
    char Buffer[5000];
    // start the network
    pMainNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
    // duplicate the name and the spec
    pMainNtk->pName = Extra_UtilStrsav(pNtk ? pNtk->pName : "inv");
    // create primary inputs
    if ( pNtk == NULL )
    {
        int Entry, nInputs = Abc_SopGetVarNum( Vec_StrArray(vSop) );
        Vec_IntForEachEntry( vCounts, Entry, i )
        {
            if ( Entry == 0 )
                continue;
            pMainObj = Abc_NtkCreatePi( pMainNtk );
            sprintf( Buffer, "pi%d", i );
            Abc_ObjAssignName( pMainObj, Buffer, NULL );
        }
        if ( Abc_NtkPiNum(pMainNtk) != nInputs )
        {
            printf( "Mismatch between number of inputs and the number of literals in the invariant.\n" );
            Abc_NtkDelete( pMainNtk );
            return NULL;
        }
    }
    else
    {
        Wlc_NtkForEachCi( pNtk, pObj, i )
        {
            if ( pObj->Type != WLC_OBJ_FO )
                continue;
            nRange = Wlc_ObjRange(pObj);
            for ( k = 0; k < nRange; k++ )
            {
                nNum = Vec_IntEntry(vCounts, nBits + k);
                if ( nNum )
                    break;
            }
            if ( k == nRange )
            {
                nBits += nRange;
                continue;
            }
            //printf( "%s[%d:%d] : ", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), pObj->End, pObj->Beg );
            for ( k = 0; k < nRange; k++ )
            {
                nNum = Vec_IntEntry( vCounts, nBits + k );
                if ( nNum == 0 )
                    continue;
                //printf( "  [%d] -> %d", k, nNum );
                pMainObj = Abc_NtkCreatePi( pMainNtk );
                sprintf( Buffer, "%s[%d]", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), k );
                Abc_ObjAssignName( pMainObj, Buffer, NULL );

            }
            //printf( "\n");
            nBits += nRange;
        }
    }
    //printf( "%d %d\n", Vec_IntSize(vCounts), nBits );
    assert( pNtk == NULL || Vec_IntSize(vCounts) == nBits );
    // create node
    pMainObj = Abc_NtkCreateNode( pMainNtk );
    Abc_NtkForEachPi( pMainNtk, pMainTemp, i )
        Abc_ObjAddFanin( pMainObj, pMainTemp );
    pMainObj->pData = Abc_SopRegister( (Mem_Flex_t *)pMainNtk->pManFunc, Vec_StrArray(vSop) );
    Vec_IntFree( vCounts );
    Vec_StrFree( vSop );
    // create PO
    pMainTemp = Abc_NtkCreatePo( pMainNtk );
    Abc_ObjAddFanin( pMainTemp, pMainObj );
    Abc_ObjAssignName( pMainTemp, "inv", NULL );
    return pMainNtk;
}

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

  Synopsis    [Translate current network into an invariant.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia )
{
    int nRegs = Gia_ManRegNum(pGia);
    Vec_Int_t * vRes = NULL;
    if ( Abc_NtkPoNum(pNtk) != 1 )
        printf( "The number of outputs is other than 1.\n" );
    else if ( Abc_NtkNodeNum(pNtk) != 1 )
        printf( "The number of internal nodes is other than 1.\n" );
    else
    {
        Abc_Nam_t * pNames = NULL;
        Abc_Obj_t * pFanin, * pNode = Abc_ObjFanin0( Abc_NtkCo(pNtk, 0) );
        char * pName, * pCube, * pSop = (char *)pNode->pData;
        Vec_Int_t * vFanins = Vec_IntAlloc( Abc_ObjFaninNum(pNode) );
        int i, k, Value, nLits, Counter = 0;
        if ( pGia->vNamesIn )
        {
            // hash the names
            pNames = Abc_NamStart( 100, 16 );
            Vec_PtrForEachEntry( char *, pGia->vNamesIn, pName, i )
            {
                Value = Abc_NamStrFindOrAdd( pNames, pName, NULL );
                assert( Value == i+1 );
                //printf( "%s(%d) ", pName, i );
            }
            //printf( "\n" );
        }
        Abc_ObjForEachFanin( pNode, pFanin, i )
        {
            assert( Abc_ObjIsCi(pFanin) );
            pName = Abc_ObjName(pFanin);
            if ( pNames )
            {
                Value = Abc_NamStrFind(pNames, pName) - 1 - Gia_ManPiNum(pGia);
                if ( Value < 0 )
                {
                    if ( Counter++ == 0 )
                        printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
                    Value = i;
                }
            }
            else
            {
                for ( k = (int)strlen(pName)-1; k >= 0; k-- )
                    if ( pName[k] < '0' || pName[k] > '9' )
                        break;
                if ( k == (int)strlen(pName)-1 )
                {
                    if ( Counter++ == 0 )
                        printf( "Cannot read input name \"%s\" of fanin %d.\n", pName, i );
                    Value = i;
                }
                else 
                    Value = atoi(pName + k + 1);
            }
            Vec_IntPush( vFanins, Value );
        }
        if ( Counter )
            printf( "Cannot read names for %d inputs of the invariant.\n", Counter );
        if ( pNames )
            Abc_NamStop( pNames );
        assert( Vec_IntSize(vFanins) == Abc_ObjFaninNum(pNode) );
        vRes = Vec_IntAlloc( 1000 );
        Vec_IntPush( vRes, Abc_SopGetCubeNum(pSop) );
        Abc_SopForEachCube( pSop, Abc_ObjFaninNum(pNode), pCube )
        {
            nLits = 0;
            Abc_CubeForEachVar( pCube, Value, k )
                if ( Value != '-' )
                    nLits++;
            Vec_IntPush( vRes, nLits );
            Abc_CubeForEachVar( pCube, Value, k )
                if ( Value != '-' )
                    Vec_IntPush( vRes, Abc_Var2Lit(Vec_IntEntry(vFanins, k), (int)Value == '0') );
        }
        Vec_IntPush( vRes, nRegs );
        Vec_IntFree( vFanins );
    }
    return vRes;
}

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


ABC_NAMESPACE_IMPL_END