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.

diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index d76356f75f46fcd400589543170b0545439cc082..4088deb94513caefc0449e10bbaa4c15e688415e 100644 (file)
--- 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 2082a5daefbfdb975b5e00776fb9d644e50a186a..e8b627249d7f2b0b963e1a79c5fa22c3ae6b1039 100644 (file)
--- 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