projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d4a23ab) | patch
(proof-new) Implementation of trust substitution (#5276)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 18 Oct 2020 23:01:24 +0000 (18:01 -0500)
committerGitHub <noreply@github.com>
Sun, 18 Oct 2020 23:01:24 +0000 (18:01 -0500)
commit738676c39badd9a03db0feaa00bb4bd467f0600a
treef7a40da5af750815d8a6832c1f6e9c0b4b5b714atree
parentd4a23ab31a6f811dc4a9c3f24acb9a325fcb6d5acommit | diff
(proof-new) Implementation of trust substitution (#5276)

Trust substitution is a data structure that is used throughout preprocessing for proofs.

This adds its implementation.
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history
src/theory/builtin/proof_checker.cpp diff | blob | history
src/theory/trust_substitutions.cpp diff | blob | history
src/theory/trust_substitutions.h diff | blob | history