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