src/theory/bv/bv_solver_bitblast_internal.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Mathias Preiner, Gereon Kremer, Haniel Barbosa
   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-blast solver that sends bit-blast lemmas directly to the internal
  14  * MiniSat.
  15  */
  16
  17 #include "theory/bv/bv_solver_bitblast_internal.h"
  18
  19 #include "proof/conv_proof_generator.h"
  20 #include "theory/bv/theory_bv.h"
  21 #include "theory/bv/theory_bv_utils.h"
  22 #include "theory/theory_model.h"
  23
  24 namespace cvc5 {
  25 namespace theory {
  26 namespace bv {
  27
  28 /* -------------------------------------------------------------------------- */
  29
  30 namespace {
  31
  32 bool isBVAtom(TNode n)
  33 {
  34   return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector())
  35          || n.getKind() == kind::BITVECTOR_ULT
  36          || n.getKind() == kind::BITVECTOR_ULE
  37          || n.getKind() == kind::BITVECTOR_SLT
  38          || n.getKind() == kind::BITVECTOR_SLE;
  39 }
  40
  41 /* Traverse Boolean nodes and collect BV atoms. */
  42 void collectBVAtoms(TNode n, std::unordered_set<Node>& atoms)
  43 {
  44   std::vector<TNode> visit;
  45   std::unordered_set<TNode> visited;
  46
  47   visit.push_back(n);
  48
  49   do
  50   {
  51     TNode cur = visit.back();
  52     visit.pop_back();
  53
  54     if (visited.find(cur) != visited.end() || !cur.getType().isBoolean())
  55       continue;
  56
  57     visited.insert(cur);
  58     if (isBVAtom(cur))
  59     {
  60       atoms.insert(cur);
  61       continue;
  62     }
  63
  64     visit.insert(visit.end(), cur.begin(), cur.end());
  65   } while (!visit.empty());
  66 }
  67
  68 }  // namespace
  69
  70 BVSolverBitblastInternal::BVSolverBitblastInternal(
  71     TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm)
  72     : BVSolver(*s, inferMgr),
  73       d_pnm(pnm),
  74       d_bitblaster(new BBProof(s, pnm, false))
  75 {
  76 }
  77
  78 void BVSolverBitblastInternal::addBBLemma(TNode fact)
  79 {
  80   if (!d_bitblaster->hasBBAtom(fact))
  81   {
  82     d_bitblaster->bbAtom(fact);
  83   }
  84   NodeManager* nm = NodeManager::currentNM();
  85
  86   Node atom_bb = d_bitblaster->getStoredBBAtom(fact);
  87   Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb);
  88
  89   if (d_pnm == nullptr)
  90   {
  91     d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
  92   }
  93   else
  94   {
  95     TrustNode tlem =
  96         TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
  97     d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA);
  98   }
  99 }
 100
 101 bool BVSolverBitblastInternal::preNotifyFact(
 102     TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
 103 {
 104   if (fact.getKind() == kind::NOT)
 105   {
 106     fact = fact[0];
 107   }
 108
 109   if (isBVAtom(fact))
 110   {
 111     addBBLemma(fact);
 112   }
 113   else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM)
 114   {
 115     TNode n = fact[0];
 116
 117     NodeManager* nm = NodeManager::currentNM();
 118     Node lemma = nm->mkNode(kind::EQUAL, fact, n);
 119
 120     if (d_pnm == nullptr)
 121     {
 122       d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
 123     }
 124     else
 125     {
 126       d_bitblaster->getProofGenerator()->addRewriteStep(
 127           fact, n, PfRule::BV_EAGER_ATOM, {}, {fact});
 128       TrustNode tlem =
 129           TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator());
 130       d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA);
 131     }
 132
 133     std::unordered_set<Node> bv_atoms;
 134     collectBVAtoms(n, bv_atoms);
 135     for (const Node& nn : bv_atoms)
 136     {
 137       addBBLemma(nn);
 138     }
 139   }
 140
 141   return true;
 142 }
 143
 144 bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m,
 145                                                   const std::set<Node>& termSet)
 146 {
 147   return d_bitblaster->collectModelValues(m, termSet);
 148 }
 149
 150 Node BVSolverBitblastInternal::getValue(TNode node, bool initialize)
 151 {
 152   if (node.isConst())
 153   {
 154     return node;
 155   }
 156
 157   if (!d_bitblaster->hasBBTerm(node))
 158   {
 159     return initialize ? utils::mkConst(utils::getSize(node), 0u) : Node();
 160   }
 161
 162   Valuation& val = d_state.getValuation();
 163
 164   std::vector<Node> bits;
 165   d_bitblaster->getBBTerm(node, bits);
 166   Integer value(0), one(1), zero(0), bit;
 167   for (size_t i = 0, size = bits.size(), j = size - 1; i < size; ++i, --j)
 168   {
 169     bool satValue;
 170     if (val.hasSatValue(bits[j], satValue))
 171     {
 172       bit = satValue ? one : zero;
 173     }
 174     else
 175     {
 176       if (!initialize) return Node();
 177       bit = zero;
 178     }
 179     value = value * 2 + bit;
 180   }
 181   return utils::mkConst(bits.size(), value);
 182 }
 183
 184 BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker()
 185 {
 186   return &d_checker;
 187 }
 188
 189 }  // namespace bv
 190 }  // namespace theory
 191 }  // namespace cvc5