Added dumping CEXes in AIGER format.

3 files changed, 134 insertions, 0 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index 7f077e29..d8277b08 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -48,6 +48,7 @@ static int IoCommandReadStatus  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWrite       ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteHie    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteAiger  ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBaf    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBblif  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBlif   ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -111,6 +112,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write",         IoCommandWrite,        0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_hie",     IoCommandWriteHie,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_aiger",   IoCommandWriteAiger,   0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_aiger_cex",   IoCommandWriteAigerCex,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_baf",     IoCommandWriteBaf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_bblif",   IoCommandWriteBblif,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
@@ -1434,6 +1436,52 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    char * pFileName;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( pAbc->pCex == NULL )
+    {
+        fprintf( pAbc->Out, "There is no current CEX.\n" );
+        return 0;
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    // get the output file name
+    pFileName = argv[globalUtilOptind];
+    Io_WriteAigerCex( pAbc->pCex, pAbc->pNtkCur, pAbc->pGia, pFileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_aiger_cex [-h] <file>\n" );
+    fprintf( pAbc->Err, "\t         writes the current CEX in the AIGER format (http://fmv.jku.at/aiger)\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     char * pFileName;
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index 841fce40..fa3f6240 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -97,6 +97,7 @@ extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fZeros, int fCheck )
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcWriteAiger.c =========================================================*/
 extern void               Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact );
+extern void               Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName );
 /*=== abcWriteBaf.c ===========================================================*/
 extern void               Io_WriteBaf( Abc_Ntk_t * pNtk, char * pFileName );
 /*=== abcWriteBblif.c ===========================================================*/
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 1087af4f..18264d6b 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -752,6 +752,91 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
     ABC_FREE(b.buf);
 }
 
+
+#include "giaAig.h"
+#include "saig.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_WriteAigerCex( Abc_Cex_t * pCex, Abc_Ntk_t * pNtk, void * pG, char * pFileName )
+{
+    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    FILE * pFile;
+    Aig_Man_t * pAig;
+    Aig_Obj_t * pObj, * pObj2;
+    Gia_Man_t * pGia = (Gia_Man_t *)pG;
+    int k, f, b;
+    assert( pCex != NULL );
+
+    // derive AIG
+    if ( pNtk != NULL && 
+         Abc_NtkPiNum(pNtk)    == pCex->nPis && 
+         Abc_NtkLatchNum(pNtk) == pCex->nRegs )
+    {
+        pAig = Abc_NtkToDar( pNtk, 0, 1 );
+    }
+    else if ( pGia != NULL && 
+         Gia_ManPiNum(pGia)  == pCex->nPis && 
+         Gia_ManRegNum(pGia) == pCex->nRegs )
+    {
+        pAig = Gia_ManToAigSimple( pGia );
+    }
+    else
+    {
+        printf( "AIG parameters do not match those of the CEX.\n" );
+        return;
+    }
+
+    // create output file
+    pFile = fopen( pFileName, "wb" );
+    fprintf( pFile, "1\n" );
+    b = pCex->nRegs;
+    for ( k = 0; k < pCex->nRegs; k++ )
+        fprintf( pFile, "0" );
+    fprintf( pFile, " " );
+    Aig_ManCleanMarkA( pAig );
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        for ( k = 0; k < pCex->nPis; k++ )
+        {
+            fprintf( pFile, "%d", Aig_InfoHasBit(pCex->pData, b) );
+            Aig_ManPi( pAig, k )->fMarkA = Aig_InfoHasBit(pCex->pData, b++);
+        }
+        fprintf( pFile, " " );
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) &
+                           (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj));
+        Saig_ManForEachPo( pAig, pObj, k )
+            fprintf( pFile, "%d", pObj->fMarkA );
+        fprintf( pFile, " " );
+        Saig_ManForEachLi( pAig, pObj, k )
+            fprintf( pFile, "%d", pObj->fMarkA );
+        fprintf( pFile, "\n" );
+        if ( f == pCex->iFrame )
+            break;
+        Saig_ManForEachLi( pAig, pObj, k )
+            fprintf( pFile, "%d", pObj->fMarkA );
+        fprintf( pFile, " " );
+        Saig_ManForEachLiLo( pAig, pObj, pObj2, k )
+            pObj2->fMarkA = pObj->fMarkA;
+    }  
+    assert( b == pCex->nBits );
+    fclose( pFile );
+    Aig_ManCleanMarkA( pAig );
+    Aig_ManStop( pAig );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////