(proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056)

This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node.

This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.

6 files changed, 237 insertions, 64 deletions

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index d0ba4ca71..8165c5d8a 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -76,7 +76,8 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
 
-  Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
+  theory::TrustNode texp = d_theoryEngine->getExplanation(lNode);
+  Node theoryExplanation = texp.getNode();
 
   if (options::unsatCores())
   {
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index f1e977fe3..5c9e6713b 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -113,7 +113,7 @@ eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
 
 void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo)
 {
-  d_te.lemma(trn.getNode(), false, LemmaProperty::NONE, atomsTo);
+  d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
 }
 
 void CombinationEngine::resetRound()
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 2334d3817..84a1d89a6 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -77,10 +77,10 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
 
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
   theory::LemmaStatus result = d_engine->lemma(
-      tlem.getNode(),
-      false,
+      tlem,
       p,
-      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
+      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+      d_theory);
   return result;
 }
 
@@ -95,8 +95,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
                        << std::endl;
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
   LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
-  theory::LemmaStatus result =
-      d_engine->lemma(tlem.getNode(), false, p, d_theory);
+  theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory);
   return result;
 }
 
@@ -117,7 +116,7 @@ void EngineOutputChannel::conflict(TNode conflictNode)
   ++d_statistics.conflicts;
   d_engine->d_outputChannelUsed = true;
   TrustNode tConf = TrustNode::mkTrustConflict(conflictNode);
-  d_engine->conflict(tConf.getNode(), d_theory);
+  d_engine->conflict(tConf, d_theory);
 }
 
 void EngineOutputChannel::demandRestart()
@@ -170,7 +169,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
   }
   ++d_statistics.conflicts;
   d_engine->d_outputChannelUsed = true;
-  d_engine->conflict(pconf.getNode(), d_theory);
+  d_engine->conflict(pconf, d_theory);
 }
 
 LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
@@ -186,10 +185,10 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
   d_engine->d_outputChannelUsed = true;
   // now, call the normal interface for lemma
   return d_engine->lemma(
-      plem.getNode(),
-      false,
+      plem,
       p,
-      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
+      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+      d_theory);
 }
 
 }  // namespace theory
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index a196d0ed0..b01cef377 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -251,7 +251,8 @@ void SharedTermsDatabase::checkForConflict() {
     std::vector<TNode> assumptions;
     d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
     Node conflict = mkAnd(assumptions);
-    d_theoryEngine->conflict(conflict, THEORY_BUILTIN);
+    TrustNode tconf = TrustNode::mkTrustConflict(conflict);
+    d_theoryEngine->conflict(tconf, THEORY_BUILTIN);
     d_conflictLHS = d_conflictRHS = Node::null();
   }
 }
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ac06d266d..123e00bc1 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -45,6 +45,7 @@
 #include "theory/relevance_manager.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/theory_engine_proof_generator.h"
 #include "theory/theory_id.h"
 #include "theory/theory_model.h"
 #include "theory/theory_traits.h"
@@ -210,6 +211,12 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_userContext(userContext),
       d_logicInfo(logicInfo),
       d_pnm(nullptr),
+      d_lazyProof(
+          d_pnm != nullptr
+              ? new LazyCDProof(
+                    d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
+              : nullptr),
+      d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
       d_sharedTerms(this, context),
       d_tc(nullptr),
       d_quantEngine(nullptr),
@@ -1023,8 +1030,10 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
     if (!normalizedLiteral.getConst<bool>()) {
       // Mark the propagation for explanations
       if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
+        // special case, trust node has no proof generator
+        TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
         // Get the explanation (conflict will figure out where it came from)
-        conflict(normalizedLiteral, toTheoryId);
+        conflict(trnn, toTheoryId);
       } else {
         Unreachable();
       }
@@ -1283,7 +1292,7 @@ static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
   return conjunction;
 }
 
-Node TheoryEngine::getExplanation(TNode node)
+TrustNode TheoryEngine::getExplanation(TNode node)
 {
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
                            << "): current propagation index = "
@@ -1300,10 +1309,9 @@ Node TheoryEngine::getExplanation(TNode node)
         << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl;
 
     TrustNode texplanation = theoryOf(atom)->explain(node);
-    Node explanation = texplanation.getNode();
     Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
-                             << ") => " << explanation << endl;
-    return explanation;
+                             << ") => " << texplanation.getNode() << endl;
+    return texplanation;
   }
 
   Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled"
@@ -1323,13 +1331,10 @@ Node TheoryEngine::getExplanation(TNode node)
   std::vector<NodeTheoryPair> explanationVector;
   explanationVector.push_back(d_propagationMap[toExplain]);
   // Process the explanation
-  getExplanation(explanationVector);
-  Node explanation = mkExplanation(explanationVector);
-
+  TrustNode texplanation = getExplanation(explanationVector);
   Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => "
-                           << explanation << endl;
-
-  return explanation;
+                           << texplanation.getNode() << endl;
+  return texplanation;
 }
 
 struct AtomsCollect {
@@ -1430,13 +1435,37 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
   }
 }
 
-theory::LemmaStatus TheoryEngine::lemma(TNode node,
-                                        bool negated,
+theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma,
                                         theory::LemmaProperty p,
-                                        theory::TheoryId atomsTo)
+                                        theory::TheoryId atomsTo,
+                                        theory::TheoryId from)
 {
   // For resource-limiting (also does a time check).
   // spendResource();
+  Assert(tlemma.getKind() == TrustNodeKind::LEMMA
+         || tlemma.getKind() == TrustNodeKind::CONFLICT);
+  // get the node
+  Node node = tlemma.getNode();
+  Node lemma = tlemma.getProven();
+
+  // when proofs are enabled, we ensure the trust node has a generator by
+  // adding a trust step to the lazy proof maintained by this class
+  if (isProofEnabled())
+  {
+    // ensure proof: set THEORY_LEMMA if no generator is provided
+    if (tlemma.getGenerator() == nullptr)
+    {
+      // internal lemmas should have generators
+      Assert(from != THEORY_LAST);
+      // add theory lemma step to proof
+      Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from);
+      d_lazyProof->addStep(lemma, PfRule::THEORY_LEMMA, {}, {lemma, tidn});
+      // update the trust node
+      tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
+    }
+    // ensure closed
+    tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
+  }
 
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
@@ -1447,10 +1476,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   }
 
   if(Dump.isOn("t-lemmas")) {
-    Node n = node;
-    if (!negated) {
-      n = node.negate();
-    }
+    // we dump the negation of the lemma, to show validity of the lemma
+    Node n = lemma.negate();
     Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
                      << CheckSatCommand(n.toExpr());
   }
@@ -1460,18 +1487,58 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   // call preprocessor
   std::vector<TrustNode> newLemmas;
   std::vector<Node> newSkolems;
-  TrustNode tlemma = d_tpp.preprocess(node, newLemmas, newSkolems, preprocess);
-
-  // !!!!!!! temporary, until this method is fully updated from proof-new
-  if (tlemma.isNull())
+  TrustNode tplemma =
+      d_tpp.preprocess(lemma, newLemmas, newSkolems, preprocess);
+  // the preprocessed lemma
+  Node lemmap;
+  if (tplemma.isNull())
   {
-    tlemma = TrustNode::mkTrustLemma(node);
+    lemmap = lemma;
+  }
+  else
+  {
+    Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
+    lemmap = tplemma.getNode();
+
+    // must update the trust lemma
+    if (lemmap != lemma)
+    {
+      // process the preprocessing
+      if (isProofEnabled())
+      {
+        Assert(d_lazyProof != nullptr);
+        // add the original proof to the lazy proof
+        d_lazyProof->addLazyStep(tlemma.getProven(), tlemma.getGenerator());
+        // only need to do anything if lemmap changed in a non-trivial way
+        if (!CDProof::isSame(lemmap, lemma))
+        {
+          d_lazyProof->addLazyStep(tplemma.getProven(),
+                                   tplemma.getGenerator(),
+                                   true,
+                                   "TheoryEngine::lemma_pp",
+                                   false,
+                                   PfRule::PREPROCESS_LEMMA);
+          // ---------- from d_lazyProof -------------- from theory preprocess
+          // lemma                       lemma = lemmap
+          // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
+          // lemmap
+          std::vector<Node> pfChildren;
+          pfChildren.push_back(lemma);
+          pfChildren.push_back(tplemma.getProven());
+          std::vector<Node> pfArgs;
+          pfArgs.push_back(lemmap);
+          d_lazyProof->addStep(
+              lemmap, PfRule::MACRO_SR_PRED_TRANSFORM, pfChildren, pfArgs);
+        }
+      }
+      tlemma = TrustNode::mkTrustLemma(lemmap, d_lazyProof.get());
+    }
   }
 
   // must use an assertion pipeline due to decision engine below
   AssertionPipeline lemmas;
   // make the assertion pipeline
-  lemmas.push_back(tlemma.getNode());
+  lemmas.push_back(lemmap);
   lemmas.updateRealAssertionsEnd();
   Assert(newSkolems.size() == newLemmas.size());
   for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
@@ -1490,16 +1557,25 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
     d_relManager->notifyPreprocessedAssertions(lemmas.ref());
   }
 
-  // assert lemmas to prop engine
-  for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
+  // do final checks on the lemmas we are about to send
+  if (isProofEnabled())
   {
-    d_propEngine->assertLemma(lemmas[i], i == 0 && negated, removable);
+    Assert(tlemma.getGenerator() != nullptr);
+    // ensure closed, make the proof node eagerly here to debug
+    tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
+    for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
+    {
+      Assert(newLemmas[i].getGenerator() != nullptr);
+      newLemmas[i].debugCheckClosed("te-proof-debug",
+                                    "TheoryEngine::lemma_new");
+    }
   }
 
-  // WARNING: Below this point don't assume lemmas[0] to be not negated.
-  if(negated) {
-    lemmas.replace(0, lemmas[0].notNode());
-    negated = false;
+  // now, send the lemmas to the prop engine
+  d_propEngine->assertLemma(tlemma.getProven(), false, removable);
+  for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i)
+  {
+    d_propEngine->assertLemma(newLemmas[i].getProven(), false, removable);
   }
 
   // assert to decision engine
@@ -1522,9 +1598,16 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
   return theory::LemmaStatus(retLemma, d_userContext->getLevel());
 }
 
-void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
-
-  Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
+void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
+{
+  Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
+  TNode conflict = tconflict.getNode();
+  Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", "
+                            << theoryId << ")" << endl;
+  Trace("te-proof-debug") << "Check closed conflict" << std::endl;
+  // doesn't require proof generator, yet, since THEORY_LEMMA is added below
+  tconflict.debugCheckClosed(
+      "te-proof-debug", "TheoryEngine::conflict_initial", false);
 
   Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
 
@@ -1539,26 +1622,91 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   // In the multiple-theories case, we need to reconstruct the conflict
   if (d_logicInfo.isSharingEnabled()) {
     // Create the workplace for explanations
-    std::vector<NodeTheoryPair> explanationVector;
-    explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
+    std::vector<NodeTheoryPair> vec;
+    vec.push_back(
+        NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
 
     // Process the explanation
-    getExplanation(explanationVector);
-    Node fullConflict = mkExplanation(explanationVector);
+    TrustNode tncExp = getExplanation(vec);
+    Trace("te-proof-debug")
+        << "Check closed conflict explained with sharing" << std::endl;
+    tncExp.debugCheckClosed("te-proof-debug",
+                            "TheoryEngine::conflict_explained_sharing");
+    Node fullConflict = tncExp.getNode();
+
+    if (isProofEnabled())
+    {
+      Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
+      Trace("te-proof-debug") << "Conflict " << tconflict << " from "
+                              << tconflict.identifyGenerator() << std::endl;
+      Trace("te-proof-debug") << "Explanation " << tncExp << " from "
+                              << tncExp.identifyGenerator() << std::endl;
+      Assert(d_lazyProof != nullptr);
+      if (tconflict.getGenerator() != nullptr)
+      {
+        d_lazyProof->addLazyStep(tconflict.getProven(),
+                                 tconflict.getGenerator());
+      }
+      else
+      {
+        // add theory lemma step
+        Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
+        Node conf = tconflict.getProven();
+        d_lazyProof->addStep(conf, PfRule::THEORY_LEMMA, {}, {conf, tidn});
+      }
+      // store the explicit step, which should come from a different
+      // generator, e.g. d_tepg.
+      Node proven = tncExp.getProven();
+      Assert(tncExp.getGenerator() != d_lazyProof.get());
+      Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
+                              << " for " << proven << std::endl;
+      d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
+      pfgEnsureClosed(proven,
+                      d_lazyProof.get(),
+                      "te-proof-debug",
+                      "TheoryEngine::conflict_during");
+      Node fullConflictNeg = fullConflict.notNode();
+      std::vector<Node> children;
+      children.push_back(proven);
+      std::vector<Node> args;
+      args.push_back(fullConflictNeg);
+      if (conflict == d_false)
+      {
+        AlwaysAssert(proven == fullConflictNeg);
+      }
+      else
+      {
+        if (fullConflict != conflict)
+        {
+          // ------------------------- explained  ---------- from theory
+          // fullConflict => conflict              ~conflict
+          // --------------------------------------------
+          // MACRO_SR_PRED_TRANSFORM ~fullConflict
+          children.push_back(conflict.notNode());
+          args.push_back(mkMethodId(MethodId::SB_LITERAL));
+          d_lazyProof->addStep(
+              fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+        }
+      }
+    }
+    // pass the processed trust node
+    TrustNode tconf =
+        TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get());
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
-    lemma(fullConflict,
-          true,
-          LemmaProperty::REMOVABLE,
-          THEORY_LAST);
+    Trace("te-proof-debug")
+        << "Check closed conflict with sharing" << std::endl;
+    tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
+    lemma(tconf, LemmaProperty::REMOVABLE);
   } else {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
-    lemma(conflict, true, LemmaProperty::REMOVABLE, THEORY_LAST);
+    // pass the trust node that was sent from the theory
+    lemma(tconflict, LemmaProperty::REMOVABLE, THEORY_LAST, theoryId);
   }
 }
 
-void TheoryEngine::getExplanation(
+theory::TrustNode TheoryEngine::getExplanation(
     std::vector<NodeTheoryPair>& explanationVector)
 {
   Assert(explanationVector.size() > 0);
@@ -1672,8 +1820,13 @@ void TheoryEngine::getExplanation(
 
   // Keep only the relevant literals
   explanationVector.resize(j);
+
+  Node expNode = mkExplanation(explanationVector);
+  return theory::TrustNode::mkTrustLemma(expNode, nullptr);
 }
 
+bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
+
 void TheoryEngine::setUserAttribute(const std::string& attr,
                                     Node n,
                                     const std::vector<Node>& node_values,
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 30b5d9fbb..550a4f496 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -53,6 +53,7 @@
 namespace CVC4 {
 
 class ResourceManager;
+class TheoryEngineProofGenerator;
 
 /**
  * A pair of a theory and a node. This is used to mark the flow of
@@ -141,6 +142,13 @@ class TheoryEngine {
   //--------------------------------- new proofs
   /** Proof node manager used by this theory engine, if proofs are enabled */
   ProofNodeManager* d_pnm;
+  /** The lazy proof object
+   *
+   * This stores instructions for how to construct proofs for all theory lemmas.
+   */
+  std::shared_ptr<LazyCDProof> d_lazyProof;
+  /** The proof generator */
+  std::shared_ptr<TheoryEngineProofGenerator> d_tepg;
   //--------------------------------- end new proofs
 
   /**
@@ -205,8 +213,12 @@ class TheoryEngine {
 
   /**
    * Called by the theories to notify of a conflict.
+   *
+   * @param conflict The trust node containing the conflict and its proof
+   * generator (if it exists),
+   * @param theoryId The theory that sent the conflict
    */
-  void conflict(TNode conflict, theory::TheoryId theoryId);
+  void conflict(theory::TrustNode conflict, theory::TheoryId theoryId);
 
   /**
    * Debugging flag to ensure that shutdown() is called before the
@@ -282,13 +294,16 @@ class TheoryEngine {
   /**
    * Adds a new lemma, returning its status.
    * @param node the lemma
-   * @param negated should the lemma be asserted negated
    * @param p the properties of the lemma.
+   * @param atomsTo the theory that atoms of the lemma should be sent to
+   * @param from the theory that sent the lemma
+   * @return a lemma status, containing the lemma and context information
+   * about when it was sent.
    */
-  theory::LemmaStatus lemma(TNode node,
-                            bool negated,
+  theory::LemmaStatus lemma(theory::TrustNode node,
                             theory::LemmaProperty p,
-                            theory::TheoryId atomsTo);
+                            theory::TheoryId atomsTo = theory::THEORY_LAST,
+                            theory::TheoryId from = theory::THEORY_LAST);
 
   /** Enusre that the given atoms are send to the given theory */
   void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
@@ -437,7 +452,11 @@ class TheoryEngine {
    * where the node is the one to be explained, and the theory is the
    * theory that sent the literal.
    */
-  void getExplanation(std::vector<NodeTheoryPair>& explanationVector);
+  theory::TrustNode getExplanation(
+      std::vector<NodeTheoryPair>& explanationVector);
+
+  /** Are proofs enabled? */
+  bool isProofEnabled() const;
 
  public:
   /**
@@ -555,7 +574,7 @@ class TheoryEngine {
   /**
    * Returns an explanation of the node propagated to the SAT solver.
    */
-  Node getExplanation(TNode node);
+  theory::TrustNode getExplanation(TNode node);
 
   /**
    * Get the pointer to the model object used by this theory engine.