More unused code elimination (#2358)

9 files changed, 11 insertions, 264 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 */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8c43e98ff..a5cd95d29 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -135,7 +135,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
   if( options::relevantTriggers() ){
-    d_quant_rel = new quantifiers::QuantRelevance(false);
+    d_quant_rel = new quantifiers::QuantRelevance;
     d_util.push_back(d_quant_rel);
   }else{
     d_quant_rel = NULL;
@@ -563,9 +563,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
 
     if( e==Theory::EFFORT_LAST_CALL ){
-      //if effort is last call, try to minimize model first
-      //uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver();
-      //if( ufss && !ufss->minimize() ){ return; }
       ++(d_statistics.d_instantiation_rounds_lc);
     }else if( e==Theory::EFFORT_FULL ){
       ++(d_statistics.d_instantiation_rounds);
@@ -908,18 +905,6 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool within
       {
         d_sygus_tdb->getEvalUnfold()->registerEvalTerm(n);
       }
-
-      // added contains also the Node that just have been asserted in this
-      // branch
-      if (d_quant_rel)
-      {
-        for (std::set<Node>::iterator i = added.begin(), end = added.end();
-             i != end;
-             i++)
-        {
-          d_quant_rel->setRelevance( i->getOperator(), 0 );
-        }
-      }
     }
   }
 }
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 65f7238c9..4efa6c2ce 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -23,7 +23,6 @@
 #include "theory/theory_model.h"
 
 //#define ONE_SPLIT_REGION
-//#define DISABLE_QUICK_CLIQUE_CHECKS
 //#define COMBINE_REGIONS_SMALL_INTO_LARGE
 //#define LAZY_REL_EQC
 
@@ -379,21 +378,6 @@ bool Region::check( Theory::Effort level, int cardinality,
   return false;
 }
 
-bool Region::getCandidateClique( int cardinality, std::vector< Node >& clique )
-{
-  if( d_testCliqueSize>=unsigned(cardinality+1) ){
-    //test clique is a clique
-    for( NodeBoolMap::iterator it = d_testClique.begin();
-         it != d_testClique.end(); ++it ){
-      if( (*it).second ){
-        clique.push_back( (*it).first );
-      }
-    }
-    return true;
-  }
-  return false;
-}
-
 void Region::getNumExternalDisequalities(
     std::map< Node, int >& num_ext_disequalities ){
   for( Region::iterator it = begin(); it != end(); ++it ){
@@ -713,25 +697,16 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
           //see if we have any recommended splits from large regions
           for( int i=0; i<(int)d_regions_index; i++ ){
             if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){
-              //just add the clique lemma
-              if( level==Theory::EFFORT_FULL && options::ufssCliqueSplits() ){
-                std::vector< Node > clique;
-                if( d_regions[i]->getCandidateClique( d_cardinality, clique ) ){
-                  //add clique lemma
-                  addCliqueLemma( clique, out );
-                  return;
-                }
-              }else{
-                int sp = addSplit( d_regions[i], out );
-                if( sp==1 ){
-                  addedLemma = true;
+
+              int sp = addSplit( d_regions[i], out );
+              if( sp==1 ){
+                addedLemma = true;
 #ifdef ONE_SPLIT_REGION
-                  break;
+                break;
 #endif
-                }else if( sp==-1 ){
-                  check( level, out );
-                  return;
-                }
+              }else if( sp==-1 ){
+                check( level, out );
+                return;
               }
             }
           }
@@ -815,67 +790,6 @@ Node SortModel::getNextDecisionRequest(){
   return Node::null();
 }
 
-bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){
-  if( options::ufssTotality() ){
-    //do nothing
-  }else{
-    if( m ){
-#if 0
-      // ensure that the constructed model is minimal
-      // if the model has terms that the strong solver does not know about
-      if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){
-        eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() );
-        while( !eqcs_i.isFinished() ){
-          Node eqc = (*eqcs_i);
-          if( eqc.getType()==d_type ){
-            //we must ensure that this equivalence class has been accounted for
-            if( d_regions_map.find( eqc )==d_regions_map.end() ){
-              //split on unaccounted for term and cardinality lemma term (as default)
-              Node splitEq = eqc.eqNode( d_cardinality_term );
-              splitEq = Rewriter::rewrite( splitEq );
-              Trace("uf-ss-minimize") << "Last chance minimize : " << splitEq << std::endl;
-              out->split( splitEq );
-              //tell the sat solver to explore the equals branch first
-              out->requirePhase( splitEq, true );
-              ++( d_thss->d_statistics.d_split_lemmas );
-              return false;
-            }
-          }
-          ++eqcs_i;
-        }
-        Assert( false );
-      }
-#endif
-    }else{
-      Trace("uf-ss-debug")  << "Minimize the UF model..." << std::endl;
-      //internal minimize, ensure that model forms a clique:
-      // if two equivalence classes are neither equal nor disequal, add a split
-      int validRegionIndex = -1;
-      for( int i=0; i<(int)d_regions_index; i++ ){
-        if( d_regions[i]->valid() ){
-          if( validRegionIndex!=-1 ){
-            combineRegions( validRegionIndex, i );
-            if( addSplit( d_regions[validRegionIndex], out )!=0 ){
-              Trace("uf-ss-debug") << "Minimize model : combined regions, found split. " << std::endl;
-              return false;
-            }
-          }else{
-            validRegionIndex = i;
-          }
-        }
-      }
-      Assert( validRegionIndex!=-1 );
-      if( addSplit( d_regions[validRegionIndex], out )!=0 ){
-        Trace("uf-ss-debug") << "Minimize model : found split. " << std::endl;
-        return false;
-      }
-      Trace("uf-ss-debug") << "Minimize success. " << std::endl;
-    }
-  }
-  return true;
-}
-
-
 int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){
   int ni = d_regions_map[n];
   int counter = 0;
@@ -950,21 +864,6 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){
         }
       }
     }else{
-      /*
-      if( options::ufssModelInference() ){
-        //check if we are at decision level 0
-        if( d_th->d_valuation.getAssertionLevel()==0 ){
-          Trace("uf-ss-mi") << "We have proved that no models of size " << c << " for type " << d_type << " exist." << std::endl;
-          Trace("uf-ss-mi") << "  # Clique lemmas : " << d_cliques[c].size() << std::endl;
-          if( d_cliques[c].size()==1 ){
-            if( d_totality_terms[c+1].empty() ){
-              Trace("uf-ss-mi") << "*** Establish model" << std::endl;
-              //d_totality_terms[c+1].insert( d_totality_terms[c].begin(), d_cliques[c][0].begin(), d_cliques[c][0].end() );
-            }
-          }
-        }
-      }
-      */
       //see if we need to request a new cardinality
       if( !d_hasCard ){
         bool needsCard = true;
@@ -1248,12 +1147,6 @@ void SortModel::addCliqueLemma( std::vector< Node >& clique, OutputChannel* out
   while( clique.size()>size_t(d_cardinality+1) ){
     clique.pop_back();
   }
-  //debugging information
-  if( Trace.isOn("uf-ss-cliques") ){
-    std::vector< Node > clique_vec;
-    clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() );
-    addClique( d_cardinality, clique_vec );
-  }
   // add as lemma
   std::vector<Node> eqs;
   for (unsigned i = 0, size = clique.size(); i < size; i++)
@@ -1323,25 +1216,14 @@ void SortModel::addTotalityAxiom( Node n, int cardinality, OutputChannel* out ){
   }
 }
 
-void SortModel::addClique( int c, std::vector< Node >& clique ) {
-  //if( d_clique_trie[c].add( clique ) ){
-  //  d_cliques[ c ].push_back( clique );
-  //}
-}
-
-
 /** apply totality */
 bool SortModel::applyTotality( int cardinality ){
   return options::ufssTotality() || cardinality<=options::ufssTotalityLimited();
-  // || ( options::ufssModelInference() && !d_totality_terms[cardinality].empty() );
 }
 
 /** get totality lemma terms */
 Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){
   return d_totality_terms[0][i];
-  //}else{
-  //  return d_totality_terms[cardinality][i];
-  //}
 }
 
 void SortModel::simpleCheckCardinality() {
@@ -1909,8 +1791,6 @@ SortModel* StrongSolverTheoryUF::getSortModel( Node n ){
   }
 }
 
-void StrongSolverTheoryUF::notifyRestart(){}
-
 /** get cardinality for sort */
 int StrongSolverTheoryUF::getCardinality( Node n ) {
   SortModel* c = getSortModel( n );
@@ -1929,18 +1809,6 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) {
   return -1;
 }
 
-bool StrongSolverTheoryUF::minimize( TheoryModel* m ){
-  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-    if( !it->second->minimize( d_out, m ) ){
-      return false;
-    }
-  }
-  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-    Trace("uf-ss-minimize") << "Cardinality( " << it->first << " ) : " << it->second->getCardinality() << std::endl;
-  }
-  return true;
-}
-
 //print debug
 void StrongSolverTheoryUF::debugPrint( const char* c ){
   //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine );
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 5108e7ba1..2e219da04 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -200,8 +200,6 @@ public:
       void getNumExternalDisequalities(std::map< Node, int >& num_ext_disequalities );
       /** check for cliques */
       bool check( Theory::Effort level, int cardinality, std::vector< Node >& clique );
-      /** get candidate clique */
-      bool getCandidateClique( int cardinality, std::vector< Node >& clique );
       //print debug
       void debugPrint( const char* c, bool incClique = false );
 
@@ -260,26 +258,6 @@ public:
     void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out );
     /** add totality axiom */
     void addTotalityAxiom( Node n, int cardinality, OutputChannel* out );
-
-    class NodeTrie {
-    public:
-      bool add( std::vector< Node >& n, unsigned i = 0 ){
-        Assert( i<n.size() );
-        if( i==(n.size()-1) ){
-          bool ret = d_children.find( n[i] )==d_children.end();
-          d_children[n[i]].d_children.clear();
-          return ret;
-        }else{
-          return d_children[n[i]].add( n, i+1 );
-        }
-      }
-    private:
-      std::map< Node, NodeTrie > d_children;
-    }; /* class NodeTrie */
-
-    std::map< int, NodeTrie > d_clique_trie;
-    void addClique( int c, std::vector< Node >& clique );
-
     /** Are we in conflict */
     context::CDO<bool> d_conflict;
     /** cardinality */
@@ -338,8 +316,6 @@ public:
     void propagate( Theory::Effort level, OutputChannel* out );
     /** get next decision request */
     Node getNextDecisionRequest();
-    /** minimize */
-    bool minimize( OutputChannel* out, TheoryModel* m );
     /** assert cardinality */
     void assertCardinality( OutputChannel* out, int c, bool val );
     /** is in conflict */
@@ -393,8 +369,6 @@ public:
   Node getNextDecisionRequest( unsigned& priority );
   /** preregister a term */
   void preRegisterTerm( TNode n );
-  /** notify restart */
-  void notifyRestart();
   /** identify */
   std::string identify() const { return std::string("StrongSolverTheoryUF"); }
   //print debug
@@ -407,8 +381,6 @@ public:
   int getCardinality( Node n );
   /** get cardinality for type */
   int getCardinality( TypeNode tn );
-  /** minimize */
-  bool minimize( TheoryModel* m = NULL );
   /** has eqc */
   bool hasEqc(Node a);