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