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

  FileName    [saigIoa.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Sequential AIG package.]

  Synopsis    [Input/output for sequential AIGs using BLIF files.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include <math.h>
#include "saig.h"

ABC_NAMESPACE_IMPL_START


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

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

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj )
{
    static char Buffer[16];
    if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) )
        sprintf( Buffer, "n%0*d", Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) );
    else if ( Saig_ObjIsPi(p, pObj) )
        sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjCioId(pObj) );
    else if ( Saig_ObjIsPo(p, pObj) )
        sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjCioId(pObj) );
    else if ( Saig_ObjIsLo(p, pObj) )
        sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPiNum(p) );
    else if ( Saig_ObjIsLi(p, pObj) )
        sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPoNum(p) );
    else 
        assert( 0 );
    return Buffer;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
{
    FILE * pFile;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i;
    if ( Aig_ManCoNum(p) == 0 )
    {
        printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" );
        return;
    }
    Aig_ManSetCioIds( p );
    // write input file
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        printf( "Saig_ManDumpBlif(): Cannot open file for writing.\n" );
        return;
    }
    fprintf( pFile, "# BLIF file written by procedure Saig_ManDumpBlif()\n" );
    fprintf( pFile, "# If unedited, this file can be read by Saig_ManReadBlif()\n" );
    fprintf( pFile, "# AIG stats: pi=%d po=%d reg=%d and=%d obj=%d maxid=%d\n", 
        Saig_ManPiNum(p), Saig_ManPoNum(p), Saig_ManRegNum(p), 
        Aig_ManNodeNum(p), Aig_ManObjNum(p), Aig_ManObjNumMax(p) );
    fprintf( pFile, ".model %s\n", p->pName );
    // write primary inputs
    fprintf( pFile, ".inputs" );
    Aig_ManForEachPiSeq( p, pObj, i )
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
    fprintf( pFile, "\n" );
    // write primary outputs
    fprintf( pFile, ".outputs" );
    Aig_ManForEachPoSeq( p, pObj, i )
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
    fprintf( pFile, "\n" );
    // write registers
    if ( Aig_ManRegNum(p) )
    {
        Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i )
        {
            fprintf( pFile, ".latch" );
            fprintf( pFile, " %s", Saig_ObjName(p, pObjLi) );
            fprintf( pFile, " %s", Saig_ObjName(p, pObjLo) );
            fprintf( pFile, " 0\n" );
        }
    } 
    // check if constant is used
    if ( Aig_ObjRefs(Aig_ManConst1(p)) )
        fprintf( pFile, ".names %s\n 1\n", Saig_ObjName(p, Aig_ManConst1(p)) );
    // write the nodes in the DFS order
    Aig_ManForEachNode( p, pObj, i )
    {
        fprintf( pFile, ".names" );
        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin1(pObj)) );
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
        fprintf( pFile, "\n%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) );
    }
    // write the POs
    Aig_ManForEachCo( p, pObj, i )
    {
        fprintf( pFile, ".names" );
        fprintf( pFile, " %s", Saig_ObjName(p, Aig_ObjFanin0(pObj)) );
        fprintf( pFile, " %s", Saig_ObjName(p, pObj) );
        fprintf( pFile, "\n%d 1\n", !Aig_ObjFaninC0(pObj) );
    }
    fprintf( pFile, ".end\n" );
    fclose( pFile );
}

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

  Synopsis    [Reads one token from file.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
char * Saig_ManReadToken( FILE * pFile )
{
    static char Buffer[1000];
    if ( fscanf( pFile, "%s", Buffer ) == 1 )
        return Buffer;
    return NULL;
}

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

  Synopsis    [Returns the corresponding number.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Saig_ManReadNumber( Aig_Man_t * p, char * pToken )
{
    if ( pToken[0] == 'n' )
        return atoi( pToken + 1 );
    if ( pToken[0] == 'p' )
        return atoi( pToken + 2 );
    if ( pToken[0] == 'l' )
        return atoi( pToken + 2 );
    assert( 0 );
    return -1;
}

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

  Synopsis    [Returns the corresponding node.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Obj_t * Saig_ManReadNode( Aig_Man_t * p, int * pNum2Id, char * pToken )
{
    int Num;
    if ( pToken[0] == 'n' )
    {
        Num = atoi( pToken + 1 );
        return Aig_ManObj( p, pNum2Id[Num] );
    }
    if ( pToken[0] == 'p' )
    {
        pToken++;
        if ( pToken[0] == 'i' )
        {
            Num = atoi( pToken + 1 );
            return Aig_ManCi( p, Num );
        }
        if ( pToken[0] == 'o' )
            return NULL;
        assert( 0 );
        return NULL;
    }
    if ( pToken[0] == 'l' )
    {
        pToken++;
        if ( pToken[0] == 'o' )
        {
            Num = atoi( pToken + 1 );
            return Saig_ManLo( p, Num );
        }
        if ( pToken[0] == 'i' )
            return NULL;
        assert( 0 );
        return NULL;
    }
    assert( 0 );
    return NULL;
}

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

  Synopsis    [Reads BLIF previously dumped by Saig_ManDumpBlif().]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Saig_ManReadBlif( char * pFileName )
{
    FILE * pFile;
    Aig_Man_t * p;
    Aig_Obj_t * pFanin0, * pFanin1, * pNode;
    char * pToken;
    int i, nPis, nPos, nRegs, Number;
    int * pNum2Id = NULL;  // mapping of node numbers in the file into AIG node IDs
    // open the file
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Saig_ManReadBlif(): Cannot open file for reading.\n" );
        return NULL;
    }
    // skip through the comments
    for ( i = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; i++ );
    if ( pToken == NULL ) 
        { printf( "Saig_ManReadBlif(): Error 1.\n" ); return NULL; }
    // get he model
    pToken = Saig_ManReadToken( pFile );
    if ( pToken == NULL ) 
        { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; }
    // start the package
    p = Aig_ManStart( 10000 );
    p->pName = Abc_UtilStrsav( pToken );
    p->pSpec = Abc_UtilStrsav( pFileName );
    // count PIs
    pToken = Saig_ManReadToken( pFile );
    if ( pToken == NULL || strcmp( pToken, ".inputs" ) ) 
        { printf( "Saig_ManReadBlif(): Error 3.\n" ); Aig_ManStop(p); return NULL; }
    for ( nPis = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPis++ );
    // count POs
    if ( pToken == NULL || strcmp( pToken, ".outputs" ) ) 
        { printf( "Saig_ManReadBlif(): Error 4.\n" ); Aig_ManStop(p); return NULL; }
    for ( nPos = 0; (pToken = Saig_ManReadToken( pFile )) && pToken[0] != '.'; nPos++ );
    // count latches
    if ( pToken == NULL ) 
        { printf( "Saig_ManReadBlif(): Error 5.\n" ); Aig_ManStop(p); return NULL; }
    for ( nRegs = 0; strcmp( pToken, ".latch" ) == 0; nRegs++ )
    {
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 6.\n" ); Aig_ManStop(p); return NULL; }
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 7.\n" ); Aig_ManStop(p); return NULL; }
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 8.\n" ); Aig_ManStop(p); return NULL; }
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 9.\n" ); Aig_ManStop(p); return NULL; }
    }
    // create PIs and LOs
    for ( i = 0; i < nPis + nRegs; i++ )
        Aig_ObjCreateCi( p );
    Aig_ManSetRegNum( p, nRegs );
    // create nodes
    for ( i = 0; strcmp( pToken, ".names" ) == 0; i++ )
    {
        // first token
        pToken = Saig_ManReadToken( pFile );
        if ( i == 0 && pToken[0] == 'n' )
        { // constant node
            // read 1
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL || strcmp( pToken, "1" ) ) 
                { printf( "Saig_ManReadBlif(): Error 10.\n" ); Aig_ManStop(p); return NULL; }
            // read next
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL ) 
                { printf( "Saig_ManReadBlif(): Error 11.\n" ); Aig_ManStop(p); return NULL; }
            continue;
        }
        pFanin0 = Saig_ManReadNode( p, pNum2Id, pToken );

        // second token
        pToken = Saig_ManReadToken( pFile );
        if ( (pToken[0] == 'p' && pToken[1] == 'o') || (pToken[0] == 'l' && pToken[1] == 'i') )
        { // buffer
            // read complemented attribute
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL ) 
                { printf( "Saig_ManReadBlif(): Error 12.\n" ); Aig_ManStop(p); return NULL; }
            if ( pToken[0] == '0' )
                pFanin0 = Aig_Not(pFanin0);
            // read 1
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL || strcmp( pToken, "1" ) ) 
                { printf( "Saig_ManReadBlif(): Error 13.\n" ); Aig_ManStop(p); return NULL; }
            Aig_ObjCreateCo( p, pFanin0 );
            // read next
            pToken = Saig_ManReadToken( pFile );
            if ( pToken == NULL ) 
                { printf( "Saig_ManReadBlif(): Error 14.\n" ); Aig_ManStop(p); return NULL; }
            continue;
        }

        // third token
        // regular node
        pFanin1 = Saig_ManReadNode( p, pNum2Id, pToken );
        pToken = Saig_ManReadToken( pFile );
        Number = Saig_ManReadNumber( p, pToken );
        // allocate mapping
        if ( pNum2Id == NULL )
        {
//            extern double pow( double x, double y );
            int Size = (int)pow(10.0, (double)(strlen(pToken) - 1));
            pNum2Id = ABC_CALLOC( int, Size );
        }

        // other tokens
        // get the complemented attributes
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 15.\n" ); Aig_ManStop(p); return NULL; }
        if ( pToken[0] == '0' )
            pFanin0 = Aig_Not(pFanin0);
        if ( pToken[1] == '0' )
            pFanin1 = Aig_Not(pFanin1);
        // read 1
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL || strcmp( pToken, "1" ) ) 
            { printf( "Saig_ManReadBlif(): Error 16.\n" ); Aig_ManStop(p); return NULL; }
        // read next
        pToken = Saig_ManReadToken( pFile );
        if ( pToken == NULL ) 
            { printf( "Saig_ManReadBlif(): Error 17.\n" ); Aig_ManStop(p); return NULL; }

        // create new node
        pNode = Aig_And( p, pFanin0, pFanin1 );
        if ( Aig_IsComplement(pNode) )
            { printf( "Saig_ManReadBlif(): Error 18.\n" ); Aig_ManStop(p); return NULL; }
        // set mapping
        pNum2Id[ Number ] = pNode->Id;
    }
    if ( pToken == NULL || strcmp( pToken, ".end" ) ) 
        { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; }
    if ( nPos + nRegs != Aig_ManCoNum(p) ) 
        { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; }
    // add non-node objects to the mapping
    Aig_ManForEachCi( p, pNode, i )
        pNum2Id[pNode->Id] = pNode->Id;
//    ABC_FREE( pNum2Id );
    p->pData = pNum2Id;
    // check the new manager
    Aig_ManSetRegNum( p, nRegs );
    if ( !Aig_ManCheck(p) )
        printf( "Saig_ManReadBlif(): Check has failed.\n" );
    return p;
}

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


ABC_NAMESPACE_IMPL_END