diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-12-18 07:01:58 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-18 09:01:58 -0600 |
| commit | 5b05e467710e07bbfa27d4a2417ec27b336c245d (patch) | |
| tree | b909dc2937e88d79a7a631b1afa9caf8fd78df88 /src/theory/arith/constraint.h | |
| parent | 8a2a526b2dab5d6efaf1435afcc1b7be113a86bf (diff) | |
Bugfix: proofs for props of non-normal arith lits (#5702)
Arith has a normal form for literals, which the rewriter computes.
Nonetheless, arith sometimes gets (and ultimately propagates) non-normal
literals. It normalizes them internally and goes about its business.
However, when asked for an explanation, it must prove the non-normal
literal, rather than the normal one.
Also includes a regression for the bug, courtesy of Andy.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
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. |