Age | Commit message (Collapse) | Author |
|
|
|
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.
|
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback