diff options
Diffstat (limited to 'src/theory/arith/constraint.h')
| -rw-r--r-- | src/theory/arith/constraint.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 952879182..70b2cad20 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -601,8 +601,17 @@ class Constraint { * hasEqualityEngineProof(). * * All return conjuncts were asserted before this constraint. + * + * Requires the given node to rewrite to the canonical literal for this + * constraint. + * + * @params n the literal to prove + * n must rewrite to the constraint's canonical literal + * + * @returns a trust node of the form: + * (=> explanation n) */ - TrustNode externalExplainForPropagation() const; + TrustNode externalExplainForPropagation(TNode n) const; /** * Explain the constraint and its negation in terms of assertions. |