Age | Commit message (Collapse) | Author |
|
This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true.
It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.
|
|
In some cases, a proof generator provided to a LazyCDProof may provide a null proof, which causes a segfault on proof-new currently. This PR makes LazyCDProof robust to this case; nullptr is interpreted as the fact is an assumption.
|
|
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.
|
|
|
|
A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
|
|
mkScope (#5012)
This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases.
A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
|
|
This includes more versions of checking whether a proof node is closed and standardizing output.
|
|
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.
|