projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a99f5aa) | patch
(proof-new) Make theory preprocessor user-context dependent (#5296)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 22 Oct 2020 02:21:42 +0000 (21:21 -0500)
committerGitHub <noreply@github.com>
Thu, 22 Oct 2020 02:21:42 +0000 (21:21 -0500)
commit0e7ebfa3ba5d5049c81b2c5ac113af62c35f5c64
treec5a9d62c560592003f9fd0003faece8585c7c30atree
parenta99f5aaa46702a4894aaddeed3a7ff5cbf69bdfdcommit | diff
(proof-new) Make theory preprocessor user-context dependent (#5296)

Previously, theory preprocessing cache was manually cleared whenever the theory preprocess pass was run. However, proofs for theory preprocessing required to be alive for the remainder of the user context. This PR changes theory preprocessing so that both the cache and proofs in theory preprocessing are user-context dependent.

This PR also makes the theory preprocess pass proof producing.
src/preprocessing/passes/theory_preprocess.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/theory_engine.h diff | blob | history
src/theory/theory_preprocessor.cpp diff | blob | history
src/theory/theory_preprocessor.h diff | blob | history