(proof-new) Separate explanation stages in proof equality engine (#5356)

This fixes potential cycles in assertLemma commands in the proof equality engine by using separate proof data structures for the topmost 2 stages of proof generation for equality engine proofs. This fix is required to support datatype proofs for lemmas.

This PR also removes support for the ProofStepBuffer interface in ProofEqEngine, since it is unused, and suffers similar issues and would require a different unique fix.

2 files changed, 56 insertions, 109 deletions

diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 18cdcf902..6377f78b6 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/uf/proof_equality_engine.h"
 
+#include "expr/lazy_proof_chain.h"
 #include "theory/rewriter.h"
 #include "theory/uf/proof_checker.h"
 
@@ -197,14 +198,6 @@ TrustNode ProofEqEngine::assertConflict(PfRule id,
 }
 
 TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
-                                        ProofStepBuffer& psb)
-{
-  Trace("pfee") << "pfee::assertConflict " << exp << " via buffer with "
-                << psb.getNumSteps() << " steps" << std::endl;
-  return assertLemma(d_false, exp, {}, psb);
-}
-
-TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
                                         ProofGenerator* pg)
 {
   Assert(pg != nullptr);
@@ -225,58 +218,32 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
   Assert(conc != d_true);
   LazyCDProof tmpProof(d_pnm, &d_proof);
   LazyCDProof* curr;
+  TrustNodeKind tnk;
+  // same policy as above: for conflicts, use existing lazy proof
   if (conc == d_false)
   {
-    // optimization: we can use the main lazy proof directly, because we
-    // know we will backtrack immediately after this call.
     curr = &d_proof;
+    tnk = TrustNodeKind::CONFLICT;
   }
   else
   {
-    // use a lazy proof that always links to d_proof
     curr = &tmpProof;
+    tnk = TrustNodeKind::LEMMA;
   }
-  // Register the proof step.
-  if (!curr->addStep(conc, id, exp, args))
+  // explain each literal in the vector
+  std::vector<TNode> assumps;
+  explainVecWithProof(tnk, assumps, exp, noExplain, curr);
+  // Register the proof step. We use a separate lazy CDProof which will make
+  // calls to curr above for the proofs of the literals in exp.
+  LazyCDProof outer(d_pnm, curr);
+  if (!outer.addStep(conc, id, exp, args))
   {
     // a step went wrong, e.g. during checking
     Assert(false) << "pfee::assertConflict: register proof step";
     return TrustNode::null();
   }
-  // We've now decided which lazy proof to use (curr), now get the proof
-  // for conc.
-  return assertLemmaInternal(conc, exp, noExplain, curr);
-}
-
-TrustNode ProofEqEngine::assertLemma(Node conc,
-                                     const std::vector<Node>& exp,
-                                     const std::vector<Node>& noExplain,
-                                     ProofStepBuffer& psb)
-{
-  Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
-                << ", noExplain = " << noExplain << " via buffer with "
-                << psb.getNumSteps() << " steps" << std::endl;
-  LazyCDProof tmpProof(d_pnm, &d_proof);
-  LazyCDProof* curr;
-  // same policy as above: for conflicts, use existing lazy proof
-  if (conc == d_false)
-  {
-    curr = &d_proof;
-  }
-  else
-  {
-    curr = &tmpProof;
-  }
-  // add all steps to the proof
-  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
-  for (const std::pair<Node, ProofStep>& ps : steps)
-  {
-    if (!curr->addStep(ps.first, ps.second))
-    {
-      return TrustNode::null();
-    }
-  }
-  return assertLemmaInternal(conc, exp, noExplain, curr);
+  // Now get the proof for conc.
+  return ensureProofForFact(conc, assumps, tnk, &outer);
 }
 
 TrustNode ProofEqEngine::assertLemma(Node conc,
@@ -290,29 +257,28 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
                 << std::endl;
   LazyCDProof tmpProof(d_pnm, &d_proof);
   LazyCDProof* curr;
+  TrustNodeKind tnk;
   // same policy as above: for conflicts, use existing lazy proof
   if (conc == d_false)
   {
     curr = &d_proof;
+    tnk = TrustNodeKind::CONFLICT;
   }
   else
   {
     curr = &tmpProof;
+    tnk = TrustNodeKind::LEMMA;
   }
-  // Register the proof. Notice we do a deep copy here because the CDProof
-  // curr should take ownership of the proof steps that pg provided for conc.
-  // In other words, this sets up the "skeleton" of proof that is the base
-  // of the proof we are constructing. The call to assertLemmaInternal below
-  // will expand the leaves of this proof. If we used a shallow copy, then
-  // the connection to these leaves would be lost since they would not be
-  // owned by curr.
-  if (!pg->addProofTo(conc, curr, CDPOverwrite::ASSUME_ONLY, true))
-  {
-    // a step went wrong, e.g. during checking
-    Assert(false) << "pfee::assertConflict: register proof step";
-    return TrustNode::null();
-  }
-  return assertLemmaInternal(conc, exp, noExplain, curr);
+  // explain each literal in the vector
+  std::vector<TNode> assumps;
+  explainVecWithProof(tnk, assumps, exp, noExplain, curr);
+  // We use a lazy proof chain here. The provided proof generator sets up the
+  // "skeleton" that is the base of the proof we are constructing. The call to
+  // LazyCDProofChain::getProofFor will expand the leaves of this proof via
+  // calls to curr.
+  LazyCDProofChain outer(d_pnm, true, nullptr, curr, false);
+  outer.addLazyStep(conc, pg);
+  return ensureProofForFact(conc, assumps, tnk, &outer);
 }
 
 TrustNode ProofEqEngine::explain(Node conc)
@@ -324,18 +290,12 @@ TrustNode ProofEqEngine::explain(Node conc)
   return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
 }
 
-TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
-                                             const std::vector<Node>& exp,
-                                             const std::vector<Node>& noExplain,
-                                             LazyCDProof* curr)
+void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk,
+                                        std::vector<TNode>& assumps,
+                                        const std::vector<Node>& exp,
+                                        const std::vector<Node>& noExplain,
+                                        LazyCDProof* curr)
 {
-  // We are a conflict if the conclusion is false and all literals are
-  // explained.
-  TrustNodeKind tnk =
-      conc == d_false ? TrustNodeKind::CONFLICT : TrustNodeKind::LEMMA;
-
-  // get the explanation, with proofs
-  std::vector<TNode> assumps;
   std::vector<Node> expn;
   for (const Node& e : exp)
   {
@@ -351,13 +311,12 @@ TrustNode ProofEqEngine::assertLemmaInternal(Node conc,
       tnk = TrustNodeKind::LEMMA;
     }
   }
-  return ensureProofForFact(conc, assumps, tnk, curr);
 }
 
 TrustNode ProofEqEngine::ensureProofForFact(Node conc,
                                             const std::vector<TNode>& assumps,
                                             TrustNodeKind tnk,
-                                            LazyCDProof* curr)
+                                            ProofGenerator* curr)
 {
   Trace("pfee-proof") << std::endl;
   Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 4659b2246..4148da1de 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -168,8 +168,6 @@ class ProofEqEngine : public EagerProofGenerator
   TrustNode assertConflict(PfRule id,
                            const std::vector<Node>& exp,
                            const std::vector<Node>& args);
-  /** Multi-step version */
-  TrustNode assertConflict(const std::vector<Node>& exp, ProofStepBuffer& psb);
   /** Generator version, where pg has a proof of false from assumptions exp */
   TrustNode assertConflict(const std::vector<Node>& exp, ProofGenerator* pg);
   //-------------------------- assert lemma
@@ -215,11 +213,6 @@ class ProofEqEngine : public EagerProofGenerator
                         const std::vector<Node>& exp,
                         const std::vector<Node>& noExplain,
                         const std::vector<Node>& args);
-  /** Multi-step version */
-  TrustNode assertLemma(Node conc,
-                        const std::vector<Node>& exp,
-                        const std::vector<Node>& noExplain,
-                        ProofStepBuffer& psb);
   /** Generator version, where pg has a proof of conc */
   TrustNode assertLemma(Node conc,
                         const std::vector<Node>& exp,
@@ -248,21 +241,6 @@ class ProofEqEngine : public EagerProofGenerator
   /** holds */
   bool holds(TNode pred, bool polarity);
   /**
-   * Assert lemma internal. This method is called for ensuring the proof of
-   * conc exists in curr, where exp / noExplain are the its explanation (see
-   * assertLemma). This method is used for conflicts as well, where noExplain
-   * must be empty and conc = d_false.
-   *
-   * If curr is null, no proof is constructed.
-   *
-   * This method returns the trust node of the lemma or conflict with this
-   * class as the proof generator.
-   */
-  TrustNode assertLemmaInternal(Node conc,
-                                const std::vector<Node>& exp,
-                                const std::vector<Node>& noExplain,
-                                LazyCDProof* curr);
-  /**
    * Ensure proof for fact. This is called by the above method after we have
    * determined the final set of assumptions used for showing conc. This
    * method is used for lemmas, conflicts, and explanations for propagations.
@@ -271,7 +249,29 @@ class ProofEqEngine : public EagerProofGenerator
   TrustNode ensureProofForFact(Node conc,
                                const std::vector<TNode>& assumps,
                                TrustNodeKind tnk,
-                               LazyCDProof* curr);
+                               ProofGenerator* curr);
+  /**
+   * This ensures the proof of the literals that are in exp but not in
+   * noExplain have been added to curr. This additionally adds the
+   * explanation of exp to assumps. It updates tnk to LEMMA if there
+   * are any literals in exp that are not in noExplain.
+   */
+  void explainVecWithProof(TrustNodeKind& tnk,
+                           std::vector<TNode>& assumps,
+                           const std::vector<Node>& exp,
+                           const std::vector<Node>& noExplain,
+                           LazyCDProof* curr);
+  /** Explain
+   *
+   * This adds to assumps the set of facts that were asserted to this
+   * class in the current SAT context that are required for showing lit.
+   *
+   * This additionally registers the equality proof steps required to
+   * regress the explanation of lit in curr.
+   */
+  void explainWithProof(Node lit,
+                        std::vector<TNode>& assumps,
+                        LazyCDProof* curr);
   /** Reference to the equality engine */
   eq::EqualityEngine& d_ee;
   /** The default proof generator (for simple facts) */
@@ -290,18 +290,6 @@ class ProofEqEngine : public EagerProofGenerator
    * SAT-context-dependent.
    */
   NodeSet d_keep;
-  /** Explain
-   *
-   * This adds to assumps the set of facts that were asserted to this
-   * class in the current SAT context by calls to assertAssume that are
-   * required for showing lit.
-   *
-   * This additionally registers the equality proof steps required to
-   * regress the explanation of lit.
-   */
-  void explainWithProof(Node lit,
-                        std::vector<TNode>& assumps,
-                        LazyCDProof* curr);
 };
 
 }  // namespace eq