summaryrefslogtreecommitdiff
path: root/src/prop/bvminisat
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/bvminisat')
-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
3 files changed, 220 insertions, 168 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");
+ }
}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback