Move quantifiers relevance module inside E-matching module (#3186)

1 files changed, 0 insertions, 10 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c17af1e1f..5bac55462 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -189,7 +189,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_eq_inference(nullptr),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
-      d_quant_rel(nullptr),
       d_rel_dom(nullptr),
       d_bv_invert(nullptr),
       d_builder(nullptr),
@@ -253,11 +252,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
-  if( options::relevantTriggers() ){
-    d_quant_rel.reset(new quantifiers::QuantRelevance);
-    d_util.push_back(d_quant_rel.get());
-  }
-
   if( options::quantEpr() ){
     Assert( !options::incrementalSolving() );
     d_qepr.reset(new quantifiers::QuantEPR);
@@ -351,10 +345,6 @@ quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const
 {
   return d_bv_invert.get();
 }
-quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const
-{
-  return d_quant_rel.get();
-}
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
   return d_builder.get();