projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ecf3e9c) | patch
Add SCOPE proof rule (#4332)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 20 Apr 2020 19:53:07 +0000 (14:53 -0500)
committerGitHub <noreply@github.com>
Mon, 20 Apr 2020 19:53:07 +0000 (14:53 -0500)
commita76b222149e828ed0fe7fb6e91684552dc7b64ec
treedaed349df6924755c2a1e32d601f03328aa00da7tree
parentecf3e9c874095e836b5ea4d9bed6b063b2a5f108commit | diff
Add SCOPE proof rule (#4332)

This rule is dual to ASSUME. It is a way of closing free assumptions to conclude an implication.

It also changes getId -> getRule.
src/expr/proof.cpp diff | blob | history
src/expr/proof_checker.cpp diff | blob | history
src/expr/proof_node.cpp diff | blob | history
src/expr/proof_node.h diff | blob | history
src/expr/proof_rule.cpp diff | blob | history
src/expr/proof_rule.h diff | blob | history