diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-20 14:53:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-20 14:53:07 -0500 |
| commit | a76b222149e828ed0fe7fb6e91684552dc7b64ec (patch) | |
| tree | daed349df6924755c2a1e32d601f03328aa00da7 /src/expr/proof.cpp | |
| parent | ecf3e9c874095e836b5ea4d9bed6b063b2a5f108 (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.
Diffstat (limited to 'src/expr/proof.cpp')
| -rw-r--r-- | src/expr/proof.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 6d2d70543..eff222b92 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -49,7 +49,7 @@ bool CDProof::addStep(Node expected, if (it != d_nodes.end()) { if (!forceOverwrite - && ((*it).second->getId() != PfRule::ASSUME || id == PfRule::ASSUME)) + && ((*it).second->getRule() != PfRule::ASSUME || id == PfRule::ASSUME)) { // we do not overwrite if forceOverwrite is false and the previously // provided step was not an assumption, or if the currently provided step @@ -144,7 +144,7 @@ bool CDProof::addProof(ProofNode* pn, bool forceOverwrite) } // can ensure children at this point bool res = addStep(curFact, - cur->getId(), + cur->getRule(), pexp, cur->getArguments(), true, |