Remove miscellaneous dead and unused code from quantifiers (#2121)

1 files changed, 0 insertions, 37 deletions

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 3f2dc7cc6..cfcfcc5a5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -571,43 +571,6 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
   }
 }
 
-/*  TODO?
-bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
-  std::map< Node, bool >::iterator itq = d_quant.find( f );
-  if( itq==d_quant.end() ){
-    //generate triggers
-    Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f );
-    std::vector< Node > vars;
-    std::vector< Node > patTerms;
-    bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms );
-    if( ret ){
-      d_quant[f] = ret;
-      //add all variables to trigger that don't already occur
-      for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
-        Node x = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i );
-        if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
-          patTerms.push_back( x );
-        }
-      }
-      Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl;
-      for( unsigned i=0; i<patTerms.size(); i++ ){
-        Trace("local-t-ext") << "  " << patTerms[i] << std::endl;
-      }
-      Trace("local-t-ext") << std::endl;
-      Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD );
-      d_lte_trigger[f] = tr;
-    }else{
-      Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
-      Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl;
-    }
-    d_quant[f] = ret;
-    return ret;
-  }else{
-    return itq->second;
-  }
-}
-*/
-
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */