diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-26 10:13:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-26 15:13:50 +0000 |
| commit | c86249b35609560be783289f0720923249a4d940 (patch) | |
| tree | 937c0c73eeee1bd74ae9fac4158434ee05939cde | |
| parent | 4eb2234bccf033e3758a7fb7309f51f4864cba0a (diff) | |
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.
| -rw-r--r-- | src/theory/trust_substitutions.cpp | 8 | ||||
| -rw-r--r-- | 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<Node>& children, const std::vector<Node>& 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<Node>& children, const std::vector<Node>& args); /** * Add substitution x -> t, which was derived from the proven field of |