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.

1 files changed, 74 insertions, 20 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)