Graph isomorphism checking code.

4 files changed, 46 insertions, 11 deletions

diff --git a/src/base/io/io.c b/src/base/io/io.c
index 92dbe9fc..550ff7dd 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1382,12 +1382,16 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pFileName;
     int fWriteSymbols;
     int fCompact;
+    int fUnique;
+    int fVerbose;
     int c;
 
-    fCompact      = 1;
     fWriteSymbols = 0;
+    fCompact      = 1;
+    fUnique       = 0;
+    fVerbose      = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "sch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "scuvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1397,6 +1401,12 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'c':
                 fCompact ^= 1;
                 break;
+            case 'u':
+                fUnique ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -1418,14 +1428,29 @@ int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
         fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
         return 1;
     }
-    Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact );
+    if ( fUnique )
+    {
+        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+        extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+        Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
+        Aig_Man_t * pCan = Saig_ManDupIsoCanonical( pAig, fVerbose );
+        Abc_Ntk_t * pTemp = Abc_NtkFromAigPhase( pCan );
+        Aig_ManStop( pCan );
+        Aig_ManStop( pAig );
+        Io_WriteAiger( pTemp, pFileName, fWriteSymbols, fCompact, fUnique );
+        Abc_NtkDelete( pTemp );
+    }
+    else
+        Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact, fUnique );
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_aiger [-sch] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_aiger [-scuvh] <file>\n" );
     fprintf( pAbc->Err, "\t         writes the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
     fprintf( pAbc->Err, "\t-s     : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
     fprintf( pAbc->Err, "\t-c     : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
+    fprintf( pAbc->Err, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
     fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .aig)\n" );
     return 1;
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index 7a38ae5c..14d688f0 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -96,7 +96,7 @@ extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fZeros, int fCheck )
 /*=== abcReadVerilog.c ========================================================*/
 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_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique );
 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 );
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index e8a018c2..dbaa9138 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -320,7 +320,7 @@ void Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileType_t FileType )
             return;
         }
         if ( FileType == IO_FILE_AIGER )
-            Io_WriteAiger( pNtk, pFileName, 1, 0 );
+            Io_WriteAiger( pNtk, pFileName, 1, 0, 0 );
         else //if ( FileType == IO_FILE_BAF )
             Io_WriteBaf( pNtk, pFileName );
         return;
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 0f725be3..93b17c37 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -581,7 +581,7 @@ int fprintfBz2Aig( bz2file * b, char * fmt, ... ) {
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact )
+void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int fCompact, int fUnique )
 {
     ProgressBar * pProgress;
 //    FILE * pFile;
@@ -591,6 +591,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
     unsigned uLit0, uLit1, uLit;
     bz2file b;
 
+    // define unique writing
+    if ( fUnique )
+    {
+        fWriteSymbols = 0;
+        fCompact = 0;
+    }
+
     // check that the network is valid
     assert( Abc_NtkIsStrash(pNtk) );
     Abc_NtkForEachLatch( pNtk, pObj, i )
@@ -750,10 +757,13 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols, int f
 
     // write the comment
     fprintfBz2Aig( &b, "c" );
-    if ( pNtk->pName && strlen(pNtk->pName) > 0 )
-        fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
-    fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
-    fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
+    if ( !fUnique )
+    {
+        if ( pNtk->pName && strlen(pNtk->pName) > 0 )
+            fprintfBz2Aig( &b, "\n%s%c", pNtk->pName, '\0' );
+        fprintfBz2Aig( &b, "\nThis file was written by ABC on %s\n", Extra_TimeStamp() );
+        fprintfBz2Aig( &b, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" );
+    }
 
     // close the file
     if (b.b) {