1 files changed, 1 insertions, 24 deletions
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index f2f013f1c..9304c84ae 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -19,6 +19,7 @@
 
 #include <vector>
 
+#include "theory/quantifiers/ematching/inst_strategy.h"
 #include "theory/quantifiers/quant_relevance.h"
 #include "theory/quantifiers/quant_util.h"
 
@@ -28,30 +29,6 @@ namespace quantifiers {
 
 class InstStrategyUserPatterns;
 class InstStrategyAutoGenTriggers;
-class InstStrategyFreeVariable;
-
-/** instantiation strategy class */
-class InstStrategy {
-public:
-  enum Status {
-    STATUS_UNFINISHED,
-    STATUS_UNKNOWN,
-  };/* enum Status */
-protected:
-  /** reference to the instantiation engine */
-  QuantifiersEngine* d_quantEngine;
-public:
-  InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){}
-  virtual ~InstStrategy(){}
-  /** presolve */
-  virtual void presolve() {}
-  /** 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;
-  /** identify */
-  virtual std::string identify() const { return std::string("Unknown"); }
-};/* class InstStrategy */
 
 class InstantiationEngine : public QuantifiersModule {
  private: