Update sets inference manager to inherit from InferenceManagerBuffered (#5007)

This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered.

It matches that base class almost exactly, with cosmetic changes.

Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR.

This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas.

1 files changed, 6 insertions, 6 deletions

diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 7787c0f9b..fed74b1bb 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -21,6 +21,8 @@
 
 #include <memory>
 
+#include "theory/sets/inference_manager.h"
+#include "theory/sets/solver_state.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
@@ -61,12 +63,6 @@ class TheorySets : public Theory
   //--------------------------------- standard check
   /** Post-check, called after the fact queue of the theory is processed. */
   void postCheck(Effort level) override;
-  /** Pre-notify fact, return true if processed. */
-  bool preNotifyFact(TNode atom,
-                     bool pol,
-                     TNode fact,
-                     bool isPrereg,
-                     bool isInternal) override;
   /** Notify fact */
   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
   //--------------------------------- end standard check
@@ -102,6 +98,10 @@ class TheorySets : public Theory
    private:
     TheorySetsPrivate& d_theory;
   };
+  /** The state of the sets solver at full effort */
+  SolverState d_state;
+  /** The inference manager */
+  InferenceManager d_im;
   /** The internal theory */
   std::unique_ptr<TheorySetsPrivate> d_internal;
   /** Instance of the above class */