From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Apr 2021 15:13:50 +0000 (-0500)
Subject: Ensure dependency is tracked for all substitutions (#6438)
X-Git-Tag: cvc5-1.0.0~1832
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c86249b35609560be783289f0720923249a4d940;p=cvc5.git

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 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