summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/gia.h2
-rw-r--r--src/aig/gia/giaAiger.c5
-rw-r--r--src/aig/gia/giaEquiv.c4
-rw-r--r--src/aig/gia/giaFalse.c2
-rw-r--r--src/aig/gia/giaHcd.c2
-rw-r--r--src/aig/gia/giaIso.c2
-rw-r--r--src/aig/gia/giaMan.c4
-rw-r--r--src/aig/gia/giaMini.c6
-rw-r--r--src/aig/gia/giaSweeper.c2
-rw-r--r--src/aig/gia/giaTim.c4
-rw-r--r--src/base/abci/abc.c29
-rw-r--r--src/base/abci/abcDetect.c2
-rw-r--r--src/base/abci/abcTim.c6
-rw-r--r--src/base/acb/acbCom.c2
-rw-r--r--src/base/acb/acbFunc.c8
-rw-r--r--src/base/bac/bacCom.c2
-rw-r--r--src/base/cba/cbaCom.c2
-rw-r--r--src/base/cmd/cmdPlugin.c2
-rw-r--r--src/base/wlc/wlcBlast.c4
-rw-r--r--src/base/wlc/wlcMem.c2
-rw-r--r--src/base/wlc/wlcReadVer.c2
-rw-r--r--src/map/if/ifTune.c4
-rw-r--r--src/misc/extra/extraUtilPath.c4
-rw-r--r--src/misc/util/utilBridge.c2
-rw-r--r--src/proof/abs/absGla.c6
-rw-r--r--src/proof/abs/absGlaOld.c2
-rw-r--r--src/proof/abs/absVta.c2
-rw-r--r--src/proof/acec/acecCore.c2
-rw-r--r--src/proof/acec/acecOrder.c2
-rw-r--r--src/proof/cec/cecCec.c2
-rw-r--r--src/proof/cec/cecCore.c4
-rw-r--r--src/proof/cec/cecCorr.c2
-rw-r--r--src/proof/cec/cecSeq.c4
-rw-r--r--src/proof/cec/cecSolve.c2
-rw-r--r--src/proof/cec/cecSynth.c2
-rw-r--r--src/sat/bmc/bmcBmcAnd.c6
-rw-r--r--src/sat/bmc/bmcCexDepth.c4
-rw-r--r--src/sat/bmc/bmcCexMin2.c4
-rw-r--r--src/sat/bmc/bmcCexTools.c4
-rw-r--r--src/sat/bmc/bmcEco.c2
-rw-r--r--src/sat/bmc/bmcFault.c4
-rw-r--r--src/sat/bmc/bmcUnroll.c4
42 files changed, 83 insertions, 79 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index fcf6fd28..d6375312 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1191,7 +1191,7 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re
extern int Gia_FileSize( char * pFileName );
extern Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSimple, int fSkipStrash, int fCheck );
extern Gia_Man_t * Gia_AigerRead( char * pFileName, int fGiaSimple, int fSkipStrash, int fCheck );
-extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact );
+extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine );
extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNumDigits );
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 );
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index cf185c33..03929aff 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -1076,10 +1076,9 @@ Vec_Str_t * Gia_AigerWriteIntoMemoryStrPart( Gia_Man_t * p, Vec_Int_t * vCis, Ve
SeeAlso []
***********************************************************************/
-void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact )
+void Gia_AigerWrite( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine )
{
int fVerbose = XAIG_VERBOSE;
- int fWriteNewLine = 0;
FILE * pFile;
Gia_Man_t * p;
Gia_Obj_t * pObj;
@@ -1438,7 +1437,7 @@ void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int iFileNum, int nFileNu
{
char Buffer[100];
sprintf( Buffer, "%s%0*d.aig", pFilePrefix, nFileNumDigits, iFileNum );
- Gia_AigerWrite( p, Buffer, 0, 0 );
+ Gia_AigerWrite( p, Buffer, 0, 0, 0 );
}
/**Function*************************************************************
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 84d9f1b1..20987687 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1994,14 +1994,14 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
}
}
// write equivalence classes
- Gia_AigerWrite( pGia, "gore.aig", 0, 0 );
+ Gia_AigerWrite( pGia, "gore.aig", 0, 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_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
+ Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0, 0 );
// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
// Gia_ManPrintStatsShort( pReduce );
Gia_ManStop( pReduce );
diff --git a/src/aig/gia/giaFalse.c b/src/aig/gia/giaFalse.c
index a055b5bc..50cb8ea7 100644
--- a/src/aig/gia/giaFalse.c
+++ b/src/aig/gia/giaFalse.c
@@ -457,7 +457,7 @@ Gia_Man_t * Gia_ManCheckOne( Gia_Man_t * p, int iOut, int iObj, int nTimeOut, in
if ( pNew )
{
Gia_Man_t * pTemp = Gia_ManDupDfsNode( p, Gia_ManObj(p, iObj) );
- Gia_AigerWrite( pTemp, "false.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "false.aig", 0, 0, 0 );
Abc_Print( 1, "Dumping cone with %d nodes into file \"%s\".\n", Gia_ManAndNum(pTemp), "false.aig" );
Gia_ManStop( pTemp );
}
diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c
index 5d3e28f5..8e8461e1 100644
--- a/src/aig/gia/giaHcd.c
+++ b/src/aig/gia/giaHcd.c
@@ -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_AigerWrite( pMiter, "m3.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "m3.aig", 0, 0, 0 );
}
else
{
diff --git a/src/aig/gia/giaIso.c b/src/aig/gia/giaIso.c
index 0e040b6c..76419e93 100644
--- a/src/aig/gia/giaIso.c
+++ b/src/aig/gia/giaIso.c
@@ -1293,7 +1293,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_AigerWrite( pDouble, "test.aig", 0, 0 );
+//Gia_AigerWrite( pDouble, "test.aig", 0, 0, 0 );
// analyze the two-output miter
pAig = Gia_ManIsoReduce( pDouble, &vPosEquivs, &vPisPerm, 0, 0, 0, 0 );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 53b686a4..25355fe3 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -241,10 +241,10 @@ void Gia_ManPrintClasses_old( Gia_Man_t * p )
{
Gia_Man_t * pTemp;
pTemp = Gia_ManDupFlopClass( p, 1 );
- Gia_AigerWrite( pTemp, "dom1.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "dom1.aig", 0, 0, 0 );
Gia_ManStop( pTemp );
pTemp = Gia_ManDupFlopClass( p, 2 );
- Gia_AigerWrite( pTemp, "dom2.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "dom2.aig", 0, 0, 0 );
Gia_ManStop( pTemp );
}
}
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index f04452ab..78d99ca8 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -573,7 +573,7 @@ int * Abc_FrameReadMiniLutNameMapping( Abc_Frame_t * pAbc )
if ( pAbc->pGiaMiniAig == NULL || pAbc->pGiaMiniLut == NULL )
return NULL;
pGia = Gia_ManDup2( pAbc->pGiaMiniAig, pAbc->pGiaMiniLut );
- //Gia_AigerWrite( pGia, "aig_m_lut.aig", 0, 0 );
+ //Gia_AigerWrite( pGia, "aig_m_lut.aig", 0, 0, 0 );
// compute equivalences in this AIG
pTemp = Gia_ManComputeGiaEquivs( pGia, nConfs, fVerbose );
Gia_ManStop( pTemp );
@@ -783,12 +783,12 @@ void Gia_MiniAigVerify( Abc_Frame_t * pAbc, char * pFileName )
pEquivs = Abc_FrameReadMiniAigEquivClasses( pAbc );
// dump miter for verification
pGia = Gia_MiniAigMiter( p, pEquivs );
- Gia_AigerWrite( pGia, pFileMiter, 0, 0 );
+ Gia_AigerWrite( pGia, pFileMiter, 0, 0, 0 );
printf( "Dumped miter AIG in file \"%s\".\n", pFileMiter );
Gia_ManStop( pGia );
// dump reduced AIG
pGia = Gia_MiniAigReduce( p, pEquivs );
- Gia_AigerWrite( pGia, pFileReduced, 0, 0 );
+ Gia_AigerWrite( pGia, pFileReduced, 0, 0, 0 );
printf( "Dumped reduced AIG in file \"%s\".\n", pFileReduced );
Gia_ManStop( pGia );
// cleanup
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index c1ce596d..de3f4049 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/src/aig/gia/giaSweeper.c
@@ -439,7 +439,7 @@ void Gia_SweeperLogicDump( Gia_Man_t * p, Vec_Int_t * vProbeIds, int fDumpConds,
Gia_ManStop( pGiaCond );
printf( " and conditions" );
}
- Gia_AigerWrite( pGiaOuts, pFileName, 0, 0 );
+ Gia_AigerWrite( pGiaOuts, pFileName, 0, 0, 0 );
Gia_ManStop( pGiaOuts );
printf( " into file \"%s\".\n", pFileName );
}
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 22212793..e136f68f 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -962,8 +962,8 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
char * pNameGeneric = Extra_FileNameGeneric( pFileSpec ? pFileSpec : pGia->pSpec );
sprintf( pFileName0, "%s_spec.aig", pNameGeneric );
sprintf( pFileName1, "%s_impl.aig", pNameGeneric );
- Gia_AigerWrite( pGia0, pFileName0, 0, 0 );
- Gia_AigerWrite( pGia1, pFileName1, 0, 0 );
+ Gia_AigerWrite( pGia0, pFileName0, 0, 0, 0 );
+ Gia_AigerWrite( pGia1, pFileName1, 0, 0, 0 );
ABC_FREE( pNameGeneric );
printf( "Dumped two parts of the miter into files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
}
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 753bf2ae..3a3ccac6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10727,7 +10727,7 @@ int Abc_CommandExpand( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_NtkDelete( pNtk2 );
// convert it into an AIG
pGia = Abc_NtkClpGia( pStrash );
- //Gia_AigerWrite( pGia, "aig_dump.aig", 0, 0 );
+ //Gia_AigerWrite( pGia, "aig_dump.aig", 0, 0, 0 );
Abc_NtkDelete( pStrash );
// get the new network
Abc_NtkExpandCubes( pNtk, pGia, fVerbose );
@@ -16857,7 +16857,7 @@ int Abc_CommandRecDump3( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "No structure in the library.\n" );
return 1;
}
- Gia_AigerWrite( pGia, FileName, 0, 0 );
+ Gia_AigerWrite( pGia, FileName, 0, 0, 0 );
}
return 0;
@@ -30070,9 +30070,10 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerilog = 0;
int fMiniAig = 0;
int fMiniLut = 0;
+ int fWriteNewLine = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "upmlvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "upmlcvh" ) ) != EOF )
{
switch ( c )
{
@@ -30088,6 +30089,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'l':
fMiniLut ^= 1;
break;
+ case 'c':
+ fWriteNewLine ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -30123,16 +30127,17 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
else if ( fMiniLut )
Gia_ManWriteMiniLut( pAbc->pGia, pFileName );
else
- Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0, fWriteNewLine );
return 0;
usage:
- Abc_Print( -2, "usage: &w [-upmlvh] <file>\n" );
+ Abc_Print( -2, "usage: &w [-upmlcvh] <file>\n" );
Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" );
Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
Abc_Print( -2, "\t-p : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
+ Abc_Print( -2, "\t-c : toggle writing \'\\n\' after \'c\' in the AIGER file [default = %s]\n", fWriteNewLine? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the file name\n");
@@ -34710,7 +34715,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
}
- Gia_AigerWrite( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0 );
+ Gia_AigerWrite( pTemp, pFileNameIn ? pFileNameIn : pFileName, 0, 0, 0 );
Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
@@ -34723,7 +34728,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
- Gia_AigerWrite( pTemp, pFileName2, 0, 0 );
+ Gia_AigerWrite( pTemp, pFileName2, 0, 0, 0 );
Abc_Print( 1, "Reduced original network was written into file \"%s\".\n", pFileName2 );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
@@ -34824,7 +34829,7 @@ int Abc_CommandAbc9Srm2( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
Gia_ManStop( pAux );
- Gia_AigerWrite( pTemp, pFileName, 0, 0 );
+ Gia_AigerWrite( pTemp, pFileName, 0, 0, 0 );
Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName );
Gia_ManPrintStatsShort( pTemp );
Gia_ManStop( pTemp );
@@ -35281,7 +35286,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fDumpMiter )
{
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
- Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
}
pAbc->Status = Cec_ManVerify( pMiter, pPars );
Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb );
@@ -40538,7 +40543,7 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pOne = Gia_ManDupDfsCone( pAbc->pGia, pObj );
sprintf( Buffer, "%s_%0*d.aig", Extra_FileNameGeneric(pAbc->pGia->pSpec), nDigits, i );
- Gia_AigerWrite( pOne, Buffer, 0, 0 );
+ Gia_AigerWrite( pOne, Buffer, 0, 0, 0 );
Gia_ManStop( pOne );
}
printf( "Dumped all outputs into individual AIGER files.\n" );
@@ -42929,8 +42934,8 @@ int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv )
sprintf( pName1, "%s_2.aig", pGen );
ABC_FREE( pGen );
}
- Gia_AigerWrite( pPart1, pName0, 0, 0 );
- Gia_AigerWrite( pPart2, pName1, 0, 0 );
+ Gia_AigerWrite( pPart1, pName0, 0, 0, 0 );
+ Gia_AigerWrite( pPart2, pName1, 0, 0, 0 );
Gia_ManStop( pPart1 );
Gia_ManStop( pPart2 );
if ( fDumpFilesTwo )
diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c
index 7adbed5d..089d3fe2 100644
--- a/src/base/abci/abcDetect.c
+++ b/src/base/abci/abcDetect.c
@@ -914,7 +914,7 @@ Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t
int i, nConfLimit = 10000;
Vec_Int_t * vPat = NULL;
int status, iVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
- //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0 );
+ //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0, 0 );
Gia_ManStop( pGia );
Cnf_DataFree( pCnf );
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
diff --git a/src/base/abci/abcTim.c b/src/base/abci/abcTim.c
index 3f68b815..c850cc56 100644
--- a/src/base/abci/abcTim.c
+++ b/src/base/abci/abcTim.c
@@ -170,7 +170,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_AigerWrite( pGia, pFileName, 0, 0 );
+ Gia_AigerWrite( pGia, pFileName, 0, 0, 0 );
Gia_ManStop( pGia );
printf( "AIG with pins derived from mapped network \"%s\" was written into file \"%s\".\n",
Abc_NtkName(pNtk), pFileName );
@@ -391,7 +391,7 @@ Gia_Man_t * Abc_NtkTestTimDeriveGia( Abc_Ntk_t * pNtk, int fVerbose )
Vec_FltFree( vArrTimes );
Vec_FltFree( vReqTimes );
-Gia_AigerWrite( pHoles, "holes00.aig", 0, 0 );
+Gia_AigerWrite( pHoles, "holes00.aig", 0, 0, 0 );
// return
pGia->pAigExtra = pHoles;
@@ -560,7 +560,7 @@ void Abc_NtkTestTimByWritingFile( Gia_Man_t * pGia, char * pFileName )
Gia_ManReverseClasses( pGia, 0 );
}
// write file
- Gia_AigerWrite( pGia, pFileName, 0, 0 );
+ Gia_AigerWrite( pGia, pFileName, 0, 0, 0 );
// unnormalize choices
if ( Gia_ManHasChoices(pGia) )
Gia_ManReverseClasses( pGia, 1 );
diff --git a/src/base/acb/acbCom.c b/src/base/acb/acbCom.c
index c2eae924..3d62454d 100644
--- a/src/base/acb/acbCom.c
+++ b/src/base/acb/acbCom.c
@@ -664,7 +664,7 @@ int Acb_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fDumpMiter )
{
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
- Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
}
pAbc->Status = Cec_ManVerify( pMiter, pPars );
//Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c
index 1efb5807..f6fcf2b0 100644
--- a/src/base/acb/acbFunc.c
+++ b/src/base/acb/acbFunc.c
@@ -2036,14 +2036,14 @@ Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars )
Gia_ManStop( p );
pCof1 = Acb_NtkEcoSynthesize( p = pCof1 );
Gia_ManStop( p );
- Gia_AigerWrite( pCof0, "eco_qbf0.aig", 0, 0 );
- Gia_AigerWrite( pCof1, "eco_qbf1.aig", 0, 0 );
+ Gia_AigerWrite( pCof0, "eco_qbf0.aig", 0, 0, 0 );
+ Gia_AigerWrite( pCof1, "eco_qbf1.aig", 0, 0, 0 );
Gia_ManStop( pCof0 );
Gia_ManStop( pCof1 );
printf( "Dumped cof0 into file \"%s\".\n", "eco_qbf0.aig" );
printf( "Dumped cof1 into file \"%s\".\n", "eco_qbf1.aig" );
}
-// Gia_AigerWrite( pCof, "eco_qbf.aig", 0, 0 );
+// Gia_AigerWrite( pCof, "eco_qbf.aig", 0, 0, 0 );
// printf( "Dumped the result of quantification into file \"%s\".\n", "eco_qbf.aig" );
pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 0, 0, 0 );
Gia_ManStop( pCof );
@@ -2445,7 +2445,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
// generate output files
Acb_GenerateFilePatch( vPatch, "patch.v" );
Acb_GenerateFileOut( vInst, pFileNameF, "out.v", vPatch );
- //Gia_AigerWrite( pGiaG, "test.aig", 0, 0 );
+ //Gia_AigerWrite( pGiaG, "test.aig", 0, 0, 0 );
cleanup:
// cleanup
if ( vGias )
diff --git a/src/base/bac/bacCom.c b/src/base/bac/bacCom.c
index e7d94d54..f1e3be5f 100644
--- a/src/base/bac/bacCom.c
+++ b/src/base/bac/bacCom.c
@@ -651,7 +651,7 @@ int Bac_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fDumpMiter )
{
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
- Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
}
pAbc->Status = Cec_ManVerify( pMiter, pPars );
//Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
diff --git a/src/base/cba/cbaCom.c b/src/base/cba/cbaCom.c
index b6a8c802..fa13030a 100644
--- a/src/base/cba/cbaCom.c
+++ b/src/base/cba/cbaCom.c
@@ -662,7 +662,7 @@ int Cba_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fDumpMiter )
{
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
- Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
}
pAbc->Status = Cec_ManVerify( pMiter, pPars );
//Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index ab517ed8..efee671d 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -502,7 +502,7 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// create input file
- Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0 );
+ Gia_AigerWrite( pAbc->pGia, pFileIn, 0, 0, 0 );
// create command line
vCommand = Vec_StrAlloc( 100 );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 4b59379b..c5c351c4 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -2361,8 +2361,8 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
assert( Gia_ManPoNum(pNew) % 2 == 0 );
sprintf( pFileName0, "%s_lhs_.aig", pNameGeneric );
sprintf( pFileName1, "%s_rhs_.aig", pNameGeneric );
- Gia_AigerWrite( pGia0, pFileName0, 0, 0 );
- Gia_AigerWrite( pGia1, pFileName1, 0, 0 );
+ Gia_AigerWrite( pGia0, pFileName0, 0, 0, 0 );
+ Gia_AigerWrite( pGia1, pFileName1, 0, 0, 0 );
Gia_ManStop( pGia0 );
Gia_ManStop( pGia1 );
Vec_IntFree( vOrder );
diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
index ccc319e5..fd844b62 100644
--- a/src/base/wlc/wlcMem.c
+++ b/src/base/wlc/wlcMem.c
@@ -1006,7 +1006,7 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo
if ( fDumpAbs )
{
char * pFileName = "mem_abs.aig";
- Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
printf( "Iteration %3d: Dumped abstraction in file \"%s\" after finding CEX in frame %d.\n", nIters, pFileName, pCex ? pCex->iFrame : -1 );
}
diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c
index 42332819..d8187bd4 100644
--- a/src/base/wlc/wlcReadVer.c
+++ b/src/base/wlc/wlcReadVer.c
@@ -1663,7 +1663,7 @@ void Io_ReadWordTest( char * pFileName )
Wlc_WriteVer( pNtk, "test.v", 0, 0 );
pNew = Wlc_NtkBitBlast( pNtk, NULL );
- Gia_AigerWrite( pNew, "test.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "test.aig", 0, 0, 0 );
Gia_ManStop( pNew );
Wlc_NtkFree( pNtk );
diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c
index d1ed7abd..13e45f47 100644
--- a/src/map/if/ifTune.c
+++ b/src/map/if/ifTune.c
@@ -622,10 +622,10 @@ sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t **
sat_solver * pSat = NULL;
*pvPiVars = *pvPoVars = NULL;
p1 = Ifn_ManStrFindModel( p );
-// Gia_AigerWrite( p1, "satbuild.aig", 0, 0 );
+// Gia_AigerWrite( p1, "satbuild.aig", 0, 0, 0 );
p2 = Ifn_ManStrFindCofactors( p->nInps, p1 );
Gia_ManStop( p1 );
-// Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 );
+// Gia_AigerWrite( p2, "satbuild2.aig", 0, 0, 0 );
pSat = Ifn_ManStrFindSolver( p2, pvPiVars, pvPoVars );
Gia_ManStop( p2 );
return pSat;
diff --git a/src/misc/extra/extraUtilPath.c b/src/misc/extra/extraUtilPath.c
index c7231a05..165f4022 100644
--- a/src/misc/extra/extraUtilPath.c
+++ b/src/misc/extra/extraUtilPath.c
@@ -98,7 +98,7 @@ void Abc_EnumeratePathsTest()
{
int nSize = 2;
Gia_Man_t * pGia = Abc_EnumeratePaths( nSize );
- Gia_AigerWrite( pGia, "testpath.aig", 0, 0 );
+ Gia_AigerWrite( pGia, "testpath.aig", 0, 0, 0 );
Gia_ManStop( pGia );
}
@@ -353,7 +353,7 @@ void Abc_GraphDeriveGiaDump( Vec_Wec_t * vNodes, Vec_Int_t * vEdges, int Size )
char pFileName[100];
Gia_Man_t * pGia = Abc_GraphDeriveGia( vNodes, vEdges );
sprintf( pFileName, "grid_%dx%d_e%03d.aig", Size, Size, Vec_IntSize(vEdges)/2 );
- Gia_AigerWrite( pGia, pFileName, 0, 0 );
+ Gia_AigerWrite( pGia, pFileName, 0, 0, 0 );
Gia_ManStop( pGia );
printf( "Finished dumping AIG into file \"%s\".\n", pFileName );
}
diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c
index f988b656..ecf87653 100644
--- a/src/misc/util/utilBridge.c
+++ b/src/misc/util/utilBridge.c
@@ -551,7 +551,7 @@ void Gia_ManFromBridgeTest( char * pFileName )
fclose ( pFile );
Gia_ManPrintStats( p, NULL );
- Gia_AigerWrite( p, "temp.aig", 0, 0 );
+ Gia_AigerWrite( p, "temp.aig", 0, 0, 0 );
Gia_ManToBridgeAbsNetlistTest( "par_.dump", p, BRIDGE_ABS_NETLIST );
Gia_ManStop( p );
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 698d415b..bd6b8c76 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1430,7 +1430,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_AigerWrite( p->pGia, pFileName, 0, 0 );
+ Gia_AigerWrite( p->pGia, pFileName, 0, 0, 0 );
}
else if ( p->pPars->fDumpVabs )
{
@@ -1443,7 +1443,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_AigerWrite( pAbs, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
Gia_ManStop( pAbs );
Vec_IntFreeP( &vGateClasses );
}
@@ -1563,7 +1563,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
Gia_ManForEachRo( pAig, pObj, i )
Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
- Gia_AigerWrite( pAig, pFileName, 0, 0 );
+ Gia_AigerWrite( pAig, pFileName, 0, 0, 0 );
Vec_IntFree( pAig->vGateClasses );
pAig->vGateClasses = vMap;
if ( p->pPars->fVerbose )
diff --git a/src/proof/abs/absGlaOld.c b/src/proof/abs/absGlaOld.c
index 70bd2e91..45ed1392 100644
--- a/src/proof/abs/absGlaOld.c
+++ b/src/proof/abs/absGlaOld.c
@@ -1619,7 +1619,7 @@ void Gia_GlaDumpAbsracted( Gla_Man_t * p, int fVerbose )
pAbs = Gia_ManDupAbsGates( p->pGia0, vGateClasses );
Vec_IntFreeP( &vGateClasses );
// write into file
- Gia_AigerWrite( pAbs, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
Gia_ManStop( pAbs );
}
diff --git a/src/proof/abs/absVta.c b/src/proof/abs/absVta.c
index 01680a3f..597e4b72 100644
--- a/src/proof/abs/absVta.c
+++ b/src/proof/abs/absVta.c
@@ -1439,7 +1439,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_AigerWrite( pAbs, pFileName, 0, 0 );
+ Gia_AigerWrite( pAbs, pFileName, 0, 0, 0 );
Gia_ManStop( pAbs );
}
diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c
index 1a575fbe..033fbc35 100644
--- a/src/proof/acec/acecCore.c
+++ b/src/proof/acec/acecCore.c
@@ -527,7 +527,7 @@ int Acec_Solve( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Acec_ParCec_t * pPars )
if ( fDumpMiter )
{
Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "acec_miter.aig" );
- Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "acec_miter.aig", 0, 0, 0 );
}
status = Cec_ManVerify( pMiter, pCecPars );
ABC_SWAP( Abc_Cex_t *, pGia0->pCexComb, pMiter->pCexComb );
diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c
index 93ef7f10..4eb79fee 100644
--- a/src/proof/acec/acecOrder.c
+++ b/src/proof/acec/acecOrder.c
@@ -173,7 +173,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
{
Gia_Man_t * pNew;
pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 );
- Gia_AigerWrite( pNew, "leftover.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "leftover.aig", 0, 0, 0 );
printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" );
Gia_ManStop( pNew );
}
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index be6df65f..ee45aa6c 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -392,7 +392,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
{
ABC_FREE( pNew->pReprs );
ABC_FREE( pNew->pNexts );
- Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "gia_cec_undecided.aig", 0, 0, 0 );
Abc_Print( 1, "The result is written into file \"%s\".\n", "gia_cec_undecided.aig" );
}
if ( pPars->TimeLimit && (Abc_Clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 250cb69e..b9529658 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -407,7 +407,7 @@ p->timeSim += Abc_Clock() - clk;
}
pSrm = Cec_ManFraSpecReduction( p );
-// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0 );
+// Gia_AigerWrite( pSrm, "gia_srm.aig", 0, 0, 0 );
if ( pPars->fVeryVerbose )
Gia_ManPrintStats( pSrm, NULL );
@@ -493,7 +493,7 @@ p->timeSat += Abc_Clock() - clk;
Abc_Print( 1, "Increasing conflict limit to %d.\n", pParsSat->nBTLimit );
if ( fOutputResult )
{
- Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0 );
+ Gia_AigerWrite( p->pAig, "gia_cec_temp.aig", 0, 0, 0 );
Abc_Print( 1,"The result is written into file \"%s\".\n", "gia_cec_temp.aig" );
}
}
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index 3bff4d38..fdc60299 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1196,7 +1196,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_AigerWrite( pNew, "reduced.aig", 0, 0 );
+ //Gia_AigerWrite( pNew, "reduced.aig", 0, 0, 0 );
}
// report the results
if ( pPars->fVerbose )
diff --git a/src/proof/cec/cecSeq.c b/src/proof/cec/cecSeq.c
index f39fb2a4..81420e03 100644
--- a/src/proof/cec/cecSeq.c
+++ b/src/proof/cec/cecSeq.c
@@ -401,14 +401,14 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
}
// write equivalence classes
- Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
+ Gia_AigerWrite( pAig, "gore.aig", 0, 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_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
+ Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0, 0 );
// Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
// Gia_ManPrintStatsShort( pReduce );
Gia_ManStop( pReduce );
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c
index ee9b8e7d..02f14b76 100644
--- a/src/proof/cec/cecSolve.c
+++ b/src/proof/cec/cecSolve.c
@@ -742,7 +742,7 @@ clk2 = Abc_Clock();
if ( status == -1 )
{
Gia_Man_t * pTemp = Gia_ManDupDfsCone( pAig, pObj );
- Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "gia_hard.aig", 0, 0, 0 );
Gia_ManStop( pTemp );
Abc_Print( 1, "Dumping hard cone into file \"%s\".\n", "gia_hard.aig" );
}
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c
index 6e5fd221..94658583 100644
--- a/src/proof/cec/cecSynth.c
+++ b/src/proof/cec/cecSynth.c
@@ -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_AigerWrite( pTemp, Buffer, 0, 0 );
+ Gia_AigerWrite( pTemp, Buffer, 0, 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 );
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 04d44353..b9c2db2c 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -711,7 +711,7 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( pPars->fDumpFrames )
{
p->pFrames = Gia_ManCleanup( p->pFrames );
- Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
Gia_ManStop( p->pFrames );
}
@@ -793,7 +793,7 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
Gia_ManPrintStats( p->pFrames, NULL );
if ( pPars->fDumpFrames )
{
- Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
}
for ( f = 0; f < nFramesMax; f++ )
@@ -977,7 +977,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
Gia_ManPrintStats( p->pFrames, NULL );
if ( pPars->fDumpFrames )
{
- Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
}
if ( pPars->fUseOldCnf )
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
index 38b57d5f..f0883f9a 100644
--- a/src/sat/bmc/bmcCexDepth.c
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -110,7 +110,7 @@ Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames )
Gia_ManPrintStats( pNew, NULL );
pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 );
Gia_ManStop( pNew );
- Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "miter3.aig", 0, 0, 0 );
return pTemp;
}
@@ -308,7 +308,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
Vec_PtrPush( vCones, pNew );
}
pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
- Gia_AigerWrite( pNew, "miter2.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "miter2.aig", 0, 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
Gia_ManStop( pTemp );
diff --git a/src/sat/bmc/bmcCexMin2.c b/src/sat/bmc/bmcCexMin2.c
index b8514601..b39b8eec 100644
--- a/src/sat/bmc/bmcCexMin2.c
+++ b/src/sat/bmc/bmcCexMin2.c
@@ -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, NULL );
if ( fVerbose )
- Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "temp.aig", 0, 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, NULL );
if ( fVerbose )
- Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "temp.aig", 0, 0, 0 );
Gia_ManStop( pNew );
}
}
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 9c80b278..5a29c8bc 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -173,7 +173,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
abctime clk = Abc_Clock();
pNew = Bmc_CexPerformUnrolling( p, pCex );
Gia_ManPrintStats( pNew, NULL );
- Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "unroll.aig", 0, 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_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 )
abctime clk = Abc_Clock();
pNew = Bmc_CexBuildNetwork( p, pCex );
Gia_ManPrintStats( pNew, NULL );
- Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "unate.aig", 0, 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop( pNew );
printf( "CE-induced network is written into file \"unate.aig\".\n" );
diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c
index 9d30fc09..b42d527a 100644
--- a/src/sat/bmc/bmcEco.c
+++ b/src/sat/bmc/bmcEco.c
@@ -291,7 +291,7 @@ void Bmc_EcoMiterTest()
Vec_IntPush( vFans, Gia_ObjId(pOld, pObj) );
pMiter = Bmc_EcoMiter( pGold, pOld, vFans );
Vec_IntFree( vFans );
- Gia_AigerWrite( pMiter, "eco_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "eco_miter.aig", 0, 0, 0 );
// find the patch
RetValue = Bmc_EcoPatch( pMiter, Gia_ManCiNum(pGold), Gia_ManCoNum(pGold) );
if ( RetValue == 1 )
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 096d8aaa..28d8a0c1 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -754,7 +754,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm, int fFfOnly )
Gia_ManStop( pTemp );
assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * (fFfOnly ? Count : Gia_ManAndNum(p)) );
// if ( fUseFaults )
-// Gia_AigerWrite( pNew, "newfault.aig", 0, 0 );
+// Gia_AigerWrite( pNew, "newfault.aig", 0, 0, 0 );
return pNew;
}
@@ -1260,7 +1260,7 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int
p1 = Gia_ManFOFUnfold( p, vMap );
if ( pPars->Algo != 1 )
p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) );
-// Gia_AigerWrite( p1, "newfault.aig", 0, 0 );
+// Gia_AigerWrite( p1, "newfault.aig", 0, 0, 0 );
// printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" );
// create miter
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index 0ad9271b..10513936 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -489,8 +489,8 @@ void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
Gia_ManPrintStats( pFrames0, NULL );
Gia_ManPrintStats( pFrames1, NULL );
-Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 );
-Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 );
+Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0, 0 );
+Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0, 0 );
Gia_ManStop( pFrames0 );
Gia_ManStop( pFrames1 );