projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 956a2b1) | patch
bv: Do not rewrite below BV leafs in BBProof's TConvProofGenerator. (#6869)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 13 Jul 2021 16:11:33 +0000 (09:11 -0700)
committerGitHub <noreply@github.com>
Tue, 13 Jul 2021 16:11:33 +0000 (16:11 +0000)
commit36d01a7fd74c6dff52bf9dcba490ff7ded29ad5d
treef55ae38faaac751276089c1e3744090a0833b10ftree
parent956a2b1b8a8ef51cd3794dc3ee4887ccf8778e1ecommit | diff
bv: Do not rewrite below BV leafs in BBProof's TConvProofGenerator. (#6869)

Introduces a TermContext class that can be used to skip rewrites below theory leafs. Fixes issues related to bit-vector leafs begin incorrectly rewritten.
src/expr/term_context.cpp diff | blob | history
src/expr/term_context.h diff | blob | history
src/theory/bv/bitblast/proof_bitblaster.cpp diff | blob | history
src/theory/bv/bitblast/proof_bitblaster.h diff | blob | history