Moving methods from quantifiers engine to quantifiers state (#5881)

Towards eliminating dependencies on quantifiers engine.

6 files changed, 61 insertions, 12 deletions

diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp
new file mode 100644
index 000000000..fc85703c0
--- /dev/null
+++ b/src/theory/quantifiers/ematching/inst_strategy.cpp
@@ -0,0 +1,45 @@
+/*********************                                                        */
+/*! \file inst_strategy.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 strategy base class
+ **/
+
+#include "theory/quantifiers/ematching/inst_strategy.h"
+
+#include "theory/quantifiers/quantifiers_state.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+InstStrategy::InstStrategy(QuantifiersEngine* qe,
+                           QuantifiersState& qs,
+                           QuantifiersInferenceManager& qim)
+    : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
+{
+}
+InstStrategy::~InstStrategy() {}
+void InstStrategy::presolve() {}
+std::string InstStrategy::identify() const { return std::string("Unknown"); }
+
+options::UserPatMode InstStrategy::getInstUserPatMode() const
+{
+  if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
+  {
+    return d_qstate.getInstRounds() % 2 == 0 ? options::UserPatMode::USE
+                                             : options::UserPatMode::RESORT;
+  }
+  return options::userPatternsQuant();
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index 3baa25fa0..b9d0aa745 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -9,7 +9,7 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Instantiation Engine classes
+ ** \brief Instantiation engine strategy base class
  **/
 
 #include "cvc4_private.h"
@@ -19,6 +19,7 @@
 
 #include <vector>
 #include "expr/node.h"
+#include "options/quantifiers_options.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
@@ -48,21 +49,23 @@ class InstStrategy
  public:
   InstStrategy(QuantifiersEngine* qe,
                QuantifiersState& qs,
-               QuantifiersInferenceManager& qim)
-      : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
-  {
-  }
-  virtual ~InstStrategy() {}
+               QuantifiersInferenceManager& qim);
+  virtual ~InstStrategy();
   /** presolve */
-  virtual void 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"); }
+  virtual std::string identify() const;
 
  protected:
+  /**
+   * Get the current user pat mode, which may be interleaved based on counters
+   * maintained by the quantifiers state.
+   */
+  options::UserPatMode getInstUserPatMode() const;
   /** reference to the instantiation engine */
   QuantifiersEngine* d_quantEngine;
   /** The quantifiers state object */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 7c8ab5ec2..881133432 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -102,7 +102,7 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
                                                         Theory::Effort effort,
                                                         int e)
 {
-  options::UserPatMode upMode = d_quantEngine->getInstUserPatMode();
+  options::UserPatMode upMode = getInstUserPatMode();
   if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
   {
     return InstStrategyStatus::STATUS_UNKNOWN;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index 9d730e055..cf6405b38 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -86,7 +86,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q,
   {
     return InstStrategyStatus::STATUS_UNFINISHED;
   }
-  options::UserPatMode upm = d_quantEngine->getInstUserPatMode();
+  options::UserPatMode upm = getInstUserPatMode();
   int peffort = upm == options::UserPatMode::RESORT ? 2 : 1;
   if (e < peffort)
   {
@@ -159,7 +159,7 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
   }
   Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
   // check match option
-  if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+  if (getInstUserPatMode() == options::UserPatMode::RESORT)
   {
     d_user_gen_wait[q].push_back(nodes);
     return;
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
index 92b427621..996adc444 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -19,6 +19,7 @@
 
 #include <map>
 #include "expr/node.h"
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/inst_strategy.h"
 #include "theory/quantifiers/ematching/trigger.h"
 
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 4f3b207be..50d91a1e1 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -120,7 +120,7 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
 }
 
 bool InstantiationEngine::needsCheck( Theory::Effort e ){
-  return d_quantEngine->getInstWhenNeedsCheck( e );
+  return d_qstate.getInstWhenNeedsCheck(e);
 }
 
 void InstantiationEngine::reset_round( Theory::Effort e ){