src/prop/bvminisat/bvminisat.cpp

   1 /*********************                                                        */
   2 /*! \file bvminisat.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors:
   6  ** Minor contributors (to current version):
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief SAT Solver.
  15  **
  16  ** Implementation of the minisat for cvc4 (bitvectors).
  17  **/
  18
  19 #include "prop/bvminisat/bvminisat.h"
  20 #include "prop/bvminisat/simp/SimpSolver.h"
  21
  22 using namespace CVC4;
  23 using namespace prop;
  24
  25 BVMinisatSatSolver::BVMinisatSatSolver(context::Context* mainSatContext, const std::string& name)
  26 : context::ContextNotifyObj(mainSatContext, false),
  27   d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
  28   d_minisatNotify(0),
  29   d_assertionsCount(0),
  30   d_assertionsRealCount(mainSatContext, 0),
  31   d_lastPropagation(mainSatContext, 0),
  32   d_statistics(name)
  33 {
  34   d_statistics.init(d_minisat);
  35 }
  36
  37
  38 BVMinisatSatSolver::~BVMinisatSatSolver() throw(AssertionException) {
  39   delete d_minisat;
  40   delete d_minisatNotify;
  41 }
  42
  43 void BVMinisatSatSolver::setNotify(Notify* notify) {
  44   d_minisatNotify = new MinisatNotify(notify);
  45   d_minisat->setNotify(d_minisatNotify);
  46 }
  47
  48 void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
  49   Debug("sat::minisat") << "Add clause " << clause <<"\n";
  50   BVMinisat::vec<BVMinisat::Lit> minisat_clause;
  51   toMinisatClause(clause, minisat_clause);
  52   // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
  53   //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
  54   // }
  55   d_minisat->addClause(minisat_clause);
  56 }
  57
  58 SatValue BVMinisatSatSolver::propagate() {
  59   return toSatLiteralValue(d_minisat->propagateAssumptions());
  60 }
  61
  62 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
  63   d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
  64   markUnremovable(lit);
  65 }
  66
  67 void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) {
  68   std::vector<BVMinisat::Lit> minisat_explanation;
  69   d_minisat->explain(toMinisatLit(lit), minisat_explanation);
  70   for (unsigned i = 0; i < minisat_explanation.size(); ++i) {
  71     explanation.push_back(toSatLiteral(minisat_explanation[i]));
  72   }
  73 }
  74
  75 SatValue BVMinisatSatSolver::assertAssumption(SatLiteral lit, bool propagate) {
  76   d_assertionsCount ++;
  77   d_assertionsRealCount = d_assertionsRealCount + 1;
  78   return toSatLiteralValue(d_minisat->assertAssumption(toMinisatLit(lit), propagate));
  79 }
  80
  81 void BVMinisatSatSolver::contextNotifyPop() {
  82   while (d_assertionsCount > d_assertionsRealCount) {
  83     popAssumption();
  84     d_assertionsCount --;
  85   }
  86 }
  87
  88 void BVMinisatSatSolver::popAssumption() {
  89   d_minisat->popAssumption();
  90 }
  91
  92 SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
  93   return d_minisat->newVar(true, true, !canErase);
  94 }
  95
  96 void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
  97   d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
  98 }
  99
 100 void BVMinisatSatSolver::spendResource(){
 101   // do nothing for the BV solver
 102 }
 103
 104 void BVMinisatSatSolver::interrupt(){
 105   d_minisat->interrupt();
 106 }
 107
 108 SatValue BVMinisatSatSolver::solve(){
 109   ++d_statistics.d_statCallsToSolve;
 110   return toSatLiteralValue(d_minisat->solve());
 111 }
 112
 113 SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
 114   Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
 115   ++d_statistics.d_statCallsToSolve;
 116   if(resource == 0) {
 117     d_minisat->budgetOff();
 118   } else {
 119     d_minisat->setConfBudget(resource);
 120   }
 121   //  BVMinisat::vec<BVMinisat::Lit> empty;
 122   unsigned long conflictsBefore = d_minisat->conflicts;
 123   SatValue result = toSatLiteralValue(d_minisat->solveLimited());
 124   d_minisat->clearInterrupt();
 125   resource = d_minisat->conflicts - conflictsBefore;
 126   Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
 127   return result;
 128 }
 129
 130 void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
 131   // TODO add assertion to check the call was after an unsat call
 132   for (int i = 0; i < d_minisat->conflict.size(); ++i) {
 133     unsatCore.push_back(toSatLiteral(d_minisat->conflict[i]));
 134   }
 135 }
 136
 137 SatValue BVMinisatSatSolver::value(SatLiteral l){
 138         return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
 139 }
 140
 141 SatValue BVMinisatSatSolver::modelValue(SatLiteral l){
 142         return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 143 }
 144
 145 void BVMinisatSatSolver::unregisterVar(SatLiteral lit) {
 146   // this should only be called when user context is implemented
 147   // in the BVSatSolver
 148   Unreachable();
 149 }
 150
 151 void BVMinisatSatSolver::renewVar(SatLiteral lit, int level) {
 152   // this should only be called when user context is implemented
 153   // in the BVSatSolver
 154
 155   Unreachable();
 156 }
 157
 158 unsigned BVMinisatSatSolver::getAssertionLevel() const {
 159   // we have no user context implemented so far
 160   return 0;
 161 }
 162
 163 // converting from internal Minisat representation
 164
 165 SatVariable BVMinisatSatSolver::toSatVariable(BVMinisat::Var var) {
 166   if (var == var_Undef) {
 167     return undefSatVariable;
 168   }
 169   return SatVariable(var);
 170 }
 171
 172 BVMinisat::Lit BVMinisatSatSolver::toMinisatLit(SatLiteral lit) {
 173   if (lit == undefSatLiteral) {
 174     return BVMinisat::lit_Undef;
 175   }
 176   return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated());
 177 }
 178
 179 SatLiteral BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
 180   if (lit == BVMinisat::lit_Undef) {
 181     return undefSatLiteral;
 182   }
 183
 184   return SatLiteral(SatVariable(BVMinisat::var(lit)),
 185                     BVMinisat::sign(lit));
 186 }
 187
 188 SatValue BVMinisatSatSolver::toSatLiteralValue(bool res) {
 189   if(res) return SAT_VALUE_TRUE;
 190   else return SAT_VALUE_FALSE;
 191 }
 192
 193 SatValue BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
 194   if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
 195   if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
 196   Assert(res == (BVMinisat::lbool((uint8_t)1)));
 197   return SAT_VALUE_FALSE;
 198 }
 199
 200 void BVMinisatSatSolver::toMinisatClause(SatClause& clause,
 201                                            BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
 202   for (unsigned i = 0; i < clause.size(); ++i) {
 203     minisat_clause.push(toMinisatLit(clause[i]));
 204   }
 205   Assert(clause.size() == (unsigned)minisat_clause.size());
 206 }
 207
 208 void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
 209                                        SatClause& sat_clause) {
 210   for (int i = 0; i < clause.size(); ++i) {
 211     sat_clause.push_back(toSatLiteral(clause[i]));
 212   }
 213   Assert((unsigned)clause.size() == sat_clause.size());
 214 }
 215
 216
 217 // Satistics for BVMinisatSatSolver
 218
 219 BVMinisatSatSolver::Statistics::Statistics(const std::string& prefix) :
 220   d_statStarts("theory::bv::"+prefix+"bvminisat::starts"),
 221   d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"),
 222   d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"),
 223   d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"),
 224   d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"),
 225   d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"),
 226   d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"),
 227   d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"),
 228   d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"),
 229   d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"),
 230   d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0),
 231   d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0),
 232   d_registerStats(!prefix.empty())
 233 {
 234   if (!d_registerStats)
 235     return;
 236
 237   StatisticsRegistry::registerStat(&d_statStarts);
 238   StatisticsRegistry::registerStat(&d_statDecisions);
 239   StatisticsRegistry::registerStat(&d_statRndDecisions);
 240   StatisticsRegistry::registerStat(&d_statPropagations);
 241   StatisticsRegistry::registerStat(&d_statConflicts);
 242   StatisticsRegistry::registerStat(&d_statClausesLiterals);
 243   StatisticsRegistry::registerStat(&d_statLearntsLiterals);
 244   StatisticsRegistry::registerStat(&d_statMaxLiterals);
 245   StatisticsRegistry::registerStat(&d_statTotLiterals);
 246   StatisticsRegistry::registerStat(&d_statEliminatedVars);
 247   StatisticsRegistry::registerStat(&d_statCallsToSolve);
 248   StatisticsRegistry::registerStat(&d_statSolveTime);
 249 }
 250
 251 BVMinisatSatSolver::Statistics::~Statistics() {
 252   if (!d_registerStats)
 253     return;
 254   StatisticsRegistry::unregisterStat(&d_statStarts);
 255   StatisticsRegistry::unregisterStat(&d_statDecisions);
 256   StatisticsRegistry::unregisterStat(&d_statRndDecisions);
 257   StatisticsRegistry::unregisterStat(&d_statPropagations);
 258   StatisticsRegistry::unregisterStat(&d_statConflicts);
 259   StatisticsRegistry::unregisterStat(&d_statClausesLiterals);
 260   StatisticsRegistry::unregisterStat(&d_statLearntsLiterals);
 261   StatisticsRegistry::unregisterStat(&d_statMaxLiterals);
 262   StatisticsRegistry::unregisterStat(&d_statTotLiterals);
 263   StatisticsRegistry::unregisterStat(&d_statEliminatedVars);
 264   StatisticsRegistry::unregisterStat(&d_statCallsToSolve);
 265   StatisticsRegistry::unregisterStat(&d_statSolveTime);
 266 }
 267
 268 void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
 269   if (!d_registerStats)
 270     return;
 271
 272   d_statStarts.setData(minisat->starts);
 273   d_statDecisions.setData(minisat->decisions);
 274   d_statRndDecisions.setData(minisat->rnd_decisions);
 275   d_statPropagations.setData(minisat->propagations);
 276   d_statConflicts.setData(minisat->conflicts);
 277   d_statClausesLiterals.setData(minisat->clauses_literals);
 278   d_statLearntsLiterals.setData(minisat->learnts_literals);
 279   d_statMaxLiterals.setData(minisat->max_literals);
 280   d_statTotLiterals.setData(minisat->tot_literals);
 281   d_statEliminatedVars.setData(minisat->eliminated_vars);
 282 }