diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-07-14 19:19:12 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-15 02:19:12 +0000 |
| commit | d7bb2484436a55c6b2df08bcae7549809e3ad264 (patch) | |
| tree | 034deafe0bfb7241dfef89f4d485f0ad367ed430 /src/theory/bv/bitblast/proof_bitblaster.h | |
| parent | bb6813731ef1059ab38cedcc5af026b6e75bd6be (diff) | |
bv: Rename BBSimple to NodeBitblaster. (#6891)
Diffstat (limited to 'src/theory/bv/bitblast/proof_bitblaster.h')
| -rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index 17be4204c..f6aa71f21 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A bit-blaster wrapper around BBSimple for proof logging. + * A bit-blaster wrapper around NodeBitblaster for proof logging. */ #include "cvc5_private.h" @@ -18,7 +18,7 @@ #define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H #include "expr/term_context.h" -#include "theory/bv/bitblast/simple_bitblaster.h" +#include "theory/bv/bitblast/node_bitblaster.h" namespace cvc5 { @@ -53,7 +53,7 @@ class BBProof bool isProofsEnabled() const; /** The associated simple bit-blaster. */ - std::unique_ptr<BBSimple> d_bb; + std::unique_ptr<NodeBitblaster> d_bb; /** The associated proof node manager. */ ProofNodeManager* d_pnm; /** Term context for d_tcpg to not rewrite below BV leafs. */ |