From 1afa8a2f38bacb9f2f8faaf06b4f01c70560a419 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 25 Jul 2008 08:01:00 -0700 Subject: Version abc80725 --- src/base/abc/abc.h | 2 +- src/base/abc/abcUtil.c | 25 ++++++- src/base/abci/abc.c | 189 ++++++++++++++++++++++++++++++++++------------- src/base/abci/abcDar.c | 5 +- src/base/abci/abcPrint.c | 8 +- src/base/io/ioWriteDot.c | 15 +++- 6 files changed, 182 insertions(+), 62 deletions(-) (limited to 'src/base') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 09ea8b16..e4b0ad69 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -748,7 +748,7 @@ extern ABC_DLL bool Abc_NodeIsBuf( Abc_Obj_t * pNode ); extern ABC_DLL bool Abc_NodeIsInv( Abc_Obj_t * pNode ); extern ABC_DLL void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcPrint.c ==========================================================*/ -extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ); +extern ABC_DLL void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes ); extern ABC_DLL void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 39f44c11..90cf50b0 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -933,15 +933,36 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode ) pNode0 = Abc_ObjFanin0(pNode); pNode1 = Abc_ObjFanin1(pNode); // if the children are not ANDs, this is not MUX - if ( Abc_ObjFaninNum(pNode0) != 2 || Abc_ObjFaninNum(pNode1) != 2 ) + if ( !Abc_AigNodeIsAnd(pNode0) || !Abc_AigNodeIsAnd(pNode1) ) return 0; - // otherwise the node is MUX iff it has a pair of equal grandchildren + // otherwise the node is MUX iff it has a pair of equal grandchildren with opposite polarity return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC0(pNode1))) || (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC1(pNode1))) || (Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC0(pNode1))) || (Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC1(pNode1))); } +/**Function************************************************************* + + Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pNode; + int i; + int Counter = 0; + Abc_NtkForEachNode( pNtk, pNode, i ) + Counter += Abc_NodeIsMuxType( pNode ); + return Counter; +} + /**Function************************************************************* Synopsis [Returns 1 if the node is the control type of the MUX.] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b8a9cefe..b0cd2f7e 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -34,6 +34,7 @@ #include "fra.h" #include "saig.h" #include "nwkMerge.h" +#include "int.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -65,6 +66,7 @@ static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandMuxStruct ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMulti ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -327,6 +329,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "balance", Abc_CommandBalance, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "mux_struct", Abc_CommandMuxStruct, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "multi", Abc_CommandMulti, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "renode", Abc_CommandRenode, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Abc_CommandCleanup, 1 ); @@ -588,6 +591,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) int fDumpResult; int fUseLutLib; int fPrintTime; + int fPrintMuxes; int c; pNtk = Abc_FrameReadNtk(pAbc); @@ -600,8 +604,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) fDumpResult = 0; fUseLutLib = 0; fPrintTime = 0; + fPrintMuxes = 1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "fbdlth" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF ) { switch ( c ) { @@ -620,6 +625,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': fPrintTime ^= 1; break; + case 'm': + fPrintMuxes ^= 1; + break; case 'h': goto usage; default: @@ -632,7 +640,12 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" ); return 1; } - Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib ); + if ( !Abc_NtkIsLogic(pNtk) && fUseLutLib ) + { + fprintf( Abc_FrameReadErr(pAbc), "Cannot print LUT delay for a non-logic network.\n" ); + return 1; + } + Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes ); if ( fPrintTime ) { pAbc->TimeTotal += pAbc->TimeCommand; @@ -643,13 +656,14 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: print_stats [-fbdlth]\n" ); + fprintf( pErr, "usage: print_stats [-fbdltmh]\n" ); fprintf( pErr, "\t prints the network statistics\n" ); fprintf( pErr, "\t-f : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" ); fprintf( pErr, "\t-b : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" ); fprintf( pErr, "\t-d : toggles dumping network into file \"_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" ); fprintf( pErr, "\t-l : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" ); fprintf( pErr, "\t-t : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" ); + fprintf( pErr, "\t-m : toggles printing MUX statistics [default = %s]\n", fPrintMuxes? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -735,7 +749,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv ) } else printf( "EXDC network statistics: \n" ); - Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0 ); + Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0 ); return 0; usage: @@ -2472,6 +2486,78 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandMuxStruct( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + int fVerbose; + + extern Abc_Ntk_t * Abc_NtkMuxRestructure( Abc_Ntk_t * pNtk, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + // get the new network + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Does not work for a logic network.\n" ); + return 1; + } + // check if balancing worked +// pNtkRes = Abc_NtkMuxRestructure( pNtk, fVerbose ); + pNtkRes = NULL; + if ( pNtkRes == NULL ) + { + fprintf( pErr, "MUX restructuring has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: mux_struct [-vh]\n" ); + fprintf( pErr, "\t performs MUX restructuring of the current network\n" ); + fprintf( pErr, "\t-v : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -15494,6 +15580,7 @@ usage: return 1; } + /**Function************************************************************* Synopsis [] @@ -15507,39 +15594,21 @@ usage: ***********************************************************************/ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) { + Inter_ManParams_t Pars, * pPars = &Pars; FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; - int nBTLimit; - int nFramesMax; - int fRewrite; - int fTransLoop; - int fUsePudlak; - int fUseOther; - int fUseMiniSat; - int fCheckInd; - int fCheckKstep; - int fVerbose; - extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose ); + extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nBTLimit = 20000; - nFramesMax = 40; - fRewrite = 0; - fTransLoop = 1; - fUsePudlak = 0; - fUseOther = 0; - fUseMiniSat= 0; - fCheckInd = 0; - fCheckKstep= 0; - fVerbose = 0; + Inter_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF ) { switch ( c ) { @@ -15549,9 +15618,20 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nBTLimit = atoi(argv[globalUtilOptind]); + pPars->nBTLimit = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nBTLimit < 0 ) + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nFramesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesMax < 0 ) goto usage; break; case 'F': @@ -15560,34 +15640,37 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFramesMax = atoi(argv[globalUtilOptind]); + pPars->nFramesK = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFramesMax < 0 ) + if ( pPars->nFramesK < 0 ) goto usage; break; case 'r': - fRewrite ^= 1; + pPars->fRewrite ^= 1; break; case 't': - fTransLoop ^= 1; + pPars->fTransLoop ^= 1; break; case 'p': - fUsePudlak ^= 1; + pPars->fUsePudlak ^= 1; break; case 'o': - fUseOther ^= 1; + pPars->fUseOther ^= 1; break; case 'm': - fUseMiniSat ^= 1; + pPars->fUseMiniSat ^= 1; break; - case 'i': - fCheckInd ^= 1; + case 'c': + pPars->fCheckKstep ^= 1; break; - case 'k': - fCheckKstep ^= 1; + case 'g': + pPars->fUseBias ^= 1; + break; + case 'b': + pPars->fUseBackward ^= 1; break; case 'v': - fVerbose ^= 1; + pPars->fVerbose ^= 1; break; case 'h': goto usage; @@ -15615,22 +15698,24 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" ); return 0; } - Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose ); + Abc_NtkDarBmcInter( pNtk, pPars ); return 0; usage: - fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" ); + fprintf( pErr, "usage: int [-CNF num] [-rtpomcgbvh]\n" ); fprintf( pErr, "\t uses interpolation to prove the property\n" ); - fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit ); - fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax ); - fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); - fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" ); - fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" ); - fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" ); - fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" ); - fprintf( pErr, "\t-i : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" ); - fprintf( pErr, "\t-k : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" ); - fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", pPars->nBTLimit ); + fprintf( pErr, "\t-N num : the limit on number of frames to unroll [default = %d]\n", pPars->nFramesMax ); + fprintf( pErr, "\t-F num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK ); + fprintf( pErr, "\t-r : toggle the use of rewriting unrolled timeframes [default = %s]\n", pPars->fRewrite? "yes": "no" ); + fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", pPars->fTransLoop? "yes": "no" ); + fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", pPars->fUsePudlak? "yes": "no" ); + fprintf( pErr, "\t-o : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", pPars->fUseOther? "yes": "no" ); + fprintf( pErr, "\t-m : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", pPars->fUseMiniSat? "yes": "no" ); + fprintf( pErr, "\t-c : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" ); + fprintf( pErr, "\t-g : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" ); + fprintf( pErr, "\t-b : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 03790c4b..71f84272 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -25,6 +25,7 @@ #include "cnf.h" #include "fra.h" #include "fraig.h" +#include "int.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1295,7 +1296,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars ) { Aig_Man_t * pMan; int RetValue, Depth, clk = clock(); @@ -1307,7 +1308,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR return -1; } assert( pMan->nRegs > 0 ); - RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose, &Depth ); + RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index b753700e..2e01a141 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -111,7 +111,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib ) +void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes ) { int Num; @@ -153,6 +153,12 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave // fprintf( pFile, " (mux = %d)", Num2-Num ); // if ( Num2 ) // fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 ); + if ( fPrintMuxes ) + { + extern int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk ); + fprintf( pFile, " (mux = %d)", Abc_NtkCountMuxes(pNtk)-Num ); + fprintf( pFile, " (pure and = %d)", Abc_NtkNodeNum(pNtk) - (Abc_NtkCountMuxes(pNtk) * 3) ); + } } else { diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 54beb8b6..64be1425 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -275,6 +275,12 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho fprintf( pFile, " Level%d;\n", Level ); Vec_PtrForEachEntry( vNodes, pNode, i ) { + if ( (int)pNode->Level != Level ) + continue; + if ( Abc_ObjFaninNum(pNode) == 0 ) + continue; + +/* int SuppSize; Vec_Ptr_t * vSupp; if ( (int)pNode->Level != Level ) @@ -284,6 +290,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 ); SuppSize = Vec_PtrSize( vSupp ); Vec_PtrFree( vSupp ); +*/ // fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id ); if ( Abc_NtkIsStrash(pNtk) ) @@ -294,10 +301,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData)); else pSopString = Abc_NtkPrintSop(pNode->pData); -// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); - fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, - SuppSize, - pSopString ); + fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString ); +// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, +// SuppSize, +// pSopString ); fprintf( pFile, ", shape = ellipse" ); if ( pNode->fMarkB ) -- cgit v1.2.3