Refactor construction of triggers (#6209)

This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.

27 files changed, 528 insertions, 443 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 44ba4e261..febb34281 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -693,6 +693,8 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/pattern_term_selector.h
   theory/quantifiers/ematching/trigger.cpp
   theory/quantifiers/ematching/trigger.h
+  theory/quantifiers/ematching/trigger_database.cpp
+  theory/quantifiers/ematching/trigger_database.h
   theory/quantifiers/ematching/trigger_term_info.cpp
   theory/quantifiers/ematching/trigger_term_info.h
   theory/quantifiers/ematching/trigger_trie.cpp
@@ -763,6 +765,8 @@ libcvc4_add_sources(
   theory/quantifiers/quantifiers_rewriter.h
   theory/quantifiers/quantifiers_state.cpp
   theory/quantifiers/quantifiers_state.h
+  theory/quantifiers/quantifiers_statistics.cpp
+  theory/quantifiers/quantifiers_statistics.h
   theory/quantifiers/query_generator.cpp
   theory/quantifiers/query_generator.h
   theory/quantifiers/relevant_domain.cpp
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 4cdce940e..a2885cdec 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -34,7 +34,6 @@ namespace quantifiers {
 namespace inst {
 
 HigherOrderTrigger::HigherOrderTrigger(
-    QuantifiersEngine* qe,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
     QuantifiersRegistry& qr,
@@ -42,7 +41,7 @@ HigherOrderTrigger::HigherOrderTrigger(
     Node q,
     std::vector<Node>& nodes,
     std::map<Node, std::vector<Node> >& ho_apps)
-    : Trigger(qe, qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps)
+    : Trigger(qs, qim, qr, tr, q, nodes), d_ho_var_apps(ho_apps)
 {
   NodeManager* nm = NodeManager::currentNM();
   // process the higher-order variable applications
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index 87c7adeec..d3489783c 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -90,11 +90,8 @@ class Trigger;
  */
 class HigherOrderTrigger : public Trigger
 {
-  friend class Trigger;
-
- private:
-  HigherOrderTrigger(QuantifiersEngine* qe,
-                     QuantifiersState& qs,
+ public:
+  HigherOrderTrigger(QuantifiersState& qs,
                      QuantifiersInferenceManager& qim,
                      QuantifiersRegistry& qr,
                      TermRegistry& tr,
@@ -103,7 +100,6 @@ class HigherOrderTrigger : public Trigger
                      std::map<Node, std::vector<Node> >& ho_apps);
   virtual ~HigherOrderTrigger();
 
- public:
   /** Collect higher order var apply terms
    *
    * Collect all top-level HO_APPLY terms in n whose head is a variable x in
@@ -224,23 +220,23 @@ class HigherOrderTrigger : public Trigger
 
   /** higher-order pattern unification algorithm
    *
-  * Sends an instantiation that is equivalent to m via
-  * d_quantEngine->addInstantiation(...),
-  * based on Huet's algorithm.
-  *
-  * This is a helper function of sendInstantiation( m ) above.
-  *
-  * var_index is the index of the variable in m that we are currently processing
-  *   i.e. we are processing the var_index^{th} higher-order variable.
-  *
-  * For example, say we are processing the match from (EX4) above.
-  *   when var_index = 0,1, we are processing possibilities for
-  *    instantiation of f1,f2 respectively.
-  */
+   * Sends an instantiation that is equivalent to m via
+   * Instantiate::addInstantiation(...),
+   * based on Huet's algorithm.
+   *
+   * This is a helper function of sendInstantiation( m ) above.
+   *
+   * var_index is the index of the variable in m that we are currently
+   * processing i.e. we are processing the var_index^{th} higher-order variable.
+   *
+   * For example, say we are processing the match from (EX4) above.
+   *   when var_index = 0,1, we are processing possibilities for
+   *    instantiation of f1,f2 respectively.
+   */
   bool sendInstantiation(std::vector<Node>& m, size_t var_index);
   /** higher-order pattern unification algorithm
    * Sends an instantiation that is equivalent to m via
-   * d_quantEngine->addInstantiation(...).
+   * Instantiate::addInstantiation(...).
    * This is a helper function of sendInstantiation( m, var_index ) above.
    *
    * var_index is the index of the variable in m that we are currently
diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp
index 48c07ba4d..06d17dea4 100644
--- a/src/theory/quantifiers/ematching/im_generator.cpp
+++ b/src/theory/quantifiers/ematching/im_generator.cpp
@@ -33,11 +33,6 @@ bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
   return d_tparent->sendInstantiation(m, id);
 }
 
-QuantifiersEngine* IMGenerator::getQuantifiersEngine()
-{
-  return d_tparent->d_quantEngine;
-}
-
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index efc65cdef..6968a0dee 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -114,8 +114,6 @@ protected:
  QuantifiersState& d_qstate;
  /** Reference to the term registry */
  TermRegistry& d_treg;
- // !!!!!!!!! temporarily available (project #15)
- QuantifiersEngine* getQuantifiersEngine();
 };/* class IMGenerator */
 
 }  // namespace inst
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index ac3e1b9be..3dee6de73 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -26,6 +26,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
@@ -74,7 +75,7 @@ int InstMatchGenerator::getActiveScore()
   if( d_match_pattern.isNull() ){
     return -1;
   }
-  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  quantifiers::TermDb* tdb = d_treg.getTermDatabase();
   if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
   {
     Node f = tdb->getMatchOperator(d_match_pattern);
@@ -157,7 +158,7 @@ void InstMatchGenerator::initialize(Node q,
   d_match_pattern_type = d_match_pattern.getType();
   Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is "
                           << d_match_pattern << std::endl;
-  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  quantifiers::TermDb* tdb = d_treg.getTermDatabase();
   d_match_pattern_op = tdb->getMatchOperator(d_match_pattern);
 
   // now, collect children of d_match_pattern
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index c7360d02f..ab30b4b2d 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -15,12 +15,11 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
-#include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 
@@ -66,7 +65,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple(Trigger* tparent,
     }
     d_match_pattern_arg_types.push_back(d_match_pattern[i].getType());
   }
-  TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  TermDb* tdb = d_treg.getTermDatabase();
   d_op = tdb->getMatchOperator(d_match_pattern);
 }
 
@@ -75,7 +74,7 @@ uint64_t InstMatchGeneratorSimple::addInstantiations(Node q)
 {
   uint64_t addedLemmas = 0;
   TNodeTrie* tat;
-  TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  TermDb* tdb = d_treg.getTermDatabase();
   if (d_eqc.isNull())
   {
     tat = tdb->getTermArgTrie(d_op);
@@ -188,7 +187,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
 
 int InstMatchGeneratorSimple::getActiveScore()
 {
-  TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
+  TermDb* tdb = d_treg.getTermDatabase();
   Node f = tdb->getMatchOperator(d_match_pattern);
   size_t ngt = tdb->getNumGroundTerms(f);
   Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) "
diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp
index 083331948..5e9899ec3 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy.cpp
@@ -20,12 +20,12 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-InstStrategy::InstStrategy(QuantifiersEngine* qe,
+InstStrategy::InstStrategy(inst::TriggerDatabase& td,
                            QuantifiersState& qs,
                            QuantifiersInferenceManager& qim,
                            QuantifiersRegistry& qr,
                            TermRegistry& tr)
-    : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
+    : d_td(td), d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
 {
 }
 InstStrategy::~InstStrategy() {}
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index cbe6e341b..9d304368c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -24,11 +24,12 @@
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
 namespace quantifiers {
 
+namespace inst {
+class TriggerDatabase;
+}
+
 class QuantifiersState;
 class QuantifiersInferenceManager;
 class QuantifiersRegistry;
@@ -49,7 +50,7 @@ enum class InstStrategyStatus
 class InstStrategy
 {
  public:
-  InstStrategy(QuantifiersEngine* qe,
+  InstStrategy(inst::TriggerDatabase& td,
                QuantifiersState& qs,
                QuantifiersInferenceManager& qim,
                QuantifiersRegistry& qr,
@@ -70,8 +71,8 @@ class InstStrategy
    * maintained by the quantifiers state.
    */
   options::UserPatMode getInstUserPatMode() const;
-  /** reference to the instantiation engine */
-  QuantifiersEngine* d_quantEngine;
+  /** reference to the trigger database */
+  inst::TriggerDatabase& d_td;
   /** The quantifiers state object */
   QuantifiersState& d_qstate;
   /** The quantifiers inference manager object */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index ba068230d..d489869ae 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -15,11 +15,11 @@
 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/trigger_database.h"
 #include "theory/quantifiers/quant_relevance.h"
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers_engine.h"
 #include "util/random.h"
 
 using namespace CVC4::kind;
@@ -62,13 +62,13 @@ struct sortTriggers {
 };
 
 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
-    QuantifiersEngine* qe,
+    inst::TriggerDatabase& td,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
     QuantifiersRegistry& qr,
     TermRegistry& tr,
     QuantRelevance* qrlv)
-    : InstStrategy(qe, qs, qim, qr, tr), d_quant_rel(qrlv)
+    : InstStrategy(td, qs, qim, qr, tr), d_quant_rel(qrlv)
 {
   //how to select trigger terms
   d_tr_strategy = options::triggerSelMode();
@@ -281,16 +281,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     Trigger* tr = NULL;
     if (d_is_single_trigger[patTerms[0]])
     {
-      tr = Trigger::mkTrigger(d_quantEngine,
-                              d_qstate,
-                              d_qim,
-                              d_qreg,
-                              d_treg,
-                              f,
-                              patTerms[0],
-                              false,
-                              Trigger::TR_RETURN_NULL,
-                              d_num_trigger_vars[f]);
+      tr = d_td.mkTrigger(f,
+                          patTerms[0],
+                          false,
+                          TriggerDatabase::TR_RETURN_NULL,
+                          d_num_trigger_vars[f]);
       d_single_trigger_gen[patTerms[0]] = true;
     }
     else
@@ -321,16 +316,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         d_made_multi_trigger[f] = true;
       }
       // will possibly want to get an old trigger
-      tr = Trigger::mkTrigger(d_quantEngine,
-                              d_qstate,
-                              d_qim,
-                              d_qreg,
-                              d_treg,
-                              f,
-                              patTerms,
-                              false,
-                              Trigger::TR_GET_OLD,
-                              d_num_trigger_vars[f]);
+      tr = d_td.mkTrigger(f,
+                          patTerms,
+                          false,
+                          TriggerDatabase::TR_GET_OLD,
+                          d_num_trigger_vars[f]);
     }
     if (tr == nullptr)
     {
@@ -366,16 +356,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                    <= nqfs_curr)
         {
           d_single_trigger_gen[patTerms[index]] = true;
-          Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
-                                            d_qstate,
-                                            d_qim,
-                                            d_qreg,
-                                            d_treg,
-                                            f,
-                                            patTerms[index],
-                                            false,
-                                            Trigger::TR_RETURN_NULL,
-                                            d_num_trigger_vars[f]);
+          Trigger* tr2 = d_td.mkTrigger(f,
+                                        patTerms[index],
+                                        false,
+                                        TriggerDatabase::TR_RETURN_NULL,
+                                        d_num_trigger_vars[f]);
           addTrigger(tr2, f);
           success = true;
         }
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index f4c74c43a..a17e7bbb5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -85,7 +85,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy
   std::map<Node, bool> d_hasUserPatterns;
 
  public:
-  InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
+  InstStrategyAutoGenTriggers(inst::TriggerDatabase& td,
                               QuantifiersState& qs,
                               QuantifiersInferenceManager& qim,
                               QuantifiersRegistry& qr,
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 412676ad4..a15baa5e4 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -15,8 +15,8 @@
 #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
 
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/trigger_database.h"
 #include "theory/quantifiers/quantifiers_state.h"
-#include "theory/quantifiers_engine.h"
 
 using namespace CVC4::kind;
 using namespace CVC4::theory::quantifiers::inst;
@@ -26,12 +26,12 @@ namespace theory {
 namespace quantifiers {
 
 InstStrategyUserPatterns::InstStrategyUserPatterns(
-    QuantifiersEngine* ie,
+    inst::TriggerDatabase& td,
     QuantifiersState& qs,
     QuantifiersInferenceManager& qim,
     QuantifiersRegistry& qr,
     TermRegistry& tr)
-    : InstStrategy(ie, qs, qim, qr, tr)
+    : InstStrategy(td, qs, qim, qr, tr)
 {
 }
 InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
@@ -107,15 +107,8 @@ 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_qstate,
-                                      d_qim,
-                                      d_qreg,
-                                      d_treg,
-                                      q,
-                                      ugw[i],
-                                      true,
-                                      Trigger::TR_RETURN_NULL);
+      Trigger* t =
+          d_td.mkTrigger(q, ugw[i], true, TriggerDatabase::TR_RETURN_NULL);
       if (t)
       {
         d_user_gen[q].push_back(t);
@@ -168,15 +161,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
     d_user_gen_wait[q].push_back(nodes);
     return;
   }
-  Trigger* t = Trigger::mkTrigger(d_quantEngine,
-                                  d_qstate,
-                                  d_qim,
-                                  d_qreg,
-                                  d_treg,
-                                  q,
-                                  nodes,
-                                  true,
-                                  Trigger::TR_MAKE_NEW);
+  Trigger* t = d_td.mkTrigger(q, nodes, true, TriggerDatabase::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 e63154a60..821d7de77 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -34,7 +34,7 @@ namespace quantifiers {
 class InstStrategyUserPatterns : public InstStrategy
 {
  public:
-  InstStrategyUserPatterns(QuantifiersEngine* qe,
+  InstStrategyUserPatterns(inst::TriggerDatabase& td,
                            QuantifiersState& qs,
                            QuantifiersInferenceManager& qim,
                            QuantifiersRegistry& qr,
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 1c301141c..9153d9280 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -42,6 +42,7 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
       d_isup(),
       d_i_ag(),
       d_quants(),
+      d_trdb(qs, qim, qr, tr),
       d_quant_rel(nullptr)
 {
   if (options::relevantTriggers())
@@ -53,14 +54,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
     // user-provided patterns
     if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
     {
-      d_isup.reset(
-          new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr, tr));
+      d_isup.reset(new InstStrategyUserPatterns(d_trdb, qs, qim, qr, tr));
       d_instStrategies.push_back(d_isup.get());
     }
 
     // auto-generated patterns
     d_i_ag.reset(new InstStrategyAutoGenTriggers(
-        d_quantEngine, qs, qim, qr, tr, d_quant_rel.get()));
+        d_trdb, qs, qim, qr, tr, d_quant_rel.get()));
     d_instStrategies.push_back(d_i_ag.get());
   }
 }
@@ -135,7 +135,7 @@ void InstantiationEngine::reset_round( Theory::Effort e ){
 
 void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
 {
-  CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
+  CodeTimer codeTimer(d_qstate.getStats().d_ematching_time);
   if (quant_e != QEFFORT_STANDARD)
   {
     return;
@@ -154,7 +154,7 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
   size_t nquant = m->getNumAssertedQuantifiers();
   for (size_t i = 0; i < nquant; i++)
   {
-    Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true);
+    Node q = m->getAssertedQuantifier(i, true);
     if (shouldProcess(q) && m->isQuantifierActive(q))
     {
       quantActive = true;
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 4042e3424..26df4f548 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -20,6 +20,7 @@
 #include <vector>
 
 #include "theory/quantifiers/ematching/inst_strategy.h"
+#include "theory/quantifiers/ematching/trigger_database.h"
 #include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_relevance.h"
 
@@ -31,22 +32,6 @@ class InstStrategyUserPatterns;
 class InstStrategyAutoGenTriggers;
 
 class InstantiationEngine : public QuantifiersModule {
- private:
-  /** instantiation strategies */
-  std::vector<InstStrategy*> d_instStrategies;
-  /** user-pattern instantiation strategy */
-  std::unique_ptr<InstStrategyUserPatterns> d_isup;
-  /** auto gen triggers; only kept for destructor cleanup */
-  std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag;
-
-  /** current processing quantified formulas */
-  std::vector<Node> d_quants;
-
-  /** is the engine incomplete for this quantifier */
-  bool isIncomplete(Node q);
-  /** do instantiation round */
-  void doInstantiationRound(Theory::Effort effort);
-
  public:
   InstantiationEngine(QuantifiersEngine* qe,
                       QuantifiersState& qs,
@@ -69,8 +54,22 @@ class InstantiationEngine : public QuantifiersModule {
   std::string identify() const override { return "InstEngine"; }
 
  private:
+  /** is the engine incomplete for this quantifier */
+  bool isIncomplete(Node q);
+  /** do instantiation round */
+  void doInstantiationRound(Theory::Effort effort);
   /** Return true if this module should process quantified formula q */
   bool shouldProcess(Node q);
+  /** instantiation strategies */
+  std::vector<InstStrategy*> d_instStrategies;
+  /** user-pattern instantiation strategy */
+  std::unique_ptr<InstStrategyUserPatterns> d_isup;
+  /** auto gen triggers; only kept for destructor cleanup */
+  std::unique_ptr<InstStrategyAutoGenTriggers> d_i_ag;
+  /** current processing quantified formulas */
+  std::vector<Node> d_quants;
+  /** all triggers will be stored in this database */
+  inst::TriggerDatabase d_trdb;
   /** for computing relevance of quantifiers */
   std::unique_ptr<QuantRelevance> d_quant_rel;
 }; /* class InstantiationEngine */
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index c93e1a99b..c739623bc 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -17,7 +17,6 @@
 #include "expr/skolem_manager.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/candidate_generator.h"
-#include "theory/quantifiers/ematching/ho_trigger.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 #include "theory/quantifiers/ematching/inst_match_generator_multi.h"
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
@@ -31,7 +30,6 @@
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
 #include "theory/valuation.h"
 
 using namespace CVC4::kind;
@@ -42,19 +40,13 @@ namespace quantifiers {
 namespace inst {
 
 /** trigger class constructor */
-Trigger::Trigger(QuantifiersEngine* qe,
-                 QuantifiersState& qs,
+Trigger::Trigger(QuantifiersState& qs,
                  QuantifiersInferenceManager& qim,
                  QuantifiersRegistry& qr,
                  TermRegistry& tr,
                  Node q,
                  std::vector<Node>& nodes)
-    : d_quantEngine(qe),
-      d_qstate(qs),
-      d_qim(qim),
-      d_qreg(qr),
-      d_treg(tr),
-      d_quant(q)
+    : d_qstate(qs), d_qim(qim), d_qreg(qr), d_treg(tr), d_quant(q)
 {
   // We must ensure that the ground subterms of the trigger have been
   // preprocessed.
@@ -74,14 +66,15 @@ Trigger::Trigger(QuantifiersEngine* qe,
       Trace("trigger") << "   " << n << std::endl;
     }
   }
+  QuantifiersStatistics& stats = qs.getStats();
   if( d_nodes.size()==1 ){
     if (TriggerTermInfo::isSimpleTrigger(d_nodes[0]))
     {
       d_mg = new InstMatchGeneratorSimple(this, q, d_nodes[0]);
-      ++(qe->d_statistics.d_triggers);
+      ++(stats.d_triggers);
     }else{
       d_mg = InstMatchGenerator::mkInstMatchGenerator(this, q, d_nodes[0]);
-      ++(qe->d_statistics.d_simple_triggers);
+      ++(stats.d_simple_triggers);
     }
   }else{
     if( options::multiTriggerCache() ){
@@ -97,7 +90,7 @@ Trigger::Trigger(QuantifiersEngine* qe,
         Trace("multi-trigger") << "   " << nc << std::endl;
       }
     }
-    ++(qe->d_statistics.d_multi_triggers);
+    ++(stats.d_multi_triggers);
   }
 
   Trace("trigger-debug") << "Finished making trigger." << std::endl;
@@ -162,163 +155,6 @@ bool Trigger::sendInstantiation(InstMatch& m, InferenceId id)
   return sendInstantiation(m.d_vals, id);
 }
 
-bool Trigger::mkTriggerTerms(Node q,
-                             std::vector<Node>& nodes,
-                             size_t nvars,
-                             std::vector<Node>& trNodes)
-{
-  //only take nodes that contribute variables to the trigger when added
-  std::vector< Node > temp;
-  temp.insert( temp.begin(), nodes.begin(), nodes.end() );
-  std::map< Node, bool > vars;
-  std::map< Node, std::vector< Node > > patterns;
-  size_t varCount = 0;
-  std::map< Node, std::vector< Node > > varContains;
-  for (const Node& pat : temp)
-  {
-    TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
-  }
-  for (const Node& t : temp)
-  {
-    const std::vector<Node>& vct = varContains[t];
-    bool foundVar = false;
-    for (const Node& v : vct)
-    {
-      Assert(TermUtil::getInstConstAttr(v) == q);
-      if( vars.find( v )==vars.end() ){
-        varCount++;
-        vars[ v ] = true;
-        foundVar = true;
-      }
-    }
-    if( foundVar ){
-      trNodes.push_back(t);
-      for (const Node& v : vct)
-      {
-        patterns[v].push_back(t);
-      }
-    }
-    if (varCount == nvars)
-    {
-      break;
-    }
-  }
-  if (varCount < nvars)
-  {
-    Trace("trigger-debug") << "Don't consider trigger since it does not contain specified number of variables." << std::endl;
-    Trace("trigger-debug") << nodes << std::endl;
-    //do not generate multi-trigger if it does not contain all variables
-    return false;
-  }
-  // now, minimize the trigger
-  for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
-  {
-    bool keepPattern = false;
-    Node n = trNodes[i];
-    const std::vector<Node>& vcn = varContains[n];
-    for (const Node& v : vcn)
-    {
-      if (patterns[v].size() == 1)
-      {
-        keepPattern = true;
-        break;
-      }
-    }
-    if (!keepPattern)
-    {
-      // remove from pattern vector
-      for (const Node& v : vcn)
-      {
-        std::vector<Node>& pv = patterns[v];
-        for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
-        {
-          if (pv[k] == n)
-          {
-            pv.erase(pv.begin() + k, pv.begin() + k + 1);
-            break;
-          }
-        }
-      }
-      // remove from trigger nodes
-      trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
-      i--;
-    }
-  }
-  return true;
-}
-
-Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
-                            QuantifiersState& qs,
-                            QuantifiersInferenceManager& qim,
-                            QuantifiersRegistry& qr,
-                            TermRegistry& tr,
-                            Node f,
-                            std::vector<Node>& nodes,
-                            bool keepAll,
-                            int trOption,
-                            size_t useNVars)
-{
-  std::vector< Node > trNodes;
-  if( !keepAll ){
-    size_t nvars = useNVars == 0 ? f[0].getNumChildren() : useNVars;
-    if (!mkTriggerTerms(f, nodes, nvars, trNodes))
-    {
-      return nullptr;
-    }
-  }else{
-    trNodes.insert( trNodes.begin(), nodes.begin(), nodes.end() );
-  }
-
-  //check for duplicate?
-  if( trOption!=TR_MAKE_NEW ){
-    Trigger* t = qe->getTriggerDatabase()->getTrigger( trNodes );
-    if( t ){
-      if( trOption==TR_GET_OLD ){
-        //just return old trigger
-        return t;
-      }else{
-        return nullptr;
-      }
-    }
-  }
-
-  // check if higher-order
-  Trace("trigger-debug") << "Collect higher-order variable triggers..."
-                         << std::endl;
-  std::map<Node, std::vector<Node> > ho_apps;
-  HigherOrderTrigger::collectHoVarApplyTerms(f, trNodes, ho_apps);
-  Trace("trigger-debug") << "...got " << ho_apps.size()
-                         << " higher-order applications." << std::endl;
-  Trigger* t;
-  if (!ho_apps.empty())
-  {
-    t = new HigherOrderTrigger(qe, qs, qim, qr, tr, f, trNodes, ho_apps);
-  }
-  else
-  {
-    t = new Trigger(qe, qs, qim, qr, tr, f, trNodes);
-  }
-
-  qe->getTriggerDatabase()->addTrigger( trNodes, t );
-  return t;
-}
-
-Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
-                            QuantifiersState& qs,
-                            QuantifiersInferenceManager& qim,
-                            QuantifiersRegistry& qr,
-                            TermRegistry& tr,
-                            Node f,
-                            Node n,
-                            bool keepAll,
-                            int trOption,
-                            size_t useNVars)
-{
-  std::vector< Node > nodes;
-  nodes.push_back( n );
-  return mkTrigger(qe, qs, qim, qr, tr, f, nodes, keepAll, trOption, useNVars);
-}
-
 int Trigger::getActiveScore() { return d_mg->getActiveScore(); }
 
 Node Trigger::ensureGroundTermPreprocessed(Valuation& val,
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index 3c218ca7b..5dd8db452 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -102,6 +102,13 @@ class Trigger {
   friend class IMGenerator;
 
  public:
+  /** trigger constructor */
+  Trigger(QuantifiersState& qs,
+          QuantifiersInferenceManager& qim,
+          QuantifiersRegistry& qr,
+          TermRegistry& tr,
+          Node q,
+          std::vector<Node>& nodes);
   virtual ~Trigger();
   /** get the generator associated with this trigger */
   IMGenerator* getGenerator() { return d_mg; }
@@ -144,67 +151,8 @@ class Trigger {
   int getActiveScore();
   /** print debug information for the trigger */
   void debugPrint(const char* c) const;
-  /** mkTrigger method
-   *
-   * This makes an instance of a trigger object.
-   *  qe     : pointer to the quantifier engine;
-   *  q      : the quantified formula we are making a trigger for
-   *  nodes  : the nodes comprising the (multi-)trigger
-   *  keepAll: don't remove unneeded patterns;
-   *  trOption : policy for dealing with triggers that already exist
-   *             (see below)
-   *  useNVars : number of variables that should be bound by the trigger
-   *             typically, the number of quantified variables in q.
-   */
-  enum{
-    TR_MAKE_NEW,    //make new trigger even if it already may exist
-    TR_GET_OLD,     //return a previous trigger if it had already been created
-    TR_RETURN_NULL  //return null if a duplicate is found
-  };
-  static Trigger* mkTrigger(QuantifiersEngine* qe,
-                            QuantifiersState& qs,
-                            QuantifiersInferenceManager& qim,
-                            QuantifiersRegistry& qr,
-                            TermRegistry& tr,
-                            Node q,
-                            std::vector<Node>& nodes,
-                            bool keepAll = true,
-                            int trOption = TR_MAKE_NEW,
-                            size_t useNVars = 0);
-  /** single trigger version that calls the above function */
-  static Trigger* mkTrigger(QuantifiersEngine* qe,
-                            QuantifiersState& qs,
-                            QuantifiersInferenceManager& qim,
-                            QuantifiersRegistry& qr,
-                            TermRegistry& tr,
-                            Node q,
-                            Node n,
-                            bool keepAll = true,
-                            int trOption = TR_MAKE_NEW,
-                            size_t useNVars = 0);
-  /** make trigger terms
-   *
-   * This takes a set of eligible trigger terms and stores a subset of them in
-   * trNodes, such that :
-   *   (1) the terms in trNodes contain at least n_vars of the quantified
-   *       variables in quantified formula q, and
-   *   (2) the set trNodes is minimal, i.e. removing one term from trNodes
-   *       always violates (1).
-   */
-  static bool mkTriggerTerms(Node q,
-                             std::vector<Node>& nodes,
-                             size_t nvars,
-                             std::vector<Node>& trNodes);
 
  protected:
-  /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
-  Trigger(QuantifiersEngine* ie,
-          QuantifiersState& qs,
-          QuantifiersInferenceManager& qim,
-          QuantifiersRegistry& qr,
-          TermRegistry& tr,
-          Node q,
-          std::vector<Node>& nodes);
   /** add an instantiation (called by InstMatchGenerator)
    *
    * This calls Instantiate::addInstantiation(...) for instantiations
@@ -250,8 +198,6 @@ class Trigger {
    * This example would fail to match when f(a) is not registered.
    */
   std::vector<Node> d_groundTerms;
-  // !!!!!!!!!!!!!!!!!! temporarily available (project #15)
-  QuantifiersEngine* d_quantEngine;
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
   /** Reference to the quantifiers inference manager */
diff --git a/src/theory/quantifiers/ematching/trigger_database.cpp b/src/theory/quantifiers/ematching/trigger_database.cpp
new file mode 100644
index 000000000..fae7a10a0
--- /dev/null
+++ b/src/theory/quantifiers/ematching/trigger_database.cpp
@@ -0,0 +1,188 @@
+/*********************                                                        */
+/*! \file trigger_database.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief trigger database class
+ **/
+
+#include "theory/quantifiers/ematching/trigger_database.h"
+
+#include "theory/quantifiers/ematching/ho_trigger.h"
+#include "theory/quantifiers/ematching/trigger.h"
+#include "theory/quantifiers/term_util.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+TriggerDatabase::TriggerDatabase(QuantifiersState& qs,
+                                 QuantifiersInferenceManager& qim,
+                                 QuantifiersRegistry& qr,
+                                 TermRegistry& tr)
+    : d_qs(qs), d_qim(qim), d_qreg(qr), d_treg(tr)
+{
+}
+TriggerDatabase::~TriggerDatabase() {}
+
+Trigger* TriggerDatabase::mkTrigger(Node q,
+                                    const std::vector<Node>& nodes,
+                                    bool keepAll,
+                                    int trOption,
+                                    size_t useNVars)
+{
+  std::vector<Node> trNodes;
+  if (!keepAll)
+  {
+    size_t nvars = useNVars == 0 ? q[0].getNumChildren() : useNVars;
+    if (!mkTriggerTerms(q, nodes, nvars, trNodes))
+    {
+      return nullptr;
+    }
+  }
+  else
+  {
+    trNodes.insert(trNodes.begin(), nodes.begin(), nodes.end());
+  }
+
+  // check for duplicate?
+  if (trOption != TR_MAKE_NEW)
+  {
+    Trigger* t = d_trie.getTrigger(trNodes);
+    if (t)
+    {
+      if (trOption == TR_GET_OLD)
+      {
+        // just return old trigger
+        return t;
+      }
+      return nullptr;
+    }
+  }
+
+  // check if higher-order
+  Trace("trigger-debug") << "Collect higher-order variable triggers..."
+                         << std::endl;
+  std::map<Node, std::vector<Node> > hoApps;
+  HigherOrderTrigger::collectHoVarApplyTerms(q, trNodes, hoApps);
+  Trace("trigger-debug") << "...got " << hoApps.size()
+                         << " higher-order applications." << std::endl;
+  Trigger* t;
+  if (!hoApps.empty())
+  {
+    t = new HigherOrderTrigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes, hoApps);
+  }
+  else
+  {
+    t = new Trigger(d_qs, d_qim, d_qreg, d_treg, q, trNodes);
+  }
+  d_trie.addTrigger(trNodes, t);
+  return t;
+}
+
+Trigger* TriggerDatabase::mkTrigger(
+    Node q, Node n, bool keepAll, int trOption, size_t useNVars)
+{
+  std::vector<Node> nodes;
+  nodes.push_back(n);
+  return mkTrigger(q, nodes, keepAll, trOption, useNVars);
+}
+
+bool TriggerDatabase::mkTriggerTerms(Node q,
+                                     const std::vector<Node>& nodes,
+                                     size_t nvars,
+                                     std::vector<Node>& trNodes)
+{
+  // only take nodes that contribute variables to the trigger when added
+  std::map<Node, bool> vars;
+  std::map<Node, std::vector<Node> > patterns;
+  size_t varCount = 0;
+  std::map<Node, std::vector<Node> > varContains;
+  for (const Node& pat : nodes)
+  {
+    TermUtil::computeInstConstContainsForQuant(q, pat, varContains[pat]);
+  }
+  for (const Node& t : nodes)
+  {
+    const std::vector<Node>& vct = varContains[t];
+    bool foundVar = false;
+    for (const Node& v : vct)
+    {
+      Assert(TermUtil::getInstConstAttr(v) == q);
+      if (vars.find(v) == vars.end())
+      {
+        varCount++;
+        vars[v] = true;
+        foundVar = true;
+      }
+    }
+    if (foundVar)
+    {
+      trNodes.push_back(t);
+      for (const Node& v : vct)
+      {
+        patterns[v].push_back(t);
+      }
+    }
+    if (varCount == nvars)
+    {
+      break;
+    }
+  }
+  if (varCount < nvars)
+  {
+    Trace("trigger-debug") << "Don't consider trigger since it does not "
+                              "contain specified number of variables."
+                           << std::endl;
+    Trace("trigger-debug") << nodes << std::endl;
+    // do not generate multi-trigger if it does not contain all variables
+    return false;
+  }
+  // now, minimize the trigger
+  for (size_t i = 0, tsize = trNodes.size(); i < tsize; i++)
+  {
+    bool keepPattern = false;
+    Node n = trNodes[i];
+    const std::vector<Node>& vcn = varContains[n];
+    for (const Node& v : vcn)
+    {
+      if (patterns[v].size() == 1)
+      {
+        keepPattern = true;
+        break;
+      }
+    }
+    if (!keepPattern)
+    {
+      // remove from pattern vector
+      for (const Node& v : vcn)
+      {
+        std::vector<Node>& pv = patterns[v];
+        for (size_t k = 0, pvsize = pv.size(); k < pvsize; k++)
+        {
+          if (pv[k] == n)
+          {
+            pv.erase(pv.begin() + k, pv.begin() + k + 1);
+            break;
+          }
+        }
+      }
+      // remove from trigger nodes
+      trNodes.erase(trNodes.begin() + i, trNodes.begin() + i + 1);
+      i--;
+    }
+  }
+  return true;
+}
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h
new file mode 100644
index 000000000..21df0e536
--- /dev/null
+++ b/src/theory/quantifiers/ematching/trigger_database.h
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file trigger_database.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief trigger trie class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+#define CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/trigger_trie.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersInferenceManager;
+class QuantifiersState;
+class QuantifiersRegistry;
+class TermRegistry;
+
+namespace inst {
+
+/**
+ * A database of triggers, which manages how triggers are constructed.
+ */
+class TriggerDatabase
+{
+ public:
+  TriggerDatabase(QuantifiersState& qs,
+                  QuantifiersInferenceManager& qim,
+                  QuantifiersRegistry& qr,
+                  TermRegistry& tr);
+  ~TriggerDatabase();
+
+  /** mkTrigger method
+   *
+   * This makes an instance of a trigger object.
+   *  qe     : pointer to the quantifier engine;
+   *  q      : the quantified formula we are making a trigger for
+   *  nodes  : the nodes comprising the (multi-)trigger
+   *  keepAll: don't remove unneeded patterns;
+   *  trOption : policy for dealing with triggers that already exist
+   *             (see below)
+   *  useNVars : number of variables that should be bound by the trigger
+   *             typically, the number of quantified variables in q.
+   */
+  enum
+  {
+    TR_MAKE_NEW,    // make new trigger even if it already may exist
+    TR_GET_OLD,     // return a previous trigger if it had already been created
+    TR_RETURN_NULL  // return null if a duplicate is found
+  };
+  Trigger* mkTrigger(Node q,
+                     const std::vector<Node>& nodes,
+                     bool keepAll = true,
+                     int trOption = TR_MAKE_NEW,
+                     size_t useNVars = 0);
+  /** single trigger version that calls the above function */
+  Trigger* mkTrigger(Node q,
+                     Node n,
+                     bool keepAll = true,
+                     int trOption = TR_MAKE_NEW,
+                     size_t useNVars = 0);
+
+  /** make trigger terms
+   *
+   * This takes a set of eligible trigger terms and stores a subset of them in
+   * trNodes, such that :
+   *   (1) the terms in trNodes contain at least n_vars of the quantified
+   *       variables in quantified formula q, and
+   *   (2) the set trNodes is minimal, i.e. removing one term from trNodes
+   *       always violates (1).
+   */
+  static bool mkTriggerTerms(Node q,
+                             const std::vector<Node>& nodes,
+                             size_t nvars,
+                             std::vector<Node>& trNodes);
+
+ private:
+  /** The trigger trie, containing the triggers */
+  TriggerTrie d_trie;
+  /** Reference to the quantifiers state */
+  QuantifiersState& d_qs;
+  /** Reference to the quantifiers inference manager */
+  QuantifiersInferenceManager& d_qim;
+  /** The quantifiers registry */
+  QuantifiersRegistry& d_qreg;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
+};
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index c58bcc863..f2a41975f 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -22,16 +22,13 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
-namespace CVC4 {
-
-using namespace kind;
-using namespace context;
+using namespace CVC4::kind;
+using namespace CVC4::context;
 
+namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-using namespace inst;
-
 InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe,
                                    QuantifiersState& qs,
                                    QuantifiersInferenceManager& qim,
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 62f15a6a6..52096a8ec 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1988,7 +1988,7 @@ inline QuantConflictFind::Effort QcfEffortEnd() {
 /** check */
 void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
 {
-  CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
+  CodeTimer codeTimer(d_qstate.getStats().d_qcf_time);
   if (quant_e != QEFFORT_CONFLICT)
   {
     return;
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 5916c446c..be691ae27 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -156,6 +156,8 @@ void QuantifiersState::debugPrintEqualityEngine(const char* c) const
 
 const LogicInfo& QuantifiersState::getLogicInfo() const { return d_logicInfo; }
 
+QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; }
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
index 40101f3e3..6b4daec61 100644
--- a/src/theory/quantifiers/quantifiers_state.h
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -17,6 +17,7 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
 
+#include "theory/quantifiers/quantifiers_statistics.h"
 #include "theory/theory.h"
 #include "theory/theory_state.h"
 
@@ -56,6 +57,8 @@ class QuantifiersState : public TheoryState
   void debugPrintEqualityEngine(const char* c) const;
   /** get the logic info */
   const LogicInfo& getLogicInfo() const;
+  /** get the stats */
+  QuantifiersStatistics& getStats();
 
  private:
   /** The number of instantiation rounds in this SAT context */
@@ -77,6 +80,8 @@ class QuantifiersState : public TheoryState
   uint64_t d_instWhenPhase;
   /** Information about the logic we're operating within. */
   const LogicInfo& d_logicInfo;
+  /** The statistics */
+  QuantifiersStatistics d_statistics;
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp
new file mode 100644
index 000000000..4567a6d4f
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_statistics.cpp
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file quantifiers_statistics.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of quantifiers statistics class
+ **/
+
+#include "theory/quantifiers/quantifiers_statistics.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+QuantifiersStatistics::QuantifiersStatistics()
+    : d_time("theory::QuantifiersEngine::time"),
+      d_qcf_time("theory::QuantifiersEngine::time_qcf"),
+      d_ematching_time("theory::QuantifiersEngine::time_ematching"),
+      d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
+      d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
+      d_instantiation_rounds_lc(
+          "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
+      d_triggers("QuantifiersEngine::Triggers", 0),
+      d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
+      d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
+      d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
+{
+  smtStatisticsRegistry()->registerStat(&d_time);
+  smtStatisticsRegistry()->registerStat(&d_qcf_time);
+  smtStatisticsRegistry()->registerStat(&d_ematching_time);
+  smtStatisticsRegistry()->registerStat(&d_num_quant);
+  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
+  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
+  smtStatisticsRegistry()->registerStat(&d_triggers);
+  smtStatisticsRegistry()->registerStat(&d_simple_triggers);
+  smtStatisticsRegistry()->registerStat(&d_multi_triggers);
+  smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
+}
+
+QuantifiersStatistics::~QuantifiersStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_time);
+  smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
+  smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
+  smtStatisticsRegistry()->unregisterStat(&d_num_quant);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
+  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
+  smtStatisticsRegistry()->unregisterStat(&d_triggers);
+  smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
+  smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
+  smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h
new file mode 100644
index 000000000..1fa053484
--- /dev/null
+++ b/src/theory/quantifiers/quantifiers_statistics.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file quantifiers_statistics.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Quantifiers statistics class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+
+#include "util/statistics_registry.h"
+#include "util/stats_timer.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Statistics class for quantifiers, which contains all statistics that need
+ * to be tracked globally within the quantifiers theory.
+ */
+class QuantifiersStatistics
+{
+ public:
+  QuantifiersStatistics();
+  ~QuantifiersStatistics();
+  TimerStat d_time;
+  TimerStat d_qcf_time;
+  TimerStat d_ematching_time;
+  IntStat d_num_quant;
+  IntStat d_instantiation_rounds;
+  IntStat d_instantiation_rounds_lc;
+  IntStat d_triggers;
+  IntStat d_simple_triggers;
+  IntStat d_multi_triggers;
+  IntStat d_red_alpha_equiv;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0155eb05a..17a76468c 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -19,8 +19,6 @@
 #include "options/smt_options.h"
 #include "options/uf_options.h"
 #include "smt/smt_engine_scope.h"
-#include "smt/smt_statistics_registry.h"
-#include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/equality_query.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
@@ -32,13 +30,11 @@
 #include "theory/quantifiers/quantifiers_registry.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/quantifiers_statistics.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/skolemize.h"
-#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_registry.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
-#include "theory/uf/equality_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -59,7 +55,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_pnm(pnm),
       d_qreg(qr),
       d_treg(tr),
-      d_tr_trie(new quantifiers::inst::TriggerTrie),
       d_model(d_treg.getModel()),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext())
@@ -137,11 +132,6 @@ quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
 {
   return d_treg.getTermDatabase();
 }
-
-quantifiers::inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
-{
-  return d_tr_trie.get();
-}
 /// !!!!!!!!!!!!!!
 
 void QuantifiersEngine::presolve() {
@@ -186,7 +176,8 @@ void QuantifiersEngine::ppNotifyAssertions(
 }
 
 void QuantifiersEngine::check( Theory::Effort e ){
-  CodeTimer codeTimer(d_statistics.d_time);
+  quantifiers::QuantifiersStatistics& stats = d_qstate.getStats();
+  CodeTimer codeTimer(stats.d_time);
   Assert(d_qstate.getEqualityEngine() != nullptr);
   if (!d_qstate.getEqualityEngine()->consistent())
   {
@@ -332,9 +323,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     if( e==Theory::EFFORT_LAST_CALL ){
-      ++(d_statistics.d_instantiation_rounds_lc);
+      ++(stats.d_instantiation_rounds_lc);
     }else if( e==Theory::EFFORT_FULL ){
-      ++(d_statistics.d_instantiation_rounds);
+      ++(stats.d_instantiation_rounds);
     }
     Trace("quant-engine-debug") << "Check modules that needed check..." << std::endl;
     for (unsigned qef = QuantifiersModule::QEFFORT_CONFLICT;
@@ -511,7 +502,7 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) {
         id = InferenceId::QUANTIFIERS_REDUCE_ALPHA_EQ;
         if( !lem.isNull() ){
           Trace("quant-engine-red") << "...alpha equivalence success." << std::endl;
-          ++(d_statistics.d_red_alpha_equiv);
+          ++(d_qstate.getStats().d_red_alpha_equiv);
         }
       }
       d_quants_red_lem[q] = lem;
@@ -535,7 +526,7 @@ void QuantifiersEngine::registerQuantifierInternal(Node f)
     Trace("quant") << "QuantifiersEngine : Register quantifier ";
     Trace("quant") << " : " << f << std::endl;
     size_t prev_lemma_waiting = d_qim.numPendingLemmas();
-    ++(d_statistics.d_num_quant);
+    ++(d_qstate.getStats().d_num_quant);
     Assert(f.getKind() == FORALL);
     // register with utilities
     for (unsigned i = 0; i < d_util.size(); i++)
@@ -666,44 +657,6 @@ void QuantifiersEngine::getSkolemTermVectors(
   d_qim.getSkolemize()->getSkolemTermVectors(sks);
 }
 
-QuantifiersEngine::Statistics::Statistics()
-    : d_time("theory::QuantifiersEngine::time"),
-      d_qcf_time("theory::QuantifiersEngine::time_qcf"),
-      d_ematching_time("theory::QuantifiersEngine::time_ematching"),
-      d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
-      d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
-      d_instantiation_rounds_lc(
-          "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
-      d_triggers("QuantifiersEngine::Triggers", 0),
-      d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
-      d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
-      d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
-{
-  smtStatisticsRegistry()->registerStat(&d_time);
-  smtStatisticsRegistry()->registerStat(&d_qcf_time);
-  smtStatisticsRegistry()->registerStat(&d_ematching_time);
-  smtStatisticsRegistry()->registerStat(&d_num_quant);
-  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
-  smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
-  smtStatisticsRegistry()->registerStat(&d_triggers);
-  smtStatisticsRegistry()->registerStat(&d_simple_triggers);
-  smtStatisticsRegistry()->registerStat(&d_multi_triggers);
-  smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
-}
-
-QuantifiersEngine::Statistics::~Statistics(){
-  smtStatisticsRegistry()->unregisterStat(&d_time);
-  smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
-  smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
-  smtStatisticsRegistry()->unregisterStat(&d_num_quant);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
-  smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
-  smtStatisticsRegistry()->unregisterStat(&d_triggers);
-  smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
-  smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
-  smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
-}
-
 Node QuantifiersEngine::getNameForQuant(Node q) const
 {
   return d_qreg.getNameForQuant(q);
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index cb60c8e88..15ea004e2 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -24,7 +24,6 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 #include "theory/quantifiers/quant_util.h"
-#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -38,10 +37,6 @@ class RepSetIterator;
 
 namespace quantifiers {
 
-namespace inst {
-class TriggerTrie;
-}
-
 class FirstOrderModel;
 class Instantiate;
 class QModelBuilder;
@@ -60,8 +55,6 @@ class TermRegistry;
 class QuantifiersEngine {
   friend class ::CVC4::TheoryEngine;
   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-  typedef context::CDList<Node> NodeList;
-  typedef context::CDList<bool> BoolList;
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
@@ -92,8 +85,6 @@ class QuantifiersEngine {
   quantifiers::FirstOrderModel* getModel() const;
   /** get term database sygus */
   quantifiers::TermDbSygus* getTermDatabaseSygus() const;
-  /** get trigger database */
-  quantifiers::inst::TriggerTrie* getTriggerDatabase() const;
   //---------------------- end utilities
  private:
   //---------------------- private initialization
@@ -191,25 +182,6 @@ public:
 
  //----------end user interface for instantiations
 
- /** statistics class */
- class Statistics
- {
-  public:
-    TimerStat d_time;
-    TimerStat d_qcf_time;
-    TimerStat d_ematching_time;
-    IntStat d_num_quant;
-    IntStat d_instantiation_rounds;
-    IntStat d_instantiation_rounds_lc;
-    IntStat d_triggers;
-    IntStat d_simple_triggers;
-    IntStat d_multi_triggers;
-    IntStat d_red_alpha_equiv;
-    Statistics();
-    ~Statistics();
-  };/* class QuantifiersEngine::Statistics */
-  Statistics d_statistics;
-
  private:
   /** The quantifiers state object */
   quantifiers::QuantifiersState& d_qstate;
@@ -230,8 +202,6 @@ public:
   quantifiers::QuantifiersRegistry& d_qreg;
   /** The term registry */
   quantifiers::TermRegistry& d_treg;
-  /** all triggers will be stored in this trie */
-  std::unique_ptr<quantifiers::inst::TriggerTrie> d_tr_trie;
   /** extended model object */
   quantifiers::FirstOrderModel* d_model;
   //------------- end quantifiers utilities