diff options
Diffstat (limited to 'src/expr/proof.cpp')
| -rw-r--r-- | src/expr/proof.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 8ec55d1f5..15e996684 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -381,4 +381,11 @@ bool CDProof::isAssumption(ProofNode* pn) return false; } +bool CDProof::isSame(TNode f, TNode g) +{ + return f == g + || (f.getKind() == EQUAL && g.getKind() == EQUAL && f[0] == g[1] + && f[1] == g[0]); +} + } // namespace CVC4 |