luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Unifification of custom extensions.

This commit is contained in:
Alan Mishchenko 2012-12-10 13:56:40 -08:00
parent f7b7ab59cf
commit 2575a5d683
27 changed files with 897 additions and 1231 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -3411,6 +3411,10 @@ SOURCE=.\src\aig\gia\giaAiger.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaAigerExt.c
# End Source File
# Begin Source File
SOURCE=.\src\aig\gia\giaBidec.c
# End Source File
# Begin Source File

62
src/aig/gia/gia.h
View File

@ -140,6 +140,10 @@ struct Gia_Man_t_
Vec_Int_t * vDoms; // dominators
unsigned char* pSwitching; // switching activity for each object
Gia_Plc_t * pPlacement; // placement of the objects
Gia_Man_t * pAigExtra; // combinational logic of holes
Vec_Flt_t * vInArrs; // PI arrival times
Vec_Flt_t * vOutReqs; // PO required times
Vec_Int_t * vPacking; // packing information
int * pTravIds; // separate traversal ID representation
int nTravIdsAlloc; // the number of trav IDs allocated
Vec_Ptr_t * vNamesIn; // the input names
@ -593,6 +597,52 @@ static inline void Gia_ObjTerSimPrint( Gia_Obj_t * pObj )
printf( "X" );
}
static inline int Gia_AigerReadInt( unsigned char * pPos )
{
int i, Value = 0;
for ( i = 0; i < 4; i++ )
Value = (Value << 8) | *pPos++;
return Value;
}
static inline void Gia_AigerWriteInt( unsigned char * pPos, int Value )
{
int i;
for ( i = 3; i >= 0; i-- )
*pPos++ = (Value >> (8*i)) & 255;
}
static inline unsigned Gia_AigerReadUnsigned( unsigned char ** ppPos )
{
unsigned x = 0, i = 0;
unsigned char ch;
while ((ch = *(*ppPos)++) & 0x80)
x |= (ch & 0x7f) << (7 * i++);
return x | (ch << (7 * i));
}
static inline void Gia_AigerWriteUnsigned( Vec_Str_t * vStr, unsigned x )
{
unsigned char ch;
while (x & ~0x7f)
{
ch = (x & 0x7f) | 0x80;
Vec_StrPush( vStr, ch );
x >>= 7;
}
ch = x;
Vec_StrPush( vStr, ch );
}
static inline int Gia_AigerWriteUnsignedBuffer( unsigned char * pBuffer, int Pos, unsigned x )
{
unsigned char ch;
while (x & ~0x7f)
{
ch = (x & 0x7f) | 0x80;
pBuffer[Pos++] = ch;
x >>= 7;
}
ch = x;
pBuffer[Pos++] = ch;
return Pos;
}
static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); }
static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; }
@ -712,13 +762,13 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
/*=== giaAiger.c ===========================================================*/
extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
extern Gia_Man_t * Gia_ReadAiger( char * pFileName, int fSkipStrash, int fCheck );
extern void Gia_WriteAiger( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
extern Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fSkipStrash, int fCheck );
extern Gia_Man_t * Gia_AigerRead( char * pFileName, int fSkipStrash, int fCheck );
extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
extern Vec_Str_t * Gia_WriteAigerIntoMemoryStr( Gia_Man_t * p );
extern Vec_Str_t * Gia_WriteAigerIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
extern void Gia_WriteAigerSimple( Gia_Man_t * pInit, char * pFileName );
extern Vec_Str_t * Gia_AigerWriteIntoMemoryStr( Gia_Man_t * p );
extern Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs );
extern void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFileName );
/*=== giaBidec.c ===========================================================*/
extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );

1654
src/aig/gia/giaAiger.c
View File

File diff suppressed because it is too large Load Diff

240
src/aig/gia/giaAigerExt.c Normal file
View File

@ -0,0 +1,240 @@
/**CFile****************************************************************
FileName [giaAigerExt.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Custom AIGER extensions.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaAigerExt.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Read/write equivalence classes information.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Rpr_t * Gia_AigerReadEquivClasses( unsigned char ** ppPos, int nSize )
{
Gia_Rpr_t * pReprs;
unsigned char * pStop;
int i, Item, fProved, iRepr, iNode;
pStop = *ppPos;
pStop += Gia_AigerReadInt( *ppPos ); *ppPos += 4;
pReprs = ABC_CALLOC( Gia_Rpr_t, nSize );
for ( i = 0; i < nSize; i++ )
pReprs[i].iRepr = GIA_VOID;
iRepr = iNode = 0;
while ( *ppPos < pStop )
{
Item = Gia_AigerReadUnsigned( ppPos );
if ( Item & 1 )
{
iRepr += (Item >> 1);
iNode = iRepr;
continue;
}
Item >>= 1;
fProved = (Item & 1);
Item >>= 1;
iNode += Item;
pReprs[iNode].fProved = fProved;
pReprs[iNode].iRepr = iRepr;
assert( iRepr < iNode );
}
return pReprs;
}
unsigned char * Gia_WriteEquivClassesInt( Gia_Man_t * p, int * pEquivSize )
{
unsigned char * pBuffer;
int iRepr, iNode, iPrevRepr, iPrevNode, iLit, nItems, iPos;
assert( p->pReprs && p->pNexts );
// count the number of entries to be written
nItems = 0;
for ( iRepr = 1; iRepr < Gia_ManObjNum(p); iRepr++ )
{
nItems += Gia_ObjIsConst( p, iRepr );
if ( !Gia_ObjIsHead(p, iRepr) )
continue;
Gia_ClassForEachObj( p, iRepr, iNode )
nItems++;
}
pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 10) );
// write constant class
iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, 4, Abc_Var2Lit(0, 1) );
iPrevNode = 0;
for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ )
if ( Gia_ObjIsConst(p, iNode) )
{
iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
iPrevNode = iNode;
iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
}
// write non-constant classes
iPrevRepr = 0;
Gia_ManForEachClass( p, iRepr )
{
iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) );
iPrevRepr = iPrevNode = iRepr;
Gia_ClassForEachObj1( p, iRepr, iNode )
{
iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) );
iPrevNode = iNode;
iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Abc_Var2Lit(iLit, 0) );
}
}
Gia_AigerWriteInt( pBuffer, iPos );
*pEquivSize = iPos;
return pBuffer;
}
Vec_Str_t * Gia_WriteEquivClasses( Gia_Man_t * p )
{
int nEquivSize;
unsigned char * pBuffer = Gia_WriteEquivClassesInt( p, &nEquivSize );
return Vec_StrAllocArray( pBuffer, nEquivSize );
}
/**Function*************************************************************
Synopsis [Read/write mapping information.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Gia_AigerReadDiffValue( unsigned char ** ppPos, int iPrev )
{
int Item = Gia_AigerReadUnsigned( ppPos );
if ( Item & 1 )
return iPrev + (Item >> 1);
return iPrev - (Item >> 1);
}
int * Gia_AigerReadMapping( unsigned char ** ppPos, int nSize )
{
int * pMapping;
unsigned char * pStop;
int k, j, nFanins, nAlloc, iNode = 0, iOffset = nSize;
pStop = *ppPos;
pStop += Gia_AigerReadInt( *ppPos ); *ppPos += 4;
nAlloc = nSize + pStop - *ppPos;
pMapping = ABC_CALLOC( int, nAlloc );
while ( *ppPos < pStop )
{
k = iOffset;
pMapping[k++] = nFanins = Gia_AigerReadUnsigned( ppPos );
for ( j = 0; j <= nFanins; j++ )
pMapping[k++] = iNode = Gia_AigerReadDiffValue( ppPos, iNode );
pMapping[iNode] = iOffset;
iOffset = k;
}
assert( iOffset <= nAlloc );
return pMapping;
}
static inline int Gia_AigerWriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis )
{
if ( iPrev < iThis )
return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) );
return Gia_AigerWriteUnsignedBuffer( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) );
}
unsigned char * Gia_AigerWriteMappingInt( Gia_Man_t * p, int * pMapSize )
{
unsigned char * pBuffer;
int i, k, iPrev, iFan, nItems, iPos = 4;
assert( p->pMapping );
// count the number of entries to be written
nItems = 0;
Gia_ManForEachLut( p, i )
nItems += 2 + Gia_ObjLutSize( p, i );
pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) );
// write non-constant classes
iPrev = 0;
Gia_ManForEachLut( p, i )
{
//printf( "\nSize = %d ", Gia_ObjLutSize(p, i) );
iPos = Gia_AigerWriteUnsignedBuffer( pBuffer, iPos, Gia_ObjLutSize(p, i) );
Gia_LutForEachFanin( p, i, iFan, k )
{
//printf( "Fan = %d ", iFan );
iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, iFan );
iPrev = iFan;
}
iPos = Gia_AigerWriteDiffValue( pBuffer, iPos, iPrev, i );
iPrev = i;
//printf( "Node = %d ", i );
}
//printf( "\n" );
Gia_AigerWriteInt( pBuffer, iPos );
*pMapSize = iPos;
return pBuffer;
}
Vec_Str_t * Gia_AigerWriteMapping( Gia_Man_t * p )
{
int nMapSize;
unsigned char * pBuffer = Gia_AigerWriteMappingInt( p, &nMapSize );
return Vec_StrAllocArray( pBuffer, nMapSize );
}
/**Function*************************************************************
Synopsis [Read/write packing information.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_AigerReadPacking( unsigned char ** ppPos, int nSize )
{
Vec_Int_t * vPacking = Vec_IntStart( nSize/4 );
assert( nSize % 4 == 0 );
memcpy( Vec_IntArray(vPacking), *ppPos, nSize );
*ppPos += nSize;
return vPacking;
}
Vec_Str_t * Gia_WritePacking( Vec_Int_t * vPacking )
{
Vec_Str_t * vBuffer = Vec_StrStart( 4*Vec_IntSize(vPacking) );
memcpy( Vec_StrArray(vBuffer), Vec_IntArray(vPacking), 4*sizeof(int) );
return vBuffer;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

14
src/aig/gia/giaEquiv.c
View File

@ -1203,7 +1203,7 @@ void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fSkipSome, int fVerb
return;
}
// read AIGER file
pMiter = Gia_ReadAiger( pFileName, 0, 0 );
pMiter = Gia_AigerRead( pFileName, 0, 0 );
if ( pMiter == NULL )
{
Abc_Print( 1, "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
@ -1722,14 +1722,14 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
}
}
// write equivalence classes
Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
Gia_AigerWrite( pGia, "gore.aig", 0, 0 );
// reduce the model
pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0, 0 );
if ( pReduce )
{
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
// Gia_ManPrintStatsShort( pReduce );
Gia_ManStop( pReduce );
@ -1762,13 +1762,13 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
Abc_Print( 1, "Equivalences are not defined.\n" );
return 0;
}
pGia1 = Gia_ReadAiger( pName1, 0, 0 );
pGia1 = Gia_AigerRead( pName1, 0, 0 );
if ( pGia1 == NULL )
{
Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
return 0;
}
pGia2 = Gia_ReadAiger( pName2, 0, 0 );
pGia2 = Gia_AigerRead( pName2, 0, 0 );
if ( pGia2 == NULL )
{
Gia_ManStop( pGia2 );
@ -1901,13 +1901,13 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
Abc_Print( 1, "Equivalences are not defined.\n" );
return 0;
}
pGia1 = Gia_ReadAiger( pName1, 0, 0 );
pGia1 = Gia_AigerRead( pName1, 0, 0 );
if ( pGia1 == NULL )
{
Abc_Print( 1, "Cannot read first file %s.\n", pName1 );
return 0;
}
pGia2 = Gia_ReadAiger( pName2, 0, 0 );
pGia2 = Gia_AigerRead( pName2, 0, 0 );
if ( pGia2 == NULL )
{
Gia_ManStop( pGia2 );

2
src/aig/gia/giaHcd.c
View File

@ -626,7 +626,7 @@ Aig_Man_t * Hcd_ComputeChoices( Aig_Man_t * pAig, int nBTLimit, int fSynthesis,
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
Gia_ManStop( pGia );
Gia_WriteAiger( pMiter, "m3.aig", 0, 0 );
Gia_AigerWrite( pMiter, "m3.aig", 0, 0 );
}
else
{

6
src/aig/gia/giaIso.c
View File

@ -1043,7 +1043,7 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_
{
assert( Gia_ManPoNum(pPart) == 1 );
assert( Gia_ManObjNum(pPart) == 2 );
vStr = Gia_WriteAigerIntoMemoryStr( pPart );
vStr = Gia_AigerWriteIntoMemoryStr( pPart );
Gia_ManStop( pPart );
if ( pvPiPerm )
*pvPiPerm = Vec_IntAlloc( 0 );
@ -1060,7 +1060,7 @@ Vec_Str_t * Gia_ManIsoFindString( Gia_Man_t * p, int iPo, int fVerbose, Vec_Int_
//printf( "Internal: " );
//Vec_IntPrint( vCis );
// derive the AIGER string
vStr = Gia_WriteAigerIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) );
vStr = Gia_AigerWriteIntoMemoryStrPart( pPart, vCis, vAnds, vCos, Gia_ManRegNum(pPart) );
// cleanup
Vec_IntFree( vCis );
Vec_IntFree( vAnds );
@ -1280,7 +1280,7 @@ void Gia_IsoTest( Gia_Man_t * p, Abc_Cex_t * pCex, int fVerbose )
// create AIG with two primary outputs (original and permuted)
pPerm = Gia_ManDupPerm( p, vPiPerm );
pDouble = Gia_ManDupAppendNew( p, pPerm );
//Gia_WriteAiger( pDouble, "test.aig", 0, 0 );
//Gia_AigerWrite( pDouble, "test.aig", 0, 0 );
// analyze the two-output miter
pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0 );

8
src/aig/gia/giaMan.c
View File

@ -94,6 +94,10 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_WrdFreeP( &p->vTtMemory );
Vec_PtrFreeP( &p->vTtInputs );
Vec_IntFreeP( &p->vMapping );
Vec_IntFreeP( &p->vPacking );
Vec_FltFreeP( &p->vInArrs );
Vec_FltFreeP( &p->vOutReqs );
Gia_ManStopP( &p->pAigExtra );
Vec_IntFree( p->vCis );
Vec_IntFree( p->vCos );
ABC_FREE( p->pData2 );
@ -161,10 +165,10 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p )
{
Gia_Man_t * pTemp;
pTemp = Gia_ManDupFlopClass( p, 1 );
Gia_WriteAiger( pTemp, "dom1.aig", 0, 0 );
Gia_AigerWrite( pTemp, "dom1.aig", 0, 0 );
Gia_ManStop( pTemp );
pTemp = Gia_ManDupFlopClass( p, 2 );
Gia_WriteAiger( pTemp, "dom2.aig", 0, 0 );
Gia_AigerWrite( pTemp, "dom2.aig", 0, 0 );
Gia_ManStop( pTemp );
}
}

1
src/aig/gia/module.make
View File

@ -1,6 +1,7 @@
SRC += src/aig/gia/gia.c \
src/aig/gia/giaAig.c \
src/aig/gia/giaAiger.c \
src/aig/gia/giaAigerExt.c \
src/aig/gia/giaBidec.c \
src/aig/gia/giaCCof.c \
src/aig/gia/giaCex.c \

30
src/base/abci/abc.c
View File

@ -12840,7 +12840,7 @@ int Abc_CommandRecStart2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pGia = Gia_ReadAiger( FileName, 1, 0 );
pGia = Gia_AigerRead( FileName, 1, 0 );
if ( pGia == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -13059,7 +13059,7 @@ int Abc_CommandRecDump2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
// get the input file name
FileName = pArgvNew[0];
Gia_WriteAiger( pGia, FileName, 0, 0 );
Gia_AigerWrite( pGia, FileName, 0, 0 );
}
return 0;
@ -13188,7 +13188,7 @@ int Abc_CommandRecMerge2( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pGia = Gia_ReadAiger( FileName, 0, 0 );
pGia = Gia_AigerRead( FileName, 0, 0 );
if ( pGia == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -13299,7 +13299,7 @@ int Abc_CommandRecStart3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pGia = Gia_ReadAiger( FileName, 1, 0 );
pGia = Gia_AigerRead( FileName, 1, 0 );
if ( pGia == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -13531,7 +13531,7 @@ int Abc_CommandRecDump3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "No structure in the library.\n" );
return 1;
}
Gia_WriteAiger( pGia, FileName, 0, 0 );
Gia_AigerWrite( pGia, FileName, 0, 0 );
}
return 0;
@ -13605,7 +13605,7 @@ int Abc_CommandRecMerge3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pGia = Gia_ReadAiger( FileName, 1, 0 );
pGia = Gia_AigerRead( FileName, 1, 0 );
if ( pGia == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -23444,7 +23444,7 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
}
fclose( pFile );
pAig = Gia_ReadAiger( FileName, fSkipStrash, 0 );
pAig = Gia_AigerRead( FileName, fSkipStrash, 0 );
Abc_CommandUpdate9( pAbc, pAig );
return 0;
@ -23830,11 +23830,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fUnique )
{
Gia_Man_t * pGia = Gia_ManIsoCanonicize( pAbc->pGia, fVerbose );
Gia_WriteAigerSimple( pGia, pFileName );
Gia_AigerWriteSimple( pGia, pFileName );
Gia_ManStop( pGia );
}
else
Gia_WriteAiger( pAbc->pGia, pFileName, 0, 0 );
Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
return 0;
usage:
@ -25942,7 +25942,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pSecond = Gia_ReadAiger( FileName, 0, 0 );
pSecond = Gia_AigerRead( FileName, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -26024,7 +26024,7 @@ int Abc_CommandAbc9Append( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pSecond = Gia_ReadAiger( FileName, 0, 0 );
pSecond = Gia_AigerRead( FileName, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
@ -26689,7 +26689,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
}
Gia_WriteAiger( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 );
Gia_AigerWrite( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 );
Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
@ -26702,7 +26702,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pTemp, pFileName2, 0, 0 );
Gia_AigerWrite( pTemp, pFileName2, 0, 0 );
Abc_Print( 1, "Reduced original network was written into file \"%s\".\n", pFileName2 );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
@ -26803,7 +26803,7 @@ int Abc_CommandAbc9Srm2( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pTemp, pFileName, 0, 0 );
Gia_AigerWrite( pTemp, pFileName, 0, 0 );
Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
@ -27122,7 +27122,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
fclose( pFile );
pSecond = Gia_ReadAiger( FileName, 0, 0 );
pSecond = Gia_AigerRead( FileName, 0, 0 );
if ( pSecond == NULL )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );

2
src/base/abci/abcRec2.c
View File

@ -581,7 +581,7 @@ void Abc_NtkRecFilter2(int nLimit)
// remove dangling nodes and POs driven by constants
newPGia = Abc_NtkDupWithoutDangling2(pGia);
sprintf( fileName, "RecLib%d_Filtered%d.aig", p->nVars, nLimit);
Gia_WriteAiger( newPGia, fileName, 0, 0 );
Gia_AigerWrite( newPGia, fileName, 0, 0 );
Abc_Print(1, "Library %s was written.", fileName);
//Gia_ManHashStop(newPGia);
Gia_ManStop(newPGia);

6
src/base/abci/abcTim.c
View File

@ -223,7 +223,7 @@ void Abc_NtkTestPinGia( Abc_Ntk_t * pNtk, int fWhiteBoxOnly, int fVerbose )
Gia_Man_t * pGia;
char * pFileName = "testpin.aig";
pGia = Abc_NtkTestPinDeriveGia( pNtk, fWhiteBoxOnly, fVerbose );
Gia_WriteAiger( pGia, pFileName, 0, 0 );
Gia_AigerWrite( pGia, pFileName, 0, 0 );
Gia_ManStop( pGia );
printf( "AIG with pins derived from mapped network \"%s\" was written into file \"%s\".\n",
Abc_NtkName(pNtk), pFileName );
@ -426,13 +426,13 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
Gia_ManReverseClasses( pGia, 0 );
}
// write file
Gia_WriteAiger( pGia, pFileName, 0, 0 );
Gia_AigerWrite( pGia, pFileName, 0, 0 );
// unnormalize choices
if ( Gia_ManWithChoices(pGia) )
Gia_ManReverseClasses( pGia, 1 );
// read file
pGia2 = Gia_ReadAiger( pFileName, 1, 1 );
pGia2 = Gia_AigerRead( pFileName, 1, 1 );
// normalize choices
if ( Gia_ManWithChoices(pGia2) )

4
src/base/cmd/cmdPlugin.c
View File

@ -391,7 +391,7 @@ Gia_Man_t * Abc_ManReadAig( char * pFileName, char * pToken )
fclose( pFile );
}
// derive AIG
pGia = Gia_ReadAigerFromMemory( pStr, nBinaryPart, 0, 0 );
pGia = Gia_AigerReadFromMemory( pStr, nBinaryPart, 0, 0 );
}
Vec_StrFree( vStr );
return pGia;
@ -513,7 +513,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// create input file
Gia_WriteAiger( pAbc->pGia, pFileIn, 0, 0 );
Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0 );
// create command line
vCommand = Vec_StrAlloc( 100 );

4
src/misc/tim/tim.h
View File

@ -122,8 +122,8 @@ extern float * Tim_ManBoxDelayTable( Tim_Man_t * p, int iBox );
extern int Tim_ManBoxCopy( Tim_Man_t * p, int iBox );
extern void Tim_ManBoxSetCopy( Tim_Man_t * p, int iBox, int iCopy );
/*=== timDump.c ===========================================================*/
extern Vec_Str_t * Tim_ManSave( Tim_Man_t * p );
extern Tim_Man_t * Tim_ManLoad( Vec_Str_t * p );
extern Vec_Str_t * Tim_ManSave( Tim_Man_t * p, int fHieOnly );
extern Tim_Man_t * Tim_ManLoad( Vec_Str_t * p, int fHieOnly );
/*=== timMan.c ===========================================================*/
extern Tim_Man_t * Tim_ManStart( int nCis, int nCos );
extern Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay );

8
src/misc/tim/timDump.c
View File

@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
Vec_Str_t * Tim_ManSave( Tim_Man_t * p, int fHieOnly )
{
Tim_Box_t * pBox;
Tim_Obj_t * pObj;
@ -71,6 +71,8 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
Vec_StrPutI_ne( vStr, Tim_ManBoxDelayTableId(p, pBox->iBox) ); // can be -1 if delay table is not given
Vec_StrPutI_ne( vStr, Tim_ManBoxCopy(p, pBox->iBox) ); // can be -1 if the copy is node defined
}
if ( fHieOnly )
return vStr;
// save the number of delay tables
Vec_StrPutI_ne( vStr, Tim_ManDelayTableNum(p) );
// save the delay tables
@ -107,7 +109,7 @@ Vec_Str_t * Tim_ManSave( Tim_Man_t * p )
SeeAlso []
***********************************************************************/
Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
Tim_Man_t * Tim_ManLoad( Vec_Str_t * p, int fHieOnly )
{
Tim_Man_t * pMan;
Tim_Obj_t * pObj;
@ -149,6 +151,8 @@ Tim_Man_t * Tim_ManLoad( Vec_Str_t * p )
curPo += nPos;
assert( curPi == nCis );
assert( curPo == nCos );
if ( fHieOnly )
return pMan;
// create delay tables
nTables = Vec_StrGetI_ne( p, &iStr );
assert( pMan->vDelayTables == NULL );

51
src/misc/util/utilBridge.c
View File

@ -41,11 +41,6 @@ ABC_NAMESPACE_IMPL_START
#define BRIDGE_VALUE_0 2
#define BRIDGE_VALUE_1 3
extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x );
extern unsigned Gia_ReadAigerDecode( unsigned char ** ppPos );
extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -79,9 +74,9 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
// write header
vStr = Vec_StrAlloc( 1000 );
Gia_WriteAigerEncodeStr( vStr, Gia_ManPiNum(p) );
Gia_WriteAigerEncodeStr( vStr, Gia_ManRegNum(p) );
Gia_WriteAigerEncodeStr( vStr, Gia_ManAndNum(p) );
Gia_AigerWriteUnsigned( vStr, Gia_ManPiNum(p) );
Gia_AigerWriteUnsigned( vStr, Gia_ManRegNum(p) );
Gia_AigerWriteUnsigned( vStr, Gia_ManAndNum(p) );
// write the nodes
Gia_ManForEachAnd( p, pObj, i )
@ -89,24 +84,24 @@ Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p )
uLit0 = Gia_ObjFanin0Copy( pObj );
uLit1 = Gia_ObjFanin1Copy( pObj );
assert( uLit0 != uLit1 );
Gia_WriteAigerEncodeStr( vStr, uLit0 << 1 );
Gia_WriteAigerEncodeStr( vStr, uLit1 );
Gia_AigerWriteUnsigned( vStr, uLit0 << 1 );
Gia_AigerWriteUnsigned( vStr, uLit1 );
}
// write latch drivers
Gia_ManForEachRi( p, pObj, i )
{
uLit0 = Gia_ObjFanin0Copy( pObj );
Gia_WriteAigerEncodeStr( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
Gia_AigerWriteUnsigned( vStr, (uLit0 << 2) | BRIDGE_VALUE_0 );
}
// write PO drivers
Gia_WriteAigerEncodeStr( vStr, Gia_ManPoNum(p) );
Gia_AigerWriteUnsigned( vStr, Gia_ManPoNum(p) );
Gia_ManForEachPo( p, pObj, i )
{
uLit0 = Gia_ObjFanin0Copy( pObj );
// complement property output!!!
Gia_WriteAigerEncodeStr( vStr, Abc_LitNot(uLit0) );
Gia_AigerWriteUnsigned( vStr, Abc_LitNot(uLit0) );
}
return vStr;
}
@ -209,20 +204,20 @@ void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex )
Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding)
Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding)
Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // depth
Gia_AigerWriteUnsigned( vStr, pCex->iFrame ); // depth
Gia_WriteAigerEncodeStr( vStr, 1 ); // concrete
Gia_WriteAigerEncodeStr( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
Gia_AigerWriteUnsigned( vStr, 1 ); // concrete
Gia_AigerWriteUnsigned( vStr, pCex->iFrame + 1 ); // number of frames (1 more than depth)
iBit = pCex->nRegs;
for ( f = 0; f <= pCex->iFrame; f++ )
{
Gia_WriteAigerEncodeStr( vStr, pCex->nPis ); // num of inputs
Gia_AigerWriteUnsigned( vStr, pCex->nPis ); // num of inputs
for ( i = 0; i < pCex->nPis; i++, iBit++ )
Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit) ? BRIDGE_VALUE_1:BRIDGE_VALUE_0) ); // value
}
assert( iBit == pCex->nBits );
Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example)
Gia_WriteAigerEncodeStr( vStr, pCex->nRegs ); // num of flops
Gia_AigerWriteUnsigned( vStr, pCex->nRegs ); // num of flops
for ( i = 0; i < pCex->nRegs; i++ )
Vec_StrPush( vStr, (char)BRIDGE_VALUE_0 ); // always zero!!!
// RetValue = fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile );
@ -264,9 +259,9 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
int i, nInputs, nFlops, nGates, nProps;
unsigned iFan0, iFan1;
nInputs = Gia_ReadAigerDecode( &pBuffer );
nFlops = Gia_ReadAigerDecode( &pBuffer );
nGates = Gia_ReadAigerDecode( &pBuffer );
nInputs = Gia_AigerReadUnsigned( &pBuffer );
nFlops = Gia_AigerReadUnsigned( &pBuffer );
nGates = Gia_AigerReadUnsigned( &pBuffer );
vLits = Vec_IntAlloc( 1000 );
Vec_IntPush( vLits, -999 );
@ -289,8 +284,8 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
Gia_ManHashAlloc( p );
for ( i = 0; i < nGates; i++ )
{
iFan0 = Gia_ReadAigerDecode( &pBuffer );
iFan1 = Gia_ReadAigerDecode( &pBuffer );
iFan0 = Gia_AigerReadUnsigned( &pBuffer );
iFan1 = Gia_AigerReadUnsigned( &pBuffer );
assert( !(iFan0 & 1) );
iFan0 >>= 1;
iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
@ -308,14 +303,14 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
pBufferPivot = pBuffer;
// scroll through flops
for ( i = 0; i < nFlops; i++ )
Gia_ReadAigerDecode( &pBuffer );
Gia_AigerReadUnsigned( &pBuffer );
// create POs
nProps = Gia_ReadAigerDecode( &pBuffer );
nProps = Gia_AigerReadUnsigned( &pBuffer );
assert( nProps == 1 );
for ( i = 0; i < nProps; i++ )
{
iFan0 = Gia_ReadAigerDecode( &pBuffer );
iFan0 = Gia_AigerReadUnsigned( &pBuffer );
iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 );
// complement property output!!!
Gia_ManAppendCo( p, Abc_LitNot(iFan0) );
@ -328,7 +323,7 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I
vInits = Vec_IntAlloc( nFlops );
for ( i = 0; i < nFlops; i++ )
{
iFan0 = Gia_ReadAigerDecode( &pBuffer );
iFan0 = Gia_AigerReadUnsigned( &pBuffer );
assert( (iFan0 & 3) == BRIDGE_VALUE_0 );
Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true
iFan0 >>= 2;
@ -487,7 +482,7 @@ void Gia_ManFromBridgeTest( char * pFileName )
fclose ( pFile );
Gia_ManPrintStats( p, 0, 0, 0 );
Gia_WriteAiger( p, "temp.aig", 0, 0 );
Gia_AigerWrite( p, "temp.aig", 0, 0 );
Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST );
Gia_ManStop( p );

4
src/proof/abs/absGla.c
View File

@ -1451,7 +1451,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
// dump abstraction map
Vec_IntFreeP( &p->pGia->vGateClasses );
p->pGia->vGateClasses = Ga2_ManAbsTranslate( p );
Gia_WriteAiger( p->pGia, pFileName, 0, 0 );
Gia_AigerWrite( p->pGia, pFileName, 0, 0 );
}
else if ( p->pPars->fDumpVabs )
{
@ -1464,7 +1464,7 @@ void Ga2_GlaDumpAbsracted( Ga2_Man_t * p, int fVerbose )
vGateClasses = Ga2_ManAbsTranslate( p );
pAbs = Gia_ManDupAbsGates( p->pGia, vGateClasses );
Gia_ManCleanValue( p->pGia );
Gia_WriteAiger( pAbs, pFileName, 0, 0 );
Gia_AigerWrite( pAbs, pFileName, 0, 0 );
Gia_ManStop( pAbs );
Vec_IntFreeP( &vGateClasses );
}

2
src/proof/abs/absGlaOld.c
View File

@ -1620,7 +1620,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
Vec_IntFreeP( &vGateClasses );
// write into file
Gia_WriteAiger( pAbs, pFileName, 0, 0 );
Gia_AigerWrite( pAbs, pFileName, 0, 0 );
Gia_ManStop( pAbs );
}

2
src/proof/abs/absVta.c
View File

@ -1440,7 +1440,7 @@ void Gia_VtaDumpAbsracted( Vta_Man_t * p, int fVerbose )
pAbs = Gia_ManDupAbsGates( p->pGia, p->pGia->vGateClasses );
Vec_IntFreeP( &p->pGia->vGateClasses );
// send it out
Gia_WriteAiger( pAbs, pFileName, 0, 0 );
Gia_AigerWrite( pAbs, pFileName, 0, 0 );
Gia_ManStop( pAbs );
}

2
src/proof/cec/cecCec.c
View File

@ -263,7 +263,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
{
ABC_FREE( pNew->pReprs );
ABC_FREE( pNew->pNexts );
Gia_WriteAiger( pNew, "gia_cec_undecided.aig", 0, 0 );
Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
}
if ( pPars->TimeLimit && (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )

4
src/proof/cec/cecCore.c
View File

@ -398,7 +398,7 @@ p->timeSim += clock() - clk;
}
pSrm = Cec_ManFraSpecReduction( p );
// Gia_WriteAiger( pSrm, "gia_srm.aig", 0, 0 );
// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
if ( pPars->fVeryVerbose )
Gia_ManPrintStats( pSrm, 0, 0, 0 );
@ -481,7 +481,7 @@ p->timeSat += clock() - clk;
Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
if ( fOutputResult )
{
Gia_WriteAiger( p->pAig, "gia_cec_temp.aig", 0, 0 );
Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
}
}

2
src/proof/cec/cecCorr.c
View File

@ -1124,7 +1124,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
pNew = Gia_ManCorrReduce( pAig );
pNew = Gia_ManSeqCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
//Gia_AigerWrite( pNew, "reduced.aig", 0, 0 );
}
// report the results
if ( pPars->fVerbose )

4
src/proof/cec/cecSeq.c
View File

@ -401,14 +401,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
}
// write equivalence classes
Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
// reduce the model
pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
if ( pReduce )
{
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
Gia_ManStop( pAux );
Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
// Gia_ManPrintStatsShort( pReduce );
Gia_ManStop( pReduce );

2
src/proof/cec/cecSolve.c
View File

@ -710,7 +710,7 @@ clk2 = clock();
if ( status == -1 )
{
Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
Gia_WriteAiger( pTemp, "gia_hard.aig", 0, 0 );
Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
Gia_ManStop( pTemp );
Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
}

2
src/proof/cec/cecSynth.c
View File

@ -309,7 +309,7 @@ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars )
{
pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL );
sprintf( Buffer, "part%03d.aig", i );
Gia_WriteAiger( pTemp, Buffer, 0, 0 );
Gia_AigerWrite( pTemp, Buffer, 0, 0 );
Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) );
Gia_ManStop( pTemp );

4
src/sat/bmc/bmcCexMin2.c
View File

@ -334,7 +334,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
printf( "%3d : ", iFrameStart );
Gia_ManPrintStats( pNew, 0, 0, 0 );
if ( fVerbose )
Gia_WriteAiger( pNew, "temp.aig", 0, 0 );
Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
Gia_ManStop( pNew );
}
else // CEX min
@ -345,7 +345,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
printf( "%3d : ", f );
Gia_ManPrintStats( pNew, 0, 0, 0 );
if ( fVerbose )
Gia_WriteAiger( pNew, "temp.aig", 0, 0 );
Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
Gia_ManStop( pNew );
}
}

4
src/sat/bmc/bmcCexTools.c
View File

@ -173,7 +173,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
clock_t clk = clock();
pNew = Bmc_CexPerformUnrolling( p, pCex );
Gia_ManPrintStats( pNew, 0, 0, 0 );
Gia_WriteAiger( pNew, "unroll.aig", 0, 0 );
Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
//Bmc_CexDumpAogStats( pNew, clock() - clk );
Gia_ManStop( pNew );
printf( "CE-induced network is written into file \"unroll.aig\".\n" );
@ -285,7 +285,7 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
clock_t clk = clock();
pNew = Bmc_CexBuildNetwork( p, pCex );
Gia_ManPrintStats( pNew, 0, 0, 0 );
Gia_WriteAiger( pNew, "unate.aig", 0, 0 );
Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
//Bmc_CexDumpAogStats( pNew, clock() - clk );
Gia_ManStop( pNew );
printf( "CE-induced network is written into file \"unate.aig\".\n" );