src/theory/bv/bitblast/proof_bitblaster.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Aina Niemetz, Mathias Preiner
   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  * A bit-blaster wrapper around BBSimple for proof logging.
  14  */
  15 #include "theory/bv/bitblast/proof_bitblaster.h"
  16
  17 #include <unordered_set>
  18
  19 #include "proof/conv_proof_generator.h"
  20 #include "theory/theory_model.h"
  21
  22 namespace cvc5 {
  23 namespace theory {
  24 namespace bv {
  25
  26 BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
  27     : d_bb(new NodeBitblaster(state)),
  28       d_pnm(pnm),
  29       d_tcontext(new TheoryLeafTermContext(theory::THEORY_BV)),
  30       d_tcpg(pnm ? new TConvProofGenerator(
  31                  pnm,
  32                  nullptr,
  33                  /* ONCE to visit each term only once, post-order.  FIXPOINT
  34                   * could lead to infinite loops due to terms being rewritten
  35                   * to terms that contain themselves */
  36                  TConvPolicy::ONCE,
  37                  /* STATIC to get the same ProofNode for a shared subterm. */
  38                  TConvCachePolicy::STATIC,
  39                  "BBProof::TConvProofGenerator",
  40                  d_tcontext.get(),
  41                  false)
  42                  : nullptr),
  43       d_recordFineGrainedProofs(fineGrained)
  44 {
  45 }
  46
  47 BBProof::~BBProof() {}
  48
  49 void BBProof::bbAtom(TNode node)
  50 {
  51   std::vector<TNode> visit;
  52   visit.push_back(node);
  53   std::unordered_set<TNode> visited;
  54
  55   bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;
  56
  57   NodeManager* nm = NodeManager::currentNM();
  58
  59   while (!visit.empty())
  60   {
  61     TNode n = visit.back();
  62     if (hasBBAtom(n) || hasBBTerm(n))
  63     {
  64       visit.pop_back();
  65       continue;
  66     }
  67
  68     if (visited.find(n) == visited.end())
  69     {
  70       visited.insert(n);
  71       if (!Theory::isLeafOf(n, theory::THEORY_BV))
  72       {
  73         visit.insert(visit.end(), n.begin(), n.end());
  74       }
  75     }
  76     else
  77     {
  78       if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst())
  79       {
  80         Bits bits;
  81         d_bb->makeVariable(n, bits);
  82         if (fpenabled)
  83         {
  84           Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
  85           d_bbMap.emplace(n, n_tobv);
  86           d_tcpg->addRewriteStep(n,
  87                                  n_tobv,
  88                                  PfRule::BV_BITBLAST_STEP,
  89                                  {},
  90                                  {n.eqNode(n_tobv)},
  91                                  false);
  92         }
  93       }
  94       else if (n.getType().isBitVector())
  95       {
  96         Bits bits;
  97         d_bb->bbTerm(n, bits);
  98         Kind kind = n.getKind();
  99         if (fpenabled)
 100         {
 101           Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits);
 102           d_bbMap.emplace(n, n_tobv);
 103           Node c_tobv;
 104           if (n.isConst())
 105           {
 106             c_tobv = n;
 107           }
 108           else
 109           {
 110             std::vector<Node> children_tobv;
 111             if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
 112             {
 113               children_tobv.push_back(n.getOperator());
 114             }
 115
 116             for (const auto& child : n)
 117             {
 118               children_tobv.push_back(d_bbMap.at(child));
 119             }
 120             c_tobv = nm->mkNode(kind, children_tobv);
 121           }
 122           d_tcpg->addRewriteStep(c_tobv,
 123                                  n_tobv,
 124                                  PfRule::BV_BITBLAST_STEP,
 125                                  {},
 126                                  {c_tobv.eqNode(n_tobv)},
 127                                  false);
 128         }
 129       }
 130       else
 131       {
 132         d_bb->bbAtom(n);
 133         if (fpenabled)
 134         {
 135           Node n_tobv = getStoredBBAtom(n);
 136           std::vector<Node> children_tobv;
 137           for (const auto& child : n)
 138           {
 139             children_tobv.push_back(d_bbMap.at(child));
 140           }
 141           Node c_tobv = nm->mkNode(n.getKind(), children_tobv);
 142           d_tcpg->addRewriteStep(c_tobv,
 143                                  n_tobv,
 144                                  PfRule::BV_BITBLAST_STEP,
 145                                  {},
 146                                  {c_tobv.eqNode(n_tobv)},
 147                                  false);
 148         }
 149       }
 150       visit.pop_back();
 151     }
 152   }
 153   /* Record coarse-grain bit-blast proof step. */
 154   if (isProofsEnabled() && !d_recordFineGrainedProofs)
 155   {
 156     Node node_tobv = getStoredBBAtom(node);
 157     d_tcpg->addRewriteStep(node,
 158                            node_tobv,
 159                            PfRule::BV_BITBLAST,
 160                            {},
 161                            {node.eqNode(node_tobv)},
 162                            false);
 163   }
 164 }
 165
 166 bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); }
 167
 168 bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); }
 169
 170 Node BBProof::getStoredBBAtom(TNode node)
 171 {
 172   return d_bb->getStoredBBAtom(node);
 173 }
 174
 175 bool BBProof::collectModelValues(TheoryModel* m,
 176                                  const std::set<Node>& relevantTerms)
 177 {
 178   return d_bb->collectModelValues(m, relevantTerms);
 179 }
 180
 181 TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); }
 182
 183 bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
 184
 185 }  // namespace bv
 186 }  // namespace theory
 187 }  // namespace cvc5