Split inst match generator class to own file (#6125)

5 files changed, 170 insertions, 108 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e65e06da3..042969884 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -669,6 +669,8 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/candidate_generator.h
   theory/quantifiers/ematching/ho_trigger.cpp
   theory/quantifiers/ematching/ho_trigger.h
+  theory/quantifiers/ematching/im_generator.cpp
+  theory/quantifiers/ematching/im_generator.h
   theory/quantifiers/ematching/inst_match_generator.cpp
   theory/quantifiers/ematching/inst_match_generator.h
   theory/quantifiers/ematching/inst_match_generator_multi.cpp
diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp
new file mode 100644
index 000000000..829ccc8b1
--- /dev/null
+++ b/src/theory/quantifiers/ematching/im_generator.cpp
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file im_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 inst match generator base class
+ **/
+
+#include "theory/quantifiers/ematching/im_generator.h"
+
+#include "theory/quantifiers/ematching/trigger.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace inst {
+
+IMGenerator::IMGenerator(Trigger* tparent)
+    : d_tparent(tparent), d_qstate(tparent->d_qstate)
+{
+}
+
+bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
+{
+  return d_tparent->sendInstantiation(m, id);
+}
+
+QuantifiersEngine* IMGenerator::getQuantifiersEngine()
+{
+  return d_tparent->d_quantEngine;
+}
+
+
+}/* CVC4::theory::inst namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
new file mode 100644
index 000000000..6bf472cb5
--- /dev/null
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -0,0 +1,123 @@
+/*********************                                                        */
+/*! \file inst_match_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Mathias Preiner, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 inst match generator base class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
+#define CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
+
+#include <map>
+#include "expr/node.h"
+#include "theory/inference_id.h"
+#include "theory/quantifiers/inst_match.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+class QuantifiersState;
+}  // namespace quantifiers
+
+namespace inst {
+
+class Trigger;
+
+/** IMGenerator class
+*
+* Virtual base class for generating InstMatch objects, which correspond to
+* quantifier instantiations. The main use of this class is as a backend utility
+* to Trigger (see theory/quantifiers/ematching/trigger.h).
+*
+* Some functions below take as argument a pointer to the current quantifiers
+* engine, which is used for making various queries about what terms and
+* equalities exist in the current context.
+*
+* Some functions below take a pointer to a parent Trigger object, which is used
+* to post-process and finalize the instantiations through
+* sendInstantiation(...), where the parent trigger will make calls to
+* qe->getInstantiate()->addInstantiation(...). The latter function is the entry
+* point in which instantiate lemmas are enqueued to be sent on the output
+* channel.
+*/
+class IMGenerator {
+public:
+ IMGenerator(Trigger* tparent);
+ virtual ~IMGenerator() {}
+ /** Reset instantiation round.
+  *
+  * Called once at beginning of an instantiation round.
+  */
+ virtual void resetInstantiationRound() {}
+ /** Reset.
+  *
+  * eqc is the equivalence class to search in (any if eqc=null).
+  * Returns true if this generator can produce instantiations, and false
+  * otherwise. An example of when it returns false is if it can be determined
+  * that no appropriate matchable terms occur based on eqc.
+  */
+ virtual bool reset(Node eqc) { return true; }
+ /** Get the next match.
+  *
+  * Must call reset( eqc ) before this function. This constructs an
+  * instantiation, which it populates in data structure m,
+  * based on the current context using the implemented matching algorithm.
+  *
+  * q is the quantified formula we are adding instantiations for
+  * m is the InstMatch object we are generating
+  *
+  * Returns a value >0 if an instantiation was successfully generated
+  */
+ virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
+ /** add instantiations
+  *
+  * This adds all available instantiations for q based on the current context
+  * using the implemented matching algorithm. It typically is implemented as a
+  * fixed point of getNextMatch above.
+  *
+  * It returns the number of instantiations added using calls to
+  * Instantiate::addInstantiation(...).
+  */
+ virtual uint64_t addInstantiations(Node q) { return 0; }
+ /** get active score
+  *
+  * A heuristic value indicating how active this generator is.
+  */
+ virtual int getActiveScore() { return 0; }
+
+protected:
+ /** send instantiation
+  *
+  * This method sends instantiation, specified by m, to the parent trigger
+  * object, which will in turn make a call to
+  * Instantiate::addInstantiation(...). This method returns true if a
+  * call to Instantiate::addInstantiation(...) was successfully made,
+  * indicating that an instantiation was enqueued in the quantifier engine's
+  * lemma cache.
+  */
+ bool sendInstantiation(InstMatch& m, InferenceId id);
+ /** The parent trigger that owns this */
+ Trigger* d_tparent;
+ /** The state of the quantifiers engine */
+ quantifiers::QuantifiersState& d_qstate;
+ // !!!!!!!!! temporarily available (project #15)
+ QuantifiersEngine* getQuantifiersEngine();
+};/* class IMGenerator */
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 584b3ebbf..5f47f70c3 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -22,7 +22,6 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/ematching/var_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
@@ -36,21 +35,6 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-IMGenerator::IMGenerator(Trigger* tparent)
-    : d_tparent(tparent), d_qstate(tparent->d_qstate)
-{
-}
-
-bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
-{
-  return d_tparent->sendInstantiation(m, id);
-}
-
-QuantifiersEngine* IMGenerator::getQuantifiersEngine()
-{
-  return d_tparent->d_quantEngine;
-}
-
 InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat)
     : IMGenerator(tparent)
 {
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 99414c90d..3f6976ca7 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -18,104 +18,14 @@
 #define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
 
 #include <map>
-#include "expr/node_trie.h"
-#include "theory/inference_id.h"
+#include "expr/node.h"
 #include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/ematching/im_generator.h"
 
 namespace CVC4 {
 namespace theory {
-
-class QuantifiersEngine;
-
-namespace quantifiers {
-class QuantifiersState;
-}  // namespace quantifiers
-
 namespace inst {
 
-class Trigger;
-
-/** IMGenerator class
-*
-* Virtual base class for generating InstMatch objects, which correspond to
-* quantifier instantiations. The main use of this class is as a backend utility
-* to Trigger (see theory/quantifiers/ematching/trigger.h).
-*
-* Some functions below take as argument a pointer to the current quantifiers
-* engine, which is used for making various queries about what terms and
-* equalities exist in the current context.
-*
-* Some functions below take a pointer to a parent Trigger object, which is used
-* to post-process and finalize the instantiations through
-* sendInstantiation(...), where the parent trigger will make calls to
-* qe->getInstantiate()->addInstantiation(...). The latter function is the entry
-* point in which instantiate lemmas are enqueued to be sent on the output
-* channel.
-*/
-class IMGenerator {
-public:
- IMGenerator(Trigger* tparent);
- virtual ~IMGenerator() {}
- /** Reset instantiation round.
-  *
-  * Called once at beginning of an instantiation round.
-  */
- virtual void resetInstantiationRound() {}
- /** Reset.
-  *
-  * eqc is the equivalence class to search in (any if eqc=null).
-  * Returns true if this generator can produce instantiations, and false
-  * otherwise. An example of when it returns false is if it can be determined
-  * that no appropriate matchable terms occur based on eqc.
-  */
- virtual bool reset(Node eqc) { return true; }
- /** Get the next match.
-  *
-  * Must call reset( eqc ) before this function. This constructs an
-  * instantiation, which it populates in data structure m,
-  * based on the current context using the implemented matching algorithm.
-  *
-  * q is the quantified formula we are adding instantiations for
-  * m is the InstMatch object we are generating
-  *
-  * Returns a value >0 if an instantiation was successfully generated
-  */
- virtual int getNextMatch(Node q, InstMatch& m) { return 0; }
- /** add instantiations
-  *
-  * This add all available instantiations for q based on the current context
-  * using the implemented matching algorithm. It typically is implemented as a
-  * fixed point of getNextMatch above.
-  *
-  * It returns the number of instantiations added using calls to calls to
-  * Instantiate::addInstantiation(...).
-  */
- virtual uint64_t addInstantiations(Node q) { return 0; }
- /** get active score
-  *
-  * A heuristic value indicating how active this generator is.
-  */
- virtual int getActiveScore() { return 0; }
-
-protected:
- /** send instantiation
-  *
-  * This method sends instantiation, specified by m, to the parent trigger
-  * object, which will in turn make a call to
-  * Instantiate::addInstantiation(...). This method returns true if a
-  * call to Instantiate::addInstantiation(...) was successfully made,
-  * indicating that an instantiation was enqueued in the quantifier engine's
-  * lemma cache.
-  */
- bool sendInstantiation(InstMatch& m, InferenceId id);
- /** The parent trigger that owns this */
- Trigger* d_tparent;
- /** The state of the quantifiers engine */
- quantifiers::QuantifiersState& d_qstate;
- // !!!!!!!!! temporarily available (project #15)
- QuantifiersEngine* getQuantifiersEngine();
-};/* class IMGenerator */
-
 class CandidateGenerator;
 
 /** InstMatchGenerator class