projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 87937a8) | patch
[proofs] Consolidate multiple substitutions to single AND proof in trust substitution...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 17 Feb 2022 14:36:32 +0000 (08:36 -0600)
committerGitHub <noreply@github.com>
Thu, 17 Feb 2022 14:36:32 +0000 (11:36 -0300)
commitbb816ef2cb29aaacda9d5f21d15b6fb120a64b19
treeb4d69e0b29d8c47cf504c9fe4ab2854a8b598689tree
parent87937a8e7410d2222d40c209a550abb3f62dc962commit | diff
[proofs] Consolidate multiple substitutions to single AND proof in trust substitution map (#8109)

This ensures that a common proof node is used for a substitution instead of copying its children. This optimization had been noted in a comment but had not yet been enabled.

This should speed up proof reconstruction for substitutions.
src/theory/trust_substitutions.cpp diff | blob | history