projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fc9c100) | patch
Make proofs of rewrites robust to use in internal subsolvers (#7411)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Oct 2021 00:35:14 +0000 (19:35 -0500)
committerGitHub <noreply@github.com>
Wed, 20 Oct 2021 00:35:14 +0000 (00:35 +0000)
commitf047038b1bec31a1ebb89e9d35e3aebb3301eddc
tree7ad69087d63811e0138a8e6f08532991a9becbe3tree
parentfc9c1005a398c537bdb491d1b161f3e316b68b5ecommit | diff
Make proofs of rewrites robust to use in internal subsolvers (#7411)

We are currently using an attribute to mark "rewritten with proofs". This is incorrect as attributes are global, but proofs of rewrites are local to the solver instance.

This enables applications of proofs within internal subsolvers, and is required for a new internal fuzzing technique.
src/theory/rewriter.cpp diff | blob | history
src/theory/rewriter.h diff | blob | history