| Age | Commit message (Collapse) | Author |
|---|
|
This improves trace/error messages for proof-new-pedantic, and also merges the proof-new-pedantic-eager with the proof-new-eager-checking option.
|
|
Some of the interfaces in the proof rule checker are unnecessary now and can be deleted.
This also updates STRING_TRUST to have pedantic level 2.
|
|
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 includes support for pedantic levels, as well as a utility for wrapping Kind in a Node (for the updated CONG rule, to be updated in a later PR).
|
|
Previously, the proof rule checkers were run on witness form for convenience. However, it is more flexible for the sake of the internal calculus to run on Skolem forms. The main reason is that the conversion to/from witness form does not preserve terms that contain witness. Our preprocessing steps rely on using witness terms. This design change additionally simplifies a lot of the code of the builtin proof rule checker.
Instead, witness forms can be queried on an as-needed basis, e.g. in MACRO_SR_PRED_TRANSFORM.
|
|
|
|
This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.
This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.
Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.
Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.
|
|
This adds new required features to proof checker and the base class of proof rule checker.
This is required as the first dependency towards merging further infrastructure related to proofs.
|
|
Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure.
ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker).
ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker.
This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.
|
