Split E-matching strategies to own files (#5807)

Code move + format only

8 files changed, 340 insertions, 185 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 632adae1e..60e79fbe3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -658,8 +658,11 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/ho_trigger.h
   theory/quantifiers/ematching/inst_match_generator.cpp
   theory/quantifiers/ematching/inst_match_generator.h
+  theory/quantifiers/ematching/inst_strategy.h
   theory/quantifiers/ematching/inst_strategy_e_matching.cpp
   theory/quantifiers/ematching/inst_strategy_e_matching.h
+  theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+  theory/quantifiers/ematching/inst_strategy_e_matching_user.h
   theory/quantifiers/ematching/instantiation_engine.cpp
   theory/quantifiers/ematching/instantiation_engine.h
   theory/quantifiers/ematching/trigger.cpp
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
new file mode 100644
index 000000000..0a4c1b76f
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -0,0 +1,66 @@
+/*********************                                                        */
+/*! \file inst_strategy.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Instantiation Engine classes
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H
+#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H
+
+#include <vector>
+#include "expr/node.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+
+/** A status response to process */
+enum class InstStrategyStatus
+{
+  // the strategy is not finished
+  STATUS_UNFINISHED,
+  // the status of the strategy is unknown
+  STATUS_UNKNOWN,
+};
+
+/**
+ * A base class for instantiation strategies within E-matching.
+ */
+class InstStrategy
+{
+ 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 InstStrategyStatus process(Node f, Theory::Effort effort, int e) = 0;
+  /** identify */
+  virtual std::string identify() const { return std::string("Unknown"); }
+
+ protected:
+  /** reference to the instantiation engine */
+  QuantifiersEngine* d_quantEngine;
+}; /* class InstStrategy */
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8947370cd..8091eded5 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -13,24 +13,16 @@
  **/
 
 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
-#include "theory/quantifiers/ematching/inst_match_generator.h"
+
 #include "theory/quantifiers/quant_relevance.h"
-#include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
 #include "util/random.h"
 
-namespace CVC4 {
-
-using namespace kind;
-using namespace context;
+using namespace CVC4::kind;
+using namespace CVC4::theory::inst;
 
+namespace CVC4 {
 namespace theory {
-
-using namespace inst;
-
 namespace quantifiers {
 
 //priority levels :
@@ -65,116 +57,6 @@ struct sortTriggers {
   }
 };
 
-void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
-  Trace("inst-alg-debug") << "reset user triggers" << std::endl;
-  //reset triggers
-  for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
-  {
-    for (Trigger* t : u.second)
-    {
-      t->resetInstantiationRound();
-      t->reset(Node::null());
-    }
-  }
-  Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
-}
-
-int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
-  if( e==0 ){
-    return STATUS_UNFINISHED;
-  }
-  options::UserPatMode upm = d_quantEngine->getInstUserPatMode();
-  int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
-  if (e < peffort)
-  {
-    return STATUS_UNFINISHED;
-  }
-  if (e != peffort)
-  {
-    return STATUS_UNKNOWN;
-  }
-  d_counter[f]++;
-
-  Trace("inst-alg") << "-> User-provided instantiate " << f << "..."
-                    << std::endl;
-  if (upm == options::UserPatMode::RESORT)
-  {
-    std::vector<std::vector<Node> >& ugw = d_user_gen_wait[f];
-    for (size_t i = 0, usize = ugw.size(); i < usize; i++)
-    {
-      Trigger* t = Trigger::mkTrigger(
-          d_quantEngine, f, ugw[i], true, Trigger::TR_RETURN_NULL);
-      if (t)
-      {
-        d_user_gen[f].push_back(t);
-      }
-    }
-    ugw.clear();
-  }
-
-  std::vector<inst::Trigger*>& ug = d_user_gen[f];
-  for (Trigger* t : ug)
-  {
-    if (Trace.isOn("process-trigger"))
-    {
-      Trace("process-trigger") << "  Process (user) ";
-      t->debugPrint("process-trigger");
-      Trace("process-trigger") << "..." << std::endl;
-    }
-    unsigned numInst = t->addInstantiations();
-    Trace("process-trigger")
-        << "  Done, numInst = " << numInst << "." << std::endl;
-    d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
-    if (t->isMultiTrigger())
-    {
-      d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
-    }
-    if (d_quantEngine->inConflict())
-    {
-      // we are already in conflict
-      break;
-    }
-  }
-  return STATUS_UNKNOWN;
-}
-
-void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
-  Assert(pat.getKind() == INST_PATTERN);
-  //add to generators
-  std::vector< Node > nodes;
-  for (const Node& p : pat)
-  {
-    Node pat_use = Trigger::getIsUsableTrigger(p, q);
-    if( pat_use.isNull() ){
-      Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
-                            << " because of " << p << std::endl;
-      return;
-    }else{
-      nodes.push_back( pat_use );
-    }
-  }
-  Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
-  // check match option
-  if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
-  {
-    d_user_gen_wait[q].push_back(nodes);
-  }
-  else
-  {
-    Trigger* t =
-        Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW);
-    if (t)
-    {
-      d_user_gen[q].push_back(t);
-    }
-    else
-    {
-      Trace("trigger-warn") << "Failed to construct trigger : " << pat
-                            << " due to variable mismatch" << std::endl;
-    }
-  }
-}
-
 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
                                                          QuantRelevance* qr)
     : InstStrategy(qe), d_quant_rel(qr)
@@ -212,11 +94,14 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
   Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
 }
 
-int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
+InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
+                                                        Theory::Effort effort,
+                                                        int e)
+{
   options::UserPatMode upMode = d_quantEngine->getInstUserPatMode();
   if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
   {
-    return STATUS_UNKNOWN;
+    return InstStrategyStatus::STATUS_UNKNOWN;
   }
   int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
                  && upMode != options::UserPatMode::RESORT)
@@ -224,7 +109,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
                     : 1;
   if (e < peffort)
   {
-    return STATUS_UNFINISHED;
+    return InstStrategyStatus::STATUS_UNFINISHED;
   }
   Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
   bool gen = false;
@@ -328,7 +213,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       break;
     }
   }
-  return STATUS_UNKNOWN;
+  return InstStrategyStatus::STATUS_UNKNOWN;
 }
 
 void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 701d4ac74..d3c7c2c67 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -17,7 +17,7 @@
 #ifndef CVC4__INST_STRATEGY_E_MATCHING_H
 #define CVC4__INST_STRATEGY_E_MATCHING_H
 
-#include "theory/quantifiers/ematching/instantiation_engine.h"
+#include "theory/quantifiers/ematching/inst_strategy.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/quant_relevance.h"
 
@@ -25,35 +25,11 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-//instantiation strategies
-
-class InstStrategyUserPatterns : public InstStrategy{
-private:
-  /** explicitly provided patterns */
-  std::map< Node, std::vector< inst::Trigger* > > d_user_gen;
-  /** waiting to be generated patterns */
-  std::map< Node, std::vector< std::vector< Node > > > d_user_gen_wait;
-  /** counter for quantifiers */
-  std::map< Node, int > d_counter;
-  /** process functions */
-  void processResetInstantiationRound(Theory::Effort effort) override;
-  int process(Node f, Theory::Effort effort, int e) override;
-
- public:
-  InstStrategyUserPatterns( QuantifiersEngine* ie ) :
-      InstStrategy( ie ){}
-  ~InstStrategyUserPatterns(){}
-public:
-  /** add pattern */
-  void addUserPattern( Node q, Node pat );
-  /** get num patterns */
-  size_t getNumUserGenerators(Node q) { return d_user_gen[q].size(); }
-  /** get user pattern */
-  inst::Trigger* getUserGenerator(Node q, size_t i) { return d_user_gen[q][i]; }
-  /** identify */
-  std::string identify() const override { return std::string("UserPatterns"); }
-};/* class InstStrategyUserPatterns */
-
+/**
+ * This class is responsible for instantiating quantifiers based on
+ * automatically generated triggers. It selects pattern terms, generates
+ * and manages triggers, and uses a strategy for processing them.
+ */
 class InstStrategyAutoGenTriggers : public InstStrategy
 {
  public:
@@ -91,7 +67,8 @@ class InstStrategyAutoGenTriggers : public InstStrategy
  private:
   /** process functions */
   void processResetInstantiationRound(Theory::Effort effort) override;
-  int process(Node q, Theory::Effort effort, int e) override;
+  /** Process */
+  InstStrategyStatus process(Node q, Theory::Effort effort, int e) override;
   /**
    * Generate triggers for quantified formula q.
    */
@@ -111,7 +88,6 @@ class InstStrategyAutoGenTriggers : public InstStrategy
   InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
   ~InstStrategyAutoGenTriggers() {}
 
- public:
   /** get auto-generated trigger */
   inst::Trigger* getAutoGenTrigger(Node q);
   /** identify */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
new file mode 100644
index 000000000..f7f2531bb
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -0,0 +1,178 @@
+/*********************                                                        */
+/*! \file inst_strategy_e_matching_user.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of e matching instantiation strategies
+ **/
+
+#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
+
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+using namespace CVC4::theory::inst;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie)
+    : InstStrategy(ie)
+{
+}
+InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
+
+size_t InstStrategyUserPatterns::getNumUserGenerators(Node q) const
+{
+  std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+      d_user_gen.find(q);
+  if (it == d_user_gen.end())
+  {
+    return 0;
+  }
+  return it->second.size();
+}
+
+inst::Trigger* InstStrategyUserPatterns::getUserGenerator(Node q,
+                                                          size_t i) const
+{
+  std::map<Node, std::vector<inst::Trigger*> >::const_iterator it =
+      d_user_gen.find(q);
+  if (it == d_user_gen.end())
+  {
+    return nullptr;
+  }
+  Assert(i < it->second.size());
+  return it->second[i];
+}
+
+std::string InstStrategyUserPatterns::identify() const
+{
+  return std::string("UserPatterns");
+}
+
+void InstStrategyUserPatterns::processResetInstantiationRound(
+    Theory::Effort effort)
+{
+  Trace("inst-alg-debug") << "reset user triggers" << std::endl;
+  // reset triggers
+  for (std::pair<const Node, std::vector<Trigger*> >& u : d_user_gen)
+  {
+    for (Trigger* t : u.second)
+    {
+      t->resetInstantiationRound();
+      t->reset(Node::null());
+    }
+  }
+  Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
+}
+
+InstStrategyStatus InstStrategyUserPatterns::process(Node q,
+                                                     Theory::Effort effort,
+                                                     int e)
+{
+  if (e == 0)
+  {
+    return InstStrategyStatus::STATUS_UNFINISHED;
+  }
+  options::UserPatMode upm = d_quantEngine->getInstUserPatMode();
+  int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
+  if (e < peffort)
+  {
+    return InstStrategyStatus::STATUS_UNFINISHED;
+  }
+  if (e != peffort)
+  {
+    return InstStrategyStatus::STATUS_UNKNOWN;
+  }
+  d_counter[q]++;
+
+  Trace("inst-alg") << "-> User-provided instantiate " << q << "..."
+                    << std::endl;
+  if (upm == options::UserPatMode::RESORT)
+  {
+    std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
+    for (size_t i = 0, usize = ugw.size(); i < usize; i++)
+    {
+      Trigger* t = Trigger::mkTrigger(
+          d_quantEngine, q, ugw[i], true, Trigger::TR_RETURN_NULL);
+      if (t)
+      {
+        d_user_gen[q].push_back(t);
+      }
+    }
+    ugw.clear();
+  }
+
+  std::vector<inst::Trigger*>& ug = d_user_gen[q];
+  for (Trigger* t : ug)
+  {
+    if (Trace.isOn("process-trigger"))
+    {
+      Trace("process-trigger") << "  Process (user) ";
+      t->debugPrint("process-trigger");
+      Trace("process-trigger") << "..." << std::endl;
+    }
+    unsigned numInst = t->addInstantiations();
+    Trace("process-trigger")
+        << "  Done, numInst = " << numInst << "." << std::endl;
+    d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
+    if (t->isMultiTrigger())
+    {
+      d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
+    }
+    if (d_quantEngine->inConflict())
+    {
+      // we are already in conflict
+      break;
+    }
+  }
+  return InstStrategyStatus::STATUS_UNKNOWN;
+}
+
+void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
+{
+  Assert(pat.getKind() == INST_PATTERN);
+  // add to generators
+  std::vector<Node> nodes;
+  for (const Node& p : pat)
+  {
+    Node pat_use = Trigger::getIsUsableTrigger(p, q);
+    if (pat_use.isNull())
+    {
+      Trace("trigger-warn") << "User-provided trigger is not usable : " << pat
+                            << " because of " << p << std::endl;
+      return;
+    }
+    nodes.push_back(pat_use);
+  }
+  Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
+  // check match option
+  if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+  {
+    d_user_gen_wait[q].push_back(nodes);
+    return;
+  }
+  Trigger* t =
+      Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW);
+  if (t)
+  {
+    d_user_gen[q].push_back(t);
+  }
+  else
+  {
+    Trace("trigger-warn") << "Failed to construct trigger : " << pat
+                          << " due to variable mismatch" << std::endl;
+  }
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
new file mode 100644
index 000000000..ed0cd0ac6
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file inst_strategy_e_matching_user.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Andrew Reynolds, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The user-provided E matching instantiation strategy
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__INST_STRATEGY_E_MATCHING_USER_H
+#define CVC4__INST_STRATEGY_E_MATCHING_USER_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/inst_strategy.h"
+#include "theory/quantifiers/ematching/trigger.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * This class is responsible for adding instantiations based on user-provided
+ * triggers.
+ */
+class InstStrategyUserPatterns : public InstStrategy
+{
+ public:
+  InstStrategyUserPatterns(QuantifiersEngine* qe);
+  ~InstStrategyUserPatterns();
+  /** add pattern */
+  void addUserPattern(Node q, Node pat);
+  /** get num patterns */
+  size_t getNumUserGenerators(Node q) const;
+  /** get user pattern */
+  inst::Trigger* getUserGenerator(Node q, size_t i) const;
+  /** identify */
+  std::string identify() const override;
+
+ private:
+  /** reset instantiation round for the given effort */
+  void processResetInstantiationRound(Theory::Effort effort) override;
+  /** Process quantified formula q at the given effort */
+  InstStrategyStatus process(Node f, Theory::Effort effort, int e) override;
+  /** explicitly provided patterns */
+  std::map<Node, std::vector<inst::Trigger*> > d_user_gen;
+  /** waiting to be generated patterns */
+  std::map<Node, std::vector<std::vector<Node> > > d_user_gen_wait;
+  /** counter for quantifiers */
+  std::map<Node, int> d_counter;
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index ad9c53e0f..7eb5a1378 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
+#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -91,11 +92,16 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
         for( unsigned j=0; j<d_instStrategies.size(); j++ ){
           InstStrategy* is = d_instStrategies[j];
           Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
-          int quantStatus = is->process( q, effort, e_use );
-          Trace("inst-engine-debug") << " -> status is " << quantStatus << ", conflict=" << d_quantEngine->inConflict() << std::endl;
+          InstStrategyStatus quantStatus = is->process(q, effort, e_use);
+          Trace("inst-engine-debug")
+              << " -> unfinished= "
+              << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
+              << ", conflict=" << d_quantEngine->inConflict() << std::endl;
           if( d_quantEngine->inConflict() ){
             return;
-          }else if( quantStatus==InstStrategy::STATUS_UNFINISHED ){
+          }
+          else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
+          {
             finished = false;
           }
         }
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: