src/theory/bv/bv_solver_bitblast.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner, Gereon Kremer, Andres Noetzli
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Bit-blasting solver that supports multiple SAT backends.
  14  */
  15
  16 #include "theory/bv/bv_solver_bitblast.h"
  17
  18 #include "options/bv_options.h"
  19 #include "prop/sat_solver_factory.h"
  20 #include "smt/smt_statistics_registry.h"
  21 #include "theory/bv/theory_bv.h"
  22 #include "theory/bv/theory_bv_utils.h"
  23 #include "theory/theory_model.h"
  24
  25 namespace cvc5 {
  26 namespace theory {
  27 namespace bv {
  28
  29 /**
  30  * Notifies the BV solver when assertions were reset.
  31  *
  32  * This class is notified after every user-context pop and maintains a flag
  33  * that indicates whether assertions have been reset. If the user-context level
  34  * reaches level 0 it means that the assertions were reset.
  35  */
  36 class NotifyResetAssertions : public context::ContextNotifyObj
  37 {
  38  public:
  39   NotifyResetAssertions(context::Context* c)
  40       : context::ContextNotifyObj(c, false),
  41         d_context(c),
  42         d_doneResetAssertions(false)
  43   {
  44   }
  45
  46   bool doneResetAssertions() { return d_doneResetAssertions; }
  47
  48   void reset() { d_doneResetAssertions = false; }
  49
  50  protected:
  51   void contextNotifyPop() override
  52   {
  53     // If the user-context level reaches 0 it means that reset-assertions was
  54     // called.
  55     if (d_context->getLevel() == 0)
  56     {
  57       d_doneResetAssertions = true;
  58     }
  59   }
  60
  61  private:
  62   /** The user-context. */
  63   context::Context* d_context;
  64
  65   /** Flag to notify whether reset assertions was called. */
  66   bool d_doneResetAssertions;
  67 };
  68
  69 /**
  70  * Bit-blasting registrar.
  71  *
  72  * The CnfStream calls preRegister() if it encounters a theory atom.
  73  * This registrar bit-blasts given atom and remembers which bit-vector atoms
  74  * were bit-blasted.
  75  *
  76  * This registrar is needed when --bitblast=eager is enabled.
  77  */
  78 class BBRegistrar : public prop::Registrar
  79 {
  80  public:
  81   BBRegistrar(NodeBitblaster* bb) : d_bitblaster(bb) {}
  82
  83   void preRegister(Node n) override
  84   {
  85     if (d_registeredAtoms.find(n) != d_registeredAtoms.end())
  86     {
  87       return;
  88     }
  89     /* We are only interested in bit-vector atoms. */
  90     if ((n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
  91         || n.getKind() == kind::BITVECTOR_ULT
  92         || n.getKind() == kind::BITVECTOR_ULE
  93         || n.getKind() == kind::BITVECTOR_SLT
  94         || n.getKind() == kind::BITVECTOR_SLE)
  95     {
  96       d_registeredAtoms.insert(n);
  97       d_bitblaster->bbAtom(n);
  98     }
  99   }
 100
 101   std::unordered_set<TNode>& getRegisteredAtoms() { return d_registeredAtoms; }
 102
 103  private:
 104   /** The bitblaster used. */
 105   NodeBitblaster* d_bitblaster;
 106
 107   /** Stores bit-vector atoms encounterd on preRegister(). */
 108   std::unordered_set<TNode> d_registeredAtoms;
 109 };
 110
 111 BVSolverBitblast::BVSolverBitblast(TheoryState* s,
 112                                    TheoryInferenceManager& inferMgr,
 113                                    ProofNodeManager* pnm)
 114     : BVSolver(*s, inferMgr),
 115       d_bitblaster(new NodeBitblaster(s)),
 116       d_bbRegistrar(new BBRegistrar(d_bitblaster.get())),
 117       d_nullContext(new context::Context()),
 118       d_bbFacts(s->getSatContext()),
 119       d_bbInputFacts(s->getSatContext()),
 120       d_assumptions(s->getSatContext()),
 121       d_assertions(s->getSatContext()),
 122       d_invalidateModelCache(s->getSatContext(), true),
 123       d_inSatMode(s->getSatContext(), false),
 124       d_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
 125                 : nullptr),
 126       d_factLiteralCache(s->getSatContext()),
 127       d_literalFactCache(s->getSatContext()),
 128       d_propagate(options::bitvectorPropagate()),
 129       d_resetNotify(new NotifyResetAssertions(s->getUserContext()))
 130 {
 131   if (pnm != nullptr)
 132   {
 133     d_bvProofChecker.registerTo(pnm->getChecker());
 134   }
 135
 136   initSatSolver();
 137 }
 138
 139 void BVSolverBitblast::postCheck(Theory::Effort level)
 140 {
 141   if (level != Theory::Effort::EFFORT_FULL)
 142   {
 143     /* Do bit-level propagation only if the SAT solver supports it. */
 144     if (!d_propagate || !d_satSolver->setPropagateOnly())
 145     {
 146       return;
 147     }
 148   }
 149
 150   // If we permanently added assertions to the SAT solver and the assertions
 151   // were reset, we have to reset the SAT solver and the CNF stream.
 152   if (options::bvAssertInput() && d_resetNotify->doneResetAssertions())
 153   {
 154     d_satSolver.reset(nullptr);
 155     d_cnfStream.reset(nullptr);
 156     initSatSolver();
 157     d_resetNotify->reset();
 158   }
 159
 160   NodeManager* nm = NodeManager::currentNM();
 161
 162   /* Process input assertions bit-blast queue. */
 163   while (!d_bbInputFacts.empty())
 164   {
 165     Node fact = d_bbInputFacts.front();
 166     d_bbInputFacts.pop();
 167     /* Bit-blast fact and cache literal. */
 168     if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
 169     {
 170       if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
 171       {
 172         handleEagerAtom(fact, true);
 173       }
 174       else
 175       {
 176         d_bitblaster->bbAtom(fact);
 177         Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
 178         d_cnfStream->convertAndAssert(bb_fact, false, false);
 179       }
 180     }
 181     d_assertions.push_back(fact);
 182   }
 183
 184   /* Process bit-blast queue and store SAT literals. */
 185   while (!d_bbFacts.empty())
 186   {
 187     Node fact = d_bbFacts.front();
 188     d_bbFacts.pop();
 189     /* Bit-blast fact and cache literal. */
 190     if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
 191     {
 192       prop::SatLiteral lit;
 193       if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
 194       {
 195         handleEagerAtom(fact, false);
 196         lit = d_cnfStream->getLiteral(fact[0]);
 197       }
 198       else
 199       {
 200         d_bitblaster->bbAtom(fact);
 201         Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
 202         d_cnfStream->ensureLiteral(bb_fact);
 203         lit = d_cnfStream->getLiteral(bb_fact);
 204       }
 205       d_factLiteralCache[fact] = lit;
 206       d_literalFactCache[lit] = fact;
 207     }
 208     d_assumptions.push_back(d_factLiteralCache[fact]);
 209   }
 210
 211   d_invalidateModelCache.set(true);
 212   std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
 213                                             d_assumptions.end());
 214   prop::SatValue val = d_satSolver->solve(assumptions);
 215   d_inSatMode = val == prop::SatValue::SAT_VALUE_TRUE;
 216   Debug("bv-bitblast") << "d_inSatMode: " << d_inSatMode << std::endl;
 217
 218   if (val == prop::SatValue::SAT_VALUE_FALSE)
 219   {
 220     std::vector<prop::SatLiteral> unsat_assumptions;
 221     d_satSolver->getUnsatAssumptions(unsat_assumptions);
 222
 223     Node conflict;
 224     // Unsat assumptions produce conflict.
 225     if (unsat_assumptions.size() > 0)
 226     {
 227       std::vector<Node> conf;
 228       for (const prop::SatLiteral& lit : unsat_assumptions)
 229       {
 230         conf.push_back(d_literalFactCache[lit]);
 231         Debug("bv-bitblast")
 232             << "unsat assumption (" << lit << "): " << conf.back() << std::endl;
 233       }
 234       conflict = nm->mkAnd(conf);
 235     }
 236     else  // Input assertions produce conflict.
 237     {
 238       std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
 239       conflict = nm->mkAnd(assertions);
 240     }
 241     d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT);
 242   }
 243 }
 244
 245 bool BVSolverBitblast::preNotifyFact(
 246     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 247 {
 248   Valuation& val = d_state.getValuation();
 249
 250   /**
 251    * Check whether `fact` is an input assertion on user-level 0.
 252    *
 253    * If this is the case we can assert `fact` to the SAT solver instead of
 254    * using assumptions.
 255    */
 256   if (options::bvAssertInput() && val.isSatLiteral(fact)
 257       && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0)
 258   {
 259     Assert(!val.isDecision(fact));
 260     d_bbInputFacts.push_back(fact);
 261   }
 262   else
 263   {
 264     d_bbFacts.push_back(fact);
 265   }
 266
 267   return false;  // Return false to enable equality engine reasoning in Theory.
 268 }
 269
 270 TrustNode BVSolverBitblast::explain(TNode n)
 271 {
 272   Debug("bv-bitblast") << "explain called on " << n << std::endl;
 273   return d_im.explainLit(n);
 274 }
 275
 276 void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
 277 {
 278   /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
 279    * equalities. As a result, these equalities are not handled by the equality
 280    * engine and terms below these equalities do not appear in `termSet`.
 281    * We need to make sure that we compute model values for all relevant terms
 282    * in BitblastMode::EAGER and therefore add all variables from the
 283    * bit-blaster to `termSet`.
 284    */
 285   if (options::bitblastMode() == options::BitblastMode::EAGER)
 286   {
 287     d_bitblaster->computeRelevantTerms(termSet);
 288   }
 289 }
 290
 291 bool BVSolverBitblast::collectModelValues(TheoryModel* m,
 292                                           const std::set<Node>& termSet)
 293 {
 294   for (const auto& term : termSet)
 295   {
 296     if (!d_bitblaster->isVariable(term))
 297     {
 298       continue;
 299     }
 300
 301     Node value = getValueFromSatSolver(term, true);
 302     Assert(value.isConst());
 303     if (!m->assertEquality(term, value, true))
 304     {
 305       return false;
 306     }
 307   }
 308
 309   // In eager bitblast mode we also have to collect the model values for
 310   // Boolean variables in the CNF stream.
 311   if (options::bitblastMode() == options::BitblastMode::EAGER)
 312   {
 313     NodeManager* nm = NodeManager::currentNM();
 314     std::vector<TNode> vars;
 315     d_cnfStream->getBooleanVariables(vars);
 316     for (TNode var : vars)
 317     {
 318       Assert(d_cnfStream->hasLiteral(var));
 319       prop::SatLiteral bit = d_cnfStream->getLiteral(var);
 320       prop::SatValue value = d_satSolver->value(bit);
 321       Assert(value != prop::SAT_VALUE_UNKNOWN);
 322       if (!m->assertEquality(
 323               var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
 324       {
 325         return false;
 326       }
 327     }
 328   }
 329
 330   return true;
 331 }
 332
 333 EqualityStatus BVSolverBitblast::getEqualityStatus(TNode a, TNode b)
 334 {
 335   Debug("bv-bitblast") << "getEqualityStatus on " << a << " and " << b
 336                        << std::endl;
 337   if (!d_inSatMode)
 338   {
 339     Debug("bv-bitblast") << EQUALITY_UNKNOWN << std::endl;
 340     return EQUALITY_UNKNOWN;
 341   }
 342   Node value_a = getValue(a);
 343   Node value_b = getValue(b);
 344
 345   if (value_a == value_b)
 346   {
 347     Debug("bv-bitblast") << EQUALITY_TRUE_IN_MODEL << std::endl;
 348     return EQUALITY_TRUE_IN_MODEL;
 349   }
 350   Debug("bv-bitblast") << EQUALITY_FALSE_IN_MODEL << std::endl;
 351   return EQUALITY_FALSE_IN_MODEL;
 352 }
 353
 354 void BVSolverBitblast::initSatSolver()
 355 {
 356   switch (options::bvSatSolver())
 357   {
 358     case options::SatSolverMode::CRYPTOMINISAT:
 359       d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
 360           smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
 361       break;
 362     default:
 363       d_satSolver.reset(prop::SatSolverFactory::createCadical(
 364           smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
 365   }
 366   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
 367                                         d_bbRegistrar.get(),
 368                                         d_nullContext.get(),
 369                                         nullptr,
 370                                         smt::currentResourceManager(),
 371                                         prop::FormulaLitPolicy::INTERNAL,
 372                                         "theory::bv::BVSolverBitblast"));
 373 }
 374
 375 Node BVSolverBitblast::getValueFromSatSolver(TNode node, bool initialize)
 376 {
 377   if (node.isConst())
 378   {
 379     return node;
 380   }
 381
 382   if (!d_bitblaster->hasBBTerm(node))
 383   {
 384     return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
 385   }
 386
 387   std::vector<Node> bits;
 388   d_bitblaster->getBBTerm(node, bits);
 389   Integer value(0), one(1), zero(0), bit;
 390   for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
 391   {
 392     if (d_cnfStream->hasLiteral(bits[j]))
 393     {
 394       prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
 395       prop::SatValue val = d_satSolver->modelValue(lit);
 396       bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
 397     }
 398     else
 399     {
 400       if (!initialize) return Node();
 401       bit = zero;
 402     }
 403     value = value * 2 + bit;
 404   }
 405   return utils::mkConst(bits.size(), value);
 406 }
 407
 408 Node BVSolverBitblast::getValue(TNode node)
 409 {
 410   if (d_invalidateModelCache.get())
 411   {
 412     d_modelCache.clear();
 413   }
 414   d_invalidateModelCache.set(false);
 415
 416   std::vector<TNode> visit;
 417
 418   TNode cur;
 419   visit.push_back(node);
 420   do
 421   {
 422     cur = visit.back();
 423     visit.pop_back();
 424
 425     auto it = d_modelCache.find(cur);
 426     if (it != d_modelCache.end() && !it->second.isNull())
 427     {
 428       continue;
 429     }
 430
 431     if (d_bitblaster->hasBBTerm(cur))
 432     {
 433       Node value = getValueFromSatSolver(cur, false);
 434       if (value.isConst())
 435       {
 436         d_modelCache[cur] = value;
 437         continue;
 438       }
 439     }
 440     if (Theory::isLeafOf(cur, theory::THEORY_BV))
 441     {
 442       Node value = getValueFromSatSolver(cur, true);
 443       d_modelCache[cur] = value;
 444       continue;
 445     }
 446
 447     if (it == d_modelCache.end())
 448     {
 449       visit.push_back(cur);
 450       d_modelCache.emplace(cur, Node());
 451       visit.insert(visit.end(), cur.begin(), cur.end());
 452     }
 453     else if (it->second.isNull())
 454     {
 455       NodeBuilder nb(cur.getKind());
 456       if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
 457       {
 458         nb << cur.getOperator();
 459       }
 460
 461       std::unordered_map<Node, Node>::iterator iit;
 462       for (const TNode& child : cur)
 463       {
 464         iit = d_modelCache.find(child);
 465         Assert(iit != d_modelCache.end());
 466         Assert(iit->second.isConst());
 467         nb << iit->second;
 468       }
 469       it->second = Rewriter::rewrite(nb.constructNode());
 470     }
 471   } while (!visit.empty());
 472
 473   auto it = d_modelCache.find(node);
 474   Assert(it != d_modelCache.end());
 475   return it->second;
 476 }
 477
 478 void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
 479 {
 480   Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
 481
 482   if (assertFact)
 483   {
 484     d_cnfStream->convertAndAssert(fact[0], false, false);
 485   }
 486   else
 487   {
 488     d_cnfStream->ensureLiteral(fact[0]);
 489   }
 490
 491   /* convertAndAssert() does not make the connection between the bit-vector
 492    * atom and it's bit-blasted form (it only calls preRegister() from the
 493    * registrar). Thus, we add the equalities now. */
 494   auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
 495   for (auto atom : registeredAtoms)
 496   {
 497     Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
 498     d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
 499   }
 500   // Clear cache since we only need to do this once per bit-blasted atom.
 501   registeredAtoms.clear();
 502 }
 503
 504 }  // namespace bv
 505 }  // namespace theory
 506 }  // namespace cvc5