diff options
Diffstat (limited to 'src/theory/uf/eq_proof.h')
| -rw-r--r-- | src/theory/uf/eq_proof.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h index c396da313..ac440dc84 100644 --- a/src/theory/uf/eq_proof.h +++ b/src/theory/uf/eq_proof.h @@ -116,7 +116,7 @@ class EqProof * Currently the equality engine can represent disequality reasoning in a * rather coarse-grained manner with EqProof. This is always the case when the * transitivity step contains a disequality, (= (= t t') false) or its - * symmetric. + * symmetric, as a premise. * * There are two cases. In the simplest one the general shape of the EqProof * is @@ -180,6 +180,9 @@ class EqProof * EqProof. These are necessary to avoid cyclic proofs, which could be * generated by creating transitivity steps for assumptions (which depend on * themselves). + * @return True if the EqProof transitivity step is in either of the above + * cases, symbolizing that the ProofNode justifying the conclusion has already + * beenproduced. */ bool expandTransitivityForDisequalities( Node conclusion, |