diff --git a/Abc/map,mapper,mapperLib.c b/Abc/map,mapper,mapperLib.c index 98d701d..8c3dc9c 100644 --- a/Abc/map,mapper,mapperLib.c +++ b/Abc/map,mapper,mapperLib.c @@ -15,6 +15,7 @@ Revision [$Id: mapperLib.c,v 1.6 2005/01/23 06:59:44 alanmi Exp $] ***********************************************************************/ +#define _DEFAULT_SOURCE #define _BSD_SOURCE #ifndef WIN32 @@ -168,9 +169,9 @@ void Map_SuperLibFree( Map_SuperLib_t * p ) { if ( p == NULL ) return; if ( p->pGenlib ) - { - if ( p->pGenlib != Abc_FrameReadLibGen() ) - Mio_LibraryDelete( p->pGenlib ); + { + if ( p->pGenlib != Abc_FrameReadLibGen() ) + Mio_LibraryDelete( p->pGenlib ); p->pGenlib = NULL; } if ( p->tTableC ) @@ -202,17 +203,17 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib, int fVerbose ) Vec_Str_t * vStr; char * pFileName; if ( pLib == NULL ) - return 0; + return 0; // compute supergates vStr = Super_PrecomputeStr( pLib, 5, 1, 100000000, 10000000, 10000000, 100, 1, 0 ); if ( vStr == NULL ) - return 0; + return 0; // create supergate library pFileName = Extra_FileNameGenericAppend( Mio_LibraryReadName(pLib), ".super" ); pLibSuper = Map_SuperLibCreate( pLib, vStr, pFileName, NULL, 1, 0 ); - Vec_StrFree( vStr ); + Vec_StrFree( vStr ); // replace the library Map_SuperLibFree( (Map_SuperLib_t *)Abc_FrameReadLibSuper() ); diff --git a/Abc/map,mio,mio.c b/Abc/map,mio,mio.c index 840dd2e..c7449fc 100644 --- a/Abc/map,mio,mio.c +++ b/Abc/map,mio,mio.c @@ -16,6 +16,7 @@ ***********************************************************************/ +#define _DEFAULT_SOURCE #define _BSD_SOURCE #ifndef WIN32 @@ -36,8 +37,8 @@ ABC_NAMESPACE_IMPL_START static int Mio_CommandReadLiberty( Abc_Frame_t * pAbc, int argc, char **argv ); static int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv ); -static int Mio_CommandWriteGenlib( Abc_Frame_t * pAbc, int argc, char **argv ); -static int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv ); +static int Mio_CommandWriteGenlib( Abc_Frame_t * pAbc, int argc, char **argv ); +static int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv ); /* // internal version of genlib library @@ -82,15 +83,15 @@ static char * pMcncGenlib[25] = { ***********************************************************************/ void Mio_Init( Abc_Frame_t * pAbc ) { -// Cmd_CommandAdd( pAbc, "SC mapping", "read_liberty", Mio_CommandReadLiberty, 0 ); - - Cmd_CommandAdd( pAbc, "SC mapping", "read_genlib", Mio_CommandReadGenlib, 0 ); - Cmd_CommandAdd( pAbc, "SC mapping", "write_genlib", Mio_CommandWriteGenlib, 0 ); - Cmd_CommandAdd( pAbc, "SC mapping", "print_genlib", Mio_CommandPrintGenlib, 0 ); - - Cmd_CommandAdd( pAbc, "SC mapping", "read_library", Mio_CommandReadGenlib, 0 ); - Cmd_CommandAdd( pAbc, "SC mapping", "write_library", Mio_CommandWriteGenlib, 0 ); - Cmd_CommandAdd( pAbc, "SC mapping", "print_library", Mio_CommandPrintGenlib, 0 ); +// Cmd_CommandAdd( pAbc, "SC mapping", "read_liberty", Mio_CommandReadLiberty, 0 ); + + Cmd_CommandAdd( pAbc, "SC mapping", "read_genlib", Mio_CommandReadGenlib, 0 ); + Cmd_CommandAdd( pAbc, "SC mapping", "write_genlib", Mio_CommandWriteGenlib, 0 ); + Cmd_CommandAdd( pAbc, "SC mapping", "print_genlib", Mio_CommandPrintGenlib, 0 ); + + Cmd_CommandAdd( pAbc, "SC mapping", "read_library", Mio_CommandReadGenlib, 0 ); + Cmd_CommandAdd( pAbc, "SC mapping", "write_library", Mio_CommandWriteGenlib, 0 ); + Cmd_CommandAdd( pAbc, "SC mapping", "print_library", Mio_CommandPrintGenlib, 0 ); } /**Function************************************************************* @@ -110,63 +111,63 @@ void Mio_End( Abc_Frame_t * pAbc ) Amap_LibFree( (Amap_Lib_t *)Abc_FrameReadLibGen2() ); } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Mio_UpdateGenlib( Mio_Library_t * pLib ) -{ - // free the current superlib because it depends on the old Mio library - if ( Abc_FrameReadLibSuper() ) - { - Map_SuperLibFree( (Map_SuperLib_t *)Abc_FrameReadLibSuper() ); - Abc_FrameSetLibSuper( NULL ); - } - - // replace the current library - Mio_LibraryDelete( (Mio_Library_t *)Abc_FrameReadLibGen() ); - Abc_FrameSetLibGen( pLib ); - - // replace the current library - Amap_LibFree( (Amap_Lib_t *)Abc_FrameReadLibGen2() ); - Abc_FrameSetLibGen2( NULL ); -} -int Mio_UpdateGenlib2( Vec_Str_t * vStr, Vec_Str_t * vStr2, char * pFileName, int fVerbose ) -{ - Mio_Library_t * pLib; - // set the new network - pLib = Mio_LibraryRead( pFileName, Vec_StrArray(vStr), NULL, fVerbose ); - if ( pLib == NULL ) - return 0; - - // free the current superlib because it depends on the old Mio library - if ( Abc_FrameReadLibSuper() ) - { - Map_SuperLibFree( (Map_SuperLib_t *)Abc_FrameReadLibSuper() ); - Abc_FrameSetLibSuper( NULL ); - } - - // replace the current library - Mio_LibraryDelete( (Mio_Library_t *)Abc_FrameReadLibGen() ); - Abc_FrameSetLibGen( pLib ); - - // set the new network - pLib = (Mio_Library_t *)Amap_LibReadAndPrepare( pFileName, Vec_StrArray(vStr2), 0, 0 ); - if ( pLib == NULL ) - return 0; - - // replace the current library - Amap_LibFree( (Amap_Lib_t *)Abc_FrameReadLibGen2() ); - Abc_FrameSetLibGen2( pLib ); - return 1; -} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Mio_UpdateGenlib( Mio_Library_t * pLib ) +{ + // free the current superlib because it depends on the old Mio library + if ( Abc_FrameReadLibSuper() ) + { + Map_SuperLibFree( (Map_SuperLib_t *)Abc_FrameReadLibSuper() ); + Abc_FrameSetLibSuper( NULL ); + } + + // replace the current library + Mio_LibraryDelete( (Mio_Library_t *)Abc_FrameReadLibGen() ); + Abc_FrameSetLibGen( pLib ); + + // replace the current library + Amap_LibFree( (Amap_Lib_t *)Abc_FrameReadLibGen2() ); + Abc_FrameSetLibGen2( NULL ); +} +int Mio_UpdateGenlib2( Vec_Str_t * vStr, Vec_Str_t * vStr2, char * pFileName, int fVerbose ) +{ + Mio_Library_t * pLib; + // set the new network + pLib = Mio_LibraryRead( pFileName, Vec_StrArray(vStr), NULL, fVerbose ); + if ( pLib == NULL ) + return 0; + + // free the current superlib because it depends on the old Mio library + if ( Abc_FrameReadLibSuper() ) + { + Map_SuperLibFree( (Map_SuperLib_t *)Abc_FrameReadLibSuper() ); + Abc_FrameSetLibSuper( NULL ); + } + + // replace the current library + Mio_LibraryDelete( (Mio_Library_t *)Abc_FrameReadLibGen() ); + Abc_FrameSetLibGen( pLib ); + + // set the new network + pLib = (Mio_Library_t *)Amap_LibReadAndPrepare( pFileName, Vec_StrArray(vStr2), 0, 0 ); + if ( pLib == NULL ) + return 0; + + // replace the current library + Amap_LibFree( (Amap_Lib_t *)Abc_FrameReadLibGen2() ); + Abc_FrameSetLibGen2( pLib ); + return 1; +} /**Function************************************************************* @@ -180,8 +181,8 @@ int Mio_UpdateGenlib2( Vec_Str_t * vStr, Vec_Str_t * vStr2, char * pFileName, in ***********************************************************************/ int Mio_CommandReadLiberty( Abc_Frame_t * pAbc, int argc, char **argv ) -{ - int fUseFileInterface = 0; +{ + int fUseFileInterface = 0; char Command[1000]; FILE * pFile; FILE * pOut, * pErr; @@ -226,29 +227,29 @@ int Mio_CommandReadLiberty( Abc_Frame_t * pAbc, int argc, char **argv ) return 1; } fclose( pFile ); - - if ( fUseFileInterface ) + + if ( fUseFileInterface ) { if ( !Amap_LibertyParse( pFileName, fVerbose ) ) - return 0; - assert( strlen(pFileName) < 900 ); + return 0; + assert( strlen(pFileName) < 900 ); sprintf( Command, "read_genlib %s", Extra_FileNameGenericAppend(pFileName, ".genlib") ); - Cmd_CommandExecute( pAbc, Command ); - } - else - { - Vec_Str_t * vStr, * vStr2; - int RetValue; - vStr = Amap_LibertyParseStr( pFileName, fVerbose ); - if ( vStr == NULL ) - return 0; - vStr2 = Vec_StrDup(vStr); - RetValue = Mio_UpdateGenlib2( vStr, vStr2, pFileName, fVerbose ); - Vec_StrFree( vStr ); - Vec_StrFree( vStr2 ); - if ( !RetValue ) - printf( "Reading library has filed.\n" ); - } + Cmd_CommandExecute( pAbc, Command ); + } + else + { + Vec_Str_t * vStr, * vStr2; + int RetValue; + vStr = Amap_LibertyParseStr( pFileName, fVerbose ); + if ( vStr == NULL ) + return 0; + vStr2 = Vec_StrDup(vStr); + RetValue = Mio_UpdateGenlib2( vStr, vStr2, pFileName, fVerbose ); + Vec_StrFree( vStr ); + Vec_StrFree( vStr2 ); + if ( !RetValue ) + printf( "Reading library has filed.\n" ); + } return 0; usage: @@ -277,10 +278,10 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) { FILE * pFile; FILE * pOut, * pErr; - Mio_Library_t * pLib; + Mio_Library_t * pLib; Amap_Lib_t * pLib2; Abc_Ntk_t * pNet; - char * pFileName; + char * pFileName; char * pExcludeFile = NULL; int fVerbose; double WireDelay; @@ -309,15 +310,15 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) if ( WireDelay <= 0.0 ) goto usage; break; - case 'E': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-E\" should be followed by a file name.\n" ); - goto usage; - } - pExcludeFile = argv[globalUtilOptind]; - globalUtilOptind++; - break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by a file name.\n" ); + goto usage; + } + pExcludeFile = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'v': fVerbose ^= 1; break; @@ -351,25 +352,25 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) { fprintf( pErr, "Reading genlib library has failed.\n" ); return 1; - } - if ( fVerbose ) - printf( "Entered genlib library with %d gates from file \"%s\".\n", Mio_LibraryReadGateNum(pLib), pFileName ); + } + if ( fVerbose ) + printf( "Entered genlib library with %d gates from file \"%s\".\n", Mio_LibraryReadGateNum(pLib), pFileName ); // add the fixed number (wire delay) to all delays in the library if ( WireDelay != 0.0 ) Mio_LibraryShiftDelay( pLib, WireDelay ); - - // prepare libraries - Mio_UpdateGenlib( pLib ); - // replace the current library + // prepare libraries + Mio_UpdateGenlib( pLib ); + + // replace the current library pLib2 = Amap_LibReadAndPrepare( pFileName, NULL, 0, 0 ); if ( pLib2 == NULL ) { fprintf( pErr, "Reading second genlib library has failed.\n" ); return 1; } - Abc_FrameSetLibGen2( pLib2 ); + Abc_FrameSetLibGen2( pLib2 ); return 0; usage: @@ -379,138 +380,138 @@ int Mio_CommandReadGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) fprintf( pErr, "\t with the same Boolean function, only the gate\n" ); fprintf( pErr, "\t with the smallest area will be used)\n" ); fprintf( pErr, "\t-W float : wire delay (added to pin-to-pin gate delays) [default = %g]\n", WireDelay ); - fprintf( pErr, "\t-E file : the file name with gates to be excluded [default = none]\n" ); + fprintf( pErr, "\t-E file : the file name with gates to be excluded [default = none]\n" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : enable verbose output\n"); return 1; } - -/**Function************************************************************* - - Synopsis [Command procedure to read LUT libraries.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Mio_CommandWriteGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) -{ - FILE * pOut, * pErr, * pFile; - Abc_Ntk_t * pNet; - char * pFileName; - int fVerbose; - int c; - - pNet = Abc_FrameReadNtk(pAbc); - pOut = Abc_FrameReadOut(pAbc); - pErr = Abc_FrameReadErr(pAbc); - - // set the defaults - fVerbose = 1; - Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) - { - switch (c) - { - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - break; - default: - goto usage; - } - } - if ( Abc_FrameReadLibGen() == NULL ) - { - printf( "Library is not available.\n" ); - return 1; - } - if ( argc != globalUtilOptind + 1 ) - { - printf( "The file name is not given.\n" ); - return 1; - } - - pFileName = argv[globalUtilOptind]; - pFile = fopen( pFileName, "w" ); - if ( pFile == NULL ) - { - printf( "Error! Cannot open file \"%s\" for writing the library.\n", pFileName ); - return 1; - } - Mio_WriteLibrary( pFile, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 ); - fclose( pFile ); - printf( "The current genlib library is written into file \"%s\".\n", pFileName ); - return 0; - -usage: - fprintf( pErr, "\nusage: write_genlib [-vh] \n"); - fprintf( pErr, "\t writes the current genlib library into a file\n" ); - fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", fVerbose? "yes" : "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); - fprintf( pErr, "\t : optional file name to write the library\n"); - return 1; -} - -/**Function************************************************************* - - Synopsis [Command procedure to read LUT libraries.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) -{ - FILE * pOut, * pErr; - Abc_Ntk_t * pNet; - int fVerbose; - int c; - - pNet = Abc_FrameReadNtk(pAbc); - pOut = Abc_FrameReadOut(pAbc); - pErr = Abc_FrameReadErr(pAbc); - - // set the defaults - fVerbose = 1; - Extra_UtilGetoptReset(); - while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) - { - switch (c) - { - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - break; - default: - goto usage; - } - } - if ( Abc_FrameReadLibGen() == NULL ) - { - printf( "Library is not available.\n" ); - return 1; - } - Mio_WriteLibrary( stdout, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 ); - return 0; - -usage: - fprintf( pErr, "\nusage: print_genlib [-vh]\n"); - fprintf( pErr, "\t print the current genlib library\n" ); - fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", fVerbose? "yes" : "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); - return 1; -} + +/**Function************************************************************* + + Synopsis [Command procedure to read LUT libraries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mio_CommandWriteGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + FILE * pOut, * pErr, * pFile; + Abc_Ntk_t * pNet; + char * pFileName; + int fVerbose; + int c; + + pNet = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set the defaults + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) + { + switch (c) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + break; + default: + goto usage; + } + } + if ( Abc_FrameReadLibGen() == NULL ) + { + printf( "Library is not available.\n" ); + return 1; + } + if ( argc != globalUtilOptind + 1 ) + { + printf( "The file name is not given.\n" ); + return 1; + } + + pFileName = argv[globalUtilOptind]; + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + printf( "Error! Cannot open file \"%s\" for writing the library.\n", pFileName ); + return 1; + } + Mio_WriteLibrary( pFile, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 ); + fclose( pFile ); + printf( "The current genlib library is written into file \"%s\".\n", pFileName ); + return 0; + +usage: + fprintf( pErr, "\nusage: write_genlib [-vh] \n"); + fprintf( pErr, "\t writes the current genlib library into a file\n" ); + fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", fVerbose? "yes" : "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\t : optional file name to write the library\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [Command procedure to read LUT libraries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Mio_CommandPrintGenlib( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNet; + int fVerbose; + int c; + + pNet = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set the defaults + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "vh")) != EOF ) + { + switch (c) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + break; + default: + goto usage; + } + } + if ( Abc_FrameReadLibGen() == NULL ) + { + printf( "Library is not available.\n" ); + return 1; + } + Mio_WriteLibrary( stdout, (Mio_Library_t *)Abc_FrameReadLibGen(), 0 ); + return 0; + +usage: + fprintf( pErr, "\nusage: print_genlib [-vh]\n"); + fprintf( pErr, "\t print the current genlib library\n" ); + fprintf( pErr, "\t-v : toggles enabling of verbose output [default = %s]\n", fVerbose? "yes" : "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/Bip/Main_bip.cc b/Bip/Main_bip.cc index f7a6eba..52959bd 100644 --- a/Bip/Main_bip.cc +++ b/Bip/Main_bip.cc @@ -508,8 +508,8 @@ static void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis) { Vec > ffs, pis; - For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w)); - For_Gatetype(N, gate_PI , w) pis.push(tuple(attr_PI (w).number, w)); + For_Gatetype(N, gate_Flop, w) ffs.push(ZZ::tuple(attr_Flop(w).number, w)); + For_Gatetype(N, gate_PI , w) pis.push(ZZ::tuple(attr_PI (w).number, w)); sort(ffs); sort(pis); diff --git a/EXTERN/SiertSat/glucose/core/Main.cc b/EXTERN/SiertSat/glucose/core/Main.cc index abbd2d5..a0d11df 100644 --- a/EXTERN/SiertSat/glucose/core/Main.cc +++ b/EXTERN/SiertSat/glucose/core/Main.cc @@ -47,19 +47,19 @@ void printStats(Solver& solver) { double cpu_time = cpuTime(); double mem_used = 0;//memUsedPeak(); - printf("c restarts : %"PRIu64" (%"PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0)); - printf("c blocked restarts : %"PRIu64" (multiple: %"PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame); - printf("c last block at restart : %"PRIu64"\n",solver.lastblockatrestart); + printf("c restarts : %" PRIu64 " (%" PRIu64 " conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0)); + printf("c blocked restarts : %" PRIu64 " (multiple: %" PRIu64 ") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame); + printf("c last block at restart : %" PRIu64 "\n",solver.lastblockatrestart); printf("c nb ReduceDB : %lld\n", solver.nbReduceDB); printf("c nb removed Clauses : %lld\n",solver.nbRemovedClauses); printf("c nb learnts DL2 : %lld\n", solver.nbDL2); printf("c nb learnts size 2 : %lld\n", solver.nbBin); printf("c nb learnts size 1 : %lld\n", solver.nbUn); - printf("c conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("c decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("c propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("c conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); + printf("c conflicts : %-12" PRIu64 " (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); + printf("c decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); + printf("c propagations : %-12" PRIu64 " (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); + printf("c conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); printf("c nb reduced Clauses : %lld\n",solver.nbReducedClauses); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); diff --git a/EXTERN/SiertSat/glucose/utils/Options.h b/EXTERN/SiertSat/glucose/utils/Options.h index 7f4a6e1..c9d4e49 100644 --- a/EXTERN/SiertSat/glucose/utils/Options.h +++ b/EXTERN/SiertSat/glucose/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); diff --git a/EXTERN/SiertSat/minisat/core/Main.cc b/EXTERN/SiertSat/minisat/core/Main.cc index 4388c3e..9d05f67 100644 --- a/EXTERN/SiertSat/minisat/core/Main.cc +++ b/EXTERN/SiertSat/minisat/core/Main.cc @@ -38,11 +38,11 @@ void printStats(Solver& solver) { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", solver.starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); + printf("restarts : %" PRIu64 "\n", solver.starts); + printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); + printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); + printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); + printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("CPU time : %g s\n", cpu_time); } diff --git a/EXTERN/SiertSat/minisat/utils/Options.h b/EXTERN/SiertSat/minisat/utils/Options.h index 4c5d5bc..ad2dc52 100644 --- a/EXTERN/SiertSat/minisat/utils/Options.h +++ b/EXTERN/SiertSat/minisat/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); diff --git a/EXTERN/SiertSat/solver-reducer-simp/Main.cc b/EXTERN/SiertSat/solver-reducer-simp/Main.cc index 5e14843..5636aec 100644 --- a/EXTERN/SiertSat/solver-reducer-simp/Main.cc +++ b/EXTERN/SiertSat/solver-reducer-simp/Main.cc @@ -54,24 +54,24 @@ void printStats(SolRed& solver) { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("c restarts : %"PRIu64"\n", solver.starts); - printf("c conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("c decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, solver.decisions?((float)solver.rnd_decisions*100 / (float)solver.decisions): 0, solver.decisions /cpu_time); - printf("c propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("c conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); + printf("c restarts : %" PRIu64 "\n", solver.starts); + printf("c conflicts : %-12" PRIu64 " (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); + printf("c decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", solver.decisions, solver.decisions?((float)solver.rnd_decisions*100 / (float)solver.decisions): 0, solver.decisions /cpu_time); + printf("c propagations : %-12" PRIu64 " (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); + printf("c conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); printf("\nc -- solver/reducer statistics --\n"); - printf("c workset inserts : %-12"PRIu64"\n", solver.workset_in); - printf("c workset inserts lits : %-12"PRIu64"\n", solver.workset_in_lits); - printf("c workset deletions : %-12"PRIu64"\n", solver.workset_deleted); - printf("c workset deletions lits: %-12"PRIu64"\n", solver.workset_deleted_lits); - printf("c reducer inputs : %-12"PRIu64"\n", solver.reducer_in); - printf("c reducer inputs lits : %-12"PRIu64"\n", solver.reducer_in_lits); - printf("c reducer outputs : %-12"PRIu64"\n", solver.reducer_out); - printf("c reducer outputs lits : %-12"PRIu64"\n", solver.reducer_out_lits); - printf("c reducer not outp. lits: %-12"PRIu64"\n", solver.reducer_notout_lits); - printf("c reducer forced backtr.: %-12"PRIu64" (avg. %1.f levels from level %.1f)\n", solver.reducer_backtracks, solver.reducer_backtracks?((float)solver.reducer_backtrack_levels / (float)solver.reducer_backtracks):0, solver.reducer_backtracks?(solver.reducer_backtrack_level_before / (float)solver.reducer_backtracks):0); - printf("c reducer f.backtr. to 0: %-12"PRIu64"\n\n", solver.reducer_backtracks_tozero); + printf("c workset inserts : %-12" PRIu64 "\n", solver.workset_in); + printf("c workset inserts lits : %-12" PRIu64 "\n", solver.workset_in_lits); + printf("c workset deletions : %-12" PRIu64 "\n", solver.workset_deleted); + printf("c workset deletions lits: %-12" PRIu64 "\n", solver.workset_deleted_lits); + printf("c reducer inputs : %-12" PRIu64 "\n", solver.reducer_in); + printf("c reducer inputs lits : %-12" PRIu64 "\n", solver.reducer_in_lits); + printf("c reducer outputs : %-12" PRIu64 "\n", solver.reducer_out); + printf("c reducer outputs lits : %-12" PRIu64 "\n", solver.reducer_out_lits); + printf("c reducer not outp. lits: %-12" PRIu64 "\n", solver.reducer_notout_lits); + printf("c reducer forced backtr.: %-12" PRIu64 " (avg. %1.f levels from level %.1f)\n", solver.reducer_backtracks, solver.reducer_backtracks?((float)solver.reducer_backtrack_levels / (float)solver.reducer_backtracks):0, solver.reducer_backtracks?(solver.reducer_backtrack_level_before / (float)solver.reducer_backtracks):0); + printf("c reducer f.backtr. to 0: %-12" PRIu64 "\n\n", solver.reducer_backtracks_tozero); if (mem_used != 0) printf("c Memory used : %.2f MB\n", mem_used); printf("c CPU time : %g s\n", cpu_time); diff --git a/EXTERN/SiertSat/solver-reducer/Main.cc b/EXTERN/SiertSat/solver-reducer/Main.cc index cdbef1d..9319332 100644 --- a/EXTERN/SiertSat/solver-reducer/Main.cc +++ b/EXTERN/SiertSat/solver-reducer/Main.cc @@ -53,24 +53,24 @@ void printStats(SolRed& solver) { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("c restarts : %"PRIu64"\n", solver.starts); - printf("c conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); - printf("c decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); - printf("c propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); - printf("c conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); + printf("c restarts : %" PRIu64 "\n", solver.starts); + printf("c conflicts : %-12" PRIu64 " (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); + printf("c decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); + printf("c propagations : %-12" PRIu64 " (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); + printf("c conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); printf("\nc -- solver/reducer statistics --\n"); - printf("c workset inserts : %-12"PRIu64"\n", solver.workset_in); - printf("c workset inserts lits : %-12"PRIu64"\n", solver.workset_in_lits); - printf("c workset deletions : %-12"PRIu64"\n", solver.workset_deleted); - printf("c workset deletions lits: %-12"PRIu64"\n", solver.workset_deleted_lits); - printf("c reducer inputs : %-12"PRIu64"\n", solver.reducer_in); - printf("c reducer inputs lits : %-12"PRIu64"\n", solver.reducer_in_lits); - printf("c reducer outputs : %-12"PRIu64"\n", solver.reducer_out); - printf("c reducer outputs lits : %-12"PRIu64"\n", solver.reducer_out_lits); - printf("c reducer not outp. lits: %-12"PRIu64"\n", solver.reducer_notout_lits); - printf("c reducer forced backtr.: %-12"PRIu64" (avg. %1.f levels from level %.1f)\n", solver.reducer_backtracks, solver.reducer_backtracks?((float)solver.reducer_backtrack_levels / (float)solver.reducer_backtracks):0, solver.reducer_backtracks?(solver.reducer_backtrack_level_before / (float)solver.reducer_backtracks):0); - printf("c reducer f.backtr. to 0: %-12"PRIu64"\n\n", solver.reducer_backtracks_tozero); + printf("c workset inserts : %-12" PRIu64 "\n", solver.workset_in); + printf("c workset inserts lits : %-12" PRIu64 "\n", solver.workset_in_lits); + printf("c workset deletions : %-12" PRIu64 "\n", solver.workset_deleted); + printf("c workset deletions lits: %-12" PRIu64 "\n", solver.workset_deleted_lits); + printf("c reducer inputs : %-12" PRIu64 "\n", solver.reducer_in); + printf("c reducer inputs lits : %-12" PRIu64 "\n", solver.reducer_in_lits); + printf("c reducer outputs : %-12" PRIu64 "\n", solver.reducer_out); + printf("c reducer outputs lits : %-12" PRIu64 "\n", solver.reducer_out_lits); + printf("c reducer not outp. lits: %-12" PRIu64 "\n", solver.reducer_notout_lits); + printf("c reducer forced backtr.: %-12" PRIu64 " (avg. %1.f levels from level %.1f)\n", solver.reducer_backtracks, solver.reducer_backtracks?((float)solver.reducer_backtrack_levels / (float)solver.reducer_backtracks):0, solver.reducer_backtracks?(solver.reducer_backtrack_level_before / (float)solver.reducer_backtracks):0); + printf("c reducer f.backtr. to 0: %-12" PRIu64 "\n\n", solver.reducer_backtracks_tozero); if (mem_used != 0) printf("c Memory used : %.2f MB\n", mem_used); printf("c CPU time : %g s\n", cpu_time); diff --git a/LutMap/Main_lutmap.cc b/LutMap/Main_lutmap.cc index 394dcd8..b450bf9 100644 --- a/LutMap/Main_lutmap.cc +++ b/LutMap/Main_lutmap.cc @@ -823,7 +823,7 @@ int main(int argc, char** argv) Vec > list; For_Map(ftbs) - list.push(tuple(Map_Value(ftbs), Map_Key(ftbs))); + list.push(ZZ::tuple(Map_Value(ftbs), Map_Key(ftbs))); sort_reverse(list); OutFile out(cli.get("ftbs").string_val); diff --git a/MetaSat/MiniSat2/Options.hh b/MetaSat/MiniSat2/Options.hh index f56be39..6d84c4e 100644 --- a/MetaSat/MiniSat2/Options.hh +++ b/MetaSat/MiniSat2/Options.hh @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); diff --git a/MetaSat/MiniSat2/Solver.cc b/MetaSat/MiniSat2/Solver.cc index b00d4f1..3d75bd7 100644 --- a/MetaSat/MiniSat2/Solver.cc +++ b/MetaSat/MiniSat2/Solver.cc @@ -991,11 +991,11 @@ void Solver::printStats() const { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", conflicts , conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", propagations, propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); + printf("restarts : %" PRIu64 "\n", starts); + printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time); + printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); + printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time); + printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("CPU time : %g s\n", cpu_time); } diff --git a/MetaSat/MiniSat2/System.cc b/MetaSat/MiniSat2/System.cc index 7bfc810..f232f85 100644 --- a/MetaSat/MiniSat2/System.cc +++ b/MetaSat/MiniSat2/System.cc @@ -20,6 +20,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include +#if defined(__linux__) +#include +#endif #include "System.hh" @@ -27,8 +30,6 @@ namespace Minisat { #if defined(__linux__) -#include - static inline int memReadStat(int field) { char name[256]; diff --git a/MiniSat/MiniSat.cc b/MiniSat/MiniSat.cc index e044d75..94737dd 100644 --- a/MiniSat/MiniSat.cc +++ b/MiniSat/MiniSat.cc @@ -1400,7 +1400,7 @@ void MiniSat::clearFilter() #define H1 "\a*" #define H2 "\a*" #define SEP0 "|" -#define SEP "\a0\a/"SEP0"\a0" +#define SEP "\a0\a/" SEP0 "\a0" #define SEPH1 SEP H1 #define SEPH2 SEP H2 @@ -1434,7 +1434,7 @@ void MiniSat::printProgressLine(bool newline) const if (lit_ratio_text.size() > 5) lit_ratio_text = (FMT "%>5%,'D", (int64)lit_ratio); } - String text = (FMT "\r%>5%,'D %>5%,'D %>5%,'D "SEP0" %>5%,'D %>5%,'D "SEP0" %>5%,'D %>5%,'D %_ "SEP0" %>6%^DB%>10%t", + String text = (FMT "\r%>5%,'D %>5%,'D %>5%,'D " SEP0 " %>5%,'D %>5%,'D " SEP0 " %>5%,'D %>5%,'D %_ " SEP0 " %>6%^DB%>10%t", stats.conflicts, stats.decisions, stats.propagations, diff --git a/Prelude/Format.ihh b/Prelude/Format.ihh index e46248b..c49c02f 100644 --- a/Prelude/Format.ihh +++ b/Prelude/Format.ihh @@ -346,7 +346,7 @@ struct ExcpFormater { assert(*fmt == 0); // -- Fails if too FEW arguments are provided for given format X excp(*out); delete out; - throw excp; } + std::terminate(); } };