Move methods from term util to quantifiers registry (#5916)

Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.

Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.

1 files changed, 6 insertions, 3 deletions

diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index aad1762c5..4188311ec 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -33,7 +33,9 @@ class QuantifiersEngine;
 namespace quantifiers {
 
 class TermDb;
-class TermUtil;
+class QuantifiersState;
+class QuantifiersInferenceManager;
+class QuantifiersRegistry;
 
 /** Instantiation rewriter
  *
@@ -91,6 +93,7 @@ class Instantiate : public QuantifiersUtil
   Instantiate(QuantifiersEngine* qe,
               QuantifiersState& qs,
               QuantifiersInferenceManager& qim,
+              QuantifiersRegistry& qr,
               ProofNodeManager* pnm = nullptr);
   ~Instantiate();
 
@@ -293,12 +296,12 @@ class Instantiate : public QuantifiersUtil
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
   QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
   /** pointer to the proof node manager */
   ProofNodeManager* d_pnm;
   /** cache of term database for quantifiers engine */
   TermDb* d_term_db;
-  /** cache of term util for quantifiers engine */
-  TermUtil* d_term_util;
   /** instantiation rewriter classes */
   std::vector<InstantiationRewriter*> d_instRewrite;