Encapsulate relevant domain (#3293)

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 70d855f45a2eb2a29eda8939db20d355afe18ea6..83856dfc4a641dbb973fec44bb8fe387a35fbc18 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -32,8 +32,8 @@ using namespace inst;
 
 namespace quantifiers {
 
-InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe)
-    : QuantifiersModule(qe)
+InstStrategyEnum::InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd)
+    : QuantifiersModule(qe), d_rd(rd)
 {
 }
 
@@ -93,18 +93,17 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
   // this stratification since effort level r=1 may be highly expensive in the
   // case where we have a quantified formula with many entailed instances.
   FirstOrderModel* fm = d_quantEngine->getModel();
-  RelevantDomain* rd = d_quantEngine->getRelevantDomain();
   unsigned nquant = fm->getNumAssertedQuantifiers();
   std::map<Node, bool> alreadyProc;
   for (unsigned r = rstart; r <= rend; r++)
   {
-    if (rd || r > 0)
+    if (d_rd || r > 0)
     {
       if (r == 0)
       {
         Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl;
         Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
-        rd->compute();
+        d_rd->compute();
         Trace("inst-alg-debug") << "...finished" << std::endl;
       }
       else
@@ -161,7 +160,6 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
   {
     return false;
   }
-  RelevantDomain* rd = d_quantEngine->getRelevantDomain();
   unsigned final_max_i = 0;
   std::vector<unsigned> maxs;
   std::vector<bool> max_zero;
@@ -178,7 +176,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
     unsigned ts;
     if (isRd)
     {
-      ts = rd->getRDomain(f, i)->d_terms.size();
+      ts = d_rd->getRDomain(f, i)->d_terms.size();
     }
     else
     {
@@ -284,9 +282,9 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
             }
             else if (isRd)
             {
-              terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]);
+              terms.push_back(d_rd->getRDomain(f, i)->d_terms[childIndex[i]]);
               Trace("inst-alg-rd")
-                  << "  " << rd->getRDomain(f, i)->d_terms[childIndex[i]]
+                  << "  " << d_rd->getRDomain(f, i)->d_terms[childIndex[i]]
                   << std::endl;
             }
             else

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index e58993182df6f6df716d846f213748eaed543f94..48285c877c54513d2e06b1d006fb2571a8aceeaa 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -20,6 +20,7 @@
 #include "context/context.h"
 #include "context/context_mm.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/relevant_domain.h"
 
 namespace CVC4 {
 namespace theory {
@@ -61,7 +62,7 @@ namespace quantifiers {
 class InstStrategyEnum : public QuantifiersModule
 {
  public:
-  InstStrategyEnum(QuantifiersEngine* qe);
+  InstStrategyEnum(QuantifiersEngine* qe, RelevantDomain* rd);
   ~InstStrategyEnum() {}
   /** Needs check. */
   bool needsCheck(Theory::Effort e) override;
@@ -79,6 +80,8 @@ class InstStrategyEnum : public QuantifiersModule
   }
 
  private:
+  /** Pointer to the relevant domain utility of quantifiers engine */
+  RelevantDomain* d_rd;
   /** process quantified formula
    *
    * q is the quantified formula we are constructing instances for.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 507d938b404feb0b28ce0ba7d0dde6d9abcdf275..1eb62945be8a295eeff133555982ebf9f758b92b 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -47,6 +47,7 @@ class QuantifiersEnginePrivate
  public:
   QuantifiersEnginePrivate()
       : d_inst_prop(nullptr),
+        d_rel_dom(nullptr),
         d_alpha_equiv(nullptr),
         d_inst_engine(nullptr),
         d_model_engine(nullptr),
@@ -66,6 +67,8 @@ class QuantifiersEnginePrivate
   //------------------------------ private quantifier utilities
   /** quantifiers instantiation propagator */
   std::unique_ptr<quantifiers::InstPropagator> d_inst_prop;
+  /** relevant domain */
+  std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
   //------------------------------ end private quantifier utilities
   //------------------------------ quantifiers modules
   /** alpha equivalence */
@@ -100,14 +103,12 @@ class QuantifiersEnginePrivate
    * This constructs the above modules based on the current options. It adds
    * a pointer to each module it constructs to modules. This method sets
    * needsBuilder to true if we require a strategy-specific model builder
-   * utility, and needsRelDom to true if we require the relevant domain
    * utility.
    */
   void initialize(QuantifiersEngine* qe,
                   context::Context* c,
                   std::vector<QuantifiersModule*>& modules,
-                  bool& needsBuilder,
-                  bool& needsRelDom)
+                  bool& needsBuilder)
   {
     // add quantifiers modules
     if (options::quantConflictFind() || options::quantRewriteRules())
@@ -176,9 +177,9 @@ class QuantifiersEnginePrivate
     // full saturation : instantiate from relevant domain, then arbitrary terms
     if (options::fullSaturateQuant() || options::fullSaturateInterleave())
     {
-      d_fs.reset(new quantifiers::InstStrategyEnum(qe));
+      d_rel_dom.reset(new quantifiers::RelevantDomain(qe));
+      d_fs.reset(new quantifiers::InstStrategyEnum(qe, d_rel_dom.get()));
       modules.push_back(d_fs.get());
-      needsRelDom = true;
     }
   }
 };
@@ -190,7 +191,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
       d_eq_query(new quantifiers::EqualityQueryQuantifiersEngine(c, this)),
       d_tr_trie(new inst::TriggerTrie),
       d_model(nullptr),
-      d_rel_dom(nullptr),
       d_builder(nullptr),
       d_qepr(nullptr),
       d_term_util(new quantifiers::TermUtil(this)),
@@ -263,14 +263,13 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
 
   bool needsBuilder = false;
-  bool needsRelDom = false;
-  d_private->initialize(this, c, d_modules, needsBuilder, needsRelDom);
+  d_private->initialize(this, c, d_modules, needsBuilder);
 
-  if( needsRelDom ){
-    d_rel_dom.reset(new quantifiers::RelevantDomain(this));
-    d_util.push_back(d_rel_dom.get());
+  if (d_private->d_rel_dom.get())
+  {
+    d_util.push_back(d_private->d_rel_dom.get());
   }
-  
+
   // if we require specialized ways of building the model
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
@@ -324,10 +323,6 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() const
 {
   return d_eq_query.get();
 }
-quantifiers::RelevantDomain* QuantifiersEngine::getRelevantDomain() const
-{
-  return d_rel_dom.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 e1fc742af29703c3ff1f088c49a2fcfb41e7486c..32315840481c67f6dc146d2dae725ce68b62a77e 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -32,7 +32,6 @@
 #include "theory/quantifiers/quant_epr.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
@@ -104,10 +103,6 @@ public:
   /** get trigger database */
   inst::TriggerTrie* getTriggerDatabase() const;
   //---------------------- end utilities
-  //---------------------- utilities (TODO move these utilities #1163)
-  /** get relevant domain */
-  quantifiers::RelevantDomain* getRelevantDomain() const;
-  //---------------------- end utilities
  private:
   /**
    * Maps quantified formulas to the module that owns them, if any module has
@@ -314,8 +309,6 @@ public:
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */
   std::unique_ptr<quantifiers::FirstOrderModel> d_model;
-  /** relevant domain */
-  std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom;
   /** model builder */
   std::unique_ptr<quantifiers::QModelBuilder> d_builder;
   /** utility for effectively propositional logic */