Changes to read multi-output testcases described using AIGER 1.9.

12 files changed, 427 insertions, 66 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 346302c5..731f7c84 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -689,6 +689,7 @@ extern void            Aig_ManSetPhase( Aig_Man_t * pAig );
 extern Vec_Ptr_t *     Aig_ManMuxesCollect( Aig_Man_t * pAig );
 extern void            Aig_ManMuxesDeref( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
 extern void            Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes );
+extern void            Aig_ManInvertConstraints( Aig_Man_t * pAig );
 
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 5e58fcbe..8cbaa63b 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -1565,6 +1565,29 @@ void Aig_ManMuxesRef( Aig_Man_t * pAig, Vec_Ptr_t * vMuxes )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Complements the constraint outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManInvertConstraints( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    if ( Aig_ManConstrNum(pAig) == 0 )
+        return;
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        if ( i >= Saig_ManPoNum(pAig) - Aig_ManConstrNum(pAig) )
+            Aig_ObjChild0Flip( pObj );
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index d3165526..5ec8de3f 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -819,6 +819,8 @@ extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
 extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs );
+extern void                Gia_ManInvertConstraints( Gia_Man_t * pAig );
+
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
 extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 9be5681a..a7d8e481 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -350,6 +350,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
     Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
     int iObj, iNode0, iNode1;
     int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
+    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
     unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
     char * pContents, * pName;
     unsigned uLit0, uLit1, uLit;
@@ -370,25 +371,76 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
         return NULL;
     }
 
-    // read the file type
-    pCur = (unsigned char *)pContents;  while ( *pCur++ != ' ' );
+    // read the parameters (M I L O A + B C J F)
+    pCur = (unsigned char *)pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of objects
-    nTotal = atoi( (char *)pCur );    while ( *pCur++ != ' ' );
+    nTotal = atoi( pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of inputs
-    nInputs = atoi( (char *)pCur );   while ( *pCur++ != ' ' );
+    nInputs = atoi( pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of latches
-    nLatches = atoi( (char *)pCur );  while ( *pCur++ != ' ' );
+    nLatches = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of outputs
-    nOutputs = atoi( (char *)pCur );  while ( *pCur++ != ' ' );
+    nOutputs = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of nodes
-    nAnds = atoi( (char *)pCur );     while ( *pCur++ != '\n' );  
+    nAnds = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+    if ( *pCur == ' ' )
+    {
+        assert( nOutputs == 0 );
+        // read the number of properties
+        pCur++;
+        nBad = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nBad;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nConstr = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nConstr;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nJust = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nJust;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nFair = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nFair;
+    }
+    if ( *pCur != '\n' )
+    {
+        fprintf( stdout, "The parameter line is in a wrong format.\n" );
+        ABC_FREE( pContents );
+        return NULL;
+    }
+    pCur++;
+
     // check the parameters
     if ( nTotal != nInputs + nLatches + nAnds )
     {
+        fprintf( stdout, "The number of objects does not match.\n" );
         ABC_FREE( pContents );
-        fprintf( stdout, "The paramters are wrong.\n" );
         return NULL;
     }
+    if ( nJust || nFair )
+    {
+        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
+        ABC_FREE( pContents );
+        return NULL;
+    }
+
+    if ( nConstr )
+    {
+        if ( nConstr == 1 )
+            fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
+        else
+            fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
+    }
 
     // allocate the empty AIG
     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
@@ -396,6 +448,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
     pNew->pName = Gia_UtilStrsav( pName );
 //    pNew->pSpec = Gia_UtilStrsav( pFileName );
     ABC_FREE( pName );
+    pNew->nConstrs = nConstr;
 
     // prepare the array of nodes
     vNodes = Vec_IntAlloc( 1 + nTotal );
@@ -548,6 +601,10 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck )
     }
     Vec_IntFree( vNodes );
 
+    // update polarity of the additional outputs
+    if ( nBad || nConstr || nJust || nFair )
+        Gia_ManInvertConstraints( pNew );
+
     // skipping the comments
 /*
     // check the result
@@ -580,31 +637,81 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
     Vec_Int_t * vNodes, * vDrivers;//, * vTerms;
     int iObj, iNode0, iNode1;
     int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
+    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
     unsigned char * pDrivers, * pSymbols, * pCur;//, * pType;
     unsigned uLit0, uLit1, uLit;
 
-    // read the file type
-    pCur = (unsigned char *)pContents;  while ( *pCur++ != ' ' );
+    // read the parameters (M I L O A + B C J F)
+    pCur = (unsigned char *)pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of objects
-    nTotal = atoi( (char *)pCur );    while ( *pCur++ != ' ' );
+    nTotal = atoi( pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of inputs
-    nInputs = atoi( (char *)pCur );   while ( *pCur++ != ' ' );
+    nInputs = atoi( pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of latches
-    nLatches = atoi( (char *)pCur );  while ( *pCur++ != ' ' );
+    nLatches = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of outputs
-    nOutputs = atoi( (char *)pCur );  while ( *pCur++ != ' ' );
+    nOutputs = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of nodes
-    nAnds = atoi( (char *)pCur );     while ( *pCur++ != '\n' );  
+    nAnds = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+    if ( *pCur == ' ' )
+    {
+        assert( nOutputs == 0 );
+        // read the number of properties
+        pCur++;
+        nBad = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nBad;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nConstr = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nConstr;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nJust = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nJust;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nFair = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nFair;
+    }
+    if ( *pCur != '\n' )
+    {
+        fprintf( stdout, "The parameter line is in a wrong format.\n" );
+        return NULL;
+    }
+    pCur++;
+
     // check the parameters
     if ( nTotal != nInputs + nLatches + nAnds )
     {
-        ABC_FREE( pContents );
-        fprintf( stdout, "The paramters are wrong.\n" );
+        fprintf( stdout, "The number of objects does not match.\n" );
+        return NULL;
+    }
+    if ( nJust || nFair )
+    {
+        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
         return NULL;
     }
 
+    if ( nConstr )
+    {
+        if ( nConstr == 1 )
+            fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
+        else
+            fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
+    }
+
     // allocate the empty AIG
     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
+    pNew->nConstrs = nConstr;
 
     // prepare the array of nodes
     vNodes = Vec_IntAlloc( 1 + nTotal );
@@ -903,6 +1010,11 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         return NULL;
     }
 */
+
+    // update polarity of the additional outputs
+    if ( nBad || nConstr || nJust || nFair )
+        Gia_ManInvertConstraints( pNew );
+
     // clean the PO drivers
     if ( vPoTypes )
     {
@@ -1243,14 +1355,19 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         p = pInit;
 
     // write the header "M I L O A" where M = I + L + A
-    fprintf( pFile, "aig%s %u %u %u %u %u\n", 
+    fprintf( pFile, "aig%s %u %u %u %u %u", 
         fCompact? "2" : "",
         Gia_ManCiNum(p) + Gia_ManAndNum(p), 
         Gia_ManPiNum(p),
         Gia_ManRegNum(p),
-        Gia_ManPoNum(p),
+        Gia_ManConstrNum(p) ? 0 : Gia_ManPoNum(p),
         Gia_ManAndNum(p) );
+    // write the extended header "B C J F"
+    if ( Gia_ManConstrNum(p) )
+        fprintf( pFile, " %u %u", Gia_ManPoNum(p) - Gia_ManConstrNum(p), Gia_ManConstrNum(p) );
+    fprintf( pFile, "\n" ); 
 
+    Gia_ManInvertConstraints( p );
     if ( !fCompact ) 
     {
         // write latch drivers
@@ -1268,6 +1385,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         Vec_StrFree( vBinary );
         Vec_IntFree( vLits );
     }
+    Gia_ManInvertConstraints( p );
 
     // write the nodes into the buffer
     Pos = 0;
@@ -1372,6 +1490,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         fwrite( Buffer, 1, 4, pFile );
         fwrite( p->pSwitching, 1, nSize, pFile );
     }
+/*
     // write constraints
     if ( p->nConstrs )
     {
@@ -1380,6 +1499,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
         fprintf( pFile, "c" );
         fwrite( Buffer, 1, 4, pFile );
     }
+*/
     // write name
     if ( p->pName )
         fprintf( pFile, "n%s%c", p->pName, '\0' );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index b9a50220..f19f0602 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -1224,6 +1224,30 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs )
     return RetValue;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Complements the constraint outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManInvertConstraints( Gia_Man_t * pAig )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    if ( Gia_ManConstrNum(pAig) == 0 )
+        return;
+    Gia_ManForEachPo( pAig, pObj, i )
+    {
+        if ( i >= Gia_ManPoNum(pAig) - Gia_ManConstrNum(pAig) )
+            Gia_ObjFlipFaninC0( pObj );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c
index 096e82e4..17c93e58 100644
--- a/src/aig/ioa/ioaReadAig.c
+++ b/src/aig/ioa/ioaReadAig.c
@@ -109,6 +109,7 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
     Aig_Obj_t * pObj, * pNode0, * pNode1;
     Aig_Man_t * pNew;
     int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
+    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
     char * pDrivers, * pSymbols, * pCur;//, * pType;
     unsigned uLit0, uLit1, uLit;
 
@@ -119,27 +120,77 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
         return NULL;
     }
 
-    // read the file type
-    pCur = pContents;         while ( *pCur++ != ' ' );
+    // read the parameters (M I L O A + B C J F)
+    pCur = pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of objects
-    nTotal = atoi( pCur );    while ( *pCur++ != ' ' );
+    nTotal = atoi( pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of inputs
-    nInputs = atoi( pCur );   while ( *pCur++ != ' ' );
+    nInputs = atoi( pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of latches
-    nLatches = atoi( pCur );  while ( *pCur++ != ' ' );
+    nLatches = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of outputs
-    nOutputs = atoi( pCur );  while ( *pCur++ != ' ' );
+    nOutputs = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of nodes
-    nAnds = atoi( pCur );     while ( *pCur++ != '\n' );  
+    nAnds = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+    if ( *pCur == ' ' )
+    {
+        assert( nOutputs == 0 );
+        // read the number of properties
+        pCur++;
+        nBad = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nBad;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nConstr = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nConstr;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nJust = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nJust;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nFair = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nFair;
+    }
+    if ( *pCur != '\n' )
+    {
+        fprintf( stdout, "The parameter line is in a wrong format.\n" );
+        return NULL;
+    }
+    pCur++;
+
     // check the parameters
     if ( nTotal != nInputs + nLatches + nAnds )
     {
-        fprintf( stdout, "The paramters are wrong.\n" );
+        fprintf( stdout, "The number of objects does not match.\n" );
+        return NULL;
+    }
+    if ( nJust || nFair )
+    {
+        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
         return NULL;
     }
 
+    if ( nConstr )
+    {
+        if ( nConstr == 1 )
+            fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
+        else
+            fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
+    }
+
     // allocate the empty AIG
     pNew = Aig_ManStart( nAnds );
+    pNew->nConstrs = nConstr;
 
     // prepare the array of nodes
     vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
@@ -352,6 +403,10 @@ Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck
     Aig_ManCleanup( pNew );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(pNew) );
 
+    // update polarity of the additional outputs
+    if ( nBad || nConstr || nJust || nFair )
+        Aig_ManInvertConstraints( pNew );
+
     // check the result
     if ( fCheck && !Aig_ManCheck( pNew ) )
     {
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index 7aa975f2..2f682775 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -466,18 +466,23 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
         Ioa_ObjSetAigerNum( pObj, nNodes++ );
 
     // write the header "M I L O A" where M = I + L + A
-    fprintf( pFile, "aig%s %u %u %u %u %u\n", 
+    fprintf( pFile, "aig%s %u %u %u %u %u", 
         fCompact? "2" : "",
         Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan), 
         Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan),
         Aig_ManRegNum(pMan),
-        Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
+        Aig_ManConstrNum(pMan) ? 0 : Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan),
         Aig_ManNodeNum(pMan) );
+    // write the extended header "B C J F"
+    if ( Aig_ManConstrNum(pMan) )
+        fprintf( pFile, " %u %u", Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) - Aig_ManConstrNum(pMan), Aig_ManConstrNum(pMan) );
+    fprintf( pFile, "\n" ); 
 
     // if the driver node is a constant, we need to complement the literal below
     // because, in the AIGER format, literal 0/1 is represented as number 0/1
     // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
 
+    Aig_ManInvertConstraints( pMan );
     if ( !fCompact ) 
     {
         // write latch drivers
@@ -502,6 +507,7 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int
         Vec_StrFree( vBinary );
         Vec_IntFree( vLits );
     }
+    Aig_ManInvertConstraints( pMan );
 
     // write the nodes into the buffer
     Pos = 0;
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index de5bc663..aaf6d534 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -938,6 +938,8 @@ extern ABC_DLL Vec_Int_t *        Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
 extern ABC_DLL void               Abc_NtkTransferCopy( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkInvertConstraints( Abc_Ntk_t * pNtk );
+
 
 /*=== abcVerify.c ==========================================================*/
 extern ABC_DLL int *              Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 1e5777b9..e002347b 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -1909,6 +1909,30 @@ void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Complements the constraint outputs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkInvertConstraints( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    if ( Abc_NtkConstrNum(pNtk) == 0 )
+        return;
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        if ( i >= Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
+            Abc_ObjXorFaninC( pObj, 0 );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 02694856..c5fc491f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -20033,6 +20033,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFrames;
     int nConfs; 
     int nProps; 
+    int fRemove;
     int fStruct;
     int fInvert;
     int fOldAlgo;
@@ -20045,13 +20046,14 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
     nFrames   =      1;
     nConfs    =   1000;
     nProps    =   1000;
+    fRemove   =      0;
     fStruct   =      0;
     fInvert   =      0;    
     fOldAlgo  =      0;
     fVerbose  =      0;
     nConstrs  =      0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNsiavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrsiavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20099,6 +20101,9 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nConstrs < 0 ) 
                 goto usage;
             break;
+        case 'r':
+            fRemove ^= 1;
+            break;
         case 's':
             fStruct ^= 1;
             break;
@@ -20132,21 +20137,26 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
+    if ( fRemove )
+    {
+        if ( Abc_NtkConstrNum(pNtk) == 0 )
+        {
+            Abc_Print( -1, "Constraints are not defined.\n" );
+            return 0;
+        }
+        Abc_Print( 1, "Constraints are converted to be primary outputs.\n" );
+        pNtk->nConstrs = 0;
+        return 0;
+    }
     // consider the case of already defined constraints
     if ( Abc_NtkConstrNum(pNtk) > 0 )
     {
         extern void Abc_NtkDarConstrProfile( Abc_Ntk_t * pNtk, int fVerbose );
         if ( fInvert )
         {
-            Abc_Obj_t * pObj;
-            int i;
-            Abc_NtkForEachPo( pNtk, pObj, i )
-            {
-                if ( i >= Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) )
-                    Abc_ObjXorFaninC( pObj, 0 );
-            }
+            Abc_NtkInvertConstraints( pNtk );
             if ( Abc_NtkConstrNum(pNtk) == 1 )
-                Abc_Print( 1, "The outputs of %d constraint is complemented.\n", Abc_NtkConstrNum(pNtk) );
+                Abc_Print( 1, "The output of %d constraint is complemented.\n", Abc_NtkConstrNum(pNtk) );
             else
                 Abc_Print( 1, "The outputs of %d constraints are complemented.\n", Abc_NtkConstrNum(pNtk) );
         }
@@ -20175,7 +20185,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_NtkDarConstr( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose );
     return 0;
 usage:
-    Abc_Print( -2, "usage: constr [-FCPN num] [-isavh]\n" );
+    Abc_Print( -2, "usage: constr [-FCPN num] [-risavh]\n" );
     Abc_Print( -2, "\t         a toolkit for constraint manipulation\n" );
     Abc_Print( -2, "\t         if constraints are absent, detect them functionally\n" );
     Abc_Print( -2, "\t         if constraints are present, profiles them using random simulation\n" );
@@ -20183,6 +20193,7 @@ usage:
     Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs );
     Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps );
     Abc_Print( -2, "\t-N num : manually set the last <num> POs to be constraints [default = %d]\n", nConstrs );
+    Abc_Print( -2, "\t-r     : manually remove the constraints [default = %s]\n", fRemove? "yes": "no" );
     Abc_Print( -2, "\t-i     : toggle inverting already defined constraints [default = %s]\n", fInvert? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle using structural detection methods [default = %s]\n", fStruct? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggle fast implication detection [default = %s]\n", !fOldAlgo? "yes": "no" );
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index a5f6fb1d..13987a1b 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -233,7 +233,9 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     Vec_Int_t * vLits = NULL;
     Abc_Obj_t * pObj, * pNode0, * pNode1;
     Abc_Ntk_t * pNtkNew;
-    int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize = -1, iTerm, nDigits, i;
+    int nTotal, nInputs, nOutputs, nLatches, nAnds;
+    int nBad = 0, nConstr = 0, nJust = 0, nFair = 0;
+    int nFileSize = -1, iTerm, nDigits, i;
     char * pContents, * pDrivers = NULL, * pSymbols, * pCur, * pName, * pType;
     unsigned uLit0, uLit1, uLit;
 
@@ -257,36 +259,88 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
     {
         fprintf( stdout, "Wrong input file format.\n" );
-        free( pContents );
+        ABC_FREE( pContents );
         return NULL;
     }
 
-    // allocate the empty AIG
-    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
-    pName = Extra_FileNameGeneric( pFileName );
-    pNtkNew->pName = Extra_UtilStrsav( pName );
-    pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
-    ABC_FREE( pName );
-
-
-    // read the file type
-    pCur = pContents;         while ( *pCur++ != ' ' );
+    // read the parameters (M I L O A + B C J F)
+    pCur = pContents;         while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of objects
-    nTotal = atoi( pCur );    while ( *pCur++ != ' ' );
+    nTotal = atoi( pCur );    while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of inputs
-    nInputs = atoi( pCur );   while ( *pCur++ != ' ' );
+    nInputs = atoi( pCur );   while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of latches
-    nLatches = atoi( pCur );  while ( *pCur++ != ' ' );
+    nLatches = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of outputs
-    nOutputs = atoi( pCur );  while ( *pCur++ != ' ' );
+    nOutputs = atoi( pCur );  while ( *pCur != ' ' ) pCur++; pCur++;
     // read the number of nodes
-    nAnds = atoi( pCur );     while ( *pCur++ != '\n' );  
+    nAnds = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+    if ( *pCur == ' ' )
+    {
+        assert( nOutputs == 0 );
+        // read the number of properties
+        pCur++;
+        nBad = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nBad;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nConstr = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nConstr;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nJust = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nJust;
+    }
+    if ( *pCur == ' ' )
+    {
+        // read the number of properties
+        pCur++;
+        nFair = atoi( pCur );     while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+        nOutputs += nFair;
+    }
+    if ( *pCur != '\n' )
+    {
+        fprintf( stdout, "The parameter line is in a wrong format.\n" );
+        ABC_FREE( pContents );
+        return NULL;
+    }
+    pCur++;
+
     // check the parameters
     if ( nTotal != nInputs + nLatches + nAnds )
     {
-        fprintf( stdout, "The paramters are wrong.\n" );
+        fprintf( stdout, "The number of objects does not match.\n" );
+        ABC_FREE( pContents );
         return NULL;
     }
+    if ( nJust || nFair )
+    {
+        fprintf( stdout, "Reading AIGER files with liveness properties are currently not supported.\n" );
+        ABC_FREE( pContents );
+        return NULL;
+    }
+
+    if ( nConstr )
+    {
+        if ( nConstr == 1 )
+            fprintf( stdout, "Warning: The last output is interpreted as a constraint.\n" );
+        else
+            fprintf( stdout, "Warning: The last %d outputs are interpreted as constraints.\n", nConstr );
+    }
+
+    // allocate the empty AIG
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
+    pName = Extra_FileNameGeneric( pFileName );
+    pNtkNew->pName = Extra_UtilStrsav( pName );
+    pNtkNew->pSpec = Extra_UtilStrsav( pFileName );
+    ABC_FREE( pName );
+    pNtkNew->nConstrs = nConstr;
 
     // prepare the array of nodes
     vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
@@ -359,7 +413,25 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     {
         Abc_NtkForEachLatchInput( pNtkNew, pObj, i )
         {
-            uLit0 = atoi( pCur );  while ( *pCur++ != '\n' );
+            uLit0 = atoi( pCur );  while ( *pCur != ' ' && *pCur != '\n' ) pCur++; 
+            if ( *pCur == ' ' ) // read initial value
+            {
+                pCur++;
+                if ( atoi( pCur ) == 1 )
+                    Abc_LatchSetInit1( Abc_NtkBox(pNtkNew, i) );
+                else if ( atoi( pCur ) == 0 )
+                    Abc_LatchSetInit0( Abc_NtkBox(pNtkNew, i) );
+                else 
+                    Abc_LatchSetInitDc( Abc_NtkBox(pNtkNew, i) );
+                while ( *pCur != ' ' && *pCur != '\n' ) pCur++;
+            }
+            if ( *pCur != '\n' )
+            {
+                fprintf( stdout, "The initial value of latch number %d is not recongnized.\n", i );
+                return NULL;
+            }
+            pCur++;
+
             pNode0 = Abc_ObjNotCond( (Abc_Obj_t *)Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
             Abc_ObjAddFanin( pObj, pNode0 );
         }
@@ -403,7 +475,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
                 vTerms = pNtkNew->vPis;
             else if ( *pCur == 'l' )
                 vTerms = pNtkNew->vBoxes;
-            else if ( *pCur == 'o' )
+            else if ( *pCur == 'o' || *pCur == 'b' || *pCur == 'c' || *pCur == 'j' || *pCur == 'f' )
                 vTerms = pNtkNew->vPos;
             else
             {
@@ -486,6 +558,10 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     // remove the extra nodes
     Abc_AigCleanup( (Abc_Aig_t *)pNtkNew->pManFunc );
 
+    // update polarity of the additional outputs
+    if ( nBad || nConstr || nJust || nFair )
+        Abc_NtkInvertConstraints( pNtkNew );
+
     // check the result
     if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )
     {
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 18264d6b..9ab0905e 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -296,18 +296,23 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i
         Io_ObjSetAigerNum( pObj, nNodes++ );
 
     // write the header "M I L O A" where M = I + L + A
-    fprintf( pFile, "aig%s %u %u %u %u %u\n", 
+    fprintf( pFile, "aig%s %u %u %u %u %u", 
         fCompact? "2" : "",
         Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
         Abc_NtkPiNum(pNtk),
         Abc_NtkLatchNum(pNtk),
-        Abc_NtkPoNum(pNtk),
+        Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
         Abc_NtkNodeNum(pNtk) );
+    // write the extended header "B C J F"
+    if ( Abc_NtkConstrNum(pNtk) )
+        fprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
+    fprintf( pFile, "\n" );
 
     // if the driver node is a constant, we need to complement the literal below
     // because, in the AIGER format, literal 0/1 is represented as number 0/1
     // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
 
+    Abc_NtkInvertConstraints( pNtk );
     if ( !fCompact ) 
     {
         // write latch drivers
@@ -331,6 +336,7 @@ void Io_WriteAiger_old( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, i
         Vec_StrFree( vBinary );
         Vec_IntFree( vLits );
     }
+    Abc_NtkInvertConstraints( pNtk );
 
     // write the nodes into the buffer
     Pos = 0;
@@ -427,30 +433,35 @@ void Io_WriteAigerGz( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols )
         Io_ObjSetAigerNum( pObj, nNodes++ );
 
     // write the header "M I L O A" where M = I + L + A
-    gzprintf( pFile, "aig %u %u %u %u %u\n", 
+    gzprintf( pFile, "aig %u %u %u %u %u", 
               Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
               Abc_NtkPiNum(pNtk),
               Abc_NtkLatchNum(pNtk),
-              Abc_NtkPoNum(pNtk),
+              Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
               Abc_NtkNodeNum(pNtk) );
+    // write the extended header "B C J F"
+    if ( Abc_NtkConstrNum(pNtk) )
+        gzprintf( pFile, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
+    gzprintf( pFile, "\n" ); 
 
     // if the driver node is a constant, we need to complement the literal below
     // because, in the AIGER format, literal 0/1 is represented as number 0/1
     // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
 
     // write latch drivers
+    Abc_NtkInvertConstraints( pNtk );
     Abc_NtkForEachLatchInput( pNtk, pObj, i )
     {
         pDriver = Abc_ObjFanin0(pObj);
         gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
     }
-
     // write PO drivers
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
         pDriver = Abc_ObjFanin0(pObj);
         gzprintf( pFile, "%u\n", Io_ObjMakeLit( Io_ObjAigerNum(pDriver), Abc_ObjFaninC0(pObj) ^ (Io_ObjAigerNum(pDriver) == 0) ) );
     }
+    Abc_NtkInvertConstraints( pNtk );
 
     // write the nodes into the buffer
     Pos = 0;
@@ -628,18 +639,23 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
         Io_ObjSetAigerNum( pObj, nNodes++ );
 
     // write the header "M I L O A" where M = I + L + A
-    fprintfBz2Aig( &b, "aig%s %u %u %u %u %u\n", 
+    fprintfBz2Aig( &b, "aig%s %u %u %u %u %u", 
         fCompact? "2" : "",
         Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) + Abc_NtkNodeNum(pNtk), 
         Abc_NtkPiNum(pNtk),
         Abc_NtkLatchNum(pNtk),
-        Abc_NtkPoNum(pNtk),
+        Abc_NtkConstrNum(pNtk) ? 0 : Abc_NtkPoNum(pNtk),
         Abc_NtkNodeNum(pNtk) );
+    // write the extended header "B C J F"
+    if ( Abc_NtkConstrNum(pNtk) )
+        fprintfBz2Aig( &b, " %u %u", Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk), Abc_NtkConstrNum(pNtk) );
+    fprintfBz2Aig( &b, "\n" );
 
     // if the driver node is a constant, we need to complement the literal below
     // because, in the AIGER format, literal 0/1 is represented as number 0/1
     // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0
 
+    Abc_NtkInvertConstraints( pNtk );
     if ( !fCompact ) 
     {
         // write latch drivers
@@ -675,6 +691,7 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
         Vec_StrFree( vBinary );
         Vec_IntFree( vLits );
     }
+    Abc_NtkInvertConstraints( pNtk );
 
     // write the nodes into the buffer
     Pos = 0;