projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9b5680a) | patch
(proof-new) Updates to proof node manager (#4617)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 23 Jun 2020 21:41:59 +0000 (16:41 -0500)
committerGitHub <noreply@github.com>
Tue, 23 Jun 2020 21:41:59 +0000 (16:41 -0500)
commitfeea2d248ebe0c024c9c5ed14a9f0bf34b06c146
treeaa68ad3f8fdd9f0976141bba7e56b86fd7849c0atree
parent9b5680a2cb6efd75c7fd1f7784cda2b6e5b98bfdcommit | 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.
src/expr/proof_node_manager.cpp diff | blob | history
src/expr/proof_node_manager.h diff | blob | history