src/theory/bv/bv_quick_check.cpp

   1 /*********************                                                        */
   2 /*! \file bv_quick_check.cpp
   3  ** \verbatim
   4  ** Original author: Liana Hadarean
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Wrapper around the SAT solver used for bitblasting.
  13  **
  14  ** Wrapper around the SAT solver used for bitblasting.
  15  **/
  16
  17 #include "theory/bv/bv_quick_check.h"
  18 #include "theory/bv/theory_bv_utils.h"
  19
  20 #include "theory/bv/bitblaster_template.h"
  21
  22 using namespace CVC4;
  23 using namespace CVC4::theory;
  24 using namespace CVC4::theory::bv;
  25 using namespace CVC4::prop;
  26
  27 BVQuickCheck::BVQuickCheck(const std::string& name, theory::bv::TheoryBV* bv)
  28   : d_ctx(new context::Context())
  29   , d_bitblaster(new TLazyBitblaster(d_ctx, bv, name, true))
  30   , d_conflict()
  31   , d_inConflict(d_ctx, false)
  32 {}
  33
  34
  35 bool BVQuickCheck::inConflict() { return d_inConflict.get(); }
  36
  37 uint64_t BVQuickCheck::computeAtomWeight(TNode node, NodeSet& seen) {
  38   return d_bitblaster->computeAtomWeight(node, seen);
  39 }
  40
  41 void BVQuickCheck::setConflict() {
  42   Assert (!inConflict());
  43   std::vector<TNode> conflict;
  44   d_bitblaster->getConflict(conflict);
  45   Node confl = utils::mkConjunction(conflict);
  46   d_inConflict = true;
  47   d_conflict = confl;
  48 }
  49
  50 prop::SatValue BVQuickCheck::checkSat(std::vector<Node>& assumptions, unsigned long budget) {
  51   Node conflict;
  52
  53   for (unsigned i = 0; i < assumptions.size(); ++i) {
  54     TNode a = assumptions[i];
  55     Assert (a.getType().isBoolean());
  56     d_bitblaster->bbAtom(a);
  57     bool ok = d_bitblaster->assertToSat(a, false);
  58     if (!ok) {
  59       setConflict();
  60       return SAT_VALUE_FALSE;
  61     }
  62   }
  63
  64   if (budget == 0) {
  65     bool ok = d_bitblaster->propagate();
  66     if (!ok) {
  67       setConflict();
  68       return SAT_VALUE_FALSE;
  69     }
  70     return SAT_VALUE_UNKNOWN; // could check if assignment is full and return SAT_VALUE_TRUE
  71   }
  72
  73   prop::SatValue res = d_bitblaster->solveWithBudget(budget);
  74   if (res == SAT_VALUE_FALSE) {
  75     setConflict();
  76     return res;
  77   }
  78   // could be unknown or could be sat
  79    return res;
  80 }
  81
  82 prop::SatValue BVQuickCheck::checkSat(unsigned long budget) {
  83   prop::SatValue res = d_bitblaster->solveWithBudget(budget);
  84   if (res == SAT_VALUE_FALSE) {
  85     setConflict();
  86   }
  87   return res;
  88 }
  89
  90 bool BVQuickCheck::addAssertion(TNode assertion) {
  91   Assert (assertion.getType().isBoolean());
  92   d_bitblaster->bbAtom(assertion);
  93   // assert to sat solver and run bcp to detect easy conflicts
  94   bool ok = d_bitblaster->assertToSat(assertion, true);
  95   if (!ok) {
  96     setConflict();
  97   }
  98   return ok;
  99 }
 100
 101
 102 void BVQuickCheck::push() {
 103   d_ctx->push();
 104 }
 105
 106 void BVQuickCheck::pop() {
 107   d_ctx->pop();
 108 }
 109
 110 BVQuickCheck::vars_iterator BVQuickCheck::beginVars() {
 111   return d_bitblaster->beginVars();
 112 }
 113 BVQuickCheck::vars_iterator BVQuickCheck::endVars() {
 114   return d_bitblaster->endVars();
 115 }
 116
 117 Node BVQuickCheck::getVarValue(TNode var) {
 118   return d_bitblaster->getVarValue(var);
 119 }
 120
 121
 122 /**
 123  * Constructs a new sat solver which requires throwing out the atomBBCache
 124  * but keeps all the termBBCache
 125  *
 126  */
 127 void BVQuickCheck::clearSolver() {
 128   popToZero();
 129   d_bitblaster->clearSolver();
 130 }
 131
 132 void BVQuickCheck::popToZero() {
 133   while (d_ctx->getLevel() > 0) {
 134     d_ctx->pop();
 135   }
 136 }
 137
 138 void BVQuickCheck::collectModelInfo(theory::TheoryModel* model, bool fullModel) {
 139   d_bitblaster->collectModelInfo(model, fullModel);
 140 }
 141
 142 BVQuickCheck::~BVQuickCheck() {
 143   delete d_bitblaster;
 144 }
 145
 146 QuickXPlain::QuickXPlain(const std::string& name, BVQuickCheck* solver, unsigned long budget)
 147   : d_solver(solver)
 148   , d_budget(budget)
 149   , d_numCalled(0)
 150   , d_minRatioSum(0)
 151   , d_numConflicts(0)
 152   , d_period(20)
 153   , d_thresh(0.7)
 154   , d_hardThresh(0.9)
 155   , d_statistics(name)
 156 {}
 157 QuickXPlain::~QuickXPlain() {}
 158
 159 unsigned QuickXPlain::selectUnsatCore(unsigned low, unsigned high,
 160                                       std::vector<TNode>& conflict) {
 161
 162   Assert(!d_solver->getConflict().isNull() &&
 163          d_solver->inConflict());
 164   Node query_confl = d_solver->getConflict();
 165
 166   // conflict wasn't actually minimized
 167   if (query_confl.getNumChildren() == high - low + 1) {
 168     return high;
 169   }
 170
 171   TNodeSet nodes;
 172   for (unsigned i = low; i <= high; i++) {
 173     nodes.insert(conflict[i]);
 174   }
 175
 176   unsigned write = low;
 177   for (unsigned i = 0; i < query_confl.getNumChildren(); ++i) {
 178     TNode current = query_confl[i];
 179     // the conflict can have nodes in lower decision levels
 180     if (nodes.find(current) != nodes.end()) {
 181       conflict[write++] = current;
 182       nodes.erase(nodes.find(current));
 183     }
 184   }
 185   // if all of the nodes in the conflict were on a lower level
 186   if (write == low) {
 187     return low;
 188   }
 189   Assert (write != 0);
 190   unsigned new_high = write - 1;
 191
 192   for (TNodeSet::const_iterator it = nodes.begin(); it != nodes.end(); ++it) {
 193     conflict[write++] = *it;
 194   }
 195   Assert (write -1 == high);
 196   Assert (new_high <= high);
 197
 198   return new_high;
 199 }
 200
 201 void QuickXPlain::minimizeConflictInternal(unsigned low, unsigned high,
 202                                            std::vector<TNode>& conflict,
 203                                            std::vector<TNode>& new_conflict) {
 204
 205   Assert (low <= high && high < conflict.size());
 206
 207   if (low == high) {
 208     new_conflict.push_back(conflict[low]);
 209     return;
 210   }
 211
 212   // check if top half is unsat
 213   unsigned new_low = (high - low + 1)/ 2 + low;
 214   d_solver->push();
 215
 216   for (unsigned i = new_low; i <=high; ++i) {
 217     bool ok = d_solver->addAssertion(conflict[i]);
 218     if (!ok) {
 219       unsigned top = selectUnsatCore(new_low, i, conflict);
 220       d_solver->pop();
 221       minimizeConflictInternal(new_low, top, conflict, new_conflict);
 222       return;
 223     }
 224   }
 225
 226   SatValue res = d_solver->checkSat(d_budget);
 227
 228   if (res == SAT_VALUE_UNKNOWN) {
 229     ++(d_statistics.d_numUnknown);
 230   } else {
 231     ++(d_statistics.d_numSolved);
 232   }
 233
 234   if (res == SAT_VALUE_FALSE) {
 235     unsigned top = selectUnsatCore(new_low, high, conflict);
 236     d_solver->pop();
 237     minimizeConflictInternal(new_low, top, conflict, new_conflict);
 238     return;
 239   }
 240
 241   d_solver->pop();
 242   unsigned new_high = new_low - 1;
 243   d_solver->push();
 244
 245   // check bottom half
 246   for (unsigned i = low; i <= new_high; ++i) {
 247     bool ok = d_solver->addAssertion(conflict[i]);
 248     if (!ok) {
 249       unsigned top = selectUnsatCore(low, i, conflict);
 250       d_solver->pop();
 251       minimizeConflictInternal(low, top, conflict, new_conflict);
 252       return;
 253     }
 254   }
 255
 256   res = d_solver->checkSat(d_budget);
 257
 258   if (res == SAT_VALUE_UNKNOWN) {
 259     ++(d_statistics.d_numUnknown);
 260   } else {
 261     ++(d_statistics.d_numSolved);
 262   }
 263
 264   if (res == SAT_VALUE_FALSE) {
 265     unsigned top = selectUnsatCore(low, new_high, conflict);
 266     d_solver->pop();
 267     minimizeConflictInternal(low, top, conflict, new_conflict);
 268     return;
 269   }
 270
 271   // conflict (probably) contains literals in both halves
 272   // keep bottom half in context (no pop)
 273   minimizeConflictInternal(new_low, high, conflict, new_conflict);
 274   d_solver->pop();
 275   d_solver->push();
 276   for (unsigned i = 0; i < new_conflict.size(); ++i) {
 277     bool ok = d_solver->addAssertion(new_conflict[i]);
 278     if (!ok) {
 279       ++(d_statistics.d_numUnknownWasUnsat);
 280       d_solver->pop();
 281       return;
 282     }
 283   }
 284   minimizeConflictInternal(low, new_high, conflict, new_conflict);
 285   d_solver->pop();
 286 }
 287
 288
 289 bool QuickXPlain::useHeuristic() {
 290   return true;
 291   // d_statistics.d_finalPeriod.setData(d_period);
 292   // // try to minimize conflict periodically
 293   // if (d_numConflicts % d_period == 0)
 294   //   return true;
 295
 296   // if (d_numCalled == 0) {
 297   //   return true;
 298   // }
 299
 300   // if (d_minRatioSum / d_numCalled >= d_thresh &&
 301   //     d_numCalled <= 20 ) {
 302   //   return false;
 303   // }
 304
 305   // if (d_minRatioSum / d_numCalled >= d_hardThresh) {
 306   //   return false;
 307   // }
 308
 309   // return true;
 310 }
 311
 312 Node QuickXPlain::minimizeConflict(TNode confl) {
 313   ++d_numConflicts;
 314
 315   if (!useHeuristic()) {
 316     return confl;
 317   }
 318
 319   ++d_numCalled;
 320   ++(d_statistics.d_numConflictsMinimized);
 321   TimerStat::CodeTimer xplainTimer(d_statistics.d_xplainTime);
 322   Assert (confl.getNumChildren() > 2);
 323   std::vector<TNode> conflict;
 324   for (unsigned i = 0; i < confl.getNumChildren(); ++i) {
 325     conflict.push_back(confl[i]);
 326   }
 327   d_solver->popToZero();
 328   std::vector<TNode> minimized;
 329   minimizeConflictInternal(0, conflict.size() - 1, conflict, minimized);
 330
 331   double minimization_ratio = ((double) minimized.size())/confl.getNumChildren();
 332   d_minRatioSum+= minimization_ratio;
 333
 334
 335   // if (minimization_ratio >= d_hardThresh) {
 336   //   d_period = d_period * 5;
 337   // }
 338
 339   // if (minimization_ratio <= d_thresh && d_period >= 40) {
 340   //   d_period = d_period *0.5;
 341   // }
 342
 343   // if (1.5* d_statistics.d_numUnknown.getData() > d_statistics.d_numSolved.getData()) {
 344   //   d_period = d_period * 2;
 345   // }
 346   d_statistics.d_avgMinimizationRatio.addEntry(minimization_ratio);
 347   return utils::mkAnd(minimized);
 348 }
 349
 350 QuickXPlain::Statistics::Statistics(const std::string& name)
 351   : d_xplainTime("theory::bv::"+name+"::QuickXplain::Time")
 352   , d_numSolved("theory::bv::"+name+"::QuickXplain::NumSolved", 0)
 353   , d_numUnknown("theory::bv::"+name+"::QuickXplain::NumUnknown", 0)
 354   , d_numUnknownWasUnsat("theory::bv::"+name+"::QuickXplain::NumUnknownWasUnsat", 0)
 355   , d_numConflictsMinimized("theory::bv::"+name+"::QuickXplain::NumConflictsMinimized", 0)
 356   , d_finalPeriod("theory::bv::"+name+"::QuickXplain::FinalPeriod", 0)
 357   , d_avgMinimizationRatio("theory::bv::"+name+"::QuickXplain::AvgMinRatio")
 358 {
 359   StatisticsRegistry::registerStat(&d_xplainTime);
 360   StatisticsRegistry::registerStat(&d_numSolved);
 361   StatisticsRegistry::registerStat(&d_numUnknown);
 362   StatisticsRegistry::registerStat(&d_numUnknownWasUnsat);
 363   StatisticsRegistry::registerStat(&d_numConflictsMinimized);
 364   StatisticsRegistry::registerStat(&d_finalPeriod);
 365   StatisticsRegistry::registerStat(&d_avgMinimizationRatio);
 366 }
 367
 368 QuickXPlain::Statistics::~Statistics() {
 369   StatisticsRegistry::unregisterStat(&d_xplainTime);
 370   StatisticsRegistry::unregisterStat(&d_numSolved);
 371   StatisticsRegistry::unregisterStat(&d_numUnknown);
 372   StatisticsRegistry::unregisterStat(&d_numUnknownWasUnsat);
 373   StatisticsRegistry::unregisterStat(&d_numConflictsMinimized);
 374   StatisticsRegistry::unregisterStat(&d_finalPeriod);
 375   StatisticsRegistry::unregisterStat(&d_avgMinimizationRatio);
 376 }
 377