diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
commit | 70c23e23c3bfc8aa3fdf285fc643b0438359d22a (patch) | |
tree | 3f8f1797e0f8dd3d977f983c1ab823c682f51551 /src/prop/bvminisat | |
parent | 0d080430206880ffc19050acfa01aae1475f1978 (diff) |
moving minisat implementation into their respective directories (regular and bv)
Diffstat (limited to 'src/prop/bvminisat')
-rw-r--r-- | src/prop/bvminisat/Makefile.am | 4 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.cpp | 232 | ||||
-rw-r--r-- | src/prop/bvminisat/bvminisat.h | 87 |
3 files changed, 322 insertions, 1 deletions
diff --git a/src/prop/bvminisat/Makefile.am b/src/prop/bvminisat/Makefile.am index 480e4e83c..685dfac7d 100644 --- a/src/prop/bvminisat/Makefile.am +++ b/src/prop/bvminisat/Makefile.am @@ -22,7 +22,9 @@ libbvminisat_la_SOURCES = \ mtl/Sort.h \ mtl/Vec.h \ mtl/XAlloc.h \ - utils/Options.h + utils/Options.h \ + bvminisat.h \ + bvminisat.cpp EXTRA_DIST = \ core/Main.cc \ diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp new file mode 100644 index 000000000..d4e123489 --- /dev/null +++ b/src/prop/bvminisat/bvminisat.cpp @@ -0,0 +1,232 @@ +/********************* */ +/*! \file bvminisat.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the minisat for cvc4 (bitvectors). + **/ + +#include "prop/bvminisat/bvminisat.h" +#include "prop/bvminisat/simp/SimpSolver.h" + +using namespace CVC4; +using namespace prop; + +MinisatSatSolver::MinisatSatSolver() : + d_minisat(new BVMinisat::SimpSolver()) +{ + d_statistics.init(d_minisat); +} + +MinisatSatSolver::~MinisatSatSolver() { + delete d_minisat; +} + +void MinisatSatSolver::addClause(SatClause& clause, bool removable) { + Debug("sat::minisat") << "Add clause " << clause <<"\n"; + BVMinisat::vec<BVMinisat::Lit> minisat_clause; + toMinisatClause(clause, minisat_clause); + // for(unsigned i = 0; i < minisat_clause.size(); ++i) { + // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); + // } + d_minisat->addClause(minisat_clause); +} + +SatVariable MinisatSatSolver::newVar(bool freeze){ + return d_minisat->newVar(true, true, freeze); +} + +void MinisatSatSolver::markUnremovable(SatLiteral lit){ + d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true); +} + +void MinisatSatSolver::interrupt(){ + d_minisat->interrupt(); +} + +SatLiteralValue MinisatSatSolver::solve(){ + return toSatLiteralValue(d_minisat->solve()); +} + +SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ + Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + if(resource == 0) { + d_minisat->budgetOff(); + } else { + d_minisat->setConfBudget(resource); + } + BVMinisat::vec<BVMinisat::Lit> empty; + unsigned long conflictsBefore = d_minisat->conflicts; + SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + d_minisat->clearInterrupt(); + resource = d_minisat->conflicts - conflictsBefore; + Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl; + return result; +} + +SatLiteralValue MinisatSatSolver::solve(const context::CDList<SatLiteral> & assumptions){ + Debug("sat::minisat") << "Solve with assumptions "; + context::CDList<SatLiteral>::const_iterator it = assumptions.begin(); + BVMinisat::vec<BVMinisat::Lit> assump; + for(; it!= assumptions.end(); ++it) { + SatLiteral lit = *it; + Debug("sat::minisat") << lit <<" "; + assump.push(toMinisatLit(lit)); + } + Debug("sat::minisat") <<"\n"; + + SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); + return result; +} + + +void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) { + // TODO add assertion to check the call was after an unsat call + for (int i = 0; i < d_minisat->conflict.size(); ++i) { + unsatCore.push_back(toSatLiteral(d_minisat->conflict[i])); + } +} + +SatLiteralValue MinisatSatSolver::value(SatLiteral l){ + Unimplemented(); + return SatValUnknown; +} + +SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){ + Unimplemented(); + return SatValUnknown; +} + +void MinisatSatSolver::unregisterVar(SatLiteral lit) { + // this should only be called when user context is implemented + // in the BVSatSolver + Unreachable(); +} + +void MinisatSatSolver::renewVar(SatLiteral lit, int level) { + // this should only be called when user context is implemented + // in the BVSatSolver + + Unreachable(); +} + +int MinisatSatSolver::getAssertionLevel() const { + // we have no user context implemented so far + return 0; +} + +// converting from internal Minisat representation + +SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) { + if (var == var_Undef) { + return undefSatVariable; + } + return SatVariable(var); +} + +BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { + if (lit == undefSatLiteral) { + return BVMinisat::lit_Undef; + } + return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); +} + +SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { + if (lit == BVMinisat::lit_Undef) { + return undefSatLiteral; + } + + return SatLiteral(SatVariable(BVMinisat::var(lit)), + BVMinisat::sign(lit)); +} + +SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) { + if(res) return SatValTrue; + else return SatValFalse; +} + +SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { + if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue; + if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown; + Assert(res == (BVMinisat::lbool((uint8_t)1))); + return SatValFalse; +} + +void MinisatSatSolver::toMinisatClause(SatClause& clause, + BVMinisat::vec<BVMinisat::Lit>& minisat_clause) { + for (unsigned i = 0; i < clause.size(); ++i) { + minisat_clause.push(toMinisatLit(clause[i])); + } + Assert(clause.size() == (unsigned)minisat_clause.size()); +} + +void MinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause, + SatClause& sat_clause) { + for (int i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert((unsigned)clause.size() == sat_clause.size()); +} + + +// Satistics for MinisatSatSolver + +MinisatSatSolver::Statistics::Statistics() : + d_statStarts("theory::bv::bvminisat::starts"), + d_statDecisions("theory::bv::bvminisat::decisions"), + d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), + d_statPropagations("theory::bv::bvminisat::propagations"), + d_statConflicts("theory::bv::bvminisat::conflicts"), + d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"), + d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), + d_statMaxLiterals("theory::bv::bvminisat::max_literals"), + d_statTotLiterals("theory::bv::bvminisat::tot_literals"), + d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars") +{ + StatisticsRegistry::registerStat(&d_statStarts); + StatisticsRegistry::registerStat(&d_statDecisions); + StatisticsRegistry::registerStat(&d_statRndDecisions); + StatisticsRegistry::registerStat(&d_statPropagations); + StatisticsRegistry::registerStat(&d_statConflicts); + StatisticsRegistry::registerStat(&d_statClausesLiterals); + StatisticsRegistry::registerStat(&d_statLearntsLiterals); + StatisticsRegistry::registerStat(&d_statMaxLiterals); + StatisticsRegistry::registerStat(&d_statTotLiterals); + StatisticsRegistry::registerStat(&d_statEliminatedVars); +} + +MinisatSatSolver::Statistics::~Statistics() { + StatisticsRegistry::unregisterStat(&d_statStarts); + StatisticsRegistry::unregisterStat(&d_statDecisions); + StatisticsRegistry::unregisterStat(&d_statRndDecisions); + StatisticsRegistry::unregisterStat(&d_statPropagations); + StatisticsRegistry::unregisterStat(&d_statConflicts); + StatisticsRegistry::unregisterStat(&d_statClausesLiterals); + StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); + StatisticsRegistry::unregisterStat(&d_statMaxLiterals); + StatisticsRegistry::unregisterStat(&d_statTotLiterals); + StatisticsRegistry::unregisterStat(&d_statEliminatedVars); +} + +void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ + d_statStarts.setData(minisat->starts); + d_statDecisions.setData(minisat->decisions); + d_statRndDecisions.setData(minisat->rnd_decisions); + d_statPropagations.setData(minisat->propagations); + d_statConflicts.setData(minisat->conflicts); + d_statClausesLiterals.setData(minisat->clauses_literals); + d_statLearntsLiterals.setData(minisat->learnts_literals); + d_statMaxLiterals.setData(minisat->max_literals); + d_statTotLiterals.setData(minisat->tot_literals); + d_statEliminatedVars.setData(minisat->eliminated_vars); +} diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h new file mode 100644 index 000000000..7c12fcbd0 --- /dev/null +++ b/src/prop/bvminisat/bvminisat.h @@ -0,0 +1,87 @@ +/********************* */ +/*! \file bvminisat.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** Implementation of the minisat for cvc4 (bitvectors). + **/ + +#pragma once + +#include "prop/sat_solver.h" +#include "prop/bvminisat/simp/SimpSolver.h" + +namespace CVC4 { +namespace prop { + +class MinisatSatSolver: public BVSatSolverInterface { + BVMinisat::SimpSolver* d_minisat; + + MinisatSatSolver(); +public: + ~MinisatSatSolver(); + void addClause(SatClause& clause, bool removable); + + SatVariable newVar(bool theoryAtom = false); + + void markUnremovable(SatLiteral lit); + + void interrupt(); + + SatLiteralValue solve(); + SatLiteralValue solve(long unsigned int&); + SatLiteralValue solve(const context::CDList<SatLiteral> & assumptions); + void getUnsatCore(SatClause& unsatCore); + + SatLiteralValue value(SatLiteral l); + SatLiteralValue modelValue(SatLiteral l); + + void unregisterVar(SatLiteral lit); + void renewVar(SatLiteral lit, int level = -1); + int getAssertionLevel() const; + + + // helper methods for converting from the internal Minisat representation + + static SatVariable toSatVariable(BVMinisat::Var var); + static BVMinisat::Lit toMinisatLit(SatLiteral lit); + static SatLiteral toSatLiteral(BVMinisat::Lit lit); + static SatLiteralValue toSatLiteralValue(bool res); + static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res); + + static void toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause); + static void toSatClause (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause); + + class Statistics { + public: + ReferenceStat<uint64_t> d_statStarts, d_statDecisions; + ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations; + ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals; + ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals; + ReferenceStat<uint64_t> d_statTotLiterals; + ReferenceStat<int> d_statEliminatedVars; + Statistics(); + ~Statistics(); + void init(BVMinisat::SimpSolver* minisat); + }; + + Statistics d_statistics; + friend class SatSolverFactory; +}; + +} +} + + + + |