More unused code elimination (#2358)

6 files changed, 2 insertions, 80 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 091c3b673..a16e03420 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -101,10 +101,6 @@ void InstMatch::clear() {
 }
 
 Node InstMatch::get(int i) const { return d_vals[i]; }
-void InstMatch::getInst(std::vector<Node>& inst) const
-{
-  inst.insert(inst.end(), d_vals.begin(), d_vals.end());
-}
 
 void InstMatch::setValue( int i, TNode n ) {
   d_vals[i] = n;
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 86138feb3..5695d1294 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -80,8 +80,6 @@ public:
   }
   /** get the i^th term in the instantiation */
   Node get(int i) const;
-  /** append the terms of this instantiation to inst */
-  void getInst(std::vector<Node>& inst) const;
   /** set/overwrites the i^th field in the instantiation with n */
   void setValue( int i, TNode n );
   /** set the i^th term in the instantiation to n
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 */
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index 75ae32318..21017e783 100644
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -39,7 +39,7 @@ class QuantRelevance : public QuantifiersUtil
    * if this is false, then all calls to getRelevance
    * return -1.
    */
-  QuantRelevance(bool cr) : d_computeRel(cr) {}
+  QuantRelevance() {}
   ~QuantRelevance() {}
   /** reset */
   bool reset(Theory::Effort e) override { return true; }
@@ -47,13 +47,6 @@ class QuantRelevance : public QuantifiersUtil
   void registerQuantifier(Node q) override;
   /** identify */
   std::string identify() const override { return "QuantRelevance"; }
-  /** set relevance of symbol s to r */
-  void setRelevance(Node s, int r);
-  /** get relevance of symbol s */
-  int getRelevance(Node s)
-  {
-    return d_relevance.find(s) == d_relevance.end() ? -1 : d_relevance[s];
-  }
   /** get number of quantifiers for symbol s */
   unsigned getNumQuantifiersForSymbol(Node s)
   {
@@ -61,8 +54,6 @@ class QuantRelevance : public QuantifiersUtil
   }
 
  private:
-  /** for computing relevance */
-  bool d_computeRel;
   /** map from quantifiers to symbols they contain */
   std::map<Node, std::vector<Node> > d_syms;
   /** map from symbols to quantifiers */
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index d0f156811..d1217d01d 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -42,27 +42,6 @@ void SygusUnif::initializeCandidate(
   d_strategy[f].initialize(qe, f, enums);
 }
 
-bool SygusUnif::constructSolution(std::vector<Node>& sols,
-                                  std::vector<Node>& lemmas)
-{
-  // initialize a call to construct solution
-  initializeConstructSol();
-  for (const Node& f : d_candidates)
-  {
-    // initialize a call to construct solution for function f
-    initializeConstructSolFor(f);
-    // call the virtual construct solution method
-    Node e = d_strategy[f].getRootEnumerator();
-    Node sol = constructSol(f, e, role_equal, 1, lemmas);
-    if (sol.isNull())
-    {
-      return false;
-    }
-    sols.push_back(sol);
-  }
-  return true;
-}
-
 Node SygusUnif::constructBestSolvedTerm(const std::vector<Node>& solved)
 {
   Assert(!solved.empty());
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index dd6922351..614a29d1c 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -85,7 +85,7 @@ class SygusUnif
    * channel by the caller.
    */
   virtual bool constructSolution(std::vector<Node>& sols,
-                                 std::vector<Node>& lemmas);
+                                 std::vector<Node>& lemmas) = 0;
 
  protected:
   /** reference to quantifier engine */