diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-12 10:00:36 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-11-12 10:00:36 -0600 |
commit | b9eee8d69e9de4641514c35d49c495bd5adead5f (patch) | |
tree | 493aff91499c84e1b3543f34c679b2c6f1aa2d17 /src/theory/uf/proof_equality_engine.cpp | |
parent | 2de877854e590e8edf89ffb1d940cd4c9717f195 (diff) |
(proof-new) Fix true explanations of propagations in pf equality engine (#5338)
This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.
Diffstat (limited to 'src/theory/uf/proof_equality_engine.cpp')
-rw-r--r-- | src/theory/uf/proof_equality_engine.cpp | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp index 184584aa9..18cdcf902 100644 --- a/src/theory/uf/proof_equality_engine.cpp +++ b/src/theory/uf/proof_equality_engine.cpp @@ -408,9 +408,20 @@ TrustNode ProofEqEngine::ensureProofForFact(Node conc, scopeAssumps.push_back(a); } } - // scope the proof constructed above, and connect the formula with the proof - // minimize the assumptions + // Scope the proof constructed above, and connect the formula with the proof + // minimize the assumptions. pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true); + // If we have no assumptions, and are proving an explanation for propagation + if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP) + { + // Must add "true" as an explicit argument. This is to ensure that the + // propagation F from true proves (=> true F) instead of F, since this is + // the form required by TrustNodeKind::PROP_EXP. We do not ensure closed or + // minimize here, since we already ensured the proof was closed above, and + // we do not want to minimize, or else "true" would be omitted. + scopeAssumps.push_back(nm->mkConst(true)); + pf = d_pnm->mkScope(pf, scopeAssumps, false); + } exp = nm->mkAnd(scopeAssumps); // Make the lemma or conflict node. This must exactly match the conclusion // of SCOPE below. |