src/theory/bv/bitblast/proof_bitblaster.h

   1 /*********************                                                        */
   2 /*! \file proof_bitblaster.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   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.\endverbatim
  11  **
  12  ** \brief A bit-blaster wrapper around BBSimple for proof logging.
  13  **/
  14 #include "cvc4_private.h"
  15
  16 #ifndef CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
  17 #define CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
  18
  19 #include "theory/bv/bitblast/simple_bitblaster.h"
  20
  21 namespace cvc5 {
  22 namespace theory {
  23 namespace bv {
  24
  25 class BBProof
  26 {
  27   using Bits = std::vector<Node>;
  28
  29  public:
  30   BBProof(TheoryState* state);
  31   ~BBProof() = default;
  32
  33   /** Bit-blast atom 'node'. */
  34   void bbAtom(TNode node);
  35   /** Check if atom was already bit-blasted. */
  36   bool hasBBAtom(TNode atom) const;
  37   /** Check if term was already bit-blasted. */
  38   bool hasBBTerm(TNode node) const;
  39   /** Get bit-blasted node stored for atom. */
  40   Node getStoredBBAtom(TNode node);
  41   /** Collect model values for all relevant terms given in 'relevantTerms'. */
  42   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
  43
  44  private:
  45   std::unique_ptr<BBSimple> d_bb;
  46 };
  47
  48 }  // namespace bv
  49 }  // namespace theory
  50 }  // namespace cvc5
  51 #endif