(proof-new) Generalize single step helper in eager proof generator (#5046)

This allows single step proofs to have premises, closed by a SCOPE. This will be useful for array lemmas.

1 files changed, 19 insertions, 4 deletions

diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index 09f02708b..ddf1a4d3a 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/eager_proof_generator.h"
 
+#include "expr/proof.h"
 #include "expr/proof_node_manager.h"
 
 namespace CVC4 {
@@ -93,13 +94,27 @@ TrustNode EagerProofGenerator::mkTrustNode(Node n,
   return TrustNode::mkTrustLemma(n, this);
 }
 
-TrustNode EagerProofGenerator::mkTrustNode(Node n,
+TrustNode EagerProofGenerator::mkTrustNode(Node conc,
                                            PfRule id,
+                                           const std::vector<Node>& exp,
                                            const std::vector<Node>& args,
                                            bool isConflict)
 {
-  std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, n);
-  return mkTrustNode(n, pf, isConflict);
+  // if no children, its easy
+  if (exp.empty())
+  {
+    std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
+    return mkTrustNode(conc, pf, isConflict);
+  }
+  // otherwise, we use CDProof + SCOPE
+  CDProof cdp(d_pnm);
+  cdp.addStep(conc, id, exp, args);
+  std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
+  // We use mkNode instead of mkScope, since there is no reason to check
+  // whether the free assumptions of pf are in exp, since they are by the
+  // construction above.
+  std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
+  return mkTrustNode(pfs->getResult(), pfs, isConflict);
 }
 
 TrustNode EagerProofGenerator::mkTrustedPropagation(
@@ -117,7 +132,7 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
 {
   // make the lemma
   Node lem = f.orNode(f.notNode());
-  return mkTrustNode(lem, PfRule::SPLIT, {f}, false);
+  return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
 }
 
 std::string EagerProofGenerator::identify() const { return d_name; }