New trigger options. --inst-no-entail on by default. Misc cleanup.

1 files changed, 0 insertions, 13 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 2d427ae0a..c69136933 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -40,21 +40,9 @@ public:
 protected:
   /** reference to the instantiation engine */
   QuantifiersEngine* d_quantEngine;
-  /** should process a quantifier */
-  std::map< Node, bool > d_quantActive;
-  /** calculate should process */
-  virtual bool calculateShouldProcess( Node f ) { return true; }
 public:
   InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
   virtual ~InstStrategy(){}
-
-  /** should process quantified formula f? */
-  bool shouldProcess( Node f ) {
-    if( d_quantActive.find( f )==d_quantActive.end() ){
-      d_quantActive[f] = calculateShouldProcess( f );
-    }
-    return d_quantActive[f];
-  }
   /** reset instantiation */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process method, returns a status */
@@ -131,7 +119,6 @@ public:
   public:
     IntStat d_instantiations_user_patterns;
     IntStat d_instantiations_auto_gen;
-    IntStat d_instantiations_auto_gen_min;
     IntStat d_instantiations_guess;
     IntStat d_instantiations_cbqi_arith;
     IntStat d_instantiations_cbqi_arith_minus;