summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/bvminisat.h66
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.h3
-rw-r--r--src/prop/bvminisat/utils/Options.h319
-rw-r--r--src/prop/cnf_stream.h9
-rw-r--r--src/prop/minisat/minisat.h45
-rw-r--r--src/prop/minisat/simp/SimpSolver.h3
-rw-r--r--src/prop/minisat/utils/Options.h319
-rw-r--r--src/prop/registrar.h2
-rw-r--r--src/prop/sat_solver.h6
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback