From 3d31caa30e094d337a4919b3d1e6ba9259e461b8 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 5 Mar 2018 15:36:50 -0800 Subject: Enable -Wsuggest-override by default. (#1643) Adds missing override keywords. --- src/prop/minisat/minisat.h | 45 +++--- src/prop/minisat/simp/SimpSolver.h | 3 +- src/prop/minisat/utils/Options.h | 319 +++++++++++++++++++++---------------- 3 files changed, 209 insertions(+), 158 deletions(-) (limited to 'src/prop/minisat') diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index ca179fbc8..58e02179c 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -39,45 +39,48 @@ public: static void toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause); static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); - void initialize(context::Context* context, TheoryProxy* theoryProxy); + void initialize(context::Context* context, TheoryProxy* theoryProxy) override; - ClauseId addClause(SatClause& clause, bool removable); - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + ClauseId addClause(SatClause& clause, bool removable) override; + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override + { Unreachable("Minisat does not support native XOR reasoning"); } - SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); - SatVariable trueVar() { return d_minisat->trueVar(); } - SatVariable falseVar() { return d_minisat->falseVar(); } + SatVariable newVar(bool isTheoryAtom, + bool preRegister, + bool canErase) override; + SatVariable trueVar() override { return d_minisat->trueVar(); } + SatVariable falseVar() override { return d_minisat->falseVar(); } - SatValue solve(); - SatValue solve(long unsigned int&); + SatValue solve() override; + SatValue solve(long unsigned int&) override; - bool ok() const; - - void interrupt(); + bool ok() const override; - SatValue value(SatLiteral l); + void interrupt() override; - SatValue modelValue(SatLiteral l); + SatValue value(SatLiteral l) override; - bool properExplanation(SatLiteral lit, SatLiteral expl) const; + SatValue modelValue(SatLiteral l) override; + + bool properExplanation(SatLiteral lit, SatLiteral expl) const override; /** Incremental interface */ - unsigned getAssertionLevel() const; + unsigned getAssertionLevel() const override; - void push(); + void push() override; - void pop(); + void pop() override; - void requirePhase(SatLiteral lit); + void requirePhase(SatLiteral lit) override; - bool flipDecision(); + bool flipDecision() override; - bool isDecision(SatVariable decn) const; + bool isDecision(SatVariable decn) const override; -private: + private: /** The SatSolver used */ Minisat::SimpSolver* d_minisat; diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h index a995c1357..335075f09 100644 --- a/src/prop/minisat/simp/SimpSolver.h +++ b/src/prop/minisat/simp/SimpSolver.h @@ -74,8 +74,7 @@ class SimpSolver : public Solver { // Memory managment: // - virtual void garbageCollect(); - + void garbageCollect() override; // Generate a (possibly simplified) DIMACS file: // diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h index 0577cbbd0..9bddd2b23 100644 --- a/src/prop/minisat/utils/Options.h +++ b/src/prop/minisat/utils/Options.h @@ -135,42 +135,58 @@ class DoubleOption : public Option operator double& (void) { return value; } DoubleOption& operator=(double x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; + bool parse(const char* str) override + { + const char* span = str; - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; - - char* end; - double tmp = strtod(span, &end); - - if (end == NULL) - return false; - else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp <= range.begin && (!range.begin_inclusive || tmp != range.begin)){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; - // fprintf(stderr, "READ VALUE: %g\n", value); + char* end; + double tmp = strtod(span, &end); - return true; + if (end == NULL) + return false; + else if (tmp >= range.end && (!range.end_inclusive || tmp != range.end)) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp <= range.begin + && (!range.begin_inclusive || tmp != range.begin)) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + // fprintf(stderr, "READ VALUE: %g\n", value); + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", - name, type_name, - range.begin_inclusive ? '[' : '(', - range.begin, - range.end, - range.end_inclusive ? ']' : ')', - value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, + " -%-12s = %-8s %c%4.2g .. %4.2g%c (default: %g)\n", + name, + type_name, + range.begin_inclusive ? '[' : '(', + range.begin, + range.end, + range.end_inclusive ? ']' : ')', + value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -193,47 +209,60 @@ class IntOption : public Option operator int32_t& (void) { return value; } IntOption& operator= (int32_t x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + bool parse(const char* str) override + { + const char* span = str; - char* end; - int32_t tmp = strtol(span, &end, 10); - - if (end == NULL) - return false; - else if (tmp > range.end){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp < range.begin){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; + char* end; + int32_t tmp = strtol(span, &end, 10); - return true; + if (end == NULL) + return false; + else if (tmp > range.end) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp < range.begin) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT32_MIN) - fprintf(stderr, "imin"); - else - fprintf(stderr, "%4d", range.begin); - - fprintf(stderr, " .. "); - if (range.end == INT32_MAX) - fprintf(stderr, "imax"); - else - fprintf(stderr, "%4d", range.end); - - fprintf(stderr, "] (default: %d)\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-12s = %-8s [", name, type_name); + if (range.begin == INT32_MIN) + fprintf(stderr, "imin"); + else + fprintf(stderr, "%4d", range.begin); + + fprintf(stderr, " .. "); + if (range.end == INT32_MAX) + fprintf(stderr, "imax"); + else + fprintf(stderr, "%4d", range.end); + + fprintf(stderr, "] (default: %d)\n", value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -255,47 +284,60 @@ class Int64Option : public Option operator int64_t& (void) { return value; } Int64Option& operator= (int64_t x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + bool parse(const char* str) override + { + const char* span = str; - char* end; - int64_t tmp = strtoll(span, &end, 10); - - if (end == NULL) - return false; - else if (tmp > range.end){ - fprintf(stderr, "ERROR! value <%s> is too large for option \"%s\".\n", span, name); - exit(1); - }else if (tmp < range.begin){ - fprintf(stderr, "ERROR! value <%s> is too small for option \"%s\".\n", span, name); - exit(1); } + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = tmp; + char* end; + int64_t tmp = strtoll(span, &end, 10); - return true; + if (end == NULL) + return false; + else if (tmp > range.end) + { + fprintf(stderr, + "ERROR! value <%s> is too large for option \"%s\".\n", + span, + name); + exit(1); + } + else if (tmp < range.begin) + { + fprintf(stderr, + "ERROR! value <%s> is too small for option \"%s\".\n", + span, + name); + exit(1); + } + + value = tmp; + + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-12s = %-8s [", name, type_name); - if (range.begin == INT64_MIN) - fprintf(stderr, "imin"); - else - 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, "] (default: %" PRIi64")\n", value); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-12s = %-8s [", name, type_name); + if (range.begin == INT64_MIN) + fprintf(stderr, "imin"); + else + 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, "] (default: %" PRIi64 ")\n", value); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; #endif @@ -315,22 +357,25 @@ class StringOption : public Option operator const char*& (void) { return value; } StringOption& operator= (const char* x) { value = x; return *this; } - virtual bool parse(const char* str){ - const char* span = str; + bool parse(const char* str) override + { + const char* span = str; - if (!match(span, "-") || !match(span, name) || !match(span, "=")) - return false; + if (!match(span, "-") || !match(span, name) || !match(span, "=")) + return false; - value = span; - return true; + value = span; + return true; } - virtual void help (bool verbose = false){ - fprintf(stderr, " -%-10s = %8s\n", name, type_name); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + void help(bool verbose = false) override + { + fprintf(stderr, " -%-10s = %8s\n", name, type_name); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; @@ -351,33 +396,37 @@ class BoolOption : public Option operator bool& (void) { return value; } BoolOption& operator=(bool b) { value = b; return *this; } - virtual bool parse(const char* str){ - const char* span = str; - - if (match(span, "-")){ - bool b = !match(span, "no-"); + bool parse(const char* str) override + { + const char* span = str; + + if (match(span, "-")) + { + bool b = !match(span, "no-"); - if (strcmp(span, name) == 0){ - value = b; - return true; } + if (strcmp(span, name) == 0) + { + value = b; + return true; } + } - return false; + return false; } - virtual void help (bool verbose = false){ + void help(bool verbose = false) override + { + fprintf(stderr, " -%s, -no-%s", name, name); - fprintf(stderr, " -%s, -no-%s", name, name); + for (uint32_t i = 0; i < 32 - strlen(name) * 2; i++) fprintf(stderr, " "); - for (uint32_t i = 0; i < 32 - strlen(name)*2; i++) - fprintf(stderr, " "); - - fprintf(stderr, " "); - fprintf(stderr, "(default: %s)\n", value ? "on" : "off"); - if (verbose){ - fprintf(stderr, "\n %s\n", description); - fprintf(stderr, "\n"); - } + fprintf(stderr, " "); + fprintf(stderr, "(default: %s)\n", value ? "on" : "off"); + if (verbose) + { + fprintf(stderr, "\n %s\n", description); + fprintf(stderr, "\n"); + } } }; -- cgit v1.2.3