Move quantifiers relevance module inside E-matching module (#3186)

1 files changed, 35 insertions, 20 deletions

diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index bb70002a0..2fe28fc61 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -36,7 +36,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
       d_instStrategies(),
       d_isup(),
       d_i_ag(),
-      d_quants() {
+      d_quants(),
+      d_quant_rel(nullptr)
+{
+  if (options::relevantTriggers())
+  {
+    d_quant_rel.reset(new quantifiers::QuantRelevance);
+  }
   if (options::eMatching()) {
     // these are the instantiation strategies for E-matching
     // user-provided patterns
@@ -46,7 +52,8 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
     }
 
     // auto-generated patterns
-    d_i_ag.reset(new InstStrategyAutoGenTriggers(d_quantEngine));
+    d_i_ag.reset(
+        new InstStrategyAutoGenTriggers(d_quantEngine, d_quant_rel.get()));
     d_instStrategies.push_back(d_i_ag.get());
   }
 }
@@ -175,24 +182,32 @@ void InstantiationEngine::checkOwnership(Node q)
   }
 }
 
-void InstantiationEngine::registerQuantifier( Node f ){
-  if( d_quantEngine->hasOwnership( f, this ) ){
-    //for( unsigned i=0; i<d_instStrategies.size(); ++i ){
-    //  d_instStrategies[i]->registerQuantifier( f );
-    //}
-    //take into account user patterns
-    if( f.getNumChildren()==3 ){
-      Node subsPat =
-          d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
-              f[2], f);
-      //add patterns
-      for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){
-        //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl;
-        if( subsPat[i].getKind()==INST_PATTERN ){
-          addUserPattern( f, subsPat[i] );
-        }else if( subsPat[i].getKind()==INST_NO_PATTERN ){
-          addUserNoPattern( f, subsPat[i] );
-        }
+void InstantiationEngine::registerQuantifier(Node q)
+{
+  if (!d_quantEngine->hasOwnership(q, this))
+  {
+    return;
+  }
+  if (d_quant_rel)
+  {
+    d_quant_rel->registerQuantifier(q);
+  }
+  // take into account user patterns
+  if (q.getNumChildren() == 3)
+  {
+    Node subsPat =
+        d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
+            q[2], q);
+    // add patterns
+    for (const Node& p : subsPat)
+    {
+      if (p.getKind() == INST_PATTERN)
+      {
+        addUserPattern(q, p);
+      }
+      else if (p.getKind() == INST_NO_PATTERN)
+      {
+        addUserNoPattern(q, p);
       }
     }
   }