1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Mathias Preiner
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * A bit-blaster wrapper around NodeBitblaster for proof logging.
15 #include "cvc5_private.h"
17 #ifndef CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
18 #define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
20 #include "expr/term_context.h"
21 #include "theory/bv/bitblast/node_bitblaster.h"
25 class TConvProofGenerator
;
30 class BBProof
: protected EnvObj
32 using Bits
= std::vector
<Node
>;
37 ProofNodeManager
* pnm
,
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
);
54 TConvProofGenerator
* getProofGenerator();
57 /** Return true if proofs are enabled. */
58 bool isProofsEnabled() const;
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
;
71 bool d_recordFineGrainedProofs
;