2 files changed, 0 insertions, 47 deletions
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 4fe5772de..433ceee85 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -322,34 +322,6 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
   }
 }
 
-#if 0
-
-void InstStrategyAddFailSplits::processResetInstantiationRound( Theory::Effort effort ){
-}
-
-int InstStrategyAddFailSplits::process( Node f, Theory::Effort effort, int e ){
-  if( e<4 ){
-    return STATUS_UNFINISHED;
-  }else{
-    for( std::map< Node, std::map< Node, std::vector< InstMatchGenerator* > > >::iterator it = InstMatchGenerator::d_match_fails.begin();
-         it != InstMatchGenerator::d_match_fails.end(); ++it ){
-      for( std::map< Node, std::vector< InstMatchGenerator* > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
-        if( !it2->second.empty() ){
-          Node n1 = it->first;
-          Node n2 = it2->first;
-          if( !d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ) && !d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ) ){
-            d_quantEngine->addSplitEquality( n1, n2, true );
-          }
-          it2->second.clear();
-        }
-      }
-    }
-    return STATUS_UNKNOWN;
-  }
-}
-
-#endif /* 0 */
-
 void InstStrategyFreeVariable::processResetInstantiationRound( Theory::Effort effort ){
 }
 
diff --git a/src/theory/uf/inst_strategy.h b/src/theory/uf/inst_strategy.h
index 5a3b9cc3d..aaa5f27a1 100644
--- a/src/theory/uf/inst_strategy.h
+++ b/src/theory/uf/inst_strategy.h
@@ -116,25 +116,6 @@ public:
   void setGenerateAdditional( bool val ) { d_generate_additional = val; }
 };/* class InstStrategyAutoGenTriggers */
 
-#if 0
-
-class InstStrategyAddFailSplits : public InstStrategy{
-private:
-  /** InstantiatorTheoryUf class */
-  InstantiatorTheoryUf* d_th;
-  /** process functions */
-  void processResetInstantiationRound( Theory::Effort effort );
-  int process( Node f, Theory::Effort effort, int e );
-public:
-  InstStrategyAddFailSplits( InstantiatorTheoryUf* th, QuantifiersEngine* ie ) :
-      InstStrategy( ie ), d_th( th ){}
-  ~InstStrategyAddFailSplits(){}
-  /** identify */
-  std::string identify() const { return std::string("AddFailSplits"); }
-};/* class InstStrategyAddFailSplits */
-
-#endif /* 0 */
-
 class InstStrategyFreeVariable : public InstStrategy{
 private:
   /** InstantiatorTheoryUf class */