diff options
Diffstat (limited to 'src/prop/bvminisat')
-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 |
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"); + } } }; |