Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Using std::numeric_limits<> instead of macros INT32/INT64_MAX/MIN #7

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Using std::numeric_limits<> instead of macros INT32/INT64_MAX/MIN #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions minisat/core/Main.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int32_t>::max()));
IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", 0, IntRange(0, std::numeric_limits<int32_t>::max()));
BoolOption strictp("MAIN", "strict", "Validate DIMACS header during parsing.", false);

parseOptions(argc, argv, true);
Expand Down
4 changes: 2 additions & 2 deletions minisat/core/Solver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int32_t>::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<int32_t>::max()));


//=================================================================================================
Expand Down
4 changes: 2 additions & 2 deletions minisat/simp/Main.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int32_t>::max()));
IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", 0, IntRange(0, std::numeric_limits<int32_t>::max()));
BoolOption strictp("MAIN", "strict", "Validate DIMACS header during parsing.", false);

parseOptions(argc, argv, true);
Expand Down
4 changes: 2 additions & 2 deletions minisat/simp/SimpSolver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<int32_t>::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<int32_t>::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));


Expand Down
13 changes: 7 additions & 6 deletions minisat/utils/Options.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 <limits>

namespace Minisat {

Expand Down Expand Up @@ -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<int32_t>::min(), std::numeric_limits<int32_t>::max()))
: Option(n, d, c, "<int32>"), range(r), value(def) {}

operator int32_t (void) const { return value; }
Expand Down Expand Up @@ -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<int32_t>::min())
fprintf(stderr, "imin");
else
fprintf(stderr, "%4d", range.begin);

fprintf(stderr, " .. ");
if (range.end == INT32_MAX)
if (range.end == std::numeric_limits<int32_t>::max())
fprintf(stderr, "imax");
else
fprintf(stderr, "%4d", range.end);
Expand All @@ -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<int64_t>::min(), std::numeric_limits<int64_t>::max()))
: Option(n, d, c, "<int64>"), range(r), value(def) {}

operator int64_t (void) const { return value; }
Expand Down Expand Up @@ -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<int64_t>::min())
fprintf(stderr, "imin");
else
fprintf(stderr, "%4"PRIi64, range.begin);

fprintf(stderr, " .. ");
if (range.end == INT64_MAX)
if (range.end == std::numeric_limits<int64_t>::max())
fprintf(stderr, "imax");
else
fprintf(stderr, "%4"PRIi64, range.end);
Expand Down