diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-23 16:41:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-23 16:41:59 -0500 |
| commit | feea2d248ebe0c024c9c5ed14a9f0bf34b06c146 (patch) | |
| tree | aa68ad3f8fdd9f0976141bba7e56b86fd7849c0a /contrib | |
| parent | 9b5680a2cb6efd75c7fd1f7784cda2b6e5b98bfd (diff) | |
(proof-new) Updates to proof node manager (#4617)
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.
Diffstat (limited to 'contrib')
0 files changed, 0 insertions, 0 deletions