diff --git a/minisat/core/Main.cc b/minisat/core/Main.cc index 69302aea..490c31ff 100644 --- a/minisat/core/Main.cc +++ b/minisat/core/Main.cc @@ -61,8 +61,8 @@ int main(int argc, char** argv) // Extra options: // 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)); + IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", 0, IntRange(0, std::numeric_limits::max())); + IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", 0, IntRange(0, std::numeric_limits::max())); BoolOption strictp("MAIN", "strict", "Validate DIMACS header during parsing.", false); parseOptions(argc, argv, true); diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 0b4f77ad..19896f7d 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -41,10 +41,10 @@ static IntOption opt_ccmin_mode (_cat, "ccmin-mode", "Controls confl static IntOption opt_phase_saving (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2)); static BoolOption opt_rnd_init_act (_cat, "rnd-init", "Randomize the initial activity", false); static BoolOption opt_luby_restart (_cat, "luby", "Use the Luby restart sequence", true); -static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX)); +static IntOption opt_restart_first (_cat, "rfirst", "The base restart interval", 100, IntRange(1, std::numeric_limits::max())); static DoubleOption opt_restart_inc (_cat, "rinc", "Restart interval increase factor", 2, DoubleRange(1, false, HUGE_VAL, false)); static DoubleOption opt_garbage_frac (_cat, "gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered", 0.20, DoubleRange(0, false, HUGE_VAL, false)); -static IntOption opt_min_learnts_lim (_cat, "min-learnts", "Minimum learnt clause limit", 0, IntRange(0, INT32_MAX)); +static IntOption opt_min_learnts_lim (_cat, "min-learnts", "Minimum learnt clause limit", 0, IntRange(0, std::numeric_limits::max())); //================================================================================================= diff --git a/minisat/simp/Main.cc b/minisat/simp/Main.cc index 87dea1b5..fe63c999 100644 --- a/minisat/simp/Main.cc +++ b/minisat/simp/Main.cc @@ -63,8 +63,8 @@ int main(int argc, char** argv) BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true); BoolOption solve ("MAIN", "solve", "Completely turn on/off solving after preprocessing.", true); 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)); + IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", 0, IntRange(0, std::numeric_limits::max())); + IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", 0, IntRange(0, std::numeric_limits::max())); BoolOption strictp("MAIN", "strict", "Validate DIMACS header during parsing.", false); parseOptions(argc, argv, true); diff --git a/minisat/simp/SimpSolver.cc b/minisat/simp/SimpSolver.cc index 0a5bed85..a87b65e2 100644 --- a/minisat/simp/SimpSolver.cc +++ b/minisat/simp/SimpSolver.cc @@ -34,8 +34,8 @@ static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false); static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true); static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0); -static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX)); -static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX)); +static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, std::numeric_limits::max())); +static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, std::numeric_limits::max())); static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false)); diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h index 4e71a18c..d9766d0e 100644 --- a/minisat/utils/Options.h +++ b/minisat/utils/Options.h @@ -28,6 +28,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "minisat/mtl/IntTypes.h" #include "minisat/mtl/Vec.h" #include "minisat/utils/ParseUtils.h" +#include namespace Minisat { @@ -185,7 +186,7 @@ class IntOption : public Option int32_t value; public: - IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(INT32_MIN, INT32_MAX)) + IntOption(const char* c, const char* n, const char* d, int32_t def = int32_t(), IntRange r = IntRange(std::numeric_limits::min(), std::numeric_limits::max())) : Option(n, d, c, ""), range(r), value(def) {} operator int32_t (void) const { return value; } @@ -217,13 +218,13 @@ class IntOption : public Option virtual void help (bool verbose = false){ fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT32_MIN) + if (range.begin == std::numeric_limits::min()) fprintf(stderr, "imin"); else fprintf(stderr, "%4d", range.begin); fprintf(stderr, " .. "); - if (range.end == INT32_MAX) + if (range.end == std::numeric_limits::max()) fprintf(stderr, "imax"); else fprintf(stderr, "%4d", range.end); @@ -247,7 +248,7 @@ class Int64Option : public Option int64_t value; public: - Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range(INT64_MIN, INT64_MAX)) + Int64Option(const char* c, const char* n, const char* d, int64_t def = int64_t(), Int64Range r = Int64Range( std::numeric_limits::min(), std::numeric_limits::max())) : Option(n, d, c, ""), range(r), value(def) {} operator int64_t (void) const { return value; } @@ -279,13 +280,13 @@ class Int64Option : public Option virtual void help (bool verbose = false){ fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT64_MIN) + if (range.begin == std::numeric_limits::min()) fprintf(stderr, "imin"); else fprintf(stderr, "%4"PRIi64, range.begin); fprintf(stderr, " .. "); - if (range.end == INT64_MAX) + if (range.end == std::numeric_limits::max()) fprintf(stderr, "imax"); else fprintf(stderr, "%4"PRIi64, range.end);