diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-28 15:44:30 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-28 15:44:30 +0000 |
commit | 4d5d28e59c6338876e8436a5fc2b9e2dd6058e30 (patch) | |
tree | e2455de003c7c2aaa19a0209fdf46a5074bfb1aa /src/prop/minisat/minisat.cpp | |
parent | 9a8d0af063302752905bda7f2043a9695c3126d3 (diff) |
Some renaming and refactoring in SAT
Diffstat (limited to 'src/prop/minisat/minisat.cpp')
-rw-r--r-- | src/prop/minisat/minisat.cpp | 54 |
1 files changed, 27 insertions, 27 deletions
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 1ec81a4f6..c8d310992 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -24,31 +24,31 @@ using namespace CVC4::prop; //// DPllMinisatSatSolver -DPLLMinisatSatSolver::DPLLMinisatSatSolver() : +MinisatSatSolver::MinisatSatSolver() : d_minisat(NULL), d_theoryProxy(NULL), d_context(NULL) {} -DPLLMinisatSatSolver::~DPLLMinisatSatSolver() { +MinisatSatSolver::~MinisatSatSolver() { delete d_minisat; } -SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) { +SatVariable MinisatSatSolver::toSatVariable(Minisat::Var var) { if (var == var_Undef) { return undefSatVariable; } return SatVariable(var); } -Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) { +Minisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { if (lit == undefSatLiteral) { return Minisat::lit_Undef; } return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); } -SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { +SatLiteral MinisatSatSolver::toSatLiteral(Minisat::Lit lit) { if (lit == Minisat::lit_Undef) { return undefSatLiteral; } @@ -57,12 +57,12 @@ SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { Minisat::sign(lit)); } -SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { +SatValue MinisatSatSolver::toSatLiteralValue(bool res) { if(res) return SAT_VALUE_TRUE; else return SAT_VALUE_FALSE; } -SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { +SatValue MinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; Assert(res == (Minisat::lbool((uint8_t)1))); @@ -70,7 +70,7 @@ SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { } -void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, +void MinisatSatSolver::toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause) { for (unsigned i = 0; i < clause.size(); ++i) { minisat_clause.push(toMinisatLit(clause[i])); @@ -78,7 +78,7 @@ void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, Assert(clause.size() == (unsigned)minisat_clause.size()); } -void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, +void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause) { for (int i = 0; i < clause.size(); ++i) { sat_clause.push_back(toSatLiteral(clause[i])); @@ -87,7 +87,7 @@ void DPLLMinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause, } -void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) +void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) { d_context = context; @@ -110,18 +110,18 @@ void DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* th d_statistics.init(d_minisat); } -void DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) { +void MinisatSatSolver::addClause(SatClause& clause, bool removable) { Minisat::vec<Minisat::Lit> minisat_clause; toMinisatClause(clause, minisat_clause); d_minisat->addClause(minisat_clause, removable); } -SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) { +SatVariable MinisatSatSolver::newVar(bool theoryAtom) { return d_minisat->newVar(true, true, theoryAtom); } -SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) { +SatValue MinisatSatSolver::solve(unsigned long& resource) { Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { d_minisat->budgetOff(); @@ -137,53 +137,53 @@ SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) { return result; } -SatValue DPLLMinisatSatSolver::solve() { +SatValue MinisatSatSolver::solve() { d_minisat->budgetOff(); return toSatLiteralValue(d_minisat->solve()); } -void DPLLMinisatSatSolver::interrupt() { +void MinisatSatSolver::interrupt() { d_minisat->interrupt(); } -SatValue DPLLMinisatSatSolver::value(SatLiteral l) { +SatValue MinisatSatSolver::value(SatLiteral l) { return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); } -SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ +SatValue MinisatSatSolver::modelValue(SatLiteral l){ return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } -bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { +bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { return true; } /** Incremental interface */ -unsigned DPLLMinisatSatSolver::getAssertionLevel() const { +unsigned MinisatSatSolver::getAssertionLevel() const { return d_minisat->getAssertionLevel(); } -void DPLLMinisatSatSolver::push() { +void MinisatSatSolver::push() { d_minisat->push(); } -void DPLLMinisatSatSolver::pop(){ +void MinisatSatSolver::pop(){ d_minisat->pop(); } -void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) { +void MinisatSatSolver::unregisterVar(SatLiteral lit) { d_minisat->unregisterVar(toMinisatLit(lit)); } -void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) { +void MinisatSatSolver::renewVar(SatLiteral lit, int level) { d_minisat->renewVar(toMinisatLit(lit), level); } -/// Statistics for DPLLMinisatSatSolver +/// Statistics for MinisatSatSolver -DPLLMinisatSatSolver::Statistics::Statistics() : +MinisatSatSolver::Statistics::Statistics() : d_statStarts("sat::starts"), d_statDecisions("sat::decisions"), d_statRndDecisions("sat::rnd_decisions"), @@ -204,7 +204,7 @@ DPLLMinisatSatSolver::Statistics::Statistics() : StatisticsRegistry::registerStat(&d_statMaxLiterals); StatisticsRegistry::registerStat(&d_statTotLiterals); } -DPLLMinisatSatSolver::Statistics::~Statistics() { +MinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statStarts); StatisticsRegistry::unregisterStat(&d_statDecisions); StatisticsRegistry::unregisterStat(&d_statRndDecisions); @@ -215,7 +215,7 @@ DPLLMinisatSatSolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_statMaxLiterals); StatisticsRegistry::unregisterStat(&d_statTotLiterals); } -void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ +void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ d_statStarts.setData(d_minisat->starts); d_statDecisions.setData(d_minisat->decisions); d_statRndDecisions.setData(d_minisat->rnd_decisions); |