Isomorphism checking code.

abclib.dsp

@@ -3439,6 +3439,10 @@ SOURCE=.\src\aig\gia\giaIf.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaIso.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaMan.c
 # End Source File
 # Begin Source File

src/aig/gia/gia.h

@@ -620,6 +620,8 @@ extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileS
 extern Gia_Man_t *         Gia_ReadAiger( char * pFileName, int fCheck );
 extern void                Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
 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 );
 /*=== 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 );
@@ -671,6 +673,7 @@ extern Gia_Man_t *         Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t *
 extern Gia_Man_t *         Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
 extern Gia_Man_t *         Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
 extern Vec_Int_t *         Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses );
+extern Gia_Man_t *         Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos );
 /*=== giaEnable.c ==========================================================*/
 extern void                Gia_ManDetectSeqSignals( Gia_Man_t * p, int fSetReset, int fVerbose );
 extern Gia_Man_t *         Gia_ManUnrollAndCofactor( Gia_Man_t * p, int nFrames, int nFanMax, int fVerbose );

src/aig/gia/giaAiger.c

@@ -1565,6 +1565,185 @@ void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNu
     Gia_WriteAiger( p, Buffer, 0, 0 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Adds one unsigned AIG edge to the output buffer.]
+
+  Description [This procedure is a slightly modified version of Armin Biere's
+  procedure "void encode (FILE * file, unsigned x)" ]
+  
+  SideEffects [Returns the current writing position.]
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x )
+{
+    unsigned char ch;
+    while (x & ~0x7f)
+    {
+        ch = (x & 0x7f) | 0x80;
+//        putc (ch, file);
+//        pBuffer[Pos++] = ch;
+        Vec_StrPush( vStr, ch );
+        x >>= 7;
+    }
+    ch = x;
+//    putc (ch, file);
+//    pBuffer[Pos++] = ch;
+    Vec_StrPush( vStr, ch );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in into the memory buffer.]
+
+  Description [The resulting buffer constains the AIG in AIGER format. 
+  The resulting buffer should be deallocated by the user.]
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p )
+{
+    Vec_Str_t * vBuffer;
+    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_ManForEachCi( p, pObj, i )
+        pObj->Value = nNodes++;
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = nNodes++;
+
+    // write the header "M I L O A" where M = I + L + A
+    vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
+    Vec_StrPrintStr( vBuffer, "aig " );
+    Vec_StrPrintNum( vBuffer, Gia_ManCandNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManPiNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManRegNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManPoNum(p) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Gia_ManAndNum(p) );
+    Vec_StrPrintStr( vBuffer, "\n" );
+
+    // write latch drivers
+    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" );
+    }
+
+    // write PO drivers
+    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" );
+    }
+    // write the nodes into the buffer
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
+        uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
+        assert( uLit0 != uLit1 );
+        if ( uLit0 > uLit1 )
+        {
+            int Temp = uLit0;
+            uLit0 = uLit1;
+            uLit1 = Temp;
+        }
+        Gia_WriteAigerEncodeStr( vBuffer, uLit  - uLit1 );
+        Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
+    }
+    Vec_StrPrintStr( vBuffer, "c" );
+    return vBuffer;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the AIG in into the memory buffer.]
+
+  Description [The resulting buffer constains the AIG in AIGER format.
+  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!!!]
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs )
+{
+    Vec_Str_t * vBuffer;
+    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_ManForEachObjVec( vCis, p, pObj, i )
+    {
+        assert( Gia_ObjIsCi(pObj) );
+        pObj->Value = nNodes++;
+    }
+    Gia_ManForEachObjVec( vAnds, p, pObj, i )
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        pObj->Value = nNodes++;
+    }
+
+    // write the header "M I L O A" where M = I + L + A
+    vBuffer = Vec_StrAlloc( 3*Gia_ManObjNum(p) );
+    Vec_StrPrintStr( vBuffer, "aig " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) + Vec_IntSize(vAnds) );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCis) - nRegs );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, nRegs );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vCos) - nRegs );
+    Vec_StrPrintStr( vBuffer, " " );
+    Vec_StrPrintNum( vBuffer, Vec_IntSize(vAnds) );
+    Vec_StrPrintStr( vBuffer, "\n" );
+
+    // write latch drivers
+    Gia_ManForEachObjVec( vCos, p, pObj, i )
+    {
+        assert( Gia_ObjIsCo(pObj) );
+        uLit = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+//        fprintf( pFile, "%u\n", uLit );
+        Vec_StrPrintNum( vBuffer, uLit );
+        Vec_StrPrintStr( vBuffer, "\n" );
+    }
+
+    // write the nodes into the buffer
+    Gia_ManForEachObjVec( vAnds, p, pObj, i )
+    {
+        uLit  = Abc_Var2Lit( Gia_ObjValue(pObj), 0 );
+        uLit0 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+        uLit1 = Abc_Var2Lit( Gia_ObjValue(Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj) );
+        assert( uLit0 != uLit1 );
+        if ( uLit0 > uLit1 )
+        {
+            int Temp = uLit0;
+            uLit0 = uLit1;
+            uLit1 = Temp;
+        }
+        Gia_WriteAigerEncodeStr( vBuffer, uLit  - uLit1 );
+        Gia_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
+    }
+    Vec_StrPrintStr( vBuffer, "c" );
+    return vBuffer;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/gia/giaDup.c

@@ -1740,6 +1740,83 @@ Vec_Int_t * Gia_GlaCollectAssigned( Gia_Man_t * p, Vec_Int_t * vGateClasses )
     return vAssigned;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Copy an AIG structure related to the selected POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDupCones_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Ptr_t * vRoots )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsAnd(pObj) )
+    {
+        Gia_ManDupCones_rec( p, Gia_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
+        Gia_ManDupCones_rec( p, Gia_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
+        Vec_PtrPush( vNodes, pObj );
+    }
+    else if ( Gia_ObjIsPo(p, pObj) )
+        Gia_ManDupCones_rec( p, Gia_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
+    else if ( Gia_ObjIsRo(p, pObj) )
+        Vec_PtrPush( vRoots, Gia_ObjRoToRi(p, pObj) );
+    else if ( Gia_ObjIsPi(p, pObj) )
+        Vec_PtrPush( vLeaves, pObj );
+    else assert( 0 );
+}
+Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos )
+{
+    Gia_Man_t * pNew;
+    Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
+    Gia_Obj_t * pObj;
+    int i;
+
+    // collect initial POs
+    vLeaves = Vec_PtrAlloc( 100 );
+    vNodes = Vec_PtrAlloc( 100 );
+    vRoots = Vec_PtrAlloc( 100 );
+    for ( i = 0; i < nPos; i++ )
+        Vec_PtrPush( vRoots, Gia_ManPo(p, pPos[i]) );
+
+    // mark internal nodes
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
+    Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
+        Gia_ManDupCones_rec( p, pObj, vLeaves, vNodes, vRoots );
+
+    // start the new manager
+    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
+    Gia_ManConst0(p)->Value = 0;
+    // create PIs
+    Vec_PtrForEachEntry( Gia_Obj_t *, vLeaves, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    // create LOs
+    Vec_PtrForEachEntryStart( Gia_Obj_t *, vRoots, pObj, i, nPos )
+        Gia_ObjRiToRo(p, pObj)->Value = Gia_ManAppendCi( pNew );
+    // create internal nodes
+    Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i )
+        pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    // create COs
+    Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    // finalize
+    Gia_ManSetRegNum( pNew, Vec_PtrSize(vRoots)-nPos );
+    Vec_PtrFree( vLeaves );
+    Vec_PtrFree( vNodes );
+    Vec_PtrFree( vRoots );
+    return pNew;
+
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///