Fixing both AIGER readers (read_aiger and &r) to work with AIGER 1.9 (except for liveness properties).

2 files changed, 49 insertions, 11 deletions

diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index d7cff42b..44b0d51a 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -177,11 +177,11 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
 {
     Gia_Man_t * pNew, * pTemp;
     Vec_Int_t * vLits = NULL, * vPoTypes = NULL;
-    Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
+    Vec_Int_t * vNodes, * vDrivers, * vInits = NULL;
     int iObj, iNode0, iNode1, fHieOnly = 0;
-    int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
+    int nTotal, nInputs, nOutputs, nLatches, nAnds, i;
     int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
-    unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
+    unsigned char * pDrivers, * pSymbols, * pCur;
     unsigned uLit0, uLit1, uLit;
 
     // read the parameters (M I L O A + B C J F)
@@ -240,7 +240,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
     }
     if ( nJust || nFair )
     {
-        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
+        fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
         return NULL;
     }
 
@@ -313,17 +313,31 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
     vDrivers = Vec_IntAlloc( nLatches + nOutputs );
     if ( pContents[3] == ' ' ) // standard AIGER
     {
+        vInits = Vec_IntAlloc( nLatches );
         pCur = pDrivers;
         for ( i = 0; i < nLatches; i++ )
         {
-            uLit0 = atoi( (char *)pCur );  while ( *pCur++ != '\n' );
+            uLit0 = atoi( (char *)pCur );   
+            while ( *pCur != ' ' && *pCur != '\n' ) 
+                pCur++;
+            if ( *pCur == ' ' )
+            {
+                pCur++;
+                Vec_IntPush( vInits, atoi( (char *)pCur ) );
+                while ( *pCur++ != '\n' );
+            }
+            else
+            {
+                pCur++;
+                Vec_IntPush( vInits, 0 );
+            }
             iNode0 = Abc_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' );
+            uLit0 = atoi( (char *)pCur );   while ( *pCur++ != '\n' );
             iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );
             Vec_IntPush( vDrivers, iNode0 );
         }
@@ -751,7 +765,31 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipS
     }
 */
 
-//    pNew->nAnd2Delay = 5;
+    if ( vInits && Vec_IntSum(vInits) )
+    {
+        char * pInit = ABC_ALLOC( char, Vec_IntSize(vInits) + 1 );
+        Gia_Obj_t * pObj;
+        int i;
+        assert( Vec_IntSize(vInits) == Gia_ManRegNum(pNew) );
+        Gia_ManForEachRo( pNew, pObj, i )
+        {
+            if ( Vec_IntEntry(vInits, i) == 0 )
+                pInit[i] = '0';
+            else if ( Vec_IntEntry(vInits, i) == 1 )
+                pInit[i] = '1';
+            else 
+            {
+                assert( Vec_IntEntry(vInits, i) == Abc_Var2Lit(Gia_ObjId(pNew, pObj), 0) );
+                pInit[i] = 'X';
+            }
+        }
+        pInit[i] = 0;
+        pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 );
+        pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0;
+        Gia_ManStop( pTemp );
+        ABC_FREE( pInit );
+    }
+    Vec_IntFreeP( &vInits );
     return pNew;
 }
 
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index c063f337..b936ceb2 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -328,7 +328,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     }
     if ( nJust || nFair )
     {
-        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
+        fprintf( stdout, "Reading AIGER files with liveness properties is currently not supported.\n" );
         ABC_FREE( pContents );
         return NULL;
     }
@@ -424,10 +424,10 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
             if ( *pCur == ' ' ) // read initial value
             {
                 pCur++;
-                if ( atoi( pCur ) == 1 )
-                    Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) );
-                else if ( atoi( pCur ) == 0 )
+                if ( atoi( pCur ) == 0 )
                     Abc_LatchSetInit0( Abc_NtkBox(pNtkNew, i) );
+                else if ( atoi( pCur ) == 1 )
+                    Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) );
                 else 
                     Abc_LatchSetInitDc( Abc_NtkBox(pNtkNew, i) );
                 while ( *pCur != ' ' && *pCur != '\n' ) pCur++;