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
  21 #include "prop/bvminisat/simp/SimpSolver.h"
  22 #include "proof/clause_id.h"
  23 #include "proof/sat_proof.h"
  24 #include "util/statistics_registry.h"
  25
  26 namespace CVC4 {
  27 namespace prop {
  28
  29 BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
  30 : context::ContextNotifyObj(mainSatContext, false),
  31   d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
  32   d_minisatNotify(0),
  33   d_assertionsCount(0),
  34   d_assertionsRealCount(mainSatContext, 0),
  35   d_lastPropagation(mainSatContext, 0),
  36   d_statistics(registry, name)
  37 {
  38   d_statistics.init(d_minisat);
  39 }
  40
  41
  42 BVMinisatSatSolver::~BVMinisatSatSolver() {
  43   delete d_minisat;
  44   delete d_minisatNotify;
  45 }
  46
  47 void BVMinisatSatSolver::setNotify(Notify* notify) {
  48   d_minisatNotify = new MinisatNotify(notify);
  49   d_minisat->setNotify(d_minisatNotify);
  50 }
  51
  52 ClauseId BVMinisatSatSolver::addClause(SatClause& clause,
  53                                        bool removable) {
  54   Debug("sat::minisat") << "Add clause " << clause <<"\n";
  55   BVMinisat::vec<BVMinisat::Lit> minisat_clause;
  56   toMinisatClause(clause, minisat_clause);
  57   // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
  58   //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
  59   // }
  60   ClauseId clause_id = ClauseIdError;
  61   d_minisat->addClause(minisat_clause, clause_id);
  62   THEORY_PROOF(Assert (clause_id != ClauseIdError););
  63   return clause_id;
  64 }
  65
  66 SatValue BVMinisatSatSolver::propagate() {
  67   return toSatLiteralValue(d_minisat->propagateAssumptions());
  68 }
  69
  70 void BVMinisatSatSolver::addMarkerLiteral(SatLiteral lit) {
  71   d_minisat->addMarkerLiteral(BVMinisat::var(toMinisatLit(lit)));
  72   markUnremovable(lit);
  73 }
  74
  75 void BVMinisatSatSolver::explain(SatLiteral lit, std::vector<SatLiteral>& explanation) {
  76   std::vector<BVMinisat::Lit> minisat_explanation;
  77   d_minisat->explain(toMinisatLit(lit), minisat_explanation);
  78   for (unsigned i = 0; i < minisat_explanation.size(); ++i) {
  79     explanation.push_back(toSatLiteral(minisat_explanation[i]));
  80   }
  81 }
  82
  83 SatValue BVMinisatSatSolver::assertAssumption(SatLiteral lit, bool propagate) {
  84   d_assertionsCount ++;
  85   d_assertionsRealCount = d_assertionsRealCount + 1;
  86   return toSatLiteralValue(d_minisat->assertAssumption(toMinisatLit(lit), propagate));
  87 }
  88
  89 void BVMinisatSatSolver::contextNotifyPop() {
  90   while (d_assertionsCount > d_assertionsRealCount) {
  91     popAssumption();
  92     d_assertionsCount --;
  93   }
  94 }
  95
  96 void BVMinisatSatSolver::popAssumption() {
  97   d_minisat->popAssumption();
  98 }
  99
 100 void BVMinisatSatSolver::setProofLog( BitVectorProof * bvp ) {
 101   d_minisat->setProofLog( bvp );
 102 }
 103
 104 SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
 105   return d_minisat->newVar(true, true, !canErase);
 106 }
 107
 108 void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
 109   d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
 110 }
 111
 112
 113 void BVMinisatSatSolver::interrupt(){
 114   d_minisat->interrupt();
 115 }
 116
 117 SatValue BVMinisatSatSolver::solve(){
 118   ++d_statistics.d_statCallsToSolve;
 119   return toSatLiteralValue(d_minisat->solve());
 120 }
 121
 122 SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
 123   Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl;
 124   ++d_statistics.d_statCallsToSolve;
 125   if(resource == 0) {
 126     d_minisat->budgetOff();
 127   } else {
 128     d_minisat->setConfBudget(resource);
 129   }
 130   //  BVMinisat::vec<BVMinisat::Lit> empty;
 131   unsigned long conflictsBefore = d_minisat->conflicts;
 132   SatValue result = toSatLiteralValue(d_minisat->solveLimited());
 133   d_minisat->clearInterrupt();
 134   resource = d_minisat->conflicts - conflictsBefore;
 135   Trace("limit") << "<MinisatSatSolver::solve(): it took " << resource << " conflicts" << std::endl;
 136   return result;
 137 }
 138
 139 bool BVMinisatSatSolver::ok() const {
 140   return d_minisat->okay();
 141 }
 142
 143 void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
 144   // TODO add assertion to check the call was after an unsat call
 145   for (int i = 0; i < d_minisat->conflict.size(); ++i) {
 146     unsatCore.push_back(toSatLiteral(d_minisat->conflict[i]));
 147   }
 148 }
 149
 150 SatValue BVMinisatSatSolver::value(SatLiteral l){
 151         return toSatLiteralValue(d_minisat->value(toMinisatLit(l)));
 152 }
 153
 154 SatValue BVMinisatSatSolver::modelValue(SatLiteral l){
 155         return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l)));
 156 }
 157
 158 void BVMinisatSatSolver::unregisterVar(SatLiteral lit) {
 159   // this should only be called when user context is implemented
 160   // in the BVSatSolver
 161   Unreachable();
 162 }
 163
 164 void BVMinisatSatSolver::renewVar(SatLiteral lit, int level) {
 165   // this should only be called when user context is implemented
 166   // in the BVSatSolver
 167
 168   Unreachable();
 169 }
 170
 171 unsigned BVMinisatSatSolver::getAssertionLevel() const {
 172   // we have no user context implemented so far
 173   return 0;
 174 }
 175
 176 // converting from internal Minisat representation
 177
 178 SatVariable BVMinisatSatSolver::toSatVariable(BVMinisat::Var var) {
 179   if (var == var_Undef) {
 180     return undefSatVariable;
 181   }
 182   return SatVariable(var);
 183 }
 184
 185 BVMinisat::Lit BVMinisatSatSolver::toMinisatLit(SatLiteral lit) {
 186   if (lit == undefSatLiteral) {
 187     return BVMinisat::lit_Undef;
 188   }
 189   return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated());
 190 }
 191
 192 SatLiteral BVMinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) {
 193   if (lit == BVMinisat::lit_Undef) {
 194     return undefSatLiteral;
 195   }
 196
 197   return SatLiteral(SatVariable(BVMinisat::var(lit)),
 198                     BVMinisat::sign(lit));
 199 }
 200
 201 SatValue BVMinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) {
 202   if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE;
 203   if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN;
 204   Assert(res == (BVMinisat::lbool((uint8_t)1)));
 205   return SAT_VALUE_FALSE;
 206 }
 207
 208 void BVMinisatSatSolver::toMinisatClause(SatClause& clause,
 209                                            BVMinisat::vec<BVMinisat::Lit>& minisat_clause) {
 210   for (unsigned i = 0; i < clause.size(); ++i) {
 211     minisat_clause.push(toMinisatLit(clause[i]));
 212   }
 213   Assert(clause.size() == (unsigned)minisat_clause.size());
 214 }
 215
 216 void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause,
 217                                      SatClause& sat_clause) {
 218   for (int i = 0; i < clause.size(); ++i) {
 219     sat_clause.push_back(toSatLiteral(clause[i]));
 220   }
 221   Assert((unsigned)clause.size() == sat_clause.size());
 222 }
 223
 224
 225 // Satistics for BVMinisatSatSolver
 226
 227 BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry, const std::string& prefix)
 228     : d_registry(registry),
 229       d_statStarts("theory::bv::"+prefix+"bvminisat::starts"),
 230       d_statDecisions("theory::bv::"+prefix+"bvminisat::decisions"),
 231       d_statRndDecisions("theory::bv::"+prefix+"bvminisat::rnd_decisions"),
 232       d_statPropagations("theory::bv::"+prefix+"bvminisat::propagations"),
 233       d_statConflicts("theory::bv::"+prefix+"bvminisat::conflicts"),
 234       d_statClausesLiterals("theory::bv::"+prefix+"bvminisat::clauses_literals"),
 235       d_statLearntsLiterals("theory::bv::"+prefix+"bvminisat::learnts_literals"),
 236       d_statMaxLiterals("theory::bv::"+prefix+"bvminisat::max_literals"),
 237       d_statTotLiterals("theory::bv::"+prefix+"bvminisat::tot_literals"),
 238       d_statEliminatedVars("theory::bv::"+prefix+"bvminisat::eliminated_vars"),
 239       d_statCallsToSolve("theory::bv::"+prefix+"bvminisat::calls_to_solve", 0),
 240       d_statSolveTime("theory::bv::"+prefix+"bvminisat::solve_time", 0),
 241       d_registerStats(!prefix.empty())
 242 {
 243   if (!d_registerStats){
 244     return;
 245   }
 246
 247   d_registry->registerStat(&d_statStarts);
 248   d_registry->registerStat(&d_statDecisions);
 249   d_registry->registerStat(&d_statRndDecisions);
 250   d_registry->registerStat(&d_statPropagations);
 251   d_registry->registerStat(&d_statConflicts);
 252   d_registry->registerStat(&d_statClausesLiterals);
 253   d_registry->registerStat(&d_statLearntsLiterals);
 254   d_registry->registerStat(&d_statMaxLiterals);
 255   d_registry->registerStat(&d_statTotLiterals);
 256   d_registry->registerStat(&d_statEliminatedVars);
 257   d_registry->registerStat(&d_statCallsToSolve);
 258   d_registry->registerStat(&d_statSolveTime);
 259 }
 260
 261 BVMinisatSatSolver::Statistics::~Statistics() {
 262   if (!d_registerStats){
 263     return;
 264   }
 265   d_registry->unregisterStat(&d_statStarts);
 266   d_registry->unregisterStat(&d_statDecisions);
 267   d_registry->unregisterStat(&d_statRndDecisions);
 268   d_registry->unregisterStat(&d_statPropagations);
 269   d_registry->unregisterStat(&d_statConflicts);
 270   d_registry->unregisterStat(&d_statClausesLiterals);
 271   d_registry->unregisterStat(&d_statLearntsLiterals);
 272   d_registry->unregisterStat(&d_statMaxLiterals);
 273   d_registry->unregisterStat(&d_statTotLiterals);
 274   d_registry->unregisterStat(&d_statEliminatedVars);
 275   d_registry->unregisterStat(&d_statCallsToSolve);
 276   d_registry->unregisterStat(&d_statSolveTime);
 277 }
 278
 279 void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
 280   if (!d_registerStats){
 281     return;
 282   }
 283
 284   d_statStarts.setData(minisat->starts);
 285   d_statDecisions.setData(minisat->decisions);
 286   d_statRndDecisions.setData(minisat->rnd_decisions);
 287   d_statPropagations.setData(minisat->propagations);
 288   d_statConflicts.setData(minisat->conflicts);
 289   d_statClausesLiterals.setData(minisat->clauses_literals);
 290   d_statLearntsLiterals.setData(minisat->learnts_literals);
 291   d_statMaxLiterals.setData(minisat->max_literals);
 292   d_statTotLiterals.setData(minisat->tot_literals);
 293   d_statEliminatedVars.setData(minisat->eliminated_vars);
 294 }
 295
 296 } /* namespace CVC4::prop */
 297 } /* namespace CVC4 */
 298
 299 namespace CVC4 {
 300 template<>
 301 prop::SatLiteral toSatLiteral< BVMinisat::Solver>(BVMinisat::Solver::TLit lit) {
 302   return prop::BVMinisatSatSolver::toSatLiteral(lit);
 303 }
 304
 305 template<>
 306 void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl,
 307                                         prop::SatClause& sat_cl) {
 308   prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl);
 309 }
 310
 311 }