src/theory/bv/lazy_bitblaster.cpp

   1 /*********************                                                        */
   2 /*! \file lazy_bitblaster.cpp
   3  ** \verbatim
   4  ** Original author: Liana Hadarean
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Morgan Deters
   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 Bitblaster for the lazy bv solver.
  13  **
  14  ** Bitblaster for the lazy bv solver.
  15  **/
  16
  17 #include "cvc4_private.h"
  18 #include "bitblaster_template.h"
  19 #include "theory_bv_utils.h"
  20 #include "theory/rewriter.h"
  21 #include "prop/cnf_stream.h"
  22 #include "prop/sat_solver.h"
  23 #include "prop/sat_solver_factory.h"
  24 #include "theory/bv/theory_bv.h"
  25 #include "theory/bv/options.h"
  26 #include "theory/theory_model.h"
  27 #include "theory/bv/abstraction.h"
  28
  29 using namespace CVC4;
  30 using namespace CVC4::theory;
  31 using namespace CVC4::theory::bv;
  32
  33
  34 TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const std::string name, bool emptyNotify)
  35   : TBitblaster<Node>()
  36   , d_bv(bv)
  37   , d_ctx(c)
  38   , d_assertedAtoms(new(true) context::CDList<prop::SatLiteral>(c))
  39   , d_explanations(new(true) ExplanationMap(c))
  40   , d_variables()
  41   , d_bbAtoms()
  42   , d_abstraction(NULL)
  43   , d_emptyNotify(emptyNotify)
  44   , d_satSolverFullModel(c, false)
  45   , d_name(name)
  46   , d_statistics(name) {
  47   d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
  48   d_nullRegistrar = new prop::NullRegistrar();
  49   d_nullContext = new context::Context();
  50   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
  51                                            d_nullRegistrar,
  52                                            d_nullContext);
  53
  54   prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
  55     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
  56     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, bv, this);
  57
  58   d_satSolver->setNotify(notify);
  59 }
  60
  61 void TLazyBitblaster::setAbstraction(AbstractionModule* abs) {
  62   d_abstraction = abs;
  63 }
  64
  65 TLazyBitblaster::~TLazyBitblaster() {
  66   delete d_cnfStream;
  67   delete d_nullRegistrar;
  68   delete d_nullContext;
  69   delete d_satSolver;
  70 }
  71
  72
  73 /**
  74  * Bitblasts the atom, assigns it a marker literal, adding it to the SAT solver
  75  * NOTE: duplicate clauses are not detected because of marker literal
  76  * @param node the atom to be bitblasted
  77  *
  78  */
  79 void TLazyBitblaster::bbAtom(TNode node) {
  80   node = node.getKind() == kind::NOT?  node[0] : node;
  81
  82   if (hasBBAtom(node)) {
  83     return;
  84   }
  85
  86   // make sure it is marked as an atom
  87   addAtom(node);
  88
  89   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
  90   ++d_statistics.d_numAtoms;
  91
  92   /// if we are using bit-vector abstraction bit-blast the original interpretation
  93   if (options::bvAbstraction() &&
  94       d_abstraction != NULL &&
  95       d_abstraction->isAbstraction(node)) {
  96     // node must be of the form P(args) = bv1
  97     Node expansion = Rewriter::rewrite(d_abstraction->getInterpretation(node));
  98
  99     Node atom_bb;
 100     if (expansion.getKind() == kind::CONST_BOOLEAN) {
 101       atom_bb = expansion;
 102     } else {
 103       Assert (expansion.getKind() == kind::AND);
 104       std::vector<Node> atoms;
 105       for (unsigned i = 0; i < expansion.getNumChildren(); ++i) {
 106         Node normalized_i = Rewriter::rewrite(expansion[i]);
 107         Node atom_i = normalized_i.getKind() != kind::CONST_BOOLEAN ?
 108           Rewriter::rewrite(d_atomBBStrategies[normalized_i.getKind()](normalized_i, this)) :
 109           normalized_i;
 110         atoms.push_back(atom_i);
 111       }
 112       atom_bb = utils::mkAnd(atoms);
 113     }
 114     Assert (!atom_bb.isNull());
 115     Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
 116     storeBBAtom(node, atom_bb);
 117     d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 118     return;
 119   }
 120
 121   // the bitblasted definition of the atom
 122   Node normalized = Rewriter::rewrite(node);
 123   Node atom_bb = normalized.getKind() != kind::CONST_BOOLEAN ?
 124     Rewriter::rewrite(d_atomBBStrategies[normalized.getKind()](normalized, this)) :
 125     normalized;
 126   // asserting that the atom is true iff the definition holds
 127   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
 128   storeBBAtom(node, atom_bb);
 129   d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 130 }
 131
 132 void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
 133   // no need to store the definition for the lazy bit-blaster
 134   d_bbAtoms.insert(atom);
 135 }
 136
 137 bool TLazyBitblaster::hasBBAtom(TNode atom) const {
 138   return d_bbAtoms.find(atom) != d_bbAtoms.end();
 139 }
 140
 141
 142 void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
 143   Assert(bits.size() == 0);
 144   for (unsigned i = 0; i < utils::getSize(var); ++i) {
 145     bits.push_back(utils::mkBitOf(var, i));
 146   }
 147   d_variables.insert(var);
 148 }
 149
 150 uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
 151   node = node.getKind() == kind::NOT?  node[0] : node;
 152
 153   Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
 154   uint64_t size = utils::numNodes(atom_bb, seen);
 155   return size;
 156 }
 157
 158 // cnf conversion ensures the atom represents itself
 159 Node TLazyBitblaster::getBBAtom(TNode node) const {
 160   return node;
 161 }
 162
 163 void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
 164
 165   if (hasBBTerm(node)) {
 166     getBBTerm(node, bits);
 167     return;
 168   }
 169
 170   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
 171   ++d_statistics.d_numTerms;
 172
 173   d_termBBStrategies[node.getKind()] (node, bits,this);
 174
 175   Assert (bits.size() == utils::getSize(node));
 176
 177   storeBBTerm(node, bits);
 178 }
 179 /// Public methods
 180
 181 void TLazyBitblaster::addAtom(TNode atom) {
 182   d_cnfStream->ensureLiteral(atom);
 183   prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
 184   d_satSolver->addMarkerLiteral(lit);
 185 }
 186
 187 void TLazyBitblaster::explain(TNode atom, std::vector<TNode>& explanation) {
 188   prop::SatLiteral lit = d_cnfStream->getLiteral(atom);
 189
 190   ++(d_statistics.d_numExplainedPropagations);
 191   if (options::bvEagerExplanations()) {
 192     Assert (d_explanations->find(lit) != d_explanations->end());
 193     const std::vector<prop::SatLiteral>& literal_explanation = (*d_explanations)[lit].get();
 194     for (unsigned i = 0; i < literal_explanation.size(); ++i) {
 195       explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
 196     }
 197     return;
 198   }
 199
 200   std::vector<prop::SatLiteral> literal_explanation;
 201   d_satSolver->explain(lit, literal_explanation);
 202   for (unsigned i = 0; i < literal_explanation.size(); ++i) {
 203     explanation.push_back(d_cnfStream->getNode(literal_explanation[i]));
 204   }
 205 }
 206
 207
 208 /*
 209  * Asserts the clauses corresponding to the atom to the Sat Solver
 210  * by turning on the marker literal (i.e. setting it to false)
 211  * @param node the atom to be asserted
 212  *
 213  */
 214
 215 bool TLazyBitblaster::propagate() {
 216   return d_satSolver->propagate() == prop::SAT_VALUE_TRUE;
 217 }
 218
 219 bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
 220   // strip the not
 221   TNode atom;
 222   if (lit.getKind() == kind::NOT) {
 223     atom = lit[0];
 224   } else {
 225     atom = lit;
 226   }
 227
 228   Assert (hasBBAtom(atom));
 229
 230   prop::SatLiteral markerLit = d_cnfStream->getLiteral(atom);
 231
 232   if(lit.getKind() == kind::NOT) {
 233     markerLit = ~markerLit;
 234   }
 235
 236   Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat asserting node: " << atom <<"\n";
 237   Debug("bitvector-bb") << "TheoryBV::TLazyBitblaster::assertToSat with literal:   " << markerLit << "\n";
 238
 239   prop::SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 240
 241   d_assertedAtoms->push_back(markerLit);
 242
 243   return ret == prop::SAT_VALUE_TRUE || ret == prop::SAT_VALUE_UNKNOWN;
 244 }
 245
 246 /**
 247  * Calls the solve method for the Sat Solver.
 248  * passing it the marker literals to be asserted
 249  *
 250  * @return true for sat, and false for unsat
 251  */
 252
 253 bool TLazyBitblaster::solve() {
 254   if (Trace.isOn("bitvector")) {
 255     Trace("bitvector") << "TLazyBitblaster::solve() asserted atoms ";
 256     context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
 257     for (; it != d_assertedAtoms->end(); ++it) {
 258       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
 259     }
 260   }
 261   Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
 262   d_satSolverFullModel.set(true);
 263   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 264 }
 265
 266 prop::SatValue TLazyBitblaster::solveWithBudget(unsigned long budget) {
 267   if (Trace.isOn("bitvector")) {
 268     Trace("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms ";
 269     context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms->begin();
 270     for (; it != d_assertedAtoms->end(); ++it) {
 271       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
 272     }
 273   }
 274   Debug("bitvector") << "TLazyBitblaster::solveWithBudget() asserted atoms " << d_assertedAtoms->size() <<"\n";
 275   return d_satSolver->solve(budget);
 276 }
 277
 278
 279 void TLazyBitblaster::getConflict(std::vector<TNode>& conflict) {
 280   prop::SatClause conflictClause;
 281   d_satSolver->getUnsatCore(conflictClause);
 282
 283   for (unsigned i = 0; i < conflictClause.size(); i++) {
 284     prop::SatLiteral lit = conflictClause[i];
 285     TNode atom = d_cnfStream->getNode(lit);
 286     Node  not_atom;
 287     if (atom.getKind() == kind::NOT) {
 288       not_atom = atom[0];
 289     } else {
 290       not_atom = NodeManager::currentNM()->mkNode(kind::NOT, atom);
 291     }
 292     conflict.push_back(not_atom);
 293   }
 294 }
 295
 296 TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
 297   d_numTermClauses("theory::bv::"+prefix+"::NumberOfTermSatClauses", 0),
 298   d_numAtomClauses("theory::bv::"+prefix+"::NumberOfAtomSatClauses", 0),
 299   d_numTerms("theory::bv::"+prefix+"::NumberOfBitblastedTerms", 0),
 300   d_numAtoms("theory::bv::"+prefix+"::NumberOfBitblastedAtoms", 0),
 301   d_numExplainedPropagations("theory::bv::"+prefix+"::NumberOfExplainedPropagations", 0),
 302   d_numBitblastingPropagations("theory::bv::"+prefix+"::NumberOfBitblastingPropagations", 0),
 303   d_bitblastTimer("theory::bv::"+prefix+"::BitblastTimer")
 304 {
 305   StatisticsRegistry::registerStat(&d_numTermClauses);
 306   StatisticsRegistry::registerStat(&d_numAtomClauses);
 307   StatisticsRegistry::registerStat(&d_numTerms);
 308   StatisticsRegistry::registerStat(&d_numAtoms);
 309   StatisticsRegistry::registerStat(&d_numExplainedPropagations);
 310   StatisticsRegistry::registerStat(&d_numBitblastingPropagations);
 311   StatisticsRegistry::registerStat(&d_bitblastTimer);
 312 }
 313
 314
 315 TLazyBitblaster::Statistics::~Statistics() {
 316   StatisticsRegistry::unregisterStat(&d_numTermClauses);
 317   StatisticsRegistry::unregisterStat(&d_numAtomClauses);
 318   StatisticsRegistry::unregisterStat(&d_numTerms);
 319   StatisticsRegistry::unregisterStat(&d_numAtoms);
 320   StatisticsRegistry::unregisterStat(&d_numExplainedPropagations);
 321   StatisticsRegistry::unregisterStat(&d_numBitblastingPropagations);
 322   StatisticsRegistry::unregisterStat(&d_bitblastTimer);
 323 }
 324
 325 bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
 326   if(options::bvEagerExplanations()) {
 327     // compute explanation
 328     if (d_lazyBB->d_explanations->find(lit) == d_lazyBB->d_explanations->end()) {
 329       std::vector<prop::SatLiteral> literal_explanation;
 330       d_lazyBB->d_satSolver->explain(lit, literal_explanation);
 331       d_lazyBB->d_explanations->insert(lit, literal_explanation);
 332     } else {
 333       // we propagated it at a lower level
 334       return true;
 335     }
 336   }
 337   ++(d_lazyBB->d_statistics.d_numBitblastingPropagations);
 338   TNode atom = d_cnf->getNode(lit);
 339   return d_bv->storePropagation(atom, SUB_BITBLAST);
 340 }
 341
 342 void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
 343   if (clause.size() > 1) {
 344     NodeBuilder<> lemmab(kind::OR);
 345     for (unsigned i = 0; i < clause.size(); ++ i) {
 346       lemmab << d_cnf->getNode(clause[i]);
 347     }
 348     Node lemma = lemmab;
 349     d_bv->d_out->lemma(lemma);
 350   } else {
 351     d_bv->d_out->lemma(d_cnf->getNode(clause[0]));
 352   }
 353 }
 354
 355 void TLazyBitblaster::MinisatNotify::safePoint() {
 356   d_bv->d_out->safePoint();
 357 }
 358
 359
 360 EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) {
 361   Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n";
 362   Debug("bv-equality-status")<< "BVSatSolver has full model? " << d_satSolverFullModel.get() <<"\n";
 363
 364   // First check if it trivially rewrites to false/true
 365   Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b));
 366
 367   if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
 368   if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
 369
 370   if (!d_satSolverFullModel.get())
 371     return theory::EQUALITY_UNKNOWN;
 372
 373   // Check if cache is valid (invalidated in check and pops)
 374   if (d_bv->d_invalidateModelCache.get()) {
 375     invalidateModelCache();
 376   }
 377   d_bv->d_invalidateModelCache.set(false);
 378
 379   Node a_value = getTermModel(a, true);
 380   Node b_value = getTermModel(b, true);
 381
 382   Assert (a_value.isConst() &&
 383           b_value.isConst());
 384
 385   if (a_value == b_value) {
 386     Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n";
 387     return theory::EQUALITY_TRUE_IN_MODEL;
 388   }
 389   Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n";
 390   return theory::EQUALITY_FALSE_IN_MODEL;
 391 }
 392
 393
 394 bool TLazyBitblaster::isSharedTerm(TNode node) {
 395   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end();
 396 }
 397
 398 bool TLazyBitblaster::hasValue(TNode a) {
 399   Assert (hasBBTerm(a));
 400   Bits bits;
 401   getBBTerm(a, bits);
 402   for (int i = bits.size() -1; i >= 0; --i) {
 403     prop::SatValue bit_value;
 404     if (d_cnfStream->hasLiteral(bits[i])) {
 405       prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
 406       bit_value = d_satSolver->value(bit);
 407       if (bit_value ==  prop::SAT_VALUE_UNKNOWN)
 408         return false;
 409     } else {
 410       return false;
 411     }
 412   }
 413   return true;
 414 }
 415 /**
 416  * Returns the value a is currently assigned to in the SAT solver
 417  * or null if the value is completely unassigned.
 418  *
 419  * @param a
 420  * @param fullModel whether to create a "full model," i.e., add
 421  * constants to equivalence classes that don't already have them
 422  *
 423  * @return
 424  */
 425 Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
 426   if (!hasBBTerm(a)) {
 427     return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
 428   }
 429
 430   Bits bits;
 431   getBBTerm(a, bits);
 432   Integer value(0);
 433   for (int i = bits.size() -1; i >= 0; --i) {
 434     prop::SatValue bit_value;
 435     if (d_cnfStream->hasLiteral(bits[i])) {
 436       prop::SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
 437       bit_value = d_satSolver->value(bit);
 438       Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
 439     } else {
 440       if (!fullModel) return Node();
 441       // unconstrained bits default to false
 442       bit_value = prop::SAT_VALUE_FALSE;
 443     }
 444     Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
 445     value = value * 2 + bit_int;
 446   }
 447   return utils::mkConst(BitVector(bits.size(), value));
 448 }
 449
 450 void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
 451   std::set<Node> termSet;
 452   d_bv->computeRelevantTerms(termSet);
 453
 454   for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
 455     TNode var = *it;
 456     // not actually a leaf of the bit-vector theory
 457     if (d_variables.find(var) == d_variables.end())
 458       continue;
 459
 460     Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var));
 461     // only shared terms could not have been bit-blasted
 462     Assert (hasBBTerm(var) || isSharedTerm(var));
 463
 464     Node const_value = getModelFromSatSolver(var, fullModel);
 465     Assert (const_value.isNull() || const_value.isConst());
 466     if(const_value != Node()) {
 467       Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
 468                                << var << " "
 469                                << const_value << "))\n";
 470         m->assertEquality(var, const_value, true);
 471     }
 472   }
 473 }
 474
 475 void TLazyBitblaster::clearSolver() {
 476   Assert (d_ctx->getLevel() == 0);
 477   delete d_satSolver;
 478   delete d_cnfStream;
 479   d_assertedAtoms->deleteSelf();
 480   d_assertedAtoms = new(true) context::CDList<prop::SatLiteral>(d_ctx);
 481   d_explanations->deleteSelf();
 482   d_explanations = new(true) ExplanationMap(d_ctx);
 483   d_bbAtoms.clear();
 484   d_variables.clear();
 485   d_termCache.clear();
 486
 487   // recreate sat solver
 488   d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
 489   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
 490                                            new prop::NullRegistrar(),
 491                                            new context::Context());
 492
 493   prop::BVSatSolverInterface::Notify* notify = d_emptyNotify ?
 494     (prop::BVSatSolverInterface::Notify*) new MinisatEmptyNotify() :
 495     (prop::BVSatSolverInterface::Notify*) new MinisatNotify(d_cnfStream, d_bv, this);
 496   d_satSolver->setNotify(notify);
 497 }