| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
pipeline (#5136)
This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline.
Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.
|
|
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.
|
