| Age | Commit message (Collapse) | Author |
|---|
|
Split proof ensure closed checks to own file
|
|
|
|
This updates the proof node updater with a mergeSubproofs field which automatically merges subproofs in the same SCOPE that prove the same thing. This is currently enabled by default, it is now configurable and disabled by default.
|
|
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating.
This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.
|
|
This includes some changes to proof node updater that are not currently on master.
This includes:
(1) Explicitly passing the result of the current proof node we are updating,
(2) Caching the results of updates based on Node. In other words, proofs (in the same scope) that we have already seen that prove the same thing as the current proof node are reused.
It also enables the compilation of proof post-processor, which was missing on master and makes Rewriter of SmtEngine public which is required for doing so.
|
|
This adds the proof generator for storing proofs of preprocessing. It stores assertions added via preprocessing passes and their rewrites. This utility will eventually live in SmtEngine.
It also adds 2 new proof rules, and fixes an issue in ProofNodeUpdater.
|
|
Adds utility for updating proof nodes. The module for post-processing proof nodes in the SmtEngine for the sake of proof conversion to external formats will build on this utility.
Requires #4617.
|
