Age | Commit message (Collapse) | Author |
|
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 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.
|
|
This will be used for a number of purposes, including tracking proofs for rewriting and preprocessing.
|
|
|
|
This is a core data structure for associating a formula with a proof generator.
|