projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cd7432f) | patch
Make trust substitution map generate proofs lazily (#6379)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 22 Apr 2021 22:53:15 +0000 (17:53 -0500)
committerGitHub <noreply@github.com>
Thu, 22 Apr 2021 22:53:15 +0000 (22:53 +0000)
commitbdc7c89b002ca65af851c226ef1956b1f2526c1d
tree3b84a07db8596faa2d525995a9cc7c538944ec74tree
parentcd7432f10ca15585df81e3ef2d49fcddbfa9c3c8commit | diff
Make trust substitution map generate proofs lazily (#6379)

This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.

This makes the proof generation in trust substitution map lazy.

Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.
src/theory/trust_substitutions.cpp diff | blob | history
src/theory/trust_substitutions.h diff | blob | history