src/prop/bvminisat/bvminisat.cpp

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