From 9c02423e90cf9cb8509d4ca6565acba06e6f9b2d Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Aug 2018 17:40:22 -0500
Subject:  More unused code elimination (#2358)

---
 src/theory/uf/theory_uf_strong_solver.h | 28 ----------------------------
 1 file changed, 28 deletions(-)

(limited to 'src/theory/uf/theory_uf_strong_solver.h')

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);
 
-- 
cgit v1.2.3