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.cpp | |
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.cpp')
-rw-r--r-- | src/theory/arith/constraint.cpp | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 03d9c50e9..c1db8e55a 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -1507,7 +1507,7 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){ return externalExplain(b, AssertionOrderSentinel); } -TrustNode Constraint::externalExplainForPropagation() const +TrustNode Constraint::externalExplainForPropagation(TNode lit) const { Assert(hasProof()); Assert(!isAssumption()); @@ -1517,6 +1517,9 @@ TrustNode Constraint::externalExplainForPropagation() const Node n = safeConstructNary(nb); if (d_database->isProofEnabled()) { + // Check that the literal we're explaining via this constraint actually + // matches the constraint's canonical literal. + Assert(Rewriter::rewrite(lit) == getLiteral()); std::vector<Node> assumptions; if (n.getKind() == Kind::AND) { @@ -1526,18 +1529,18 @@ TrustNode Constraint::externalExplainForPropagation() const { assumptions.push_back(n); } - if (getProofLiteral() != getLiteral()) + if (getProofLiteral() != lit) { pfFromAssumptions = d_database->d_pnm->mkNode( - PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {getLiteral()}); + PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {lit}); } auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions); return d_database->d_pfGen->mkTrustedPropagation( - getLiteral(), safeConstructNary(Kind::AND, assumptions), pf); + lit, safeConstructNary(Kind::AND, assumptions), pf); } else { - return TrustNode::mkTrustPropExp(getLiteral(), n); + return TrustNode::mkTrustPropExp(lit, n); } } |