src/theory/bv/bv_quick_check.cpp

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