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.

2 files changed, 13 insertions, 12 deletions

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