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

Towards eliminating dependencies on quantifiers engine.

10 files changed, 231 insertions, 15 deletions

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 02b9ca635..57c5533a9 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -336,7 +336,7 @@ bool ConjectureGenerator::isGroundTerm( TNode n ) {
 
 bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
   // synchonized with instantiation engine
-  return d_quantEngine->getInstWhenNeedsCheck( e );
+  return d_qstate.getInstWhenNeedsCheck(e);
 }
 
 bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
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 ){
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 1b011481b..d448699af 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -52,7 +52,8 @@ bool InstStrategyEnum::needsCheck(Theory::Effort e)
   }
   if (options::fullSaturateInterleave())
   {
-    if (d_quantEngine->getInstWhenNeedsCheck(e))
+    // if interleaved, we run at the same time as E-matching
+    if (d_qstate.getInstWhenNeedsCheck(e))
     {
       return true;
     }
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 48b6b2b66..07bd97918 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -14,6 +14,8 @@
 
 #include "theory/quantifiers/quantifiers_state.h"
 
+#include "options/quantifiers_options.h"
+
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
@@ -21,8 +23,133 @@ namespace quantifiers {
 QuantifiersState::QuantifiersState(context::Context* c,
                                    context::UserContext* u,
                                    Valuation val)
-    : TheoryState(c, u, val)
+    : TheoryState(c, u, val), d_ierCounterc(c)
+{
+  // allow theory combination to go first, once initially
+  d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
+  d_ierCounterc = d_ierCounter;
+  d_ierCounterLc = 0;
+  d_ierCounterLastLc = 0;
+  d_instWhenPhase =
+      1 + (options::instWhenPhase() < 1 ? 1 : options::instWhenPhase());
+}
+
+void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
+{
+  if (e == Theory::EFFORT_FULL)
+  {
+    // increment if a last call happened, we are not strictly enforcing
+    // interleaving, or already were in phase
+    if (d_ierCounterLastLc != d_ierCounterLc
+        || !options::instWhenStrictInterleave()
+        || d_ierCounter % d_instWhenPhase != 0)
+    {
+      d_ierCounter = d_ierCounter + 1;
+      d_ierCounterLastLc = d_ierCounterLc;
+      d_ierCounterc = d_ierCounterc.get() + 1;
+    }
+  }
+  else if (e == Theory::EFFORT_LAST_CALL)
+  {
+    d_ierCounterLc = d_ierCounterLc + 1;
+  }
+}
+
+bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const
+{
+  Trace("qstate-debug") << "Get inst when needs check, counts=" << d_ierCounter
+                        << ", " << d_ierCounterLc << std::endl;
+  // determine if we should perform check, based on instWhenMode
+  bool performCheck = false;
+  if (options::instWhenMode() == options::InstWhenMode::FULL)
+  {
+    performCheck = (e >= Theory::EFFORT_FULL);
+  }
+  else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
+  {
+    performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck();
+  }
+  else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
+  {
+    performCheck =
+        ((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0)
+         || e == Theory::EFFORT_LAST_CALL);
+  }
+  else if (options::instWhenMode()
+           == options::InstWhenMode::FULL_DELAY_LAST_CALL)
+  {
+    performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck()
+                     && d_ierCounter % d_instWhenPhase != 0)
+                    || e == Theory::EFFORT_LAST_CALL);
+  }
+  else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
+  {
+    performCheck = (e >= Theory::EFFORT_LAST_CALL);
+  }
+  else
+  {
+    performCheck = true;
+  }
+  Trace("qstate-debug") << "...returned " << performCheck << std::endl;
+  return performCheck;
+}
+
+uint64_t QuantifiersState::getInstRoundDepth() const
+{
+  return d_ierCounterc.get();
+}
+
+uint64_t QuantifiersState::getInstRounds() const { return d_ierCounter; }
+
+void QuantifiersState::debugPrintEqualityEngine(const char* c) const
 {
+  bool traceEnabled = Trace.isOn(c);
+  if (!traceEnabled)
+  {
+    return;
+  }
+  eq::EqualityEngine* ee = getEqualityEngine();
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+  std::map<TypeNode, uint64_t> tnum;
+  while (!eqcs_i.isFinished())
+  {
+    TNode r = (*eqcs_i);
+    TypeNode tr = r.getType();
+    if (tnum.find(tr) == tnum.end())
+    {
+      tnum[tr] = 0;
+    }
+    tnum[tr]++;
+    bool firstTime = true;
+    Trace(c) << "  " << r;
+    Trace(c) << " : { ";
+    eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
+    while (!eqc_i.isFinished())
+    {
+      TNode n = (*eqc_i);
+      if (r != n)
+      {
+        if (firstTime)
+        {
+          Trace(c) << std::endl;
+          firstTime = false;
+        }
+        Trace(c) << "    " << n << std::endl;
+      }
+      ++eqc_i;
+    }
+    if (!firstTime)
+    {
+      Trace(c) << "  ";
+    }
+    Trace(c) << "}" << std::endl;
+    ++eqcs_i;
+  }
+  Trace(c) << std::endl;
+  for (const std::pair<const TypeNode, uint64_t>& t : tnum)
+  {
+    Trace(c) << "# eqc for " << t.first << " : " << t.second << std::endl;
+  }
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
index 76baab7ca..d45938f98 100644
--- a/src/theory/quantifiers/quantifiers_state.h
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -17,6 +17,7 @@
 #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
 
+#include "theory/theory.h"
 #include "theory/theory_state.h"
 
 namespace CVC4 {
@@ -31,6 +32,44 @@ class QuantifiersState : public TheoryState
  public:
   QuantifiersState(context::Context* c, context::UserContext* u, Valuation val);
   ~QuantifiersState() {}
+  /**
+   * Increment the instantiation counters, called once at the beginning of when
+   * we perform a check with quantifiers engine for the given effort.
+   */
+  void incrementInstRoundCounters(Theory::Effort e);
+  /**
+   * Get whether we need to check at effort e based on the inst-when mode. This
+   * option determines the policy of quantifier instantiation and theory
+   * combination, e.g. does it run before, after, or interleaved with theory
+   * combination. This is based on the state of the counters maintained by this
+   * class.
+   */
+  bool getInstWhenNeedsCheck(Theory::Effort e) const;
+  /** Get the number of instantiation rounds performed in this SAT context */
+  uint64_t getInstRoundDepth() const;
+  /** Get the total number of instantiation rounds performed */
+  uint64_t getInstRounds() const;
+  /** debug print equality engine on trace c */
+  void debugPrintEqualityEngine(const char* c) const;
+
+ private:
+  /** The number of instantiation rounds in this SAT context */
+  context::CDO<uint64_t> d_ierCounterc;
+  /** The number of total instantiation rounds (full effort) */
+  uint64_t d_ierCounter;
+  /** The number of total instantiation rounds (last call effort) */
+  uint64_t d_ierCounterLc;
+  /**
+   * A counter to remember the last value of d_ierCounterLc where we a
+   * full effort check. This is used for interleaving theory combination
+   * and quantifier instantiation rounds.
+   */
+  uint64_t d_ierCounterLastLc;
+  /**
+   * The number of instantiation rounds we run for each call to theory
+   * combination.
+   */
+  uint64_t d_instWhenPhase;
 };
 
 }  // namespace quantifiers