src/theory/bv/bitblast/proof_bitblaster.h

   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 NodeBitblaster for proof logging.
  14  */
  15 #include "cvc5_private.h"
  16
  17 #ifndef CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
  18 #define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
  19
  20 #include "expr/term_context.h"
  21 #include "theory/bv/bitblast/node_bitblaster.h"
  22
  23 namespace cvc5 {
  24
  25 class TConvProofGenerator;
  26
  27 namespace theory {
  28 namespace bv {
  29
  30 class BBProof
  31 {
  32   using Bits = std::vector<Node>;
  33
  34  public:
  35   BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained);
  36   ~BBProof();
  37
  38   /** Bit-blast atom 'node'. */
  39   void bbAtom(TNode node);
  40   /** Check if atom was already bit-blasted. */
  41   bool hasBBAtom(TNode atom) const;
  42   /** Check if term was already bit-blasted. */
  43   bool hasBBTerm(TNode node) const;
  44   /** Get bit-blasted node stored for atom. */
  45   Node getStoredBBAtom(TNode node);
  46   /** Get bit-blasted bits stored for node. */
  47   void getBBTerm(TNode node, Bits& bits) const;
  48   /** Collect model values for all relevant terms given in 'relevantTerms'. */
  49   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
  50
  51   TConvProofGenerator* getProofGenerator();
  52
  53  private:
  54   /** Return true if proofs are enabled. */
  55   bool isProofsEnabled() const;
  56
  57   /** The associated simple bit-blaster. */
  58   std::unique_ptr<NodeBitblaster> d_bb;
  59   /** The associated proof node manager. */
  60   ProofNodeManager* d_pnm;
  61   /** Term context for d_tcpg to not rewrite below BV leafs. */
  62   std::unique_ptr<TermContext> d_tcontext;
  63   /** The associated term conversion proof generator. */
  64   std::unique_ptr<TConvProofGenerator> d_tcpg;
  65   /** Map bit-vector nodes to bit-blasted nodes. */
  66   std::unordered_map<Node, Node> d_bbMap;
  67
  68   bool d_recordFineGrainedProofs;
  69 };
  70
  71 }  // namespace bv
  72 }  // namespace theory
  73 }  // namespace cvc5
  74 #endif