wlcAbc.c

Go to the documentation of this file.

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



void Wlc_NtkPrintInputInfo( Wlc_Ntk_t * pNtk )
{
    Wlc_Obj_t * pObj;
    int i, k, nRange, nBeg, nEnd, nBits = 0;
    FILE * output;
 
    output = fopen("abc_blast_input.info","w");
 
    Wlc_NtkForEachCi( pNtk, pObj, i )
    {
        nRange = Wlc_ObjRange(pObj);
        nBeg = pObj->Beg;
        nEnd = pObj->End;
 
        for ( k = 0; k < nRange; k++ )
        {
            int index = nEnd > nBeg ? nBeg + k : nEnd + k;
            char c = pObj->Type != WLC_OBJ_FO ? 'i' : pNtk->pInits[nBits + k];
            fprintf(output,"%s[%d] : %c \n", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), index , c );
        }
        if (pObj->Type == WLC_OBJ_FO)
            nBits += nRange;
    }
 
    Wlc_NtkForEachPo( pNtk, pObj, i )
    {
        nRange = Wlc_ObjRange(pObj);
        nBeg = pObj->Beg;
        nEnd = pObj->End;
 
        for ( k = 0; k < nRange; k++ )
        {
            int index = nEnd > nBeg ? nBeg + k : nEnd + k;
            fprintf(output,"%s[%d] : o \n", Wlc_ObjName(pNtk, Wlc_ObjId(pNtk, pObj)), index);
        }
    }
 
    fclose(output);
    return;
}

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 );
}

Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Ptr_t * vNamesIn )
{
    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 );
            // If vNamesIn is given, take names from there for as many entries as possible
            // otherwise generate names from counter
            if (vNamesIn != NULL && i < Vec_PtrSize(vNamesIn)) {
                Abc_ObjAssignName( pMainObj, (char *)Vec_PtrEntry(vNamesIn, i), NULL );
            }
            else
            {
                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;
}

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;
}

 
 
ABC_NAMESPACE_IMPL_END