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

6 files changed, 81 insertions, 55 deletions

diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index c4b15a852..876e4e369 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -42,11 +42,11 @@ namespace quantifiers {
 // user-pat=interleave alternates between use and resort
 
 struct sortQuantifiersForSymbol {
-  QuantifiersEngine* d_qe;
+  QuantRelevance* d_quant_rel;
   std::map< Node, Node > d_op_map;
   bool operator() (Node i, Node j) {
-    int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[i] );
-    int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_op_map[j] );
+    int nqfsi = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[i]);
+    int nqfsj = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[j]);
     if( nqfsi<nqfsj ){
       return true;
     }else if( nqfsi>nqfsj ){
@@ -155,7 +155,10 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
   }
 }
 
-InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
+                                                         QuantRelevance* qr)
+    : InstStrategy(qe), d_quant_rel(qr)
+{
   //how to select trigger terms
   d_tr_strategy = options::triggerSelMode();
   //whether to select new triggers during the search
@@ -429,8 +432,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
       //sort terms based on relevance
       if( options::relevantTriggers() ){
+        Assert(d_quant_rel);
         sortQuantifiersForSymbol sqfs;
-        sqfs.d_qe = d_quantEngine;
+        sqfs.d_quant_rel = d_quant_rel;
         for( unsigned i=0; i<patTerms.size(); i++ ){
           Assert( d_pat_to_mpat.find( patTerms[i] )!=d_pat_to_mpat.end() );
           Assert( d_pat_to_mpat[patTerms[i]].hasOperator() );
@@ -438,10 +442,19 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         }        
         //sort based on # occurrences (this will cause Trigger to select rarer symbols)
         std::sort( patTerms.begin(), patTerms.end(), sqfs );
-        Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
-        for( unsigned i=0; i<patTerms.size(); i++ ){
-          Debug("relevant-trigger") << "   " << patTerms[i] << " from " << d_pat_to_mpat[patTerms[i]] << " (";
-          Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( d_pat_to_mpat[patTerms[i]].getOperator() ) << ")" << std::endl;
+        if (Debug.isOn("relevant-trigger"))
+        {
+          Debug("relevant-trigger")
+              << "Terms based on relevance: " << std::endl;
+          for (const Node& p : patTerms)
+          {
+            Debug("relevant-trigger")
+                << "   " << p << " from " << d_pat_to_mpat[p] << " (";
+            Debug("relevant-trigger")
+                << d_quant_rel->getNumQuantifiersForSymbol(
+                       d_pat_to_mpat[p].getOperator())
+                << ")" << std::endl;
+          }
         }
       }
       //now, generate the trigger...
@@ -482,14 +495,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
             //check if similar patterns exist, and if so, add them additionally
             unsigned nqfs_curr = 0;
             if( options::relevantTriggers() ){
-              nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
+              nqfs_curr = d_quant_rel->getNumQuantifiersForSymbol(
+                  patTerms[0].getOperator());
             }
             index++;
             bool success = true;
             while( success && index<patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
               success = false;
-              if( !options::relevantTriggers() ||
-                  d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
+              if (!options::relevantTriggers()
+                  || d_quant_rel->getNumQuantifiersForSymbol(
+                         patTerms[index].getOperator())
+                         <= nqfs_curr)
+              {
                 d_single_trigger_gen[ patTerms[index] ] = true;
                 Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], false, Trigger::TR_RETURN_NULL, d_num_trigger_vars[f] );
                 addTrigger( tr2, f );
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index b71b8ee47..1a014939f 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -17,12 +17,9 @@
 #ifndef CVC4__INST_STRATEGY_E_MATCHING_H
 #define CVC4__INST_STRATEGY_E_MATCHING_H
 
-#include "context/context.h"
-#include "context/context_mm.h"
 #include "theory/quantifiers/ematching/instantiation_engine.h"
 #include "theory/quantifiers/ematching/trigger.h"
-#include "util/statistics_registry.h"
-#include "options/quantifiers_options.h"
+#include "theory/quantifiers/quant_relevance.h"
 
 namespace CVC4 {
 namespace theory {
@@ -99,9 +96,11 @@ private:
  bool hasUserPatterns(Node q);
  /** has user patterns */
  std::map<Node, bool> d_hasUserPatterns;
+
 public:
-  InstStrategyAutoGenTriggers( QuantifiersEngine* qe );
-  ~InstStrategyAutoGenTriggers(){}
+ InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
+ ~InstStrategyAutoGenTriggers() {}
+
 public:
   /** get auto-generated trigger */
   inst::Trigger* getAutoGenTrigger( Node q );
@@ -112,6 +111,13 @@ public:
   }
   /** add pattern */
   void addUserNoPattern( Node q, Node pat );
+
+ private:
+  /**
+   * Pointer to the module that computes relevance of quantifiers, which is
+   * owned by the instantiation engine that owns this class.
+   */
+  QuantRelevance* d_quant_rel;
 };/* class InstStrategyAutoGenTriggers */
 
 
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);
       }
     }
   }
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index b959bef2d..26fc3767b 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/quant_relevance.h"
 #include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
@@ -50,8 +51,6 @@ public:
   virtual int process( Node f, Theory::Effort effort, int e ) = 0;
   /** identify */
   virtual std::string identify() const { return std::string("Unknown"); }
-  /** register quantifier */
-  //virtual void registerQuantifier( Node q ) {}
 };/* class InstStrategy */
 
 class InstantiationEngine : public QuantifiersModule {
@@ -87,6 +86,10 @@ class InstantiationEngine : public QuantifiersModule {
   void addUserNoPattern(Node q, Node pat);
   /** Identify this module */
   std::string identify() const override { return "InstEngine"; }
+
+ private:
+  /** for computing relevance of quantifiers */
+  std::unique_ptr<QuantRelevance> d_quant_rel;
 }; /* class InstantiationEngine */
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c17af1e1f..5bac55462 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -189,7 +189,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_eq_inference(nullptr),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
-      d_quant_rel(nullptr),
       d_rel_dom(nullptr),
       d_bv_invert(nullptr),
       d_builder(nullptr),
@@ -253,11 +252,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
 
-  if( options::relevantTriggers() ){
-    d_quant_rel.reset(new quantifiers::QuantRelevance);
-    d_util.push_back(d_quant_rel.get());
-  }
-
   if( options::quantEpr() ){
     Assert( !options::incrementalSolving() );
     d_qepr.reset(new quantifiers::QuantEPR);
@@ -351,10 +345,6 @@ quantifiers::BvInverter* QuantifiersEngine::getBvInverter() const
 {
   return d_bv_invert.get();
 }
-quantifiers::QuantRelevance* QuantifiersEngine::getQuantifierRelevance() const
-{
-  return d_quant_rel.get();
-}
 quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
 {
   return d_builder.get();
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 7a9f5e7da..dfe8a44ad 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -34,7 +34,6 @@
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_epr.h"
-#include "theory/quantifiers/quant_relevance.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/relevant_domain.h"
@@ -117,8 +116,6 @@ public:
   quantifiers::RelevantDomain* getRelevantDomain() const;
   /** get the BV inverter utility */
   quantifiers::BvInverter* getBvInverter() const;
-  /** get quantifier relevance */
-  quantifiers::QuantRelevance* getQuantifierRelevance() const;
   //---------------------- end utilities
   //---------------------- modules (TODO remove these #1163)
   /** get bounded integers utility */
@@ -310,8 +307,6 @@ public:
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */
   std::unique_ptr<quantifiers::FirstOrderModel> d_model;
-  /** for computing relevance of quantifiers */
-  std::unique_ptr<quantifiers::QuantRelevance> d_quant_rel;
   /** relevant domain */
   std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
   /** inversion utility for BV instantiation */