projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9a939de) | patch
(proof-new) Make proofs in term formula removal term context sensitive (#5008)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Sep 2020 20:53:30 +0000 (15:53 -0500)
committerGitHub <noreply@github.com>
Wed, 9 Sep 2020 20:53:30 +0000 (15:53 -0500)
commit6ed06a895c7e2c5b83c8fd470c1ee4cf42827a7f
treeb8f3866a1862f611246c06c43eb2cbfcdb6c667dtree
parent9a939deab1a788b29b573ae7fb72a6088a1d7edfcommit | diff
(proof-new) Make proofs in term formula removal term context sensitive (#5008)

Previously term formula removal proofs didnt not take the term context into account. This updates it to make use of the term context sensitive support in TConvProofGenerator. More generally, it uses the term context computation as the standard way of caching the results of rewrites in this class (regardless of proofs).
src/smt/term_formula_removal.cpp diff | blob | history
src/smt/term_formula_removal.h diff | blob | history