1 files changed, 18 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index 76b7d0982..aa7fc1b6a 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -24,6 +24,11 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+class Instantiate;
+class Skolemize;
+class QuantifiersRegistry;
+class TermRegistry;
+class FirstOrderModel;
 /**
  * The quantifiers inference manager.
  */
@@ -32,12 +37,25 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
  public:
   QuantifiersInferenceManager(Theory& t,
                               QuantifiersState& state,
+                              QuantifiersRegistry& qr,
+                              TermRegistry& tr,
+                              FirstOrderModel* m,
                               ProofNodeManager* pnm);
   ~QuantifiersInferenceManager();
+  /** get instantiate utility */
+  Instantiate* getInstantiate();
+  /** get skolemize utility */
+  Skolemize* getSkolemize();
   /**
    * Do all pending lemmas, then do all pending phase requirements.
    */
   void doPending();
+
+ private:
+  /** instantiate utility */
+  std::unique_ptr<Instantiate> d_instantiate;
+  /** skolemize utility */
+  std::unique_ptr<Skolemize> d_skolemize;
 };
 
 }  // namespace quantifiers