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.

13 files changed, 54 insertions, 34 deletions

diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 0ab2988d2..4c606a273 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -17,7 +17,6 @@
 #include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"
@@ -31,10 +30,11 @@ namespace inst {
 HigherOrderTrigger::HigherOrderTrigger(
     QuantifiersEngine* qe,
     quantifiers::QuantifiersInferenceManager& qim,
+    quantifiers::QuantifiersRegistry& qr,
     Node q,
     std::vector<Node>& nodes,
     std::map<Node, std::vector<Node> >& ho_apps)
-    : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps)
+    : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
 {
   NodeManager* nm = NodeManager::currentNM();
   // process the higher-order variable applications
@@ -201,11 +201,10 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m)
     // get substitution corresponding to m
     std::vector<TNode> vars;
     std::vector<TNode> subs;
-    quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
     for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
     {
       subs.push_back(m.d_vals[i]);
-      vars.push_back(tutil->getInstantiationConstant(d_quant, i));
+      vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
     }
 
     Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index e424f69d1..af7020bfc 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -94,6 +94,7 @@ class HigherOrderTrigger : public Trigger
  private:
   HigherOrderTrigger(QuantifiersEngine* qe,
                      quantifiers::QuantifiersInferenceManager& qim,
+                     quantifiers::QuantifiersRegistry& qr,
                      Node q,
                      std::vector<Node>& nodes,
                      std::map<Node, std::vector<Node> >& ho_apps);
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index a0114ba80..4f393bc4f 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -238,8 +238,6 @@ void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
   if (trieIndex < iio->d_order.size())
   {
     size_t curr_index = iio->d_order[trieIndex];
-    // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
-    // curr_index );
     Node n = m.get(curr_index);
     if (n.isNull())
     {
diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp
index fc85703c0..fe771b4e7 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy.cpp
@@ -22,8 +22,9 @@ namespace quantifiers {
 
 InstStrategy::InstStrategy(QuantifiersEngine* qe,
                            QuantifiersState& qs,
-                           QuantifiersInferenceManager& qim)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
+                           QuantifiersInferenceManager& qim,
+                           QuantifiersRegistry& qr)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
 {
 }
 InstStrategy::~InstStrategy() {}
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index b9d0aa745..1455ce0c5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -31,6 +31,7 @@ namespace quantifiers {
 
 class QuantifiersState;
 class QuantifiersInferenceManager;
+class QuantifiersRegistry;
 
 /** A status response to process */
 enum class InstStrategyStatus
@@ -49,7 +50,8 @@ class InstStrategy
  public:
   InstStrategy(QuantifiersEngine* qe,
                QuantifiersState& qs,
-               QuantifiersInferenceManager& qim);
+               QuantifiersInferenceManager& qim,
+               QuantifiersRegistry& qr);
   virtual ~InstStrategy();
   /** presolve */
   virtual void presolve();
@@ -72,6 +74,8 @@ class InstStrategy
   QuantifiersState& d_qstate;
   /** The quantifiers inference manager object */
   QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
 }; /* class InstStrategy */
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 90d8de128..2a1e38c3c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -62,8 +62,9 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
     QuantifiersEngine* qe,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
-    QuantRelevance* qr)
-    : InstStrategy(qe, qs, qim), d_quant_rel(qr)
+    QuantifiersRegistry& qr,
+    QuantRelevance* qrlv)
+    : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv)
 {
   //how to select trigger terms
   d_tr_strategy = options::triggerSelMode();
@@ -283,6 +284,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     {
       tr = Trigger::mkTrigger(d_quantEngine,
                               d_qim,
+                              d_qreg,
                               f,
                               patTerms[0],
                               false,
@@ -320,6 +322,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       // will possibly want to get an old trigger
       tr = Trigger::mkTrigger(d_quantEngine,
                               d_qim,
+                              d_qreg,
                               f,
                               patTerms,
                               false,
@@ -362,6 +365,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
           d_single_trigger_gen[patTerms[index]] = true;
           Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
                                             d_qim,
+                                            d_qreg,
                                             f,
                                             patTerms[index],
                                             false,
@@ -390,7 +394,6 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
   bool ntrivTriggers = options::relationalTriggers();
   std::vector<Node> patTermsF;
   std::map<Node, inst::TriggerTermInfo> tinfo;
-  TermUtil* tu = d_quantEngine->getTermUtil();
   NodeManager* nm = NodeManager::currentNM();
   // well-defined function: can assume LHS is only pattern
   if (options::quantFunWellDefined())
@@ -398,7 +401,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
     Node hd = QuantAttributes::getFunDefHead(f);
     if (!hd.isNull())
     {
-      hd = tu->substituteBoundVariablesToInstConstants(hd, f);
+      hd = d_qreg.substituteBoundVariablesToInstConstants(hd, f);
       patTermsF.push_back(hd);
       tinfo[hd].init(f, hd);
     }
@@ -406,7 +409,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
   // otherwise, use algorithm for collecting pattern terms
   if (patTermsF.empty())
   {
-    Node bd = tu->getInstConstantBody(f);
+    Node bd = d_qreg.getInstConstantBody(f);
     PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true);
     pts.collect(bd, patTermsF, tinfo);
     if (ntrivTriggers)
@@ -486,7 +489,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
       std::vector<Node> vcs[2];
       for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
       {
-        Node ic = tu->getInstantiationConstant(f, i);
+        Node ic = d_qreg.getInstantiationConstant(f, i);
         vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]);
       }
       for (size_t i = 0; i < 2; i++)
@@ -621,8 +624,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
     NodeManager* nm = NodeManager::currentNM();
     // partial trigger : generate implication to mark user pattern
     Node pat =
-        d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
-            tr->getInstPattern(), q);
+        d_qreg.substituteInstConstantsToBoundVariables(tr->getInstPattern(), q);
     Node ipl = nm->mkNode(INST_PATTERN_LIST, pat);
     Node qq = nm->mkNode(FORALL,
                          d_vc_partition[1][q],
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 81b40f067..6170d3067 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -88,7 +88,8 @@ class InstStrategyAutoGenTriggers : public InstStrategy
   InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
                               QuantifiersState& qs,
                               QuantifiersInferenceManager& qim,
-                              QuantRelevance* qr);
+                              QuantifiersRegistry& qr,
+                              QuantRelevance* qrlv);
   ~InstStrategyAutoGenTriggers() {}
 
   /** get auto-generated trigger */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index cf6405b38..ca2f1bdc5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -27,8 +27,9 @@ namespace quantifiers {
 InstStrategyUserPatterns::InstStrategyUserPatterns(
     QuantifiersEngine* ie,
     QuantifiersState& qs,
-    QuantifiersInferenceManager& qim)
-    : InstStrategy(ie, qs, qim)
+    QuantifiersInferenceManager& qim,
+    QuantifiersRegistry& qr)
+    : InstStrategy(ie, qs, qim, qr)
 {
 }
 InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
@@ -105,8 +106,13 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
     std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
     for (size_t i = 0, usize = ugw.size(); i < usize; i++)
     {
-      Trigger* t = Trigger::mkTrigger(
-          d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL);
+      Trigger* t = Trigger::mkTrigger(d_quantEngine,
+                                      d_qim,
+                                      d_qreg,
+                                      q,
+                                      ugw[i],
+                                      true,
+                                      Trigger::TR_RETURN_NULL);
       if (t)
       {
         d_user_gen[q].push_back(t);
@@ -165,7 +171,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
     return;
   }
   Trigger* t = Trigger::mkTrigger(
-      d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW);
+      d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW);
   if (t)
   {
     d_user_gen[q].push_back(t);
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
index 996adc444..1cad77fef 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -36,7 +36,8 @@ class InstStrategyUserPatterns : public InstStrategy
  public:
   InstStrategyUserPatterns(QuantifiersEngine* qe,
                            QuantifiersState& qs,
-                           QuantifiersInferenceManager& qim);
+                           QuantifiersInferenceManager& qim,
+                           QuantifiersRegistry& qr);
   ~InstStrategyUserPatterns();
   /** add pattern */
   void addUserPattern(Node q, Node pat);
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 50d91a1e1..3e344f7fb 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
     // user-provided patterns
     if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
     {
-      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim));
+      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr));
       d_instStrategies.push_back(d_isup.get());
     }
 
     // auto-generated patterns
     d_i_ag.reset(new InstStrategyAutoGenTriggers(
-        d_quantEngine, qs, qim, d_quant_rel.get()));
+        d_quantEngine, qs, qim, qr, d_quant_rel.get()));
     d_instStrategies.push_back(d_i_ag.get());
   }
 }
@@ -228,9 +228,7 @@ void InstantiationEngine::registerQuantifier(Node q)
   // take into account user patterns
   if (q.getNumChildren() == 3)
   {
-    Node subsPat =
-        d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
-            q[2], q);
+    Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
     // add patterns
     for (const Node& p : subsPat)
     {
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 016784152..e27277933 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -20,8 +20,8 @@
 #include <vector>
 
 #include "theory/quantifiers/ematching/inst_strategy.h"
+#include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_relevance.h"
-#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 3bc5ded16..ac43d3bc9 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -36,9 +36,10 @@ namespace inst {
 /** trigger class constructor */
 Trigger::Trigger(QuantifiersEngine* qe,
                  quantifiers::QuantifiersInferenceManager& qim,
+                 quantifiers::QuantifiersRegistry& qr,
                  Node q,
                  std::vector<Node>& nodes)
-    : d_quantEngine(qe), d_qim(qim), d_quant(q)
+    : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q)
 {
   // We must ensure that the ground subterms of the trigger have been
   // preprocessed.
@@ -233,6 +234,7 @@ bool Trigger::mkTriggerTerms(Node q,
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node f,
                             std::vector<Node>& nodes,
                             bool keepAll,
@@ -273,11 +275,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
   Trigger* t;
   if (!ho_apps.empty())
   {
-    t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps);
+    t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps);
   }
   else
   {
-    t = new Trigger(qe, qim, f, trNodes);
+    t = new Trigger(qe, qim, qr, f, trNodes);
   }
 
   qe->getTriggerDatabase()->addTrigger( trNodes, t );
@@ -286,6 +288,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 
 Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node f,
                             Node n,
                             bool keepAll,
@@ -294,7 +297,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
 {
   std::vector< Node > nodes;
   nodes.push_back( n );
-  return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars);
+  return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars);
 }
 
 int Trigger::getActiveScore() {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index e2ce61bd1..21888ff8f 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -31,6 +31,7 @@ class QuantifiersEngine;
 
 namespace quantifiers {
 class QuantifiersInferenceManager;
+class QuantifiersRegistry;
 }
 
 namespace inst {
@@ -163,6 +164,7 @@ class Trigger {
   };
   static Trigger* mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node q,
                             std::vector<Node>& nodes,
                             bool keepAll = true,
@@ -171,6 +173,7 @@ class Trigger {
   /** single trigger version that calls the above function */
   static Trigger* mkTrigger(QuantifiersEngine* qe,
                             quantifiers::QuantifiersInferenceManager& qim,
+                            quantifiers::QuantifiersRegistry& qr,
                             Node q,
                             Node n,
                             bool keepAll = true,
@@ -194,6 +197,7 @@ class Trigger {
   /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
   Trigger(QuantifiersEngine* ie,
           quantifiers::QuantifiersInferenceManager& qim,
+          quantifiers::QuantifiersRegistry& qr,
           Node q,
           std::vector<Node>& nodes);
   /** add an instantiation (called by InstMatchGenerator)
@@ -243,6 +247,8 @@ class Trigger {
   QuantifiersEngine* d_quantEngine;
   /** Reference to the quantifiers inference manager */
   quantifiers::QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  quantifiers::QuantifiersRegistry& d_qreg;
   /** The quantified formula this trigger is for. */
   Node d_quant;
   /** match generator