Isomorphism checking code.

src/aig/gia/gia.h

@@ -623,6 +623,7 @@ extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int
 extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
 extern Vec_Str_t *         Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p );
 extern Vec_Str_t *         Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
+extern void                Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName );
 /*=== giaBidec.c ===========================================================*/
 extern unsigned *          Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
 extern Gia_Man_t *         Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
@@ -735,6 +736,9 @@ extern void                Gia_ManHashProfile( Gia_Man_t * p );
 extern int                 Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
 /*=== giaIf.c ===========================================================*/
 extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
+/*=== giaIso.c ===========================================================*/
+extern Gia_Man_t *         Gia_ManIsoCanonicize( Gia_Man_t * p, int fVerbose );
+extern Gia_Man_t *         Gia_ManIsoReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
 /*=== giaLogic.c ===========================================================*/
 extern void                Gia_ManTestDistance( Gia_Man_t * p );
 extern void                Gia_ManSolveProblem( Gia_Man_t * pGia, Emb_Par_t * pPars );

src/aig/gia/giaAiger.c

@@ -1614,7 +1614,7 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int nNodes = 0, i, uLit, uLit0, uLit1; 
     // set the node numbers to be used in the output file
-    Gia_ManConst1(p)->Value = nNodes++;
+    Gia_ManConst0(p)->Value = nNodes++;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = nNodes++;
     Gia_ManForEachAnd( p, pObj, i )
@@ -1638,7 +1638,6 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
     Gia_ManForEachRi( p, pObj, i )
     {
         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-//        fprintf( pFile, "%u\n", uLit );
         Vec_StrPrintNum( vBuffer, uLit );
         Vec_StrPrintStr( vBuffer, "\n" );
     }
@@ -1647,7 +1646,6 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
     Gia_ManForEachPo( p, pObj, i )
     {
         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-//        fprintf( pFile, "%u\n", uLit );
         Vec_StrPrintNum( vBuffer, uLit );
         Vec_StrPrintStr( vBuffer, "\n" );
     }
@@ -1679,7 +1677,7 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
   The CI/CO/AND nodes are assumed to be ordered according to some rule.
   The resulting buffer should be deallocated by the user.]
   
-  SideEffects [Note that in vCos, the latches should be ordered first!!!]
+  SideEffects [Note that in vCos, PIs are order first, followed by latches!]
 
   SeeAlso     []
 
@@ -1690,7 +1688,7 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
     Gia_Obj_t * pObj;
     int nNodes = 0, i, uLit, uLit0, uLit1; 
     // set the node numbers to be used in the output file
-    Gia_ManConst1(p)->Value = nNodes++;
+    Gia_ManConst0(p)->Value = nNodes++;
     Gia_ManForEachObjVec( vCis, p, pObj, i )
     {
         assert( Gia_ObjIsCi(pObj) );
@@ -1720,8 +1718,19 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
     Gia_ManForEachObjVec( vCos, p, pObj, i )
     {
         assert( Gia_ObjIsCo(pObj) );
+        if ( i < Vec_IntSize(vCos) - nRegs )
+            continue;
+        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        Vec_StrPrintNum( vBuffer, uLit );
+        Vec_StrPrintStr( vBuffer, "\n" );
+    }
+    // write output drivers
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
+    {
+        assert( Gia_ObjIsCo(pObj) );
+        if ( i >= Vec_IntSize(vCos) - nRegs )
+            continue;
         uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
-//        fprintf( pFile, "%u\n", uLit );
         Vec_StrPrintNum( vBuffer, uLit );
         Vec_StrPrintStr( vBuffer, "\n" );
     }
@@ -1746,6 +1755,40 @@ Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
     return vBuffer;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName )
+{
+    FILE * pFile;
+    Vec_Str_t * vStr;
+    if ( Gia_ManPoNum(pInit) == 0 )
+    {
+        printf( "Gia_WriteAigerSimple(): AIG cannot be written because it has no POs.\n" );
+        return;
+    }
+    // start the output stream
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        fprintf( stdout, "Gia_WriteAigerSimple(): Cannot open the output file \"%s\".\n", pFileName );
+        return;
+    }
+    // write the buffer
+    vStr = Gia_WriteAigerIntoMemoryStr( pInit );
+    fwrite( Vec_StrArray(vStr), 1, Vec_StrSize(vStr), pFile );
+    Vec_StrFree( vStr );
+    fclose( pFile );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaDup.c

@@ -1791,7 +1791,7 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos )
         Gia_ManDupCones_rec( p, pObj, vLeaves, vNodes, vRoots );
 
     // start the new manager
-    Gia_ManFillValue( p );
+//    Gia_ManFillValue( p );
     pNew = Gia_ManStart( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1);
     pNew->pName = Abc_UtilStrsav( p->pName );
     // map the constant node

src/base/abci/abc.c

@@ -21982,11 +21982,19 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     char * pFileName;
     char ** pArgvNew;
     int c, nArgcNew;
+    int fUnique = 0;
+    int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "uvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'u':
+            fUnique ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -22005,14 +22013,22 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Write(): There is no AIG to write.\n" );
         return 1;
     }
-    // create the design to write
     pFileName = argv[globalUtilOptind];
+    if ( fUnique )
+    {
+        Gia_Man_t * pGia = Gia_ManIsoCanonicize( pAbc->pGia, fVerbose );
+        Gia_WriteAigerSimple( pGia, pFileName );
+        Gia_ManStop( pGia );
+    }
+    else
         Gia_WriteAiger( pAbc->pGia, pFileName, 0, 0 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &w [-h] <file>\n" );
+    Abc_Print( -2, "usage: &w [-uvh] <file>\n" );
     Abc_Print( -2, "\t         writes the current AIG into the AIGER file\n" );
+    Abc_Print( -2, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
+    Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<file> : the file name\n");
     return 1;
@@ -27839,8 +27855,6 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Iso( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Gia_ManIsoReduce( Gia_Man_t * pGia, Vec_Ptr_t ** pvPosEquivs, int fVerbose );
-
     Gia_Man_t * pAig;
     Vec_Ptr_t * vPosEquivs;
     int c, fVerbose = 0;