Add interfaces for making trust nodes in TheoryInferenceManager. (#5016)

This gives theories a finer grained control over explained lemmas and conflicts.

A theory may now use an inference manager to construct "explained" lemmas/conflicts e.g. via mkLemmaExp, subsequently do any theory-specific debugging or modification to that lemma before sending it via trustedLemma.

This is required for the new strings inference manager on proof-new.

This also adds a missing variant of conflicts for the proof equality engine. It also does a minor simplification of a previous variant for constructing conflicts from proof equality engine based on a proof step buffer.

4 files changed, 136 insertions, 35 deletions

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 330613e2e..40fa9c5ae 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -50,6 +50,8 @@ void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
   }
 }
 
+bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
+
 void TheoryInferenceManager::reset()
 {
   d_numCurrentLemmas = 0;
@@ -96,21 +98,52 @@ void TheoryInferenceManager::conflictExp(PfRule id,
 {
   if (!d_theoryState.isInConflict())
   {
-    if (d_pfee != nullptr)
-    {
-      // use proof equality engine to construct the trust node
-      TrustNode tconf = d_pfee->assertConflict(id, exp, args);
-      d_out.trustedConflict(tconf);
-    }
-    else
-    {
-      // version without proofs
-      Node conf = mkExplainPartial(exp, {});
-      conflict(conf);
-    }
+    // make the trust node
+    TrustNode tconf = mkConflictExp(id, exp, args);
+    // send it on the output channel
+    trustedConflict(tconf);
   }
 }
 
+TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
+                                                const std::vector<Node>& exp,
+                                                const std::vector<Node>& args)
+{
+  if (d_pfee != nullptr)
+  {
+    // use proof equality engine to construct the trust node
+    return d_pfee->assertConflict(id, exp, args);
+  }
+  // version without proofs
+  Node conf = mkExplainPartial(exp, {});
+  return TrustNode::mkTrustConflict(conf, nullptr);
+}
+
+void TheoryInferenceManager::conflictExp(const std::vector<Node>& exp,
+                                         ProofGenerator* pg)
+{
+  if (!d_theoryState.isInConflict())
+  {
+    // make the trust node
+    TrustNode tconf = mkConflictExp(exp, pg);
+    // send it on the output channel
+    trustedConflict(tconf);
+  }
+}
+
+TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
+                                                ProofGenerator* pg)
+{
+  if (d_pfee != nullptr)
+  {
+    // use proof equality engine to construct the trust node
+    return d_pfee->assertConflict(exp, pg);
+  }
+  // version without proofs
+  Node conf = mkExplainPartial(exp, {});
+  return TrustNode::mkTrustConflict(conf, nullptr);
+}
+
 bool TheoryInferenceManager::propagateLit(TNode lit)
 {
   // If already in conflict, no more propagation
@@ -191,16 +224,27 @@ bool TheoryInferenceManager::lemmaExp(Node conc,
                                       LemmaProperty p,
                                       bool doCache)
 {
+  // make the trust node
+  TrustNode trn = mkLemmaExp(conc, id, exp, noExplain, args);
+  // send it on the output channel
+  return trustedLemma(trn, p, doCache);
+}
+
+TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
+                                             PfRule id,
+                                             const std::vector<Node>& exp,
+                                             const std::vector<Node>& noExplain,
+                                             const std::vector<Node>& args)
+{
   if (d_pfee != nullptr)
   {
     // make the trust node from the proof equality engine
-    TrustNode trn = d_pfee->assertLemma(conc, id, exp, noExplain, args);
-    return trustedLemma(trn, p, doCache);
+    return d_pfee->assertLemma(conc, id, exp, noExplain, args);
   }
-  // otherwise, not using proofs, explain and send lemma
+  // otherwise, not using proofs, explain and make trust node
   Node ant = mkExplainPartial(exp, noExplain);
   Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
-  return lemma(lem, p, doCache);
+  return TrustNode::mkTrustLemma(lem, nullptr);
 }
 
 bool TheoryInferenceManager::lemmaExp(Node conc,
@@ -210,16 +254,26 @@ bool TheoryInferenceManager::lemmaExp(Node conc,
                                       LemmaProperty p,
                                       bool doCache)
 {
+  // make the trust node
+  TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
+  // send it on the output channel
+  return trustedLemma(trn, p, doCache);
+}
+
+TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
+                                             const std::vector<Node>& exp,
+                                             const std::vector<Node>& noExplain,
+                                             ProofGenerator* pg)
+{
   if (d_pfee != nullptr)
   {
     // make the trust node from the proof equality engine
-    TrustNode trn = d_pfee->assertLemma(conc, exp, noExplain, pg);
-    return trustedLemma(trn, p, doCache);
+    return d_pfee->assertLemma(conc, exp, noExplain, pg);
   }
-  // otherwise, not using proofs, explain and send lemma
+  // otherwise, not using proofs, explain and make trust node
   Node ant = mkExplainPartial(exp, noExplain);
   Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
-  return lemma(lem, p, doCache);
+  return TrustNode::mkTrustLemma(lem, nullptr);
 }
 
 bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 080a09ba8..92116648e 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -77,6 +77,11 @@ class TheoryInferenceManager
    */
   void setEqualityEngine(eq::EqualityEngine* ee);
   /**
+   * Are proofs enabled in this inference manager? Returns true if the proof
+   * node manager pnm provided to the constructor of this class was non-null.
+   */
+  bool isProofEnabled() const;
+  /**
    * Reset, which resets counters regarding the number of added lemmas and
    * internal facts. This method should be manually called by the theory at
    * the appropriate time for the purpose of tracking the usage of this
@@ -127,7 +132,7 @@ class TheoryInferenceManager
   void conflict(TNode conf);
   /**
    * Raise trusted conflict tconf (of any form) where a proof generator has
-   * been provided in a custom way.
+   * been provided (as part of the trust node) in a custom way.
    */
   void trustedConflict(TrustNode tconf);
   /**
@@ -140,6 +145,29 @@ class TheoryInferenceManager
   void conflictExp(PfRule id,
                    const std::vector<Node>& exp,
                    const std::vector<Node>& args);
+  /**
+   * Make the trust node corresponding to the conflict of the above form. It is
+   * the responsibility of the caller to subsequently call trustedConflict with
+   * the returned trust node.
+   */
+  TrustNode mkConflictExp(PfRule id,
+                          const std::vector<Node>& exp,
+                          const std::vector<Node>& args);
+  /**
+   * Explain and send conflict from contradictory facts. This method is called
+   * when proof generator pg has a proof of false from free assumptions exp.
+   * This method sends a trusted conflict corresponding to the official
+   * equality engine's explanation of literals in exp, with the proof equality
+   * engine as the proof generator (if it exists), where pg provides the
+   * final step(s) of this proof during this call.
+   */
+  void conflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
+  /**
+   * Make the trust node corresponding to the conflict of the above form. It is
+   * the responsibility of the caller to subsequently call trustedConflict with
+   * the returned trust node.
+   */
+  TrustNode mkConflictExp(const std::vector<Node>& exp, ProofGenerator* pg);
   //--------------------------------------- lemmas
   /**
    * Send (trusted) lemma lem with property p on the output channel.
@@ -191,9 +219,19 @@ class TheoryInferenceManager
                 LemmaProperty p = LemmaProperty::NONE,
                 bool doCache = true);
   /**
+   * Make the trust node for the above method. It is responsibility of the
+   * caller to subsequently call trustedLemma with the returned trust node.
+   */
+  TrustNode mkLemmaExp(Node conc,
+                       PfRule id,
+                       const std::vector<Node>& exp,
+                       const std::vector<Node>& noExplain,
+                       const std::vector<Node>& args);
+  /**
    * Same as above, but where pg can provide a proof of conc from free
-   * assumptions in exp. It is required to do so in the remainder of the user
-   * context when this method returns true.
+   * assumptions in exp. This sends a trusted lemma on the output channel where
+   * the proof equality engine is the proof generator. The generator pg
+   * is asked to provide the final step(s) of this proof during this call.
    *
    * @param conc The conclusion of the lemma
    * @param exp The set of (all) literals that imply conc
@@ -211,6 +249,14 @@ class TheoryInferenceManager
                 LemmaProperty p = LemmaProperty::NONE,
                 bool doCache = true);
   /**
+   * Make the trust node for the above method. It is responsibility of the
+   * caller to subsequently call trustedLemma with the returned trust node.
+   */
+  TrustNode mkLemmaExp(Node conc,
+                       const std::vector<Node>& exp,
+                       const std::vector<Node>& noExplain,
+                       ProofGenerator* pg = nullptr);
+  /**
    * Has this inference manager cached and sent the given lemma (in this user
    * context)? This method can be overridden by the particular manager. If not,
    * this returns true if lem is in the cache d_lemmasSent maintained by this
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 021a737c0..66c36ed95 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -260,9 +260,8 @@ TrustNode ProofEqEngine::assertConflict(PfRule id,
 {
   Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp
                 << ", args = " << args << std::endl;
-  // conflict is same as proof of false
-  std::vector<Node> empVec;
-  return assertLemma(d_false, id, exp, empVec, args);
+  // conflict is same as lemma concluding false
+  return assertLemma(d_false, id, exp, {}, args);
 }
 
 TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
@@ -270,15 +269,15 @@ TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
 {
   Trace("pfee") << "pfee::assertConflict " << exp << " via buffer with "
                 << psb.getNumSteps() << " steps" << std::endl;
-  if (d_pfEnabled)
-  {
-    if (!d_proof.addSteps(psb))
-    {
-      return TrustNode::null();
-    }
-  }
-  std::vector<Node> empVec;
-  return assertLemmaInternal(d_false, exp, empVec, &d_proof);
+  return assertLemma(d_false, exp, {}, psb);
+}
+
+TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
+                                        ProofGenerator* pg)
+{
+  Trace("pfee") << "pfee::assertConflict " << exp << " via generator"
+                << std::endl;
+  return assertLemma(d_false, exp, {}, pg);
 }
 
 TrustNode ProofEqEngine::assertLemma(Node conc,
diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 314353131..e1105623a 100644
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -180,6 +180,8 @@ class ProofEqEngine : public EagerProofGenerator
                            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
   /**
    * Called when we have concluded conc, typically via theory specific