src/theory/bv/bv_subtheory_bitblast.cpp

   1 /*********************                                                        */
   2 /*! \file bv_subtheory_bitblast.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Aina Niemetz, Dejan Jovanovic
   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 Algebraic solver.
  13  **
  14  ** Algebraic solver.
  15  **/
  16
  17 #include "theory/bv/bv_subtheory_bitblast.h"
  18
  19 #include "decision/decision_attributes.h"
  20 #include "options/bv_options.h"
  21 #include "options/decision_options.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "theory/bv/abstraction.h"
  24 #include "theory/bv/bitblast/lazy_bitblaster.h"
  25 #include "theory/bv/bv_quick_check.h"
  26 #include "theory/bv/bv_solver_lazy.h"
  27 #include "theory/bv/theory_bv_utils.h"
  28
  29 using namespace std;
  30 using namespace CVC4::context;
  31
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace bv {
  35
  36 BitblastSolver::BitblastSolver(context::Context* c, BVSolverLazy* bv)
  37     : SubtheorySolver(c, bv),
  38       d_bitblaster(new TLazyBitblaster(c, bv, "theory::bv::lazy")),
  39       d_bitblastQueue(c),
  40       d_statistics(),
  41       d_validModelCache(c, true),
  42       d_lemmaAtomsQueue(c),
  43       d_useSatPropagation(options::bitvectorPropagate()),
  44       d_abstractionModule(NULL),
  45       d_quickCheck(),
  46       d_quickXplain()
  47 {
  48   if (options::bitvectorQuickXplain())
  49   {
  50     d_quickCheck.reset(new BVQuickCheck("bb", bv));
  51     d_quickXplain.reset(new QuickXPlain("bb", d_quickCheck.get()));
  52   }
  53 }
  54
  55 BitblastSolver::~BitblastSolver() {}
  56
  57 BitblastSolver::Statistics::Statistics()
  58   : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
  59   , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
  60 {
  61   smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
  62   smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
  63 }
  64 BitblastSolver::Statistics::~Statistics() {
  65   smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
  66   smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas);
  67 }
  68
  69 void BitblastSolver::setAbstraction(AbstractionModule* abs) {
  70   d_abstractionModule = abs;
  71   d_bitblaster->setAbstraction(abs);
  72 }
  73
  74 void BitblastSolver::preRegister(TNode node) {
  75   if ((node.getKind() == kind::EQUAL ||
  76        node.getKind() == kind::BITVECTOR_ULT ||
  77        node.getKind() == kind::BITVECTOR_ULE ||
  78        node.getKind() == kind::BITVECTOR_SLT ||
  79        node.getKind() == kind::BITVECTOR_SLE) &&
  80       !d_bitblaster->hasBBAtom(node)) {
  81     CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer);
  82     d_bitblastQueue.push_back(node);
  83     if ((options::decisionUseWeight() || options::decisionThreshold() != 0) &&
  84         !node.hasAttribute(decision::DecisionWeightAttr())) {
  85       node.setAttribute(decision::DecisionWeightAttr(),computeAtomWeight(node));
  86     }
  87   }
  88 }
  89
  90 uint64_t BitblastSolver::computeAtomWeight(TNode node) {
  91   NodeSet seen;
  92   return d_bitblaster->computeAtomWeight(node, seen);
  93 }
  94
  95 void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
  96   d_bitblaster->explain(literal, assumptions);
  97 }
  98
  99 void BitblastSolver::bitblastQueue() {
 100   while (!d_bitblastQueue.empty()) {
 101     TNode atom = d_bitblastQueue.front();
 102     d_bitblastQueue.pop();
 103     Debug("bv-bitblast-queue") << "BitblastSolver::bitblastQueue (" << atom << ")\n";
 104     if (options::bvAbstraction() &&
 105         d_abstractionModule->isLemmaAtom(atom)) {
 106       // don't bit-blast lemma atoms
 107       continue;
 108     }
 109     if( !utils::isBitblastAtom(atom) ){
 110       continue;
 111     }
 112     Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
 113     {
 114       TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
 115       d_bitblaster->bbAtom(atom);
 116     }
 117   }
 118 }
 119
 120 bool BitblastSolver::check(Theory::Effort e)
 121 {
 122   Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
 123   Assert(options::bitblastMode() == options::BitblastMode::LAZY);
 124
 125   ++(d_statistics.d_numCallstoCheck);
 126
 127   Debug("bv-bitblast-debug") << "...process queue" << std::endl;
 128   //// Lazy bit-blasting
 129   // bit-blast enqueued nodes
 130   bitblastQueue();
 131
 132   // Processing assertions
 133   while (!done())
 134   {
 135     TNode fact = get();
 136     d_validModelCache = false;
 137     Debug("bv-bitblast") << "  fact " << fact << ")\n";
 138
 139     if (options::bvAbstraction())
 140     {
 141       // skip atoms that are the result of abstraction lemmas
 142       if (d_abstractionModule->isLemmaAtom(fact))
 143       {
 144         d_lemmaAtomsQueue.push_back(fact);
 145         continue;
 146       }
 147     }
 148     // skip facts involving integer equalities (from bv2nat)
 149     if (!utils::isBitblastAtom(fact))
 150     {
 151       continue;
 152     }
 153
 154     if (!d_bv->inConflict()
 155         && (!d_bv->wasPropagatedBySubtheory(fact)
 156             || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST))
 157     {
 158       // Some atoms have not been bit-blasted yet
 159       d_bitblaster->bbAtom(fact);
 160       // Assert to sat
 161       bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
 162       if (!ok)
 163       {
 164         std::vector<TNode> conflictAtoms;
 165         d_bitblaster->getConflict(conflictAtoms);
 166         setConflict(utils::mkAnd(conflictAtoms));
 167         return false;
 168       }
 169     }
 170   }
 171
 172   Debug("bv-bitblast-debug") << "...do propagation" << std::endl;
 173   // We need to ensure we are fully propagated, so propagate now
 174   if (d_useSatPropagation)
 175   {
 176     d_bv->spendResource(ResourceManager::Resource::BvPropagationStep);
 177     bool ok = d_bitblaster->propagate();
 178     if (!ok)
 179     {
 180       std::vector<TNode> conflictAtoms;
 181       d_bitblaster->getConflict(conflictAtoms);
 182       setConflict(utils::mkAnd(conflictAtoms));
 183       return false;
 184     }
 185   }
 186
 187   // Solving
 188   Debug("bv-bitblast-debug") << "...do solving" << std::endl;
 189   if (e == Theory::EFFORT_FULL)
 190   {
 191     Assert(!d_bv->inConflict());
 192     Debug("bitvector::bitblaster")
 193         << "BitblastSolver::addAssertions solving. \n";
 194     bool ok = d_bitblaster->solve();
 195     if (!ok)
 196     {
 197       std::vector<TNode> conflictAtoms;
 198       d_bitblaster->getConflict(conflictAtoms);
 199       Node conflict = utils::mkAnd(conflictAtoms);
 200       setConflict(conflict);
 201       return false;
 202     }
 203   }
 204
 205   Debug("bv-bitblast-debug") << "...do abs bb" << std::endl;
 206   if (options::bvAbstraction() && e == Theory::EFFORT_FULL
 207       && d_lemmaAtomsQueue.size())
 208   {
 209     // bit-blast lemma atoms
 210     while (!d_lemmaAtomsQueue.empty())
 211     {
 212       TNode lemma_atom = d_lemmaAtomsQueue.front();
 213       d_lemmaAtomsQueue.pop();
 214       if (!utils::isBitblastAtom(lemma_atom))
 215       {
 216         continue;
 217       }
 218       d_bitblaster->bbAtom(lemma_atom);
 219       // Assert to sat and check for conflicts
 220       bool ok = d_bitblaster->assertToSat(lemma_atom, d_useSatPropagation);
 221       if (!ok)
 222       {
 223         std::vector<TNode> conflictAtoms;
 224         d_bitblaster->getConflict(conflictAtoms);
 225         setConflict(utils::mkAnd(conflictAtoms));
 226         return false;
 227       }
 228     }
 229
 230     Assert(!d_bv->inConflict());
 231     bool ok = d_bitblaster->solve();
 232     if (!ok)
 233     {
 234       std::vector<TNode> conflictAtoms;
 235       d_bitblaster->getConflict(conflictAtoms);
 236       Node conflict = utils::mkAnd(conflictAtoms);
 237       setConflict(conflict);
 238       ++(d_statistics.d_numBBLemmas);
 239       return false;
 240     }
 241   }
 242
 243
 244   return true;
 245 }
 246
 247 EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
 248   return d_bitblaster->getEqualityStatus(a, b);
 249 }
 250
 251 bool BitblastSolver::collectModelValues(TheoryModel* m,
 252                                         const std::set<Node>& termSet)
 253 {
 254   return d_bitblaster->collectModelValues(m, termSet);
 255 }
 256
 257 Node BitblastSolver::getModelValue(TNode node)
 258 {
 259   if (d_bv->d_invalidateModelCache.get()) {
 260     d_bitblaster->invalidateModelCache();
 261   }
 262   d_bv->d_invalidateModelCache.set(false);
 263   Node val = d_bitblaster->getTermModel(node, true);
 264   return val;
 265 }
 266
 267 void BitblastSolver::setConflict(TNode conflict)
 268 {
 269   Node final_conflict = conflict;
 270   if (options::bitvectorQuickXplain() &&
 271       conflict.getKind() == kind::AND) {
 272     // std::cout << "Original conflict " << conflict.getNumChildren() << "\n";
 273     final_conflict = d_quickXplain->minimizeConflict(conflict);
 274     //std::cout << "Minimized conflict " << final_conflict.getNumChildren() << "\n";
 275   }
 276   d_bv->setConflict(final_conflict);
 277 }
 278
 279 }/* namespace CVC4::theory::bv */
 280 }/* namespace CVC4::theory */
 281 }/* namespace CVC4 */