From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 13 Feb 2021 14:42:36 +0000 (-0600)
Subject: Moving methods from quantifiers engine to quantifiers state (#5881)
X-Git-Tag: cvc5-1.0.0~2279
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ff53d70b3e0a11e4ae5c1c8f612d809dca2d004;p=cvc5.git

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

Towards eliminating dependencies on quantifiers engine.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 42370b8fc..12e3f24b3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -664,6 +664,7 @@ libcvc4_add_sources(
   theory/quantifiers/ematching/inst_match_generator_multi_linear.h
   theory/quantifiers/ematching/inst_match_generator_simple.cpp
   theory/quantifiers/ematching/inst_match_generator_simple.h
+  theory/quantifiers/ematching/inst_strategy.cpp
   theory/quantifiers/ematching/inst_strategy.h
   theory/quantifiers/ematching/inst_strategy_e_matching.cpp
   theory/quantifiers/ematching/inst_strategy_e_matching.h
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
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 33ec3cbf8..e85d6f2ff 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -54,7 +54,6 @@ QuantifiersEngine::QuantifiersEngine(
       d_term_enum(new quantifiers::TermEnumeration),
       d_quants_prereg(qstate.getUserContext()),
       d_quants_red(qstate.getUserContext()),
-      d_ierCounter_c(qstate.getSatContext()),
       d_presolve(qstate.getUserContext(), true),
       d_presolve_in(qstate.getUserContext()),
       d_presolve_cache(qstate.getUserContext())
@@ -77,13 +76,6 @@ QuantifiersEngine::QuantifiersEngine(
 
   //---- end utilities
 
-  //allow theory combination to go first, once initially
-  d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
-  d_ierCounter_c = d_ierCounter;
-  d_ierCounter_lc = 0;
-  d_ierCounterLastLc = 0;
-  d_inst_when_phase = 1 + ( options::instWhenPhase()<1 ? 1 : options::instWhenPhase() );
-
   // Finite model finding requires specialized ways of building the model.
   // We require constructing the model and model builder here, since it is
   // required for initializing the CombinationEngine.
@@ -377,7 +369,8 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
     if( Trace.isOn("quant-engine-debug") ){
       Trace("quant-engine-debug") << "Quantifiers Engine check, level = " << e << std::endl;
-      Trace("quant-engine-debug") << "  depth : " << d_ierCounter_c << std::endl;
+      Trace("quant-engine-debug")
+          << "  depth : " << d_qstate.getInstRoundDepth() << std::endl;
       Trace("quant-engine-debug") << "  modules to check : ";
       for( unsigned i=0; i<qm.size(); i++ ){
         Trace("quant-engine-debug") << qm[i]->identify() << " ";
@@ -398,7 +391,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
     }
     if( Trace.isOn("quant-engine-ee-pre") ){
       Trace("quant-engine-ee-pre") << "Equality engine (pre-inference): " << std::endl;
-      debugPrintEqualityEngine( "quant-engine-ee-pre" );
+      d_qstate.debugPrintEqualityEngine("quant-engine-ee-pre");
     }
     if( Trace.isOn("quant-engine-assert") ){
       Trace("quant-engine-assert") << "Assertions : " << std::endl;
@@ -426,7 +419,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
     if( Trace.isOn("quant-engine-ee") ){
       Trace("quant-engine-ee") << "Equality engine : " << std::endl;
-      debugPrintEqualityEngine( "quant-engine-ee" );
+      d_qstate.debugPrintEqualityEngine("quant-engine-ee");
     }
 
     //reset the model
@@ -499,16 +492,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
         Assert(!d_qstate.isInConflict());
         if (quant_e == QuantifiersModule::QEFFORT_CONFLICT)
         {
-          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_ierCounter_lc || !options::instWhenStrictInterleave() || d_ierCounter%d_inst_when_phase!=0 ){
-              d_ierCounter = d_ierCounter + 1;
-              d_ierCounterLastLc = d_ierCounter_lc;
-              d_ierCounter_c = d_ierCounter_c.get() + 1;
-            }
-          }else if( e==Theory::EFFORT_LAST_CALL ){
-            d_ierCounter_lc = d_ierCounter_lc + 1;
-          }
+          d_qstate.incrementInstRoundCounters(e);
         }
         else if (quant_e == QuantifiersModule::QEFFORT_MODEL)
         {
@@ -617,9 +601,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
 }
 
 void QuantifiersEngine::notifyCombineTheories() {
-  //if allowing theory combination to happen at most once between instantiation rounds
-  //d_ierCounter = 1;
-  //d_ierCounterLastLc = -1;
+  // If allowing theory combination to happen at most once between instantiation
+  // rounds, this would reset d_ierCounter to 1 and d_ierCounterLastLc to -1
+  // in quantifiers state.
 }
 
 bool QuantifiersEngine::reduceQuantifier( Node q ) {
@@ -789,55 +773,6 @@ void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
 }
 
-bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
-  Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << 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_qstate.getValuation().needCheck();
-  }
-  else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
-  {
-    performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
-  }
-  else if (options::instWhenMode()
-           == options::InstWhenMode::FULL_DELAY_LAST_CALL)
-  {
-    performCheck =
-        ((e == Theory::EFFORT_FULL && !d_qstate.getValuation().needCheck()
-          && d_ierCounter % d_inst_when_phase != 0)
-         || e == Theory::EFFORT_LAST_CALL);
-  }
-  else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
-  {
-    performCheck = ( e >= Theory::EFFORT_LAST_CALL );
-  }
-  else
-  {
-    performCheck = true;
-  }
-  return performCheck;
-}
-
-options::UserPatMode QuantifiersEngine::getInstUserPatMode()
-{
-  if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
-  {
-    return d_ierCounter % 2 == 0 ? options::UserPatMode::USE
-                                 : options::UserPatMode::RESORT;
-  }
-  else
-  {
-    return options::userPatternsQuant();
-  }
-}
-
 void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
   d_instantiate->getInstantiationTermVectors(q, tvecs);
 }
@@ -960,41 +895,5 @@ bool QuantifiersEngine::getSynthSolutions(
   return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
 }
 
-void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
-  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
-  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-  std::map< TypeNode, int > typ_num;
-  while( !eqcs_i.isFinished() ){
-    TNode r = (*eqcs_i);
-    TypeNode tr = r.getType();
-    if( typ_num.find( tr )==typ_num.end() ){
-      typ_num[tr] = 0;
-    }
-    typ_num[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( std::map< TypeNode, int >::iterator it = typ_num.begin(); it != typ_num.end(); ++it ){
-    Trace(c) << "# eqc for " << it->first << " : " << it->second << std::endl;
-  }
-}
-
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index cab452e2b..99e4ad5cc 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -178,18 +178,10 @@ public:
  /** mark relevant quantified formula, this will indicate it should be checked
   * before the others */
  void markRelevant(Node q);
- /** get needs check */
- bool getInstWhenNeedsCheck(Theory::Effort e);
- /** get user pat mode */
- options::UserPatMode getInstUserPatMode();
-
-public:
  /** add term to database */
  void addTermToDatabase(Node n, bool withinQuant = false);
  /** notification when master equality engine is updated */
  void eqNotifyNewClass(TNode t);
- /** debug print equality engine */
- void debugPrintEqualityEngine(const char* c);
  /** get internal representative
   *
   * Choose a term that is equivalent to a in the current context that is the
@@ -329,12 +321,6 @@ public:
   /** quantifiers reduced */
   BoolMap d_quants_red;
   std::map<Node, Node> d_quants_red_lem;
-  /** inst round counters TODO: make context-dependent? */
-  context::CDO<int> d_ierCounter_c;
-  int d_ierCounter;
-  int d_ierCounter_lc;
-  int d_ierCounterLastLc;
-  int d_inst_when_phase;
   /** has presolve been called */
   context::CDO<bool> d_presolve;
   /** presolve cache */