Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by default in EPR mode.

1 files changed, 0 insertions, 10 deletions

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index d0bcd3a69..3017238ca 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -76,12 +76,6 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes )
     ++(qe->d_statistics.d_multi_triggers);
   }
   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
-  if( options::eagerInstQuant() ){
-    for( int i=0; i<(int)d_nodes.size(); i++ ){
-      Node op = qe->getTermDatabase()->getMatchOperator( d_nodes[i] );
-      qe->getTermDatabase()->registerTrigger( this, op );
-    }
-  }
   Trace("trigger-debug") << "Finished making trigger." << std::endl;
 }
 
@@ -107,10 +101,6 @@ bool Trigger::getMatch( Node f, Node t, InstMatch& m ){
   return ((InstMatchGenerator*)d_mg)->getMatch( f, t, m, d_quantEngine );
 }
 
-int Trigger::addTerm( Node t ){
-  return d_mg->addTerm( d_f, t, d_quantEngine );
-}
-
 Node Trigger::getInstPattern(){
   return NodeManager::currentNM()->mkNode( INST_PATTERN, d_nodes );
 }