| Age | Commit message (Collapse) | Author |
|---|
|
This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.
|
|
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.
|
|
|
|
Main feature added is the mkScope interface, which is agnostic to symmetry of (dis)equalities.
It also adds a check for cyclic proofs when using the interface ProofNodeManager::updateNode.
Note that an earlier version of this method was agnostics to predicates vs Boolean equality with constants. This is no longer required.
|
|
|
|
This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites.
|
|
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.
|
