1 files changed, 0 insertions, 53 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 4d535a8af..1f55a4b90 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -820,40 +820,6 @@ namespace eq{
   class EqualityEngine;
 }
 
-/** instantiation strategy class */
-class InstStrategy {
-public:
-  enum Status {
-    STATUS_UNFINISHED,
-    STATUS_UNKNOWN,
-    STATUS_SAT,
-  };/* enum Status */
-protected:
-  /** reference to the instantiation engine */
-  QuantifiersEngine* d_quantEngine;
-
-
-public:
-  InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
-  virtual ~InstStrategy(){}
-
-  /** reset instantiation */
-  virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
-  /** process method, returns a status */
-  virtual int process( Node f, Theory::Effort effort, int e ) = 0;
-  /** update status */
-  static void updateStatus( int& currStatus, int addStatus ){
-    if( addStatus==STATUS_UNFINISHED ){
-      currStatus = STATUS_UNFINISHED;
-    }else if( addStatus==STATUS_UNKNOWN ){
-      if( currStatus==STATUS_SAT ){
-        currStatus = STATUS_UNKNOWN;
-      }
-    }
-  }
-  /** identify */
-  virtual std::string identify() const { return std::string("Unknown"); }
-};/* class InstStrategy */
 
 /** instantiator class */
 class Instantiator {
@@ -863,21 +829,6 @@ protected:
   QuantifiersEngine* d_quantEngine;
   /** reference to the theory that it looks at */
   Theory* d_th;
-  /** instantiation strategies */
-  std::vector< InstStrategy* > d_instStrategies;
-  /** instantiation strategies active */
-  std::map< InstStrategy*, bool > d_instStrategyActive;
-  /** has constraints from quantifier */
-  std::map< Node, bool > d_quantActive;
-  /** is instantiation strategy active */
-  bool isActiveStrategy( InstStrategy* is ) {
-    return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is];
-  }
-  /** add inst strategy */
-  void addInstStrategy( InstStrategy* is ){
-    d_instStrategies.push_back( is );
-    d_instStrategyActive[is] = true;
-  }
   /** reset instantiation round */
   virtual void processResetInstantiationRound( Theory::Effort effort ) = 0;
   /** process quantifier */
@@ -899,10 +850,6 @@ public:
   /** print debug information */
   virtual void debugPrint( const char* c ) {}
 public:
-  /** set has constraints from quantifier f */
-  void setQuantifierActive( Node f ) { d_quantActive[f] = true; }
-  /** has constraints from */
-  bool getQuantifierActive( Node f ) { return d_quantActive.find(f) != d_quantActive.end() && d_quantActive[f]; }
   /** reset instantiation round */
   void resetInstantiationRound( Theory::Effort effort );
   /** do instantiation method*/