Introduce quantifiers inference manager (#5821)

This is the second prerequisite for eliminating dependencies on quantifiers engine. This PR threads a quantifiers inference manager through all modules in quantifiers that add lemmas.

The code for adding lemmas in quantifiers engine will be migrated to this class.

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 10363f5a2..4820398be 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -62,7 +62,9 @@ namespace quantifiers {
 class SygusInst : public QuantifiersModule
 {
  public:
-  SygusInst(QuantifiersEngine* qe, QuantifiersState& qs);
+  SygusInst(QuantifiersEngine* qe,
+            QuantifiersState& qs,
+            QuantifiersInferenceManager& qim);
   ~SygusInst() = default;
 
   bool needsCheck(Theory::Effort e) override;