From c86249b35609560be783289f0720923249a4d940 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 26 Apr 2021 10:13:50 -0500 Subject: [PATCH] Ensure dependency is tracked for all substitutions (#6438) This ensures that dependencies are tracked for all inferred substitutions, even if a trusted step is added. This is required to ensure unsat cores are sound when we use e.g. non-clausal simplification + unsat cores. --- src/theory/trust_substitutions.cpp | 8 +++++--- src/theory/trust_substitutions.h | 1 + 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp index d76356f75..4088deb94 100644 --- a/src/theory/trust_substitutions.cpp +++ b/src/theory/trust_substitutions.cpp @@ -61,6 +61,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, ProofGenerator* pg) void TrustSubstitutionMap::addSubstitution(TNode x, TNode t, PfRule id, + const std::vector& children, const std::vector& args) { if (!isProofEnabled()) @@ -70,7 +71,7 @@ void TrustSubstitutionMap::addSubstitution(TNode x, } LazyCDProof* stepPg = d_helperPf.allocateProof(nullptr, d_ctx); Node eq = x.eqNode(t); - stepPg->addStep(eq, id, {}, args); + stepPg->addStep(eq, id, children, args); addSubstitution(x, t, stepPg); } @@ -103,8 +104,9 @@ ProofGenerator* TrustSubstitutionMap::addSubstitutionSolved(TNode x, // Try to transform tn.getProven() to (= x t) here, if necessary if (!d_tspb->applyPredTransform(proven, eq, {})) { - // failed to rewrite - addSubstitution(x, t, nullptr); + // failed to rewrite, it is critical for unsat cores that proven is a + // premise here, since the conclusion depends on it + addSubstitution(x, t, PfRule::TRUST_SUBS_MAP, {proven}, {eq}); Trace("trust-subs") << "...failed to rewrite" << std::endl; return nullptr; } diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h index 2082a5dae..e8b627249 100644 --- a/src/theory/trust_substitutions.h +++ b/src/theory/trust_substitutions.h @@ -60,6 +60,7 @@ class TrustSubstitutionMap : public ProofGenerator void addSubstitution(TNode x, TNode t, PfRule id, + const std::vector& children, const std::vector& args); /** * Add substitution x -> t, which was derived from the proven field of -- 2.30.2