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, 49 insertions, 3 deletions

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