Changes to incorporate AIG parsing in memory and user-specified PI/PO/FF numbers.

src/aig/gia/gia.h

@@ -138,8 +138,9 @@ struct Gia_Man_t_
     int            nTravIdsAlloc; // the number of trav IDs allocated
     Vec_Ptr_t *    vNamesIn;      // the input names 
     Vec_Ptr_t *    vNamesOut;     // the output names
-    Vec_Int_t *    vCiNumsOrig;   // original names of the CIs
-    Vec_Int_t *    vCoNumsOrig;   // original names of the COs
+    Vec_Int_t *    vUserPiIds;    // numbers assigned to PIs by the user
+    Vec_Int_t *    vUserPoIds;    // numbers assigned to POs by the user
+    Vec_Int_t *    vUserFfIds;    // numbers assigned to FFs by the user
     Vec_Vec_t *    vClockDoms;    // clock domains
     Vec_Flt_t *    vTiming;       // arrival/required/slack
     void *         pManTime;      // the timing manager
@@ -596,6 +597,7 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
+extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
 extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
 extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );

src/aig/gia/giaAbs.c

@@ -138,8 +138,8 @@ Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops )
     pNew = Saig_ManDeriveAbstraction( pTemp = pNew, vFlops );
     Aig_ManStop( pTemp );
     pGia = Gia_ManFromAig( pNew );
-    pGia->vCiNumsOrig = pNew->vCiNumsOrig; 
-    pNew->vCiNumsOrig = NULL;
+//    pGia->vCiNumsOrig = pNew->vCiNumsOrig; 
+//    pNew->vCiNumsOrig = NULL;
     Aig_ManStop( pNew );
     return pGia;
 

src/aig/gia/giaAiger.c

@@ -342,7 +342,7 @@ Gia_Plc_t * Gia_ReadPlacement( unsigned char ** ppPos, int nSize )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
+Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
 {
     FILE * pFile;
     Gia_Man_t * pNew;
@@ -558,6 +558,304 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
 
 /**Function*************************************************************
 
+  Synopsis    [Reads the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck )
+{
+    Gia_Man_t * pNew;
+    Vec_Int_t * vLits = NULL;
+    Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
+    int iObj, iNode0, iNode1;
+    int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
+    unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
+    unsigned uLit0, uLit1, uLit;
+
+    // read the file type
+    pCur = (unsigned char *)pContents;  while ( *pCur++ != ' ' );
+    // read the number of objects
+    nTotal = atoi( (char *)pCur );    while ( *pCur++ != ' ' );
+    // read the number of inputs
+    nInputs = atoi( (char *)pCur );   while ( *pCur++ != ' ' );
+    // read the number of latches
+    nLatches = atoi( (char *)pCur );  while ( *pCur++ != ' ' );
+    // read the number of outputs
+    nOutputs = atoi( (char *)pCur );  while ( *pCur++ != ' ' );
+    // read the number of nodes
+    nAnds = atoi( (char *)pCur );     while ( *pCur++ != '\n' );  
+    // check the parameters
+    if ( nTotal != nInputs + nLatches + nAnds )
+    {
+        ABC_FREE( pContents );
+        fprintf( stdout, "The paramters are wrong.\n" );
+        return NULL;
+    }
+
+    // allocate the empty AIG
+    pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
+
+    // prepare the array of nodes
+    vNodes = Vec_IntAlloc( 1 + nTotal );
+    Vec_IntPush( vNodes, 0 );
+
+    // create the PIs
+    for ( i = 0; i < nInputs + nLatches; i++ )
+    {
+        iObj = Gia_ManAppendCi(pNew);    
+        Vec_IntPush( vNodes, iObj );
+    }
+
+    // remember the beginning of latch/PO literals
+    pDrivers = pCur;
+    if ( pContents[3] == ' ' ) // standard AIGER
+    {
+        // scroll to the beginning of the binary data
+        for ( i = 0; i < nLatches + nOutputs; )
+            if ( *pCur++ == '\n' )
+                i++;
+    }
+    else // modified AIGER
+    {
+        vLits = Gia_WriteDecodeLiterals( &pCur, nLatches + nOutputs );
+    }
+
+    // create the AND gates
+    for ( i = 0; i < nAnds; i++ )
+    {
+        uLit = ((i + 1 + nInputs + nLatches) << 1);
+        uLit1 = uLit  - Gia_ReadAigerDecode( &pCur );
+        uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur );
+//        assert( uLit1 > uLit0 );
+        iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 );
+        iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 );
+        assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches );
+//        Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) );
+        Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) );
+    }
+
+    // remember the place where symbols begin
+    pSymbols = pCur;
+
+    // read the latch driver literals
+    vDrivers = Vec_IntAlloc( nLatches + nOutputs );
+    if ( pContents[3] == ' ' ) // standard AIGER
+    {
+        pCur = pDrivers;
+        for ( i = 0; i < nLatches; i++ )
+        {
+            uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
+            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            Vec_IntPush( vDrivers, iNode0 );
+        }
+        // read the PO driver literals
+        for ( i = 0; i < nOutputs; i++ )
+        {
+            uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
+            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            Vec_IntPush( vDrivers, iNode0 );
+        }
+
+    }
+    else
+    {
+        // read the latch driver literals
+        for ( i = 0; i < nLatches; i++ )
+        {
+            uLit0 = Vec_IntEntry( vLits, i );
+            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            Vec_IntPush( vDrivers, iNode0 );
+        }
+        // read the PO driver literals
+        for ( i = 0; i < nOutputs; i++ )
+        {
+            uLit0 = Vec_IntEntry( vLits, i+nLatches );
+            iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
+            Vec_IntPush( vDrivers, iNode0 );
+        }
+        Vec_IntFree( vLits );
+    }
+
+    // create the POs
+    for ( i = 0; i < nOutputs; i++ )
+        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, nLatches + i) );
+    for ( i = 0; i < nLatches; i++ )
+        Gia_ManAppendCo( pNew, Vec_IntEntry(vDrivers, i) );
+    Vec_IntFree( vDrivers );
+
+    // create the latches
+    Gia_ManSetRegNum( pNew, nLatches );
+
+    // check if there are other types of information to read
+    pCur = pSymbols;
+    if ( (char *)pCur + 1 < pContents + nFileSize && *pCur == 'c' )
+    {
+        pCur++;
+        if ( *pCur == 'e' )
+        {
+            pCur++;
+            // read equivalence classes
+            pNew->pReprs = Gia_ReadEquivClasses( &pCur, Gia_ManObjNum(pNew) );
+            pNew->pNexts = Gia_ManDeriveNexts( pNew );
+        }
+        if ( *pCur == 'f' )
+        {
+            pCur++;
+            // read flop classes
+            pNew->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pNew) );
+            Gia_ReadFlopClasses( &pCur, pNew->vFlopClasses, Gia_ManRegNum(pNew) );
+        }
+        if ( *pCur == 'm' )
+        {
+            pCur++;
+            // read mapping
+            pNew->pMapping = Gia_ReadMapping( &pCur, Gia_ManObjNum(pNew) );
+        }
+        if ( *pCur == 'p' )
+        {
+            pCur++;
+            // read placement
+            pNew->pPlacement = Gia_ReadPlacement( &pCur, Gia_ManObjNum(pNew) );
+        }
+        if ( *pCur == 's' )
+        { 
+            pCur++;
+            // read switching activity
+            pNew->pSwitching = Gia_ReadSwitching( &pCur, Gia_ManObjNum(pNew) );
+        }
+        if ( *pCur == 'c' )
+        {
+            pCur++;
+            // read number of constraints
+            pNew->nConstrs = Gia_ReadInt( pCur ); pCur += 4;
+        }
+        if ( *pCur == 'n' )
+        {
+            pCur++;
+            // read model name
+            ABC_FREE( pNew->pName );
+            pNew->pName = Gia_UtilStrsav( (char *)pCur );
+        }
+    }
+
+    // read signal names if they are of the special type
+    if ( *pCur != 'c' )
+    {
+        int fBreakUsed = 0;
+        pNew->vUserPiIds = Vec_IntStartFull( Gia_ManPiNum(pNew) );
+        pNew->vUserPoIds = Vec_IntStartFull( Gia_ManPoNum(pNew) );
+        pNew->vUserFfIds = Vec_IntStartFull( Gia_ManRegNum(pNew) );
+        while ( pCur < pContents + nFileSize && *pCur != 'c' )
+        {
+            int iTerm;
+            char * pType = pCur;
+            // check terminal type
+            if ( *pCur != 'i' && *pCur != 'o' && *pCur != 'l'  )
+            {
+                fprintf( stdout, "Wrong terminal type.\n" );
+                fBreakUsed = 1;
+                break;
+            }
+            // get terminal number
+            iTerm = atoi( ++pCur );  while ( *pCur++ != ' ' );
+            // skip spaces
+            while ( *pCur++ == ' ' );
+            // decode the user numbers:
+            // flops are named: @l<num>
+            // PIs are named: @i<num>
+            // POs are named: @o<num>
+            if ( *pCur++ != '@' )
+            {
+                fBreakUsed = 1;
+                break;
+            }
+            if ( *pCur == 'i' && *pType == 'i' )
+                Vec_IntWriteEntry( pNew->vUserPiIds, iTerm, atoi(pCur+1) );
+            else if ( *pCur == 'o' && *pType == 'o' )
+                Vec_IntWriteEntry( pNew->vUserPoIds, iTerm, atoi(pCur+1) );
+            else if ( *pCur == 'l' && *pType == 'l' )
+                Vec_IntWriteEntry( pNew->vUserFfIds, iTerm, atoi(pCur+1) );
+            else
+            {
+                fprintf( stdout, "Wrong name format.\n" );
+                fBreakUsed = 1;
+                break;
+            }
+            // skip digits
+            while ( *pCur++ != '\n' );
+        }
+        // in case of abnormal termination, remove the arrays
+        if ( fBreakUsed )
+        {
+            Vec_IntFreeP( &pNew->vUserPiIds );
+            Vec_IntFreeP( &pNew->vUserPoIds );
+            Vec_IntFreeP( &pNew->vUserFfIds );
+        }
+    }
+
+
+    // skipping the comments
+    ABC_FREE( pContents );
+    Vec_IntFree( vNodes );
+/*
+    // check the result
+    if ( fCheck && !Gia_ManCheck( pNew ) )
+    {
+        printf( "Gia_ReadAiger: The network check has failed.\n" );
+        Gia_ManStop( pNew );
+        return NULL;
+    }
+*/
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
+{
+    FILE * pFile;
+    Gia_Man_t * pNew;
+    char * pName, * pContents;
+    int nFileSize;
+
+    // read the file into the buffer
+    Gia_FixFileName( pFileName );
+    nFileSize = Gia_FileSize( pFileName );
+    pFile = fopen( pFileName, "rb" );
+    pContents = ABC_ALLOC( char, nFileSize );
+    fread( pContents, nFileSize, 1, pFile );
+    fclose( pFile );
+
+    pNew = Gia_ReadAigerFromMemory( pContents, nFileSize, fCheck );
+    ABC_FREE( pContents );
+    if ( pNew )
+    {
+        pName = Gia_FileNameGeneric( pFileName );
+        pNew->pName = Gia_UtilStrsav( pName );
+//        pNew->pSpec = Ioa_UtilStrsav( pFileName );
+        ABC_FREE( pName );
+    }
+    return pNew;
+}
+
+
+
+/**Function*************************************************************
+
   Synopsis    [Adds one unsigned AIG edge to the output buffer.]
 
   Description [This procedure is a slightly modified version of Armin Biere's

src/aig/gia/giaMan.c

@@ -77,8 +77,9 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_FltFreeP( &p->vTiming );
     Vec_VecFreeP( &p->vClockDoms );
     Vec_IntFreeP( &p->vLutConfigs );
-    Vec_IntFreeP( &p->vCiNumsOrig );
-    Vec_IntFreeP( &p->vCoNumsOrig );
+    Vec_IntFreeP( &p->vUserPiIds );
+    Vec_IntFreeP( &p->vUserPoIds );
+    Vec_IntFreeP( &p->vUserFfIds );
     Vec_IntFreeP( &p->vFlopClasses );
     Vec_IntFreeP( &p->vLevels );
     Vec_IntFreeP( &p->vTruths );

src/base/cmd/cmdPlugin.c

@@ -318,6 +318,69 @@ Vec_Int_t * Abc_ManExpandCex( Gia_Man_t * pGia, Vec_Int_t * vCex )
 
 /**Function*************************************************************
 
+  Synopsis    [Procedure to convert the AIG from text into binary form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static unsigned textToBin(char* text, unsigned long text_sz)
+{
+    char*       dst = text;
+    const char* src = text;
+    unsigned sz, i;
+    sscanf(src, "%lu ", &sz);
+    while(*src++ != ' ');
+
+    for ( i = 0; i < sz; i += 3 )
+    {
+        dst[0] = (char)( (unsigned)src[0] - '0')       | (((unsigned)src[1] - '0') << 6);
+        dst[1] = (char)(((unsigned)src[1] - '0') >> 2) | (((unsigned)src[2] - '0') << 4);
+        dst[2] = (char)(((unsigned)src[2] - '0') >> 4) | (((unsigned)src[3] - '0') << 2);
+        src += 4;
+        dst += 3;
+    }
+    return sz;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG from the text string in the file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Abc_ManReadAig( char * pFileName, char * pToken )
+{
+    Gia_Man_t * pGia = NULL;
+    unsigned nBinaryPart;
+    Vec_Str_t * vStr;
+    char * pStr;
+    vStr = Abc_ManReadFile( pFileName );
+    if ( vStr == NULL )
+        return NULL;
+    pStr = Vec_StrArray( vStr );
+    pStr = strstr( pStr, pToken );
+    if ( pStr != NULL )
+    {
+        pStr += strlen(pToken);
+        nBinaryPart = textToBin( pStr, strlen(pStr) );
+        pGia = Gia_ReadAigerFromMemory( pStr, nBinaryPart, 0 ); 
+    }
+    Vec_StrFree( vStr );
+    return pGia;
+
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -349,9 +412,26 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 */
+
     if ( pAbc->pGia == NULL )
     {
+        if (argc == 2 && strcmp(argv[1], "-h") == 0)
+        {
+            // Run command to produce help string:
+            vCommand = Vec_StrAlloc( 100 );
+            pFileNameBinary = Abc_GetBinaryName( pAbc, argc, argv );
+            Vec_StrAppend( vCommand, pFileNameBinary );
+            Vec_StrAppend( vCommand, " -abc " );
+            Vec_StrAppend( vCommand, argv[0] );
+            Vec_StrAppend( vCommand, " -h" );
+            Vec_StrPush( vCommand, 0 );
+            Util_SignalSystem( Vec_StrArray(vCommand) );
+            Vec_StrFree( vCommand );
+        }
+        else
+        {
             Abc_Print( -1, "Current AIG does not exist (try command &ps).\n" );
+        }
         return 1;
     }
 
@@ -508,6 +588,8 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             Vec_IntFreeP( &vCex );
         }
+        // derive AIG if present
+
     }