diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 66 | ||||
-rw-r--r-- | src/prop/bvminisat/simp/SimpSolver.h | 3 | ||||
-rw-r--r-- | src/prop/bvminisat/utils/Options.h | 319 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 9 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 45 | ||||
-rw-r--r-- | src/prop/minisat/simp/SimpSolver.h | 3 | ||||
-rw-r--r-- | src/prop/minisat/utils/Options.h | 319 | ||||
-rw-r--r-- | src/prop/registrar.h | 2 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 6 |
9 files changed, 436 insertions, 336 deletions
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 7dd708ca2..4395cdf6d 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -37,13 +37,16 @@ class BVMinisatSatSolver : public BVSatSolverInterface, public: MinisatNotify(BVSatSolverInterface::Notify* notify) : d_notify(notify) {} - bool notify(BVMinisat::Lit lit) + bool notify(BVMinisat::Lit lit) override { return d_notify->notify(toSatLiteral(lit)); } - void notify(BVMinisat::vec<BVMinisat::Lit>& clause); - void spendResource(unsigned amount) { d_notify->spendResource(amount); } - void safePoint(unsigned amount) { d_notify->safePoint(amount); } + void notify(BVMinisat::vec<BVMinisat::Lit>& clause) override; + void spendResource(unsigned amount) override + { + d_notify->spendResource(amount); + } + void safePoint(unsigned amount) override { d_notify->safePoint(amount); } }; BVMinisat::SimpSolver* d_minisat; @@ -54,45 +57,46 @@ class BVMinisatSatSolver : public BVSatSolverInterface, context::CDO<unsigned> d_lastPropagation; protected: - - void contextNotifyPop(); + void contextNotifyPop() override; public: BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = ""); virtual ~BVMinisatSatSolver(); - void setNotify(Notify* notify); + void setNotify(Notify* notify) override; - ClauseId addClause(SatClause& clause, bool removable); + ClauseId addClause(SatClause& clause, bool removable) override; - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override + { Unreachable("Minisat does not support native XOR reasoning"); } - - SatValue propagate(); - SatVariable newVar(bool isTheoryAtom = false, bool preRegister = false, bool canErase = true); + SatValue propagate() override; - SatVariable trueVar() { return d_minisat->trueVar(); } - SatVariable falseVar() { return d_minisat->falseVar(); } + SatVariable newVar(bool isTheoryAtom = false, + bool preRegister = false, + bool canErase = true) override; - void markUnremovable(SatLiteral lit); + SatVariable trueVar() override { return d_minisat->trueVar(); } + SatVariable falseVar() override { return d_minisat->falseVar(); } - void interrupt(); + void markUnremovable(SatLiteral lit) override; - SatValue solve(); - SatValue solve(long unsigned int&); - bool ok() const; - void getUnsatCore(SatClause& unsatCore); + void interrupt() override; - SatValue value(SatLiteral l); - SatValue modelValue(SatLiteral l); + SatValue solve() override; + SatValue solve(long unsigned int&) override; + bool ok() const override; + void getUnsatCore(SatClause& unsatCore) override; + + SatValue value(SatLiteral l) override; + SatValue modelValue(SatLiteral l) override; void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); - unsigned getAssertionLevel() const; - + unsigned getAssertionLevel() const override; // helper methods for converting from the internal Minisat representation @@ -103,17 +107,17 @@ public: static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); static void toSatClause (const BVMinisat::Clause& clause, SatClause& sat_clause); - void addMarkerLiteral(SatLiteral lit); + void addMarkerLiteral(SatLiteral lit) override; - void explain(SatLiteral lit, std::vector<SatLiteral>& explanation); + void explain(SatLiteral lit, std::vector<SatLiteral>& explanation) override; - SatValue assertAssumption(SatLiteral lit, bool propagate); + SatValue assertAssumption(SatLiteral lit, bool propagate) override; - void popAssumption(); - - void setProofLog( BitVectorProof * bvp ); + void popAssumption() override; -private: + void setProofLog(BitVectorProof* bvp) override; + + private: /* Disable the default constructor. */ BVMinisatSatSolver() CVC4_UNDEFINED; diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 9854bf77d..246bb7152 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -69,8 +69,7 @@ class SimpSolver : public Solver { // Memory managment: // - virtual void garbageCollect(); - + void garbageCollect() override; // Generate a (possibly simplified) DIMACS file: // diff --git a/src/prop/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h index 12321cba2..698035b7c 100644 --- a/src/prop/bvminisat/utils/Options.h +++ b/src/prop/bvminisat/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"); + } } }; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 80f8742a3..174263be0 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -286,8 +286,11 @@ class TseitinCnfStream : public CnfStream { * @param removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool removable, bool negated, - ProofRule rule, TNode from = TNode::null()); + void convertAndAssert(TNode node, + bool removable, + bool negated, + ProofRule rule, + TNode from = TNode::null()) override; private: /** @@ -328,7 +331,7 @@ class TseitinCnfStream : public CnfStream { */ SatLiteral toCNF(TNode node, bool negated = false); - void ensureLiteral(TNode n, bool noPreregistration = false); + void ensureLiteral(TNode n, bool noPreregistration = false) override; }; /* class TseitinCnfStream */ 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::Lit>& 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"); + } } }; diff --git a/src/prop/registrar.h b/src/prop/registrar.h index ec774e979..9735aa43d 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -35,7 +35,7 @@ public: class NullRegistrar : public Registrar { public: - void preRegister(Node n) {} + void preRegister(Node n) override {} };/* class NullRegistrar */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 7be5305ad..4dc95e060 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -137,10 +137,6 @@ public: virtual void popAssumption() = 0; - virtual bool ok() const = 0; - - virtual void setProofLog( BitVectorProof * bvp ) {} - };/* class BVSatSolverInterface */ @@ -159,8 +155,6 @@ public: virtual bool flipDecision() = 0; virtual bool isDecision(SatVariable decn) const = 0; - - virtual bool ok() const = 0; };/* class DPLLSatSolverInterface */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { |