From 386e4f372688526aed987a26f38f18160d2d4fcb Mon Sep 17 00:00:00 2001 From: Niklas Sorensson Date: Wed, 31 Oct 2012 12:20:45 +0000 Subject: [PATCH] Silence DIMACS warnings by default. Added a -strict flag that checks correctness of "p cnf" line. --- minisat/core/Dimacs.h | 12 +++++------- minisat/core/Main.cc | 3 ++- minisat/simp/Main.cc | 3 ++- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/minisat/core/Dimacs.h b/minisat/core/Dimacs.h index 3c77e754..d5db4139 100644 --- a/minisat/core/Dimacs.h +++ b/minisat/core/Dimacs.h @@ -45,7 +45,7 @@ static void readClause(B& in, Solver& S, vec& lits) { } template -static void parse_DIMACS_main(B& in, Solver& S) { +static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) { vec lits; int vars = 0; int clauses = 0; @@ -70,18 +70,16 @@ static void parse_DIMACS_main(B& in, Solver& S) { readClause(in, S, lits); S.addClause_(lits); } } - if (vars != S.nVars()) - fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of variables.\n"); - if (cnt != clauses) - fprintf(stderr, "WARNING! DIMACS header mismatch: wrong number of clauses.\n"); + if (strictp && cnt != clauses) + printf("PARSE ERROR! DIMACS header mismatch: wrong number of clauses\n"); } // Inserts problem into solver. // template -static void parse_DIMACS(gzFile input_stream, Solver& S) { +static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) { StreamBuffer in(input_stream); - parse_DIMACS_main(in, S); } + parse_DIMACS_main(in, S, strictp); } //================================================================================================= } diff --git a/minisat/core/Main.cc b/minisat/core/Main.cc index a70d9d2c..69302aea 100644 --- a/minisat/core/Main.cc +++ b/minisat/core/Main.cc @@ -63,6 +63,7 @@ int main(int argc, char** argv) IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2)); IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", 0, IntRange(0, INT32_MAX)); IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", 0, IntRange(0, INT32_MAX)); + BoolOption strictp("MAIN", "strict", "Validate DIMACS header during parsing.", false); parseOptions(argc, argv, true); @@ -91,7 +92,7 @@ int main(int argc, char** argv) printf("============================[ Problem Statistics ]=============================\n"); printf("| |\n"); } - parse_DIMACS(in, S); + parse_DIMACS(in, S, (bool)strictp); gzclose(in); FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL; diff --git a/minisat/simp/Main.cc b/minisat/simp/Main.cc index 6c70adf8..87dea1b5 100644 --- a/minisat/simp/Main.cc +++ b/minisat/simp/Main.cc @@ -65,6 +65,7 @@ int main(int argc, char** argv) StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file."); IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", 0, IntRange(0, INT32_MAX)); IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", 0, IntRange(0, INT32_MAX)); + BoolOption strictp("MAIN", "strict", "Validate DIMACS header during parsing.", false); parseOptions(argc, argv, true); @@ -95,7 +96,7 @@ int main(int argc, char** argv) printf("============================[ Problem Statistics ]=============================\n"); printf("| |\n"); } - parse_DIMACS(in, S); + parse_DIMACS(in, S, (bool)strictp); gzclose(in); FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;