summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--abclib.dsp16
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigDup.c37
-rw-r--r--src/aig/aig/module.make1
-rw-r--r--src/aig/ioa/ioa.h1
-rw-r--r--src/aig/ioa/ioaWriteAig.c27
-rw-r--r--src/aig/saig/module.make3
-rw-r--r--src/aig/saig/saig.h6
-rw-r--r--src/aig/saig/saigIso.c597
-rw-r--r--src/aig/saig/saigIsoFast.c352
-rw-r--r--src/aig/saig/saigIsoSlow.c (renamed from src/aig/aig/aigIso.c)777
-rw-r--r--src/base/abci/abc.c88
-rw-r--r--src/base/io/io.c33
-rw-r--r--src/base/io/ioAbc.h2
-rw-r--r--src/base/io/ioUtil.c2
-rw-r--r--src/base/io/ioWriteAiger.c20
-rw-r--r--src/misc/vec/vecInt.h20
-rw-r--r--src/misc/vec/vecStr.h20
18 files changed, 1467 insertions, 536 deletions
diff --git a/abclib.dsp b/abclib.dsp
index dca2c9b5..42ccb2c6 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3043,10 +3043,6 @@ SOURCE=.\src\aig\aig\aigInter.c
# End Source File
# Begin Source File
-SOURCE=.\src\aig\aig\aigIso.c
-# End Source File
-# Begin Source File
-
SOURCE=.\src\aig\aig\aigJust.c
# End Source File
# Begin Source File
@@ -3231,6 +3227,18 @@ SOURCE=.\src\aig\saig\saigIoa.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\saig\saigIso.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigIsoFast.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigIsoSlow.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\saig\saigMiter.c
# End Source File
# Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 0a2ea6b6..52985546 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -504,6 +504,7 @@ extern Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs );
extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
extern Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs );
extern Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray );
+extern Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * pMan, Vec_Ptr_t * vArray );
/*=== aigFanout.c ==========================================================*/
extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index c2127262..59547586 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -1342,6 +1342,43 @@ Aig_Man_t * Aig_ManDupArray( Vec_Ptr_t * vArray )
return pNew;
}
+/**Function*************************************************************
+
+ Synopsis [Duplicates AIG with only one primary output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * pMan, Vec_Ptr_t * vArray )
+{
+ Aig_Man_t * pNew;
+ Vec_Ptr_t * vObjs;
+ Aig_Obj_t * pObj;
+ int i;
+ if ( Vec_PtrSize(vArray) == 0 )
+ return NULL;
+ vObjs = Aig_ManDfsNodes( pMan, (Aig_Obj_t **)Vec_PtrArray(vArray), Vec_PtrSize(vArray) );
+ // create the new manager
+ pNew = Aig_ManStart( 10000 );
+ pNew->pName = Abc_UtilStrsav( pMan->pName );
+ Aig_ManConst1(pMan)->pData = Aig_ManConst1(pNew);
+ Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, i )
+ if ( Aig_ObjIsPi(pObj) )
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, i )
+ if ( Aig_ObjIsNode(pObj) )
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Vec_PtrForEachEntry( Aig_Obj_t *, vArray, pObj, i )
+ Aig_ObjCreatePo( pNew, pObj->pData );
+ Aig_ManSetRegNum( pNew, 0 );
+ Vec_PtrFree( vObjs );
+ return pNew;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make
index 04fe8771..aaf5bf6d 100644
--- a/src/aig/aig/module.make
+++ b/src/aig/aig/module.make
@@ -6,7 +6,6 @@ SRC += src/aig/aig/aigCheck.c \
src/aig/aig/aigFanout.c \
src/aig/aig/aigFrames.c \
src/aig/aig/aigInter.c \
- src/aig/aig/aigIso.c \
src/aig/aig/aigJust.c \
src/aig/aig/aigMan.c \
src/aig/aig/aigMem.c \
diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h
index b86bc13a..a427f507 100644
--- a/src/aig/ioa/ioa.h
+++ b/src/aig/ioa/ioa.h
@@ -65,6 +65,7 @@ ABC_NAMESPACE_HEADER_START
extern Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
extern Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck );
/*=== ioaWriteAig.c =======================================================*/
+extern Vec_Str_t * Ioa_WriteAigerIntoMemoryStr( Aig_Man_t * pMan );
extern char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize );
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
/*=== ioaUtil.c =======================================================*/
diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c
index 2f682775..d19d23ff 100644
--- a/src/aig/ioa/ioaWriteAig.c
+++ b/src/aig/ioa/ioaWriteAig.c
@@ -283,9 +283,8 @@ Vec_Str_t * Ioa_WriteEncodeLiterals( Vec_Int_t * vLits )
SeeAlso []
***********************************************************************/
-char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
+Vec_Str_t * Ioa_WriteAigerIntoMemoryStr( Aig_Man_t * pMan )
{
- char * pBuffer;
Vec_Str_t * vBuffer;
Aig_Obj_t * pObj, * pDriver;
int nNodes, i, uLit, uLit0, uLit1;
@@ -357,10 +356,28 @@ char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
Ioa_WriteAigerEncodeStr( vBuffer, uLit - uLit1 );
Ioa_WriteAigerEncodeStr( vBuffer, uLit1 - uLit0 );
}
-// fprintf( pFile, "c" );
-// if ( pMan->pName )
-// fprintf( pFile, "n%s%c", pMan->pName, '\0' );
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 returned size (pnSize) gives the number of bytes in the buffer.
+ The resulting buffer should be deallocated by the user.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Ioa_WriteAigerIntoMemory( Aig_Man_t * pMan, int * pnSize )
+{
+ char * pBuffer;
+ Vec_Str_t * vBuffer;
+ vBuffer = Ioa_WriteAigerIntoMemoryStr( pMan );
if ( pMan->pName )
{
Vec_StrPrintStr( vBuffer, "n" );
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 327b9dd5..42e3c090 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -18,6 +18,9 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigHaig.c \
src/aig/saig/saigInd.c \
src/aig/saig/saigIoa.c \
+ src/aig/saig/saigIso.c \
+ src/aig/saig/saigIsoFast.c \
+ src/aig/saig/saigIsoSlow.c \
src/aig/saig/saigMiter.c \
src/aig/saig/saigOutDec.c \
src/aig/saig/saigPhase.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 74566966..218cb31c 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -182,6 +182,12 @@ extern int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int n
/*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
+/*=== saigIso.c ==========================================================*/
+extern Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose );
+extern Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose );
+extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose );
+/*=== saigIsoFast.c ==========================================================*/
+extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
/*=== saigMiter.c ==========================================================*/
extern Sec_MtrStatus_t Sec_MiterStatus( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c
new file mode 100644
index 00000000..1001f153
--- /dev/null
+++ b/src/aig/saig/saigIso.c
@@ -0,0 +1,597 @@
+/**CFile****************************************************************
+
+ FileName [saigIso.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Sequential cleanup.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigIso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "src/aig/ioa/ioa.h"
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Find the canonical permutation of the COs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis )
+{
+ extern int Iso_ObjCompareAigObjByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 );
+ Vec_Int_t * vPermCos;
+ Aig_Obj_t * pObj, * pFanin;
+ int i, Entry, Diff;
+ assert( Vec_IntSize(vPermCis) == Aig_ManPiNum(pAig) );
+ vPermCos = Vec_IntAlloc( Aig_ManPoNum(pAig) );
+ if ( Saig_ManPoNum(pAig) == 1 )
+ Vec_IntPush( vPermCos, 0 );
+ else
+ {
+ Vec_Ptr_t * vRoots = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ pFanin = Aig_ObjFanin0(pObj);
+ assert( Aig_ObjIsConst1(pFanin) || pFanin->iData > 0 );
+ pObj->iData = Abc_Var2Lit( pFanin->iData, Aig_ObjFaninC0(pObj) );
+ Vec_PtrPush( vRoots, pObj );
+ }
+ Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareAigObjByData );
+ Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
+ Vec_IntPush( vPermCos, Aig_ObjPioNum(pObj) );
+ Vec_PtrFree( vRoots );
+ }
+ // add flop outputs
+ Diff = Saig_ManPoNum(pAig) - Saig_ManPiNum(pAig);
+ Vec_IntForEachEntryStart( vPermCis, Entry, i, Saig_ManPiNum(pAig) )
+ Vec_IntPush( vPermCos, Entry + Diff );
+ return vPermCos;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs canonical duplication of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManDupIsoCanonical_rec( Aig_Man_t * pNew, Aig_Man_t * pAig, Aig_Obj_t * pObj )
+{
+ if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(pAig, pObj);
+ assert( Aig_ObjIsNode(pObj) );
+ if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) || !Aig_ObjIsNode(Aig_ObjFanin1(pObj)) )
+ {
+ Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+ Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
+ }
+ else
+ {
+ assert( Aig_ObjFanin0(pObj)->iData != Aig_ObjFanin1(pObj)->iData );
+ if ( Aig_ObjFanin0(pObj)->iData < Aig_ObjFanin1(pObj)->iData )
+ {
+ Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+ Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
+ }
+ else
+ {
+ Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin1(pObj) );
+ Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+ }
+ }
+ pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs canonical duplication of the AIG.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose )
+{
+ Aig_Man_t * pNew;
+ Aig_Obj_t * pObj;
+ Vec_Int_t * vPerm, * vPermCo;
+ int i, Entry;
+ // derive permutations
+ vPerm = Saig_ManFindIsoPerm( pAig, fVerbose );
+ vPermCo = Saig_ManFindIsoPermCos( pAig, vPerm );
+ // create the new manager
+ pNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ pNew->pName = Abc_UtilStrsav( pAig->pName );
+ Aig_ManIncrementTravId( pAig );
+ // create constant
+ pObj = Aig_ManConst1(pAig);
+ pObj->pData = Aig_ManConst1(pNew);
+ Aig_ObjSetTravIdCurrent( pAig, pObj );
+ // create PIs
+ Vec_IntForEachEntry( vPerm, Entry, i )
+ {
+ pObj = Aig_ManPi(pAig, Entry);
+ pObj->pData = Aig_ObjCreatePi(pNew);
+ Aig_ObjSetTravIdCurrent( pAig, pObj );
+ }
+ // traverse from the POs
+ Vec_IntForEachEntry( vPermCo, Entry, i )
+ {
+ pObj = Aig_ManPo(pAig, Entry);
+ Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) );
+ }
+ // create POs
+ Vec_IntForEachEntry( vPermCo, Entry, i )
+ {
+ pObj = Aig_ManPo(pAig, Entry);
+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+ }
+ Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) );
+ Vec_IntFreeP( &vPerm );
+ Vec_IntFreeP( &vPermCo );
+ return pNew;
+}
+
+
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Checks structural equivalence of AIG1 and AIG2.]
+
+ Description [Returns 1 if AIG1 and AIG2 are structurally equivalent
+ under this mapping.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2to1, int fVerbose )
+{
+ Aig_Obj_t * pObj, * pFanin0, * pFanin1;
+ int i;
+ assert( Aig_ManPiNum(pAig1) == Aig_ManPiNum(pAig2) );
+ assert( Aig_ManPoNum(pAig1) == Aig_ManPoNum(pAig2) );
+ assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) );
+ assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) );
+ Aig_ManCleanData( pAig1 );
+ // map const and PI nodes
+ Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1);
+ Aig_ManForEachPi( pAig2, pObj, i )
+ pObj->pData = Aig_ManPi( pAig1, Vec_IntEntry(vMap2to1, i) );
+ // try internal nodes
+ Aig_ManForEachNode( pAig2, pObj, i )
+ {
+ pFanin0 = Aig_ObjChild0Copy( pObj );
+ pFanin1 = Aig_ObjChild1Copy( pObj );
+ pObj->pData = Aig_TableLookupTwo( pAig1, pFanin0, pFanin1 );
+ if ( pObj->pData == NULL )
+ {
+ if ( fVerbose )
+ printf( "Structural equivalence failed at node %d.\n", i );
+ return 0;
+ }
+ }
+ // make sure the first PO points to the same node
+ if ( Aig_ManPoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManPo(pAig2, 0)) != Aig_ObjChild0(Aig_ManPo(pAig1, 0)) )
+ {
+ if ( fVerbose )
+ printf( "Structural equivalence failed at primary output 0.\n" );
+ return 0;
+ }
+ return 1;
+}
+
+//static int s_Counter;
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
+{
+ Aig_Obj_t * pObj;
+ int i, Counter = 0;
+ if ( pAig->nComplEdges > 0 )
+ return pAig->nComplEdges;
+ Aig_ManForEachObj( pAig, pObj, i )
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ Counter += Aig_ObjFaninC0(pObj);
+ Counter += Aig_ObjFaninC1(pObj);
+ }
+ else if ( Aig_ObjIsPo(pObj) )
+ Counter += Aig_ObjFaninC0(pObj);
+ return (pAig->nComplEdges = Counter);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds mapping of CIs of AIG2 into those of AIG1.]
+
+ Description [Returns the mapping of CIs of the two AIGs, or NULL
+ if there is no mapping.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose )
+{
+ Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2;
+ int i, Entry;
+ if ( Aig_ManPiNum(pAig1) != Aig_ManPiNum(pAig2) )
+ return NULL;
+ if ( Aig_ManPoNum(pAig1) != Aig_ManPoNum(pAig2) )
+ return NULL;
+ if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) )
+ return NULL;
+ if ( Aig_ManNodeNum(pAig1) != Aig_ManNodeNum(pAig2) )
+ return NULL;
+ if ( Aig_ManLevelNum(pAig1) != Aig_ManLevelNum(pAig2) )
+ return NULL;
+// if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) )
+// return NULL;
+// s_Counter++;
+
+ if ( fVerbose )
+ printf( "AIG1:\n" );
+ vPerm1 = vPerm1_ ? vPerm1_ : Saig_ManFindIsoPerm( pAig1, fVerbose );
+ if ( fVerbose )
+ printf( "AIG1:\n" );
+ vPerm2 = vPerm2_ ? vPerm2_ : Saig_ManFindIsoPerm( pAig2, fVerbose );
+ if ( vPerm1_ )
+ assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) );
+ if ( vPerm2_ )
+ assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) );
+ // find canonical permutation
+ // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2
+ vInvPerm2 = Vec_IntInvert( vPerm2, -1 );
+ Vec_IntForEachEntry( vInvPerm2, Entry, i )
+ {
+ assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) );
+ Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) );
+ }
+ if ( vPerm1_ == NULL )
+ Vec_IntFree( vPerm1 );
+ if ( vPerm2_ == NULL )
+ Vec_IntFree( vPerm2 );
+ // check if they are indeed equivalent
+ if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) )
+ Vec_IntFreeP( &vInvPerm2 );
+ return vInvPerm2;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose )
+{
+ int fVeryVerbose = 0;
+ Vec_Ptr_t * vParts, * vPerms, * vAigs;
+ Vec_Int_t * vPos, * vMap;
+ Aig_Man_t * pPart, * pTemp;
+ int i, k, nPos;
+
+ // derive AIG for each PO
+ nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
+ vParts = Vec_PtrAlloc( nPos );
+ vPerms = Vec_PtrAlloc( nPos );
+ for ( i = 0; i < nPos; i++ )
+ {
+ pPart = Saig_ManDupCones( pAig, &i, 1 );
+ vMap = Saig_ManFindIsoPerm( pPart, fVeryVerbose );
+ Vec_PtrPush( vParts, pPart );
+ Vec_PtrPush( vPerms, vMap );
+ }
+// s_Counter = 0;
+
+ // check AIGs for each PO
+ vAigs = Vec_PtrAlloc( 1000 );
+ vPos = Vec_IntAlloc( 1000 );
+ Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+ {
+ if ( fVeryVerbose )
+ {
+ printf( "AIG %4d : ", i );
+ Aig_ManPrintStats( pPart );
+ }
+ Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k )
+ {
+ if ( fVeryVerbose )
+ printf( "Comparing AIG %4d and AIG %4d. ", Vec_IntEntry(vPos,k), i );
+ vMap = Iso_ManFindMapping( pTemp, pPart,
+ (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)),
+ (Vec_Int_t *)Vec_PtrEntry(vPerms, i),
+ fVeryVerbose );
+ if ( vMap != NULL )
+ {
+ if ( fVeryVerbose )
+ printf( "Found match\n" );
+ if ( fVerbose )
+ printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
+ Vec_IntFree( vMap );
+ break;
+ }
+ if ( fVeryVerbose )
+ printf( "No match.\n" );
+ }
+ if ( k == Vec_PtrSize(vAigs) )
+ {
+ Vec_PtrPush( vAigs, pPart );
+ Vec_IntPush( vPos, i );
+ }
+ }
+ // delete AIGs
+ Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+ Aig_ManStop( pPart );
+ Vec_PtrFree( vParts );
+ Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i )
+ Vec_IntFree( vMap );
+ Vec_PtrFree( vPerms );
+ // derive the resulting AIG
+ pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) );
+ Vec_PtrFree( vAigs );
+ Vec_IntFree( vPos );
+
+// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
+ return pPart;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Takes multi-output sequential AIG.]
+
+ Description [Returns candidate equivalence classes of POs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Iso_StoCompareVecStr( Vec_Str_t ** p1, Vec_Str_t ** p2 )
+{
+ return Vec_StrCompareVec( *p1, *p2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
+{
+ int fVeryVerbose = 0;
+ Aig_Man_t * pPart, * pTemp;
+ Vec_Ptr_t * vBuffers, * vClasses;
+ Vec_Int_t * vLevel, * vRemain;
+ Vec_Str_t * vStr, * vPrev;
+ int i, nPos, nUnique = 0, clk = clock();
+
+ // derive AIG for each PO
+ nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
+ vBuffers = Vec_PtrAlloc( nPos );
+ for ( i = 0; i < nPos; i++ )
+ {
+// if ( i % 100 == 0 )
+// printf( "%d finished...\n", i );
+ pPart = Saig_ManDupCones( pAig, &i, 1 );
+ pTemp = Saig_ManDupIsoCanonical( pPart, 0 );
+ vStr = Ioa_WriteAigerIntoMemoryStr( pTemp );
+ Vec_PtrPush( vBuffers, vStr );
+ Aig_ManStop( pTemp );
+ Aig_ManStop( pPart );
+ // remember the output number in nCap (attention: hack!)
+ vStr->nCap = i;
+ }
+// s_Counter = 0;
+ if ( fVerbose )
+ Abc_PrintTime( 1, "Isomorph time", clock() - clk );
+
+ // sort the infos
+ clk = clock();
+ Vec_PtrSort( vBuffers, (int (*)(void))Iso_StoCompareVecStr );
+
+ // create classes
+ clk = clock();
+ vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+ // start the first class
+ Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
+ vPrev = (Vec_Str_t *)Vec_PtrEntry( vBuffers, 0 );
+ Vec_IntPush( vLevel, vPrev->nCap );
+ // consider other classes
+ Vec_PtrForEachEntryStart( Vec_Str_t *, vBuffers, vStr, i, 1 )
+ {
+ if ( Vec_StrCompareVec(vPrev, vStr) )
+ Vec_PtrPush( vClasses, Vec_IntAlloc(4) );
+ vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses );
+ Vec_IntPush( vLevel, vStr->nCap );
+ vPrev = vStr;
+ }
+ Vec_VecFree( (Vec_Vec_t *)vBuffers );
+
+ if ( fVerbose )
+ Abc_PrintTime( 1, "Sorting time", clock() - clk );
+// Abc_PrintTime( 1, "Traversal time", time_Trav );
+
+ // report the results
+// Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
+// printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
+ if ( fVerbose )
+ {
+ Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
+ if ( Vec_IntSize(vLevel) > 1 )
+ printf( "%d ", Vec_IntSize(vLevel) );
+ else
+ nUnique++;
+ printf( " Unique = %d\n", nUnique );
+ }
+
+ // collect the first ones
+ vRemain = Vec_IntAlloc( 100 );
+ Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
+ Vec_IntPush( vRemain, Vec_IntEntry(vLevel, 0) );
+
+ // derive the resulting AIG
+ pPart = Saig_ManDupCones( pAig, Vec_IntArray(vRemain), Vec_IntSize(vRemain) );
+ Vec_IntFree( vRemain );
+
+// return (Vec_Vec_t *)vClasses;
+ Vec_VecFree( (Vec_Vec_t *)vClasses );
+
+// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
+ return pPart;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose )
+{
+ Vec_Int_t * vPerm;
+ int clk = clock();
+ vPerm = Saig_ManFindIsoPerm( pAig, fVerbose );
+ Vec_IntFree( vPerm );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ return NULL;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, int fVerbose )
+{
+ Aig_Man_t * pPart;
+ int clk = clock();
+ pPart = Iso_ManFilterPos( pAig, fVerbose );
+ printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+// Aig_ManStop( pPart );
+ return pPart;
+}
+
+
+#include "src/base/abc/abc.h"
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Iso_ManTest888( Aig_Man_t * pAig1, int fVerbose )
+{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+ extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+ Abc_Ntk_t * pNtk;
+ Aig_Man_t * pAig2;
+ Vec_Int_t * vMap;
+
+ pNtk = Abc_NtkFromAigPhase( pAig1 );
+ Abc_NtkPermute( pNtk, 1, 0, 1 );
+ pAig2 = Abc_NtkToDar( pNtk, 0, 1 );
+ Abc_NtkDelete( pNtk );
+
+ vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose );
+ Aig_ManStop( pAig2 );
+
+ if ( vMap != NULL )
+ {
+ printf( "Mapping of AIGs is found.\n" );
+ if ( fVerbose )
+ Vec_IntPrint( vMap );
+ }
+ else
+ printf( "Mapping of AIGs is NOT found.\n" );
+ Vec_IntFreeP( &vMap );
+ return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c
new file mode 100644
index 00000000..6556b90f
--- /dev/null
+++ b/src/aig/saig/saigIsoFast.c
@@ -0,0 +1,352 @@
+/**CFile****************************************************************
+
+ FileName [aigIsoFast.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Graph isomorphism package.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigIsoFast.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define AIG_ISO_NUM 16
+
+typedef struct Iso_Dat_t_ Iso_Dat_t;
+struct Iso_Dat_t_
+{
+ unsigned nFiNeg : 3;
+ unsigned nFoNeg : 2;
+ unsigned nFoPos : 2;
+ unsigned Fi0Lev : 3;
+ unsigned Fi1Lev : 3;
+ unsigned Level : 3;
+ unsigned fVisit : 16;
+};
+
+typedef struct Iso_Dat2_t_ Iso_Dat2_t;
+struct Iso_Dat2_t_
+{
+ unsigned Data : 16;
+};
+
+typedef struct Iso_Sto_t_ Iso_Sto_t;
+struct Iso_Sto_t_
+{
+ Aig_Man_t * pAig; // user's AIG manager
+ int nObjs; // number of objects
+ Iso_Dat_t * pData; // data for each object
+ Vec_Int_t * vVisited; // visited nodes
+ Vec_Ptr_t * vRoots; // root nodes
+ Vec_Int_t * vPlaces; // places in the counter lists
+ int * pCounters; // counters
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Iso_Sto_t * Iso_StoStart( Aig_Man_t * pAig )
+{
+ Iso_Sto_t * p;
+ p = ABC_CALLOC( Iso_Sto_t, 1 );
+ p->pAig = pAig;
+ p->nObjs = Aig_ManObjNumMax( pAig );
+ p->pData = ABC_CALLOC( Iso_Dat_t, p->nObjs );
+ p->vVisited = Vec_IntStart( 1000 );
+ p->vPlaces = Vec_IntStart( 1000 );
+ p->vRoots = Vec_PtrStart( 1000 );
+ p->pCounters = ABC_CALLOC( int, (1 << AIG_ISO_NUM) );
+ return p;
+}
+void Iso_StoStop( Iso_Sto_t * p )
+{
+ Vec_IntFree( p->vPlaces );
+ Vec_IntFree( p->vVisited );
+ Vec_PtrFree( p->vRoots );
+ ABC_FREE( p->pCounters );
+ ABC_FREE( p->pData );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collect statistics about one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Iso_StoCollectInfo_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fCompl, Vec_Int_t * vVisited, Iso_Dat_t * pData, Vec_Ptr_t * vRoots )
+{
+ Iso_Dat_t * pThis = pData + Aig_ObjId(pObj);
+ assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) );
+ if ( pThis->fVisit )
+ {
+ if ( fCompl )
+ pThis->nFoNeg++;
+ else
+ pThis->nFoPos++;
+ return;
+ }
+ assert( *((int *)pThis) == 0 );
+ pThis->fVisit = 1;
+ if ( fCompl )
+ pThis->nFoNeg++;
+ else
+ pThis->nFoPos++;
+ pThis->Level = pObj->Level;
+ pThis->nFiNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ if ( Aig_ObjFaninC0(pObj) < Aig_ObjFaninC1(pObj) || (Aig_ObjFaninC0(pObj) == Aig_ObjFaninC1(pObj) && Aig_ObjFanin0(pObj)->Level < Aig_ObjFanin1(pObj)->Level) )
+ {
+ pThis->Fi0Lev = pObj->Level - Aig_ObjFanin0(pObj)->Level;
+ pThis->Fi1Lev = pObj->Level - Aig_ObjFanin1(pObj)->Level;
+ }
+ else
+ {
+ pThis->Fi0Lev = pObj->Level - Aig_ObjFanin1(pObj)->Level;
+ pThis->Fi1Lev = pObj->Level - Aig_ObjFanin0(pObj)->Level;
+ }
+ Iso_StoCollectInfo_rec( p, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj), vVisited, pData, vRoots );
+ Iso_StoCollectInfo_rec( p, Aig_ObjFanin1(pObj), Aig_ObjFaninC1(pObj), vVisited, pData, vRoots );
+ }
+ else if ( Saig_ObjIsLo(p, pObj) )
+ {
+ pThis->Fi0Lev = 1;
+ pThis->Fi1Lev = 0;
+ Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
+ }
+ else if ( Saig_ObjIsPi(p, pObj) )
+ {
+ pThis->Fi0Lev = 0;
+ pThis->Fi1Lev = 0;
+ }
+ else
+ assert( 0 );
+ assert( pThis->nFoNeg + pThis->nFoPos );
+ Vec_IntPush( vVisited, Aig_ObjId(pObj) );
+}
+
+//static int time_Trav = 0;
+
+/**Function*************************************************************
+
+ Synopsis [Collect statistics about one output.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo )
+{
+ int fVerboseShow = 0;
+ Vec_Int_t * vInfo;
+ Iso_Dat2_t * pData2 = (Iso_Dat2_t *)p->pData;
+ Aig_Man_t * pAig = p->pAig;
+ Aig_Obj_t * pObj;
+ int i, Value, Entry, * pPerm;
+ int clk = clock();
+
+ assert( Aig_ObjIsPo(pPo) );
+
+ // collect initial POs
+ Vec_IntClear( p->vVisited );
+ Vec_PtrClear( p->vRoots );
+ Vec_PtrPush( p->vRoots, pPo );
+
+ // mark internal nodes
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vRoots, pObj, i )
+ if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
+ Iso_StoCollectInfo_rec( pAig, Aig_ObjFanin0(pObj), Aig_ObjFaninC0(pObj), p->vVisited, p->pData, p->vRoots );
+// time_Trav += clock() - clk;
+
+ // count how many times each data entry appears
+ Vec_IntClear( p->vPlaces );
+ Vec_IntForEachEntry( p->vVisited, Entry, i )
+ {
+ Value = pData2[Entry].Data;
+// assert( Value > 0 );
+ if ( p->pCounters[Value]++ == 0 )
+ Vec_IntPush( p->vPlaces, Value );
+// pData2[Entry].Data = 0;
+ *((int *)(p->pData + Entry)) = 0;
+ }
+
+ // collect non-trivial counters
+ Vec_IntClear( p->vVisited );
+ Vec_IntForEachEntry( p->vPlaces, Entry, i )
+ {
+ assert( p->pCounters[Entry] );
+ Vec_IntPush( p->vVisited, p->pCounters[Entry] );
+ p->pCounters[Entry] = 0;
+ }
+// printf( "%d ", Vec_IntSize(p->vVisited) );
+
+ // sort the costs in the increasing order
+ pPerm = Abc_SortCost( Vec_IntArray(p->vVisited), Vec_IntSize(p->vVisited) );
+ assert( Vec_IntEntry(p->vVisited, pPerm[0]) <= Vec_IntEntry(p->vVisited, pPerm[Vec_IntSize(p->vVisited)-1]) );
+
+ // create information
+ vInfo = Vec_IntAlloc( Vec_IntSize(p->vVisited) );
+ for ( i = Vec_IntSize(p->vVisited)-1; i >= 0; i-- )
+ {
+ Entry = Vec_IntEntry( p->vVisited, pPerm[i] );
+ Entry = (Entry << AIG_ISO_NUM) | Vec_IntEntry( p->vPlaces, pPerm[i] );
+ Vec_IntPush( vInfo, Entry );
+ }
+ ABC_FREE( pPerm );
+
+ // show the final result
+ if ( fVerboseShow )
+ Vec_IntForEachEntry( vInfo, Entry, i )
+ {
+ Iso_Dat2_t Data = { Entry & 0xFFFF };
+ Iso_Dat_t * pData = (Iso_Dat_t *)&Data;
+
+ printf( "%6d : ", i );
+ printf( "Freq =%6d ", Entry >> 16 );
+
+ printf( "FiNeg =%3d ", pData->nFiNeg );
+ printf( "FoNeg =%3d ", pData->nFoNeg );
+ printf( "FoPos =%3d ", pData->nFoPos );
+ printf( "Fi0L =%3d ", pData->Fi0Lev );
+ printf( "Fi1L =%3d ", pData->Fi1Lev );
+ printf( "Lev =%3d ", pData->Level );
+ printf( "\n" );
+ }
+ return vInfo;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Takes multi-output sequential AIG.]
+
+ Description [Returns candidate equivalence classes of POs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Iso_StoCompareVecInt( Vec_Int_t ** p1, Vec_Int_t ** p2 )
+{
+ return Vec_IntCompareVec( *p1, *p2 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Takes multi-output sequential AIG.]
+
+ Description [Returns candidate equivalence classes of POs.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig )
+{
+ Iso_Sto_t * pMan;
+ Aig_Obj_t * pObj;
+ Vec_Ptr_t * vClasses, * vInfos;
+ Vec_Int_t * vInfo, * vPrev, * vLevel;
+ int i, Number, nUnique = 0, clk = clock();
+
+ // collect infos and remember their number
+ pMan = Iso_StoStart( pAig );
+ vInfos = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+ Saig_ManForEachPo( pAig, pObj, i )
+ {
+ vInfo = Iso_StoCollectInfo(pMan, pObj);
+ Vec_IntPush( vInfo, i );
+ Vec_PtrPush( vInfos, vInfo );
+ }
+ Iso_StoStop( pMan );
+ Abc_PrintTime( 1, "Info computation time", clock() - clk );
+
+ // sort the infos
+ clk = clock();
+ Vec_PtrSort( vInfos, (int (*)(void))Iso_StoCompareVecInt );
+
+ // create classes
+ clk = clock();
+ vClasses = Vec_PtrAlloc( Saig_ManPoNum(pAig) );
+ // start the first class
+ Vec_PtrPush( vClasses, (vLevel = Vec_IntAlloc(4)) );
+ vPrev = (Vec_Int_t *)Vec_PtrEntry( vInfos, 0 );
+ Vec_IntPush( vLevel, Vec_IntPop(vPrev) );
+ // consider other classes
+ Vec_PtrForEachEntryStart( Vec_Int_t *, vInfos, vInfo, i, 1 )
+ {
+ Number = Vec_IntPop( vInfo );
+ if ( Vec_IntCompareVec(vPrev, vInfo) )
+ Vec_PtrPush( vClasses, Vec_IntAlloc(4) );
+ vLevel = (Vec_Int_t *)Vec_PtrEntryLast( vClasses );
+ Vec_IntPush( vLevel, Number );
+ vPrev = vInfo;
+ }
+ Vec_VecFree( (Vec_Vec_t *)vInfos );
+ Abc_PrintTime( 1, "Sorting time", clock() - clk );
+// Abc_PrintTime( 1, "Traversal time", time_Trav );
+
+ // report the results
+// Vec_VecPrintInt( (Vec_Vec_t *)vClasses );
+ printf( "Devided %d outputs into %d cand equiv classes.\n", Saig_ManPoNum(pAig), Vec_PtrSize(vClasses) );
+
+ Vec_PtrForEachEntry( Vec_Int_t *, vClasses, vLevel, i )
+ if ( Vec_IntSize(vLevel) > 1 )
+ printf( "%d ", Vec_IntSize(vLevel) );
+ else
+ nUnique++;
+ printf( " Unique = %d\n", nUnique );
+
+// return (Vec_Vec_t *)vClasses;
+ Vec_VecFree( (Vec_Vec_t *)vClasses );
+ return NULL;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/aig/aigIso.c b/src/aig/saig/saigIsoSlow.c
index 27789107..7510c911 100644
--- a/src/aig/aig/aigIso.c
+++ b/src/aig/saig/saigIsoSlow.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "aig.h"
+#include "saig.h"
ABC_NAMESPACE_IMPL_START
@@ -33,15 +33,14 @@ typedef struct Iso_Obj_t_ Iso_Obj_t;
struct Iso_Obj_t_
{
// hashing entries (related to the parameter ISO_NUM_INTS!)
- int Level;
- unsigned fFlop : 1;
- unsigned fMux : 1;
- unsigned nFinPos : 2;
- unsigned nFoutPos : 28;
- unsigned fCLow : 1;
- unsigned fCHigh : 1;
+ unsigned Level : 30;
unsigned nFinNeg : 2;
- unsigned nFoutNeg : 28;
+ unsigned nFoutPos : 16;
+ unsigned nFoutNeg : 16;
+ unsigned nFinLev0 : 16;
+ unsigned nFinLev1 : 16;
+// unsigned nNodes : 16;
+// unsigned nEdges : 16;
// other data
int iNext; // hash table entry
int iClass; // next one in class
@@ -61,16 +60,15 @@ struct Iso_Man_t_
int nObjs; // total objects
int nBins; // hash table size
int * pBins; // hash table
- Vec_Int_t * vPolRefs; // polarity references
Vec_Ptr_t * vSingles; // singletons
Vec_Ptr_t * vClasses; // other classes
+ Vec_Ptr_t * vTemp1; // other classes
+ Vec_Ptr_t * vTemp2; // other classes
};
static inline Iso_Obj_t * Iso_ManObj( Iso_Man_t * p, int i ) { assert( i >= 0 && i < p->nObjs ); return i ? p->pObjs + i : NULL; }
static inline int Iso_ObjId( Iso_Man_t * p, Iso_Obj_t * pObj ) { assert( pObj > p->pObjs && pObj < p->pObjs + p->nObjs ); return pObj - p->pObjs; }
-
-static inline void Iso_ObjIncPolRef0( Vec_Int_t * vPolRefs, Aig_Obj_t * pObj ) { Vec_IntAddToEntry( vPolRefs, 2*Aig_ObjFaninId0(pObj)+Aig_ObjFaninC0(pObj), 1 ); }
-static inline void Iso_ObjIncPolRef1( Vec_Int_t * vPolRefs, Aig_Obj_t * pObj ) { Vec_IntAddToEntry( vPolRefs, 2*Aig_ObjFaninId1(pObj)+Aig_ObjFaninC1(pObj), 1 ); }
+static inline Aig_Obj_t * Iso_AigObj( Iso_Man_t * p, Iso_Obj_t * q ) { return Aig_ManObj( p->pAig, Iso_ObjId(p, q) ); }
#define Iso_ManForEachObj( p, pObj, i ) \
for ( i = 1; (i < p->nObjs) && ((pObj) = Iso_ManObj(p, i)); i++ ) if ( pIso->Level == -1 ) {} else
@@ -90,49 +88,24 @@ static inline void Iso_ObjIncPolRef1( Vec_Int_t * vPolRefs, Aig_Obj_t * pObj ) {
SeeAlso []
***********************************************************************/
-int Iso_ManNegEdgeNum( Aig_Man_t * pAig )
+void Iso_ManObjCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges )
{
- Aig_Obj_t * pObj;
- int i, Counter = 0;
- if ( pAig->nComplEdges > 0 )
- return pAig->nComplEdges;
- Aig_ManForEachObj( pAig, pObj, i )
- if ( Aig_ObjIsNode(pObj) )
- {
- Counter += Aig_ObjFaninC0(pObj);
- Counter += Aig_ObjFaninC1(pObj);
- }
- else if ( Aig_ObjIsPo(pObj) )
- Counter += Aig_ObjFaninC0(pObj);
- return (pAig->nComplEdges = Counter);
+ if ( Aig_ObjIsPi(pObj) )
+ return;
+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+ return;
+ Aig_ObjSetTravIdCurrent(p, pObj);
+ Iso_ManObjCount_rec( p, Aig_ObjFanin0(pObj), pnNodes, pnEdges );
+ Iso_ManObjCount_rec( p, Aig_ObjFanin1(pObj), pnNodes, pnEdges );
+ (*pnEdges) += Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
+ (*pnNodes)++;
}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Iso_ManComputePolRefs( Aig_Man_t * pAig )
+void Iso_ManObjCount( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges )
{
- Vec_Int_t * vPolRefs;
- Aig_Obj_t * pObj;
- int i;
- vPolRefs = Vec_IntStart( 2 * Aig_ManObjNumMax( pAig ) );
- Aig_ManForEachObj( pAig, pObj, i )
- if ( Aig_ObjIsNode(pObj) )
- {
- Iso_ObjIncPolRef0( vPolRefs, pObj );
- Iso_ObjIncPolRef1( vPolRefs, pObj );
- }
- else if ( Aig_ObjIsPo(pObj) )
- Iso_ObjIncPolRef0( vPolRefs, pObj );
- return vPolRefs;
+ assert( Aig_ObjIsNode(pObj) );
+ *pnNodes = *pnEdges = 0;
+ Aig_ManIncrementTravId( p );
+ Iso_ManObjCount_rec( p, pObj, pnNodes, pnEdges );
}
/**Function*************************************************************
@@ -155,9 +128,10 @@ Iso_Man_t * Iso_ManStart( Aig_Man_t * pAig )
p->pObjs = ABC_CALLOC( Iso_Obj_t, p->nObjs );
p->nBins = Abc_PrimeCudd( p->nObjs );
p->pBins = ABC_CALLOC( int, p->nBins );
- p->vPolRefs = Iso_ManComputePolRefs( pAig );
p->vSingles = Vec_PtrAlloc( 1000 );
p->vClasses = Vec_PtrAlloc( 1000 );
+ p->vTemp1 = Vec_PtrAlloc( 1000 );
+ p->vTemp2 = Vec_PtrAlloc( 1000 );
p->nObjIds = 1;
return p;
}
@@ -167,9 +141,10 @@ void Iso_ManStop( Iso_Man_t * p )
int i;
Iso_ManForEachObj( p, pIso, i )
Vec_IntFreeP( &pIso->vAllies );
+ Vec_PtrFree( p->vTemp1 );
+ Vec_PtrFree( p->vTemp2 );
Vec_PtrFree( p->vClasses );
Vec_PtrFree( p->vSingles );
- Vec_IntFree( p->vPolRefs );
ABC_FREE( p->pBins );
ABC_FREE( p->pObjs );
ABC_FREE( p );
@@ -187,54 +162,14 @@ void Iso_ManStop( Iso_Man_t * p )
SeeAlso []
***********************************************************************/
-int Iso_ObjCompareBasic( Iso_Obj_t * pIso1, Iso_Obj_t * pIso2 )
-{
- int fCLow1, fCLow2, fCHigh1, fCHigh2, Diff;
-
- fCLow1 = pIso1->fCLow; pIso1->fCLow = 0;
- fCLow2 = pIso2->fCLow; pIso2->fCLow = 0;
- fCHigh1 = pIso1->fCHigh; pIso1->fCHigh = 0;
- fCHigh2 = pIso2->fCHigh; pIso2->fCHigh = 0;
-
- Diff = memcmp( pIso1, pIso2, sizeof(int) * ISO_NUM_INTS );
-
- pIso1->fCLow = fCLow1;
- pIso2->fCLow = fCLow2;
- pIso1->fCHigh = fCHigh1;
- pIso2->fCHigh = fCHigh2;
-
- return -Diff;
-}
-
-/**Function*************************************************************
-
- Synopsis [Compares two objects by their signature.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Iso_ObjCompare( Iso_Obj_t ** pp1, Iso_Obj_t ** pp2 )
{
Iso_Obj_t * pIso1 = *pp1;
Iso_Obj_t * pIso2 = *pp2;
- int Diff = memcmp( pIso1, pIso2, sizeof(int) * ISO_NUM_INTS );
- if ( Diff )
- return -Diff;
-// return 0;
- if ( pIso1->vAllies == NULL && pIso2->vAllies == NULL )
- return 0;
- if ( pIso1->vAllies == NULL && pIso2->vAllies != NULL )
- return 1;
- if ( pIso1->vAllies != NULL && pIso2->vAllies == NULL )
- return -1;
- Diff = Vec_IntSize(pIso1->vAllies) - Vec_IntSize(pIso2->vAllies);
+ int Diff = -memcmp( pIso1, pIso2, sizeof(int) * ISO_NUM_INTS );
if ( Diff )
- return -Diff;
- return memcmp( Vec_IntArray(pIso1->vAllies), Vec_IntArray(pIso2->vAllies), Vec_IntSize(pIso1->vAllies) * sizeof(int) );
+ return Diff;
+ return -Vec_IntCompareVec( pIso1->vAllies, pIso2->vAllies );
}
/**Function*************************************************************
@@ -270,7 +205,8 @@ int Iso_ObjCompareAigObjByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
{
Aig_Obj_t * pIso1 = *pp1;
Aig_Obj_t * pIso2 = *pp2;
- assert( Aig_ObjIsPi(pIso1) && Aig_ObjIsPi(pIso2) );
+ assert( Aig_ObjIsPi(pIso1) || Aig_ObjIsPo(pIso1) );
+ assert( Aig_ObjIsPi(pIso2) || Aig_ObjIsPo(pIso2) );
return pIso1->iData - pIso2->iData;
}
@@ -332,55 +268,29 @@ static inline int Iso_ObjHashAdd( Iso_Man_t * p, Iso_Obj_t * pIso )
SeeAlso []
***********************************************************************/
-Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
+void Iso_ManCollectClasses( Iso_Man_t * p )
{
- Iso_Man_t * p;
Iso_Obj_t * pIso;
- Aig_Obj_t * pObj;
int i;
- p = Iso_ManStart( pAig );
- Iso_ManForEachObj( p, pIso, i )
- pIso->Level = -1;
- Aig_ManForEachObj( pAig, pObj, i )
- {
- if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
- continue;
- pIso = p->pObjs + i;
- if ( Aig_ObjIsNode(pObj) )
+ Vec_PtrClear( p->vSingles );
+ Vec_PtrClear( p->vClasses );
+ for ( i = 0; i < p->nBins; i++ )
+ for ( pIso = Iso_ManObj(p, p->pBins[i]); pIso; pIso = Iso_ManObj(p, pIso->iNext) )
{
- pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
- pIso->nFinPos = 2 - pIso->nFinNeg;
- pIso->fMux = Aig_ObjIsMuxType( pObj );
- if ( Aig_ObjFaninC0(pObj) != Aig_ObjFaninC1(pObj) )
- {
- // fanins are already assigned!!!
- if ( Aig_ObjFaninC0(pObj) )
- {
- int Diff = Iso_ObjCompareBasic( Iso_ManObj(p,Aig_ObjFaninId0(pObj)), Iso_ManObj(p,Aig_ObjFaninId1(pObj)) );
- if ( Diff < 0 )
- pIso->fCLow = 1;
- else if ( Diff > 0 )
- pIso->fCHigh = 1;
- }
- else
- {
- int Diff = Iso_ObjCompareBasic( Iso_ManObj(p,Aig_ObjFaninId1(pObj)), Iso_ManObj(p,Aig_ObjFaninId0(pObj)) );
- if ( Diff < 0 )
- pIso->fCLow = 1;
- else if ( Diff > 0 )
- pIso->fCHigh = 1;
- }
- }
+ assert( pIso->Id == 0 );
+ if ( pIso->iClass )
+ Vec_PtrPush( p->vClasses, pIso );
+ else
+ Vec_PtrPush( p->vSingles, pIso );
}
- else
- pIso->fFlop = (int)(Aig_ObjPioNum(pObj) >= Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig));
- pIso->nFoutPos = Vec_IntEntry( p->vPolRefs, 2*i );
- pIso->nFoutNeg = Vec_IntEntry( p->vPolRefs, 2*i+1 );
- pIso->Level = pObj->Level;
- // add to the hash table
- Iso_ObjHashAdd( p, pIso );
- }
- return p;
+ Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare );
+ Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare );
+ assert( Vec_PtrSize(p->vSingles) == p->nSingles );
+ assert( Vec_PtrSize(p->vClasses) == p->nClasses );
+ // assign IDs to singletons
+ Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
+ if ( pIso->Id == 0 )
+ pIso->Id = p->nObjIds++;
}
/**Function*************************************************************
@@ -394,25 +304,71 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
SeeAlso []
***********************************************************************/
-void Iso_ManCollectClasses( Iso_Man_t * p )
+Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig )
{
+ Iso_Man_t * p;
Iso_Obj_t * pIso;
- int i;
- Vec_PtrClear( p->vSingles );
- Vec_PtrClear( p->vClasses );
- for ( i = 0; i < p->nBins; i++ )
- for ( pIso = Iso_ManObj(p, p->pBins[i]); pIso; pIso = Iso_ManObj(p, pIso->iNext) )
+ Aig_Obj_t * pObj;
+ int i, nNodes = 0, nEdges = 0;
+ p = Iso_ManStart( pAig );
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ if ( Aig_ObjIsNode(pObj) )
{
-// assert( pIso->Id == 0 );
- if ( pIso->iClass )
- Vec_PtrPush( p->vClasses, pIso );
- else
- Vec_PtrPush( p->vSingles, pIso );
+ pIso = p->pObjs + Aig_ObjFaninId0(pObj);
+ if ( Aig_ObjFaninC0(pObj) )
+ pIso->nFoutNeg++;
+ else
+ pIso->nFoutPos++;
+ pIso = p->pObjs + Aig_ObjFaninId1(pObj);
+ if ( Aig_ObjFaninC1(pObj) )
+ pIso->nFoutNeg++;
+ else
+ pIso->nFoutPos++;
}
- Vec_PtrSort( p->vSingles, (int (*)(void))Iso_ObjCompare );
- Vec_PtrSort( p->vClasses, (int (*)(void))Iso_ObjCompare );
- assert( Vec_PtrSize(p->vSingles) == p->nSingles );
- assert( Vec_PtrSize(p->vClasses) == p->nClasses );
+ else if ( Aig_ObjIsPo(pObj) )
+ {
+ pIso = p->pObjs + Aig_ObjFaninId0(pObj);
+ if ( Aig_ObjFaninC0(pObj) )
+ pIso->nFoutNeg++;
+ else
+ pIso->nFoutPos++;
+ }
+ }
+ Aig_ManForEachObj( pAig, pObj, i )
+ {
+ if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
+ continue;
+ pIso = p->pObjs + i;
+ pIso->Level = pObj->Level;
+ pIso->nFinNeg = Aig_ObjFaninC0(pObj) + Aig_ObjFaninC1(pObj);
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ if ( Aig_ObjIsMuxType(pObj) ) // uniqify MUX/XOR
+ pIso->nFinNeg = 3;
+ if ( Aig_ObjFaninC0(pObj) < Aig_ObjFaninC1(pObj) || (Aig_ObjFaninC0(pObj) == Aig_ObjFaninC1(pObj) && Aig_ObjFanin0(pObj)->Level < Aig_ObjFanin1(pObj)->Level) )
+ {
+ pIso->nFinLev0 = Aig_ObjFanin0(pObj)->Level;
+ pIso->nFinLev1 = Aig_ObjFanin1(pObj)->Level;
+ }
+ else
+ {
+ pIso->nFinLev0 = Aig_ObjFanin1(pObj)->Level;
+ pIso->nFinLev1 = Aig_ObjFanin0(pObj)->Level;
+ }
+// Iso_ManObjCount( pAig, pObj, &nNodes, &nEdges );
+// pIso->nNodes = nNodes;
+// pIso->nEdges = nEdges;
+ }
+ else
+ {
+ pIso->nFinLev0 = (int)(Aig_ObjPioNum(pObj) >= Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig)); // uniqify flop
+ }
+ // add to the hash table
+ Iso_ObjHashAdd( p, pIso );
+ }
+ Iso_ManCollectClasses( p );
+ return p;
}
/**Function*************************************************************
@@ -440,8 +396,6 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
if ( !fVeryVerbose )
return;
- Iso_ManCollectClasses( p );
-
printf( "Non-trivial classes:\n" );
Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
{
@@ -452,10 +406,10 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
{
if ( fOnlyCis )
- printf( " %d", Aig_ObjPioNum(Aig_ManObj(p->pAig, Iso_ObjId(p, pTemp))) );
+ printf( " %d", Aig_ObjPioNum( Iso_AigObj(p, pTemp) ) );
else
{
- Aig_Obj_t * pObj = Aig_ManObj(p->pAig, Iso_ObjId(p, pTemp));
+ Aig_Obj_t * pObj = Iso_AigObj(p, pTemp);
if ( Aig_ObjIsNode(pObj) )
printf( " %d{%s%d(%d),%s%d(%d)}", Iso_ObjId(p, pTemp),
Aig_ObjFaninC0(pObj)? "-": "+", Aig_ObjFaninId0(pObj), Aig_ObjLevel(Aig_ObjFanin0(pObj)),
@@ -489,12 +443,12 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose )
SeeAlso []
***********************************************************************/
-static inline void Iso_ObjAddToAllies( Iso_Obj_t * pIso, int Id )
+static inline void Iso_ObjAddToAllies( Iso_Obj_t * pIso, int Id, int fCompl )
{
assert( pIso->Id == 0 );
if ( pIso->vAllies == NULL )
pIso->vAllies = Vec_IntAlloc( 8 );
- Vec_IntPush( pIso->vAllies, Id );
+ Vec_IntPush( pIso->vAllies, fCompl ? -Id : Id );
}
void Iso_ManAssignAdjacency( Iso_Man_t * p )
{
@@ -518,34 +472,34 @@ void Iso_ManAssignAdjacency( Iso_Man_t * p )
if ( pIso->Id ) // unique - add to non-unique fanins
{
if ( pIso0->Id == 0 )
- Iso_ObjAddToAllies( pIso0, pIso->Id );
+ Iso_ObjAddToAllies( pIso0, pIso->Id, Aig_ObjFaninC0(pObj) );
if ( pIso1->Id == 0 )
- Iso_ObjAddToAllies( pIso1, pIso->Id );
+ Iso_ObjAddToAllies( pIso1, pIso->Id, Aig_ObjFaninC1(pObj) );
}
else // non-unique - assign unique fanins to it
{
if ( pIso0->Id != 0 )
- Iso_ObjAddToAllies( pIso, pIso0->Id );
+ Iso_ObjAddToAllies( pIso, pIso0->Id, Aig_ObjFaninC0(pObj) );
if ( pIso1->Id != 0 )
- Iso_ObjAddToAllies( pIso, pIso1->Id );
+ Iso_ObjAddToAllies( pIso, pIso1->Id, Aig_ObjFaninC1(pObj) );
}
}
// consider flops
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObj, i )
{
- if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore!
+ if ( Aig_ObjFaninId0(pObjLi) == 0 ) // ignore constant!
continue;
pIso = Iso_ManObj( p, Aig_ObjId(pObj) );
pIso0 = Iso_ManObj( p, Aig_ObjFaninId0(pObjLi) );
if ( pIso->Id ) // unique - add to non-unique fanins
{
if ( pIso0->Id == 0 )
- Iso_ObjAddToAllies( pIso0, pIso->Id );
+ Iso_ObjAddToAllies( pIso0, pIso->Id, Aig_ObjFaninC0(pObjLi) );
}
else // non-unique - assign unique fanins to it
{
if ( pIso0->Id != 0 )
- Iso_ObjAddToAllies( pIso, pIso0->Id );
+ Iso_ObjAddToAllies( pIso, pIso0->Id, Aig_ObjFaninC0(pObjLi) );
}
}
// sort
@@ -574,26 +528,39 @@ void Iso_ManRehashClassNodes( Iso_Man_t * p )
Iso_Obj_t * pIso, * pTemp;
int i;
// collect nodes
- Vec_PtrClear( p->vSingles );
+ Vec_PtrClear( p->vTemp1 );
+ Vec_PtrClear( p->vTemp2 );
Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
+ {
for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
- Vec_PtrPush( p->vSingles, pTemp );
+ if ( pTemp->Id == 0 )
+ Vec_PtrPush( p->vTemp1, pTemp );
+ else
+ Vec_PtrPush( p->vTemp2, pTemp );
+ }
// clean and add nodes
p->nClasses = 0; // total number of classes
p->nEntries = 0; // total number of entries
p->nSingles = 0; // total number of singletons
memset( p->pBins, 0, sizeof(int) * p->nBins );
- Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
+ Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp1, pTemp, i )
{
- pIso->iClass = pIso->iNext = 0;
- Iso_ObjHashAdd( p, pIso );
+ assert( pTemp->Id == 0 );
+ pTemp->iClass = pTemp->iNext = 0;
+ Iso_ObjHashAdd( p, pTemp );
}
- Vec_PtrClear( p->vSingles );
+ Vec_PtrForEachEntry( Iso_Obj_t *, p->vTemp2, pTemp, i )
+ {
+ assert( pTemp->Id != 0 );
+ pTemp->iClass = pTemp->iNext = 0;
+ }
+ // collect new classes
+ Iso_ManCollectClasses( p );
}
/**Function*************************************************************
- Synopsis [Returns one if there are unclassified CIs.]
+ Synopsis [Find nodes with the min number of edges.]
Description []
@@ -602,84 +569,33 @@ void Iso_ManRehashClassNodes( Iso_Man_t * p )
SeeAlso []
***********************************************************************/
-int Iso_ManCheckCis( Iso_Man_t * p )
+Iso_Obj_t * Iso_ManFindBestObj( Iso_Man_t * p, Iso_Obj_t * pIso )
{
- Aig_Obj_t * pObj;
- int i;
- Aig_ManForEachPi( p->pAig, pObj, i )
- if ( Aig_ObjRefs(pObj) > 0 && Iso_ManObj(p, Aig_ObjId(pObj))->Id == 0 )
- return 0;
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Finalizes unification of combinational outputs.]
-
- Description [Assigns IDs to the unclassified CIs in the order of obj IDs.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
-{
- Vec_Int_t * vRes;
- Vec_Ptr_t * vClass, * vClass2;
- Iso_Obj_t * pIso, * pTemp;
- Aig_Obj_t * pObj;
- int i, k;
-
- vClass = Vec_PtrAlloc( Aig_ManPiNum(p->pAig)-Aig_ManRegNum(p->pAig) );
- vClass2 = Vec_PtrAlloc( Aig_ManRegNum(p->pAig) );
- Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
+ Iso_Obj_t * pTemp, * pBest = NULL;
+ int nNodesBest = -1, nNodes;
+ int nEdgesBest = -1, nEdges;
+ assert( pIso->Id == 0 );
+ if ( pIso->Level == 0 )
+ return pIso;
+ for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
{
- if ( pIso->Level > 0 )
- continue;
- Vec_PtrClear( vClass );
- for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
+ assert( pTemp->Id == 0 );
+ Iso_ManObjCount( p->pAig, Iso_AigObj(p, pTemp), &nNodes, &nEdges );
+// printf( "%d,%d ", nNodes, nEdges );
+ if ( nNodesBest < nNodes || (nNodesBest == nNodes && nEdgesBest < nEdges) )
{
- assert( pTemp->Id == 0 );
- pTemp->Id = Aig_ObjPioNum(Aig_ManObj(p->pAig, Iso_ObjId(p, pTemp)));
- Vec_PtrPush( vClass, pTemp );
+ nNodesBest = nNodes;
+ nEdgesBest = nEdges;
+ pBest = pTemp;
}
- Vec_PtrSort( vClass, (int (*)(void))Iso_ObjCompareById );
- // assign IDs in this order
- Vec_PtrForEachEntry( Iso_Obj_t *, vClass, pIso, k )
- pIso->Id = p->nObjIds++;
}
-
- // assign unique IDs to the CIs
- Vec_PtrClear( vClass );
- Vec_PtrClear( vClass2 );
- Aig_ManForEachPi( p->pAig, pObj, i )
- {
- pObj->iData = Iso_ManObj(p, Aig_ObjId(pObj))->Id;
- if ( Aig_ObjPioNum(pObj) >= Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig) )
- Vec_PtrPush( vClass2, pObj );
- else
- Vec_PtrPush( vClass, pObj );
- }
- // sort CIs by their IDs
- Vec_PtrSort( vClass, (int (*)(void))Iso_ObjCompareAigObjByData );
- Vec_PtrSort( vClass2, (int (*)(void))Iso_ObjCompareAigObjByData );
-
- // create the result
- vRes = Vec_IntAlloc( Aig_ManPiNum(p->pAig) );
- Vec_PtrForEachEntry( Aig_Obj_t *, vClass, pObj, i )
- Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
- Vec_PtrForEachEntry( Aig_Obj_t *, vClass2, pObj, i )
- Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
-
- Vec_PtrFree( vClass );
- Vec_PtrFree( vClass2 );
- return vRes;
+// printf( "\n" );
+ return pBest;
}
/**Function*************************************************************
- Synopsis []
+ Synopsis [Find nodes with the min number of edges.]
Description []
@@ -688,169 +604,125 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
SeeAlso []
***********************************************************************/
-Vec_Int_t * Iso_ManFindPerm( Aig_Man_t * pAig, int fVerbose )
+void Iso_ManBreakTies( Iso_Man_t * p, int fVerbose )
{
- Iso_Man_t * p;
- Iso_Obj_t * pIso;
- Vec_Int_t * vRes;
- int i;
- p = Iso_ManCreate( pAig );
- Iso_ManPrintClasses( p, fVerbose, 0 );
- while ( p->nSingles )
+ int fUseOneBest = 0;
+ Iso_Obj_t * pIso, * pTemp;
+ int i, LevelStart = 0;
+ pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
+ LevelStart = pIso->Level;
+ if ( fVerbose )
+ printf( "Best level %d\n", LevelStart );
+ Vec_PtrForEachEntry( Iso_Obj_t *, p->vClasses, pIso, i )
{
- // collect singletons and classes
- Iso_ManCollectClasses( p );
- // assign IDs to singletons
- Vec_PtrForEachEntry( Iso_Obj_t *, p->vSingles, pIso, i )
- pIso->Id = p->nObjIds++;
- // check termination
- if ( p->nClasses == 0 )
+ if ( (int)pIso->Level < LevelStart )
break;
- // assign adjacency to classes
- Iso_ManAssignAdjacency( p );
- // rehash the class nodes
- Iso_ManRehashClassNodes( p );
- Iso_ManPrintClasses( p, fVerbose, 0 );
-
- if ( p->nSingles == 0 )
+ if ( !fUseOneBest )
{
- // assign ID to the first class
- pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
- assert( pIso->Id == 0 );
- pIso->Id = p->nObjIds++;
- // assign adjacency to classes
- Iso_ManAssignAdjacency( p );
- // rehash the class nodes
- Iso_ManRehashClassNodes( p );
- Iso_ManPrintClasses( p, fVerbose, 0 );
- if ( p->nSingles == 0 )
+ for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
{
- pIso->Id = 0;
- p->nObjIds--;
+ assert( pTemp->Id == 0 );
+ pTemp->Id = p->nObjIds++;
}
+ continue;
}
+ if ( pIso->Level == 0 && pIso->nFoutPos + pIso->nFoutNeg == 0 )
+ {
+ for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
+ pTemp->Id = p->nObjIds++;
+ continue;
+ }
+ pIso = Iso_ManFindBestObj( p, pIso );
+ pIso->Id = p->nObjIds++;
}
-// Iso_ManPrintClasses( p, fVerbose, 1 );
- vRes = Iso_ManFinalize( p );
- Iso_ManStop( p );
- return vRes;
}
/**Function*************************************************************
- Synopsis [Checks structural equivalence of AIG1 and AIG2.]
+ Synopsis [Finalizes unification of combinational outputs.]
- Description [Returns 1 if AIG1 and AIG2 are structurally equivalent
- under this mapping.]
+ Description [Assigns IDs to the unclassified CIs in the order of obj IDs.]
SideEffects []
SeeAlso []
***********************************************************************/
-int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2to1, int fVerbose )
+Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p )
{
- Aig_Obj_t * pObj, * pFanin0, * pFanin1;
+ Vec_Int_t * vRes;
+ Aig_Obj_t * pObj;
int i;
- assert( Aig_ManPiNum(pAig1) == Aig_ManPiNum(pAig2) );
- assert( Aig_ManPoNum(pAig1) == Aig_ManPoNum(pAig2) );
- assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) );
- assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) );
- Aig_ManCleanData( pAig1 );
- // map const and PI nodes
- Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1);
- Aig_ManForEachPi( pAig2, pObj, i )
- pObj->pData = Aig_ManPi( pAig1, Vec_IntEntry(vMap2to1, i) );
- // try internal nodes
- Aig_ManForEachNode( pAig2, pObj, i )
+ assert( p->nClasses == 0 );
+ assert( Vec_PtrSize(p->vClasses) == 0 );
+ // set canonical numbers
+ Aig_ManForEachObj( p->pAig, pObj, i )
{
- pFanin0 = Aig_ObjChild0Copy( pObj );
- pFanin1 = Aig_ObjChild1Copy( pObj );
- pObj->pData = Aig_TableLookupTwo( pAig1, pFanin0, pFanin1 );
- if ( pObj->pData == NULL )
+ if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) )
{
- if ( fVerbose )
- printf( "Structural equivalence failed at node %d.\n", i );
- return 0;
+ pObj->iData = -1;
+ continue;
}
+ pObj->iData = Iso_ManObj(p, Aig_ObjId(pObj))->Id;
+ assert( pObj->iData > 0 );
}
- // make sure the first PO points to the same node
- if ( Aig_ManPoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManPo(pAig2, 0)) != Aig_ObjChild0(Aig_ManPo(pAig1, 0)) )
+ Aig_ManConst1(p->pAig)->iData = 0;
+ // assign unique IDs to the CIs
+ Vec_PtrClear( p->vTemp1 );
+ Vec_PtrClear( p->vTemp2 );
+ Aig_ManForEachPi( p->pAig, pObj, i )
{
- if ( fVerbose )
- printf( "Structural equivalence failed at primary output 0.\n" );
- return 0;
+ assert( pObj->iData > 0 );
+ if ( Aig_ObjPioNum(pObj) >= Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop
+ Vec_PtrPush( p->vTemp2, pObj );
+ else // PI
+ Vec_PtrPush( p->vTemp1, pObj );
}
- return 1;
+ // sort CIs by their IDs
+ Vec_PtrSort( p->vTemp1, (int (*)(void))Iso_ObjCompareAigObjByData );
+ Vec_PtrSort( p->vTemp2, (int (*)(void))Iso_ObjCompareAigObjByData );
+ // create the result
+ vRes = Vec_IntAlloc( Aig_ManPiNum(p->pAig) );
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i )
+ Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
+ Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i )
+ Vec_IntPush( vRes, Aig_ObjPioNum(pObj) );
+ return vRes;
}
-//static int s_Counter;
-
/**Function*************************************************************
- Synopsis [Finds mapping of CIs of AIG2 into those of AIG1.]
+ Synopsis [Find nodes with the min number of edges.]
- Description [Returns the mapping of CIs of the two AIGs, or NULL
- if there is no mapping.]
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vPerm1_, Vec_Int_t * vPerm2_, int fVerbose )
+void Iso_ManDumpOneClass( Iso_Man_t * p )
{
- Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2;
- int i, Entry;
- if ( Aig_ManPiNum(pAig1) != Aig_ManPiNum(pAig2) )
- return NULL;
- if ( Aig_ManPoNum(pAig1) != Aig_ManPoNum(pAig2) )
- return NULL;
- if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) )
- return NULL;
- if ( Aig_ManNodeNum(pAig1) != Aig_ManNodeNum(pAig2) )
- return NULL;
- if ( Aig_ManLevelNum(pAig1) != Aig_ManLevelNum(pAig2) )
- return NULL;
- if ( Iso_ManNegEdgeNum(pAig1) != Iso_ManNegEdgeNum(pAig2) )
- return NULL;
-// s_Counter++;
-
- if ( fVerbose )
- printf( "AIG1:\n" );
- vPerm1 = vPerm1_ ? vPerm1_ : Iso_ManFindPerm( pAig1, fVerbose );
- if ( fVerbose )
- printf( "AIG1:\n" );
- vPerm2 = vPerm2_ ? vPerm2_ : Iso_ManFindPerm( pAig2, fVerbose );
- if ( vPerm1_ )
- assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) );
- if ( vPerm2_ )
- assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) );
- // find canonical permutation
- // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2
- vInvPerm2 = Vec_IntInvert( vPerm2, -1 );
- Vec_IntForEachEntry( vInvPerm2, Entry, i )
+ Vec_Ptr_t * vNodes = Vec_PtrAlloc( 100 );
+ Iso_Obj_t * pIso, * pTemp;
+ Aig_Man_t * pNew = NULL;
+ assert( p->nClasses > 0 );
+ pIso = (Iso_Obj_t *)Vec_PtrEntry( p->vClasses, 0 );
+ assert( pIso->Id == 0 );
+ for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) )
{
- assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) );
- Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) );
+ assert( pTemp->Id == 0 );
+ Vec_PtrPush( vNodes, Iso_AigObj(p, pTemp) );
}
- if ( vPerm1_ == NULL )
- Vec_IntFree( vPerm1 );
- if ( vPerm2_ == NULL )
- Vec_IntFree( vPerm2 );
- // check if they are indeed equivalent
- if ( !Iso_ManCheckMapping( pAig1, pAig2, vInvPerm2, fVerbose ) )
- Vec_IntFreeP( &vInvPerm2 );
- return vInvPerm2;
+ pNew = Aig_ManDupNodes( p->pAig, vNodes );
+ Vec_PtrFree( vNodes );
+ Aig_ManShow( pNew, 0, NULL );
+ Aig_ManStopP( &pNew );
}
-
-
-#include "src/aig/saig/saig.h"
-
/**Function*************************************************************
- Synopsis []
+ Synopsis [Finds canonical permutation of CIs and assigns unique IDs.]
Description []
@@ -859,161 +731,40 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t
SeeAlso []
***********************************************************************/
-Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, int fVerbose )
+Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose )
{
- int fVeryVerbose = 0;
- Vec_Ptr_t * vParts, * vPerms, * vAigs;
- Vec_Int_t * vPos, * vMap;
- Aig_Man_t * pPart, * pTemp;
- int i, k, nPos;
-
- // derive AIG for each PO
- nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig);
- vParts = Vec_PtrAlloc( nPos );
- vPerms = Vec_PtrAlloc( nPos );
- for ( i = 0; i < nPos; i++ )
- {
- pPart = Saig_ManDupCones( pAig, &i, 1 );
- vMap = Iso_ManFindPerm( pPart, fVeryVerbose );
- Vec_PtrPush( vParts, pPart );
- Vec_PtrPush( vPerms, vMap );
- }
-// s_Counter = 0;
-
- // check AIGs for each PO
- vAigs = Vec_PtrAlloc( 1000 );
- vPos = Vec_IntAlloc( 1000 );
- Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
+ Vec_Int_t * vRes;
+ Iso_Man_t * p;
+ p = Iso_ManCreate( pAig );
+ Iso_ManPrintClasses( p, fVerbose, 0 );
+ while ( p->nClasses )
{
- if ( fVeryVerbose )
- {
- printf( "AIG %4d : ", i );
- Aig_ManPrintStats( pPart );
- }
- Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, k )
- {
- if ( fVeryVerbose )
- printf( "Comparing AIG %4d and AIG %4d. ", Vec_IntEntry(vPos,k), i );
- vMap = Iso_ManFindMapping( pTemp, pPart,
- (Vec_Int_t *)Vec_PtrEntry(vPerms, Vec_IntEntry(vPos,k)),
- (Vec_Int_t *)Vec_PtrEntry(vPerms, i),
- fVeryVerbose );
- if ( vMap != NULL )
- {
- if ( fVeryVerbose )
- printf( "Found match\n" );
- if ( fVerbose )
- printf( "Found match for AIG %4d and AIG %4d.\n", Vec_IntEntry(vPos,k), i );
- Vec_IntFree( vMap );
- break;
- }
- if ( fVeryVerbose )
- printf( "No match.\n" );
- }
- if ( k == Vec_PtrSize(vAigs) )
+ // assign adjacency to classes
+ Iso_ManAssignAdjacency( p );
+ // rehash the class nodes
+ Iso_ManRehashClassNodes( p );
+ Iso_ManPrintClasses( p, fVerbose, 0 );
+ // force refinement
+ while ( p->nSingles == 0 && p->nClasses )
{
- Vec_PtrPush( vAigs, pPart );
- Vec_IntPush( vPos, i );
+ // assign IDs to the topmost level of classes
+ Iso_ManBreakTies( p, fVerbose );
+ // assign adjacency to classes
+ Iso_ManAssignAdjacency( p );
+ // rehash the class nodes
+ Iso_ManRehashClassNodes( p );
+ Iso_ManPrintClasses( p, fVerbose, 0 );
}
}
- // delete AIGs
- Vec_PtrForEachEntry( Aig_Man_t *, vParts, pPart, i )
- Aig_ManStop( pPart );
- Vec_PtrFree( vParts );
- Vec_PtrForEachEntry( Vec_Int_t *, vPerms, vMap, i )
- Vec_IntFree( vMap );
- Vec_PtrFree( vPerms );
- // derive the resulting AIG
- pPart = Saig_ManDupCones( pAig, Vec_IntArray(vPos), Vec_IntSize(vPos) );
- Vec_PtrFree( vAigs );
- Vec_IntFree( vPos );
-
-// printf( "The number of all checks %d. Complex checks %d.\n", nPos*(nPos-1)/2, s_Counter );
- return pPart;
-}
-
-
-#include "src/base/abc/abc.h"
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig1, int fVerbose )
-{
- extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
- extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
- Abc_Ntk_t * pNtk;
- Aig_Man_t * pAig2;
- Vec_Int_t * vMap;
-
- pNtk = Abc_NtkFromAigPhase( pAig1 );
- Abc_NtkPermute( pNtk, 1, 0, 1 );
- pAig2 = Abc_NtkToDar( pNtk, 0, 1 );
- Abc_NtkDelete( pNtk );
-
- vMap = Iso_ManFindMapping( pAig1, pAig2, NULL, NULL, fVerbose );
- Aig_ManStop( pAig2 );
-
- if ( vMap != NULL )
- {
- printf( "Mapping of AIGs is found.\n" );
- if ( fVerbose )
- Vec_IntPrint( vMap );
- }
- else
- printf( "Mapping of AIGs is NOT found.\n" );
- Vec_IntFreeP( &vMap );
- return NULL;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Iso_ManTest666( Aig_Man_t * pAig, int fVerbose )
-{
- Aig_Man_t * pPart;
- int clk = clock();
- pPart = Iso_ManFilterPos( pAig, fVerbose );
- printf( "Reduced %d outputs to %d outputs. ", Saig_ManPoNum(pAig), Saig_ManPoNum(pPart) );
- Abc_PrintTime( 1, "Time", clock() - clk );
-// Aig_ManStop( pPart );
- return pPart;
+// printf( "IDs assigned = %d. Objects = %d.\n", p->nObjIds, 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
+ assert( p->nObjIds == 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) );
+// if ( p->nClasses )
+// Iso_ManDumpOneClass( p );
+ vRes = Iso_ManFinalize( p );
+ Iso_ManStop( p );
+ return vRes;
}
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Aig_Man_t * Iso_ManTest777( Aig_Man_t * pAig, int fVerbose )
-{
- Vec_Int_t * vPerm;
- vPerm = Iso_ManFindPerm( pAig, fVerbose );
- Vec_IntFree( vPerm );
- return NULL;
-}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a4b5d566..8a95e252 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -278,6 +278,7 @@ static int Abc_CommandReconcile ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandCexMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDualRail ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlockPo ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIso ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -690,6 +691,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "cexmin", Abc_CommandCexMin, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dualrail", Abc_CommandDualRail, 1 );
Cmd_CommandAdd( pAbc, "Verification", "blockpo", Abc_CommandBlockPo, 1 );
+ Cmd_CommandAdd( pAbc, "Verification", "iso", Abc_CommandIso, 1 );
Cmd_CommandAdd( pAbc, "ABC9", "&get", Abc_CommandAbc9Get, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&put", Abc_CommandAbc9Put, 0 );
@@ -8839,17 +8841,26 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern int Abc_NtkSuppSizeTest( Abc_Ntk_t * p );
extern Aig_Man_t * Iso_ManTest( Aig_Man_t * pAig, int fVerbose );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+ extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig );
if ( pNtk )
{
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Aig_Man_t * pRes;
- Abc_Ntk_t * pNtkRes;
+// Abc_Ntk_t * pNtkRes;
// Aig_ManInterRepar( pAig, 1 );
// Aig_ManInterTest( pAig, 1 );
// Aig_ManSupportsTest( pAig );
// Aig_SupportSizeTest( pAig );
+ if ( !fNewAlgo )
+ Saig_IsoDetectFast( pAig );
+ else
+ {
+ pRes = Iso_ManTest( pAig, fVerbose );
+ Aig_ManStopP( &pRes );
+ }
+
+/*
pRes = Iso_ManTest( pAig, fVerbose );
- Aig_ManStop( pAig );
if ( pRes != NULL )
{
pNtkRes = Abc_NtkFromAigPhase( pRes );
@@ -8859,6 +8870,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
pNtkRes->pName = Extra_UtilStrsav(pNtk->pName);
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
+*/
+ Aig_ManStop( pAig );
}
}
@@ -21300,6 +21313,77 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandIso( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+ extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+ Abc_Ntk_t * pNtk, * pNtkNew = NULL;
+ Aig_Man_t * pAig, * pTemp;
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ Abc_Print( -2, "Unknown switch.\n");
+ goto usage;
+ }
+ }
+
+ // check the main AIG
+ pNtk = Abc_FrameReadNtk(pAbc);
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Main AIG: There is no current network.\n");
+ return 0;
+ }
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
+ return 0;
+ }
+ if ( Abc_NtkPoNum(pNtk) == 1 )
+ {
+ Abc_Print( 1, "Current AIG has only one PO. Transformation is not performed.\n");
+ return 0;
+ }
+
+ // transform
+ pAig = Abc_NtkToDar( pNtk, 0, 1 );
+ pTemp = Saig_ManIsoReduce( pAig, fVerbose );
+ pNtkNew = Abc_NtkFromAigPhase( pTemp );
+ Aig_ManStop( pTemp );
+ Aig_ManStop( pAig );
+
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: iso [-vh]\n" );
+ Abc_Print( -2, "\t removes POs with isomorphic sequential COI\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandTraceStart( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
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) {
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index be54e583..39ab2623 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -1259,6 +1259,26 @@ static inline void Vec_IntPrint( Vec_Int_t * vVec )
printf( " }\n" );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Vec_IntCompareVec( Vec_Int_t * p1, Vec_Int_t * p2 )
+{
+ if ( p1 == NULL || p2 == NULL )
+ return (p1 != NULL) - (p2 != NULL);
+ if ( Vec_IntSize(p1) != Vec_IntSize(p2) )
+ return Vec_IntSize(p1) - Vec_IntSize(p2);
+ return memcmp( Vec_IntArray(p1), Vec_IntArray(p2), sizeof(int)*Vec_IntSize(p1) );
+}
+
ABC_NAMESPACE_HEADER_END
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index cec3e7e1..c794dc2f 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -650,6 +650,26 @@ static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
(int (*)(const void *, const void *)) Vec_StrSortCompare1 );
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Vec_StrCompareVec( Vec_Str_t * p1, Vec_Str_t * p2 )
+{
+ if ( p1 == NULL || p2 == NULL )
+ return (p1 != NULL) - (p2 != NULL);
+ if ( Vec_StrSize(p1) != Vec_StrSize(p2) )
+ return Vec_StrSize(p1) - Vec_StrSize(p2);
+ return memcmp( Vec_StrArray(p1), Vec_StrArray(p2), Vec_StrSize(p1) );
+}
+
ABC_NAMESPACE_HEADER_END
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 22:40:49 +0000