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_epg(pnm ? new EagerProofGenerator(pnm, s->getUserContext(), "")
 123                 : nullptr),
 124       d_factLiteralCache(s->getSatContext()),
 125       d_literalFactCache(s->getSatContext()),
 126       d_propagate(options::bitvectorPropagate()),
 127       d_resetNotify(new NotifyResetAssertions(s->getUserContext()))
 128 {
 129   if (pnm != nullptr)
 130   {
 131     d_bvProofChecker.registerTo(pnm->getChecker());
 132   }
 133
 134   initSatSolver();
 135 }
 136
 137 void BVSolverBitblast::postCheck(Theory::Effort level)
 138 {
 139   if (level != Theory::Effort::EFFORT_FULL)
 140   {
 141     /* Do bit-level propagation only if the SAT solver supports it. */
 142     if (!d_propagate || !d_satSolver->setPropagateOnly())
 143     {
 144       return;
 145     }
 146   }
 147
 148   // If we permanently added assertions to the SAT solver and the assertions
 149   // were reset, we have to reset the SAT solver and the CNF stream.
 150   if (options::bvAssertInput() && d_resetNotify->doneResetAssertions())
 151   {
 152     d_satSolver.reset(nullptr);
 153     d_cnfStream.reset(nullptr);
 154     initSatSolver();
 155     d_resetNotify->reset();
 156   }
 157
 158   NodeManager* nm = NodeManager::currentNM();
 159
 160   /* Process input assertions bit-blast queue. */
 161   while (!d_bbInputFacts.empty())
 162   {
 163     Node fact = d_bbInputFacts.front();
 164     d_bbInputFacts.pop();
 165     /* Bit-blast fact and cache literal. */
 166     if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
 167     {
 168       if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
 169       {
 170         handleEagerAtom(fact, true);
 171       }
 172       else
 173       {
 174         d_bitblaster->bbAtom(fact);
 175         Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
 176         d_cnfStream->convertAndAssert(bb_fact, false, false);
 177       }
 178     }
 179     d_assertions.push_back(fact);
 180   }
 181
 182   /* Process bit-blast queue and store SAT literals. */
 183   while (!d_bbFacts.empty())
 184   {
 185     Node fact = d_bbFacts.front();
 186     d_bbFacts.pop();
 187     /* Bit-blast fact and cache literal. */
 188     if (d_factLiteralCache.find(fact) == d_factLiteralCache.end())
 189     {
 190       prop::SatLiteral lit;
 191       if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
 192       {
 193         handleEagerAtom(fact, false);
 194         lit = d_cnfStream->getLiteral(fact[0]);
 195       }
 196       else
 197       {
 198         d_bitblaster->bbAtom(fact);
 199         Node bb_fact = d_bitblaster->getStoredBBAtom(fact);
 200         d_cnfStream->ensureLiteral(bb_fact);
 201         lit = d_cnfStream->getLiteral(bb_fact);
 202       }
 203       d_factLiteralCache[fact] = lit;
 204       d_literalFactCache[lit] = fact;
 205     }
 206     d_assumptions.push_back(d_factLiteralCache[fact]);
 207   }
 208
 209   std::vector<prop::SatLiteral> assumptions(d_assumptions.begin(),
 210                                             d_assumptions.end());
 211   prop::SatValue val = d_satSolver->solve(assumptions);
 212
 213   if (val == prop::SatValue::SAT_VALUE_FALSE)
 214   {
 215     std::vector<prop::SatLiteral> unsat_assumptions;
 216     d_satSolver->getUnsatAssumptions(unsat_assumptions);
 217
 218     Node conflict;
 219     // Unsat assumptions produce conflict.
 220     if (unsat_assumptions.size() > 0)
 221     {
 222       std::vector<Node> conf;
 223       for (const prop::SatLiteral& lit : unsat_assumptions)
 224       {
 225         conf.push_back(d_literalFactCache[lit]);
 226         Debug("bv-bitblast")
 227             << "unsat assumption (" << lit << "): " << conf.back() << std::endl;
 228       }
 229       conflict = nm->mkAnd(conf);
 230     }
 231     else  // Input assertions produce conflict.
 232     {
 233       std::vector<Node> assertions(d_assertions.begin(), d_assertions.end());
 234       conflict = nm->mkAnd(assertions);
 235     }
 236     d_im.conflict(conflict, InferenceId::BV_BITBLAST_CONFLICT);
 237   }
 238 }
 239
 240 bool BVSolverBitblast::preNotifyFact(
 241     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 242 {
 243   Valuation& val = d_state.getValuation();
 244
 245   /**
 246    * Check whether `fact` is an input assertion on user-level 0.
 247    *
 248    * If this is the case we can assert `fact` to the SAT solver instead of
 249    * using assumptions.
 250    */
 251   if (options::bvAssertInput() && val.isSatLiteral(fact)
 252       && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0)
 253   {
 254     Assert(!val.isDecision(fact));
 255     d_bbInputFacts.push_back(fact);
 256   }
 257   else
 258   {
 259     d_bbFacts.push_back(fact);
 260   }
 261
 262   return false;  // Return false to enable equality engine reasoning in Theory.
 263 }
 264
 265 TrustNode BVSolverBitblast::explain(TNode n)
 266 {
 267   Debug("bv-bitblast") << "explain called on " << n << std::endl;
 268   return d_im.explainLit(n);
 269 }
 270
 271 void BVSolverBitblast::computeRelevantTerms(std::set<Node>& termSet)
 272 {
 273   /* BITVECTOR_EAGER_ATOM wraps input assertions that may also contain
 274    * equalities. As a result, these equalities are not handled by the equality
 275    * engine and terms below these equalities do not appear in `termSet`.
 276    * We need to make sure that we compute model values for all relevant terms
 277    * in BitblastMode::EAGER and therefore add all variables from the
 278    * bit-blaster to `termSet`.
 279    */
 280   if (options::bitblastMode() == options::BitblastMode::EAGER)
 281   {
 282     d_bitblaster->computeRelevantTerms(termSet);
 283   }
 284 }
 285
 286 bool BVSolverBitblast::collectModelValues(TheoryModel* m,
 287                                           const std::set<Node>& termSet)
 288 {
 289   for (const auto& term : termSet)
 290   {
 291     if (!d_bitblaster->isVariable(term))
 292     {
 293       continue;
 294     }
 295
 296     Node value = getValue(term, true);
 297     Assert(value.isConst());
 298     if (!m->assertEquality(term, value, true))
 299     {
 300       return false;
 301     }
 302   }
 303
 304   // In eager bitblast mode we also have to collect the model values for
 305   // Boolean variables in the CNF stream.
 306   if (options::bitblastMode() == options::BitblastMode::EAGER)
 307   {
 308     NodeManager* nm = NodeManager::currentNM();
 309     std::vector<TNode> vars;
 310     d_cnfStream->getBooleanVariables(vars);
 311     for (TNode var : vars)
 312     {
 313       Assert(d_cnfStream->hasLiteral(var));
 314       prop::SatLiteral bit = d_cnfStream->getLiteral(var);
 315       prop::SatValue value = d_satSolver->value(bit);
 316       Assert(value != prop::SAT_VALUE_UNKNOWN);
 317       if (!m->assertEquality(
 318               var, nm->mkConst(value == prop::SAT_VALUE_TRUE), true))
 319       {
 320         return false;
 321       }
 322     }
 323   }
 324
 325   return true;
 326 }
 327
 328 void BVSolverBitblast::initSatSolver()
 329 {
 330   switch (options::bvSatSolver())
 331   {
 332     case options::SatSolverMode::CRYPTOMINISAT:
 333       d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
 334           smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
 335       break;
 336     default:
 337       d_satSolver.reset(prop::SatSolverFactory::createCadical(
 338           smtStatisticsRegistry(), "theory::bv::BVSolverBitblast::"));
 339   }
 340   d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
 341                                         d_bbRegistrar.get(),
 342                                         d_nullContext.get(),
 343                                         nullptr,
 344                                         smt::currentResourceManager(),
 345                                         prop::FormulaLitPolicy::INTERNAL,
 346                                         "theory::bv::BVSolverBitblast"));
 347 }
 348
 349 Node BVSolverBitblast::getValue(TNode node, bool initialize)
 350 {
 351   if (node.isConst())
 352   {
 353     return node;
 354   }
 355
 356   if (!d_bitblaster->hasBBTerm(node))
 357   {
 358     return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
 359   }
 360
 361   std::vector<Node> bits;
 362   d_bitblaster->getBBTerm(node, bits);
 363   Integer value(0), one(1), zero(0), bit;
 364   for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
 365   {
 366     if (d_cnfStream->hasLiteral(bits[j]))
 367     {
 368       prop::SatLiteral lit = d_cnfStream->getLiteral(bits[j]);
 369       prop::SatValue val = d_satSolver->modelValue(lit);
 370       bit = val == prop::SatValue::SAT_VALUE_TRUE ? one : zero;
 371     }
 372     else
 373     {
 374       if (!initialize) return Node();
 375       bit = zero;
 376     }
 377     value = value * 2 + bit;
 378   }
 379   return utils::mkConst(bits.size(), value);
 380 }
 381
 382 void BVSolverBitblast::handleEagerAtom(TNode fact, bool assertFact)
 383 {
 384   Assert(fact.getKind() == kind::BITVECTOR_EAGER_ATOM);
 385
 386   if (assertFact)
 387   {
 388     d_cnfStream->convertAndAssert(fact[0], false, false);
 389   }
 390   else
 391   {
 392     d_cnfStream->ensureLiteral(fact[0]);
 393   }
 394
 395   /* convertAndAssert() does not make the connection between the bit-vector
 396    * atom and it's bit-blasted form (it only calls preRegister() from the
 397    * registrar). Thus, we add the equalities now. */
 398   auto& registeredAtoms = d_bbRegistrar->getRegisteredAtoms();
 399   for (auto atom : registeredAtoms)
 400   {
 401     Node bb_atom = d_bitblaster->getStoredBBAtom(atom);
 402     d_cnfStream->convertAndAssert(atom.eqNode(bb_atom), false, false);
 403   }
 404   // Clear cache since we only need to do this once per bit-blasted atom.
 405   registeredAtoms.clear();
 406 }
 407
 408 }  // namespace bv
 409 }  // namespace theory
 410 }  // namespace cvc5