1 files changed, 0 insertions, 42 deletions
diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp
index b9e4d0650..a05388d17 100644
--- a/src/theory/quantifiers/quant_relevance.cpp
+++ b/src/theory/quantifiers/quant_relevance.cpp
@@ -28,21 +28,6 @@ void QuantRelevance::registerQuantifier(Node f)
   std::vector<Node> syms;
   computeSymbols(f[1], syms);
   d_syms[f].insert(d_syms[f].begin(), syms.begin(), syms.end());
-  // set initial relevance
-  int minRelevance = -1;
-  for (int i = 0; i < (int)syms.size(); i++)
-  {
-    d_syms_quants[syms[i]].push_back(f);
-    int r = getRelevance(syms[i]);
-    if (r != -1 && (minRelevance == -1 || r < minRelevance))
-    {
-      minRelevance = r;
-    }
-  }
-  if (minRelevance != -1)
-  {
-    setRelevance(f, minRelevance + 1);
-  }
 }
 
 /** compute symbols */
@@ -65,33 +50,6 @@ void QuantRelevance::computeSymbols(Node n, std::vector<Node>& syms)
   }
 }
 
-/** set relevance */
-void QuantRelevance::setRelevance(Node s, int r)
-{
-  if (d_computeRel)
-  {
-    int rOld = getRelevance(s);
-    if (rOld == -1 || r < rOld)
-    {
-      d_relevance[s] = r;
-      if (s.getKind() == FORALL)
-      {
-        for (int i = 0; i < (int)d_syms[s].size(); i++)
-        {
-          setRelevance(d_syms[s][i], r);
-        }
-      }
-      else
-      {
-        for (int i = 0; i < (int)d_syms_quants[s].size(); i++)
-        {
-          setRelevance(d_syms_quants[s][i], r + 1);
-        }
-      }
-    }
-  }
-}
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */