Make buffered inference manager more robust to backtracking (#6833)

This makes TheoryEngine notify all theories when a theory sends a conflict. This means that buffered inference managers always clear their buffers when any theory sends a conflict.

This is required for making theories robust to conflicts that may arise when using the central equality engine, where a different theory may raise a conflict during another theory's check.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h
index 080033562..cc4bd7ba4 100644
--- a/src/theory/inference_manager_buffered.h
+++ b/src/theory/inference_manager_buffered.h
@@ -159,6 +159,14 @@ class InferenceManagerBuffered : public TheoryInferenceManager
    */
   void assertInternalFactTheoryInference(TheoryInference* fact);
 
+  /**
+   * Notify this inference manager that a conflict was sent in this SAT context.
+   * This method is called via TheoryEngine when a conflict is sent. This
+   * method will clear all pending facts, lemmas, and phase requirements, as
+   * these will be stale after the solver backtracks.
+   */
+  void notifyInConflict() override;
+
  protected:
   /** A set of pending inferences to be processed as lemmas */
   std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;