Skip to content

A
abc
Commit c5067f7d by Alan Mishchenko
Options

Graph isomorphism checking code.

parent 71891354
Showing with 254 additions and 23 deletions
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
......
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 );
......
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 ///
......
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 \
......
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 =======================================================*/
......
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" );
......
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 \
......
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 );
......
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);
......
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;
......
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 );
......
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;
......
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) {
......
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
......
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
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment