From f807ab4124630719dcbed14f22d03a857dcdab02 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 17 Sep 2018 20:36:36 -0500
Subject: [PATCH] Clean remaining references to getNextDecisionRequest in
 quantifiers. (#2484)

---
 src/theory/quantifiers/kinds                  |  2 +-
 src/theory/quantifiers/quant_util.h           |  5 -----
 src/theory/quantifiers/theory_quantifiers.cpp |  4 ----
 src/theory/quantifiers/theory_quantifiers.h   |  1 -
 src/theory/quantifiers_engine.cpp             | 13 -------------
 src/theory/quantifiers_engine.h               |  2 --
 6 files changed, 1 insertion(+), 26 deletions(-)

diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index b03c4ad3b..dc11ed562 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -7,7 +7,7 @@
 theory THEORY_QUANTIFIERS ::CVC4::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
 
-properties check presolve getNextDecisionRequest
+properties check presolve
 
 rewriter ::CVC4::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
 
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index bb3bd68e3..e324bc36f 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -134,11 +134,6 @@ class QuantifiersModule {
    * Called when a quantified formula q is asserted to the quantifiers theory
    */
   virtual void assertNode(Node q) {}
-  /* Get the next decision request.
-   *
-   * Identical to Theory::getNextDecisionRequest(...)
-   */
-  virtual Node getNextDecisionRequest( unsigned& priority ) { return TNode::null(); }
   /** Identify this module (for debugging, dynamic configuration, etc..) */
   virtual std::string identify() const = 0;
   //----------------------------general queries
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 2ab45aa96..6f647aeb1 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -171,10 +171,6 @@ void TheoryQuantifiers::check(Effort e) {
   getQuantifiersEngine()->check( e );
 }
 
-Node TheoryQuantifiers::getNextDecisionRequest( unsigned& priority ){
-  return getQuantifiersEngine()->getNextDecisionRequest( priority );
-}
-
 void TheoryQuantifiers::assertUniversal( Node n ){
   Assert( n.getKind()==FORALL );
   if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 074e288c6..55047fe2b 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -45,7 +45,6 @@ class TheoryQuantifiers : public Theory {
   void presolve() override;
   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
   void check(Effort e) override;
-  Node getNextDecisionRequest(unsigned& priority) override;
   bool collectModelInfo(TheoryModel* m) override;
   void shutdown() override {}
   std::string identify() const override
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 516f31efc..7a5652e2f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -936,19 +936,6 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
   addTermToDatabase(d_term_util->getInstConstantBody(f), true);
 }
 
-Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){
-  unsigned min_priority = 0;
-  Node dec;  
-  for( unsigned i=0; i<d_modules.size(); i++ ){
-    Node n = d_modules[i]->getNextDecisionRequest( priority );
-    if( !n.isNull() && ( dec.isNull() || priority<min_priority ) ){
-      dec = n;
-      min_priority = priority;
-    }
-  }
-  return dec;
-}
-
 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant, bool withinInstClosure ){
   if( options::incrementalSolving() ){
     if( d_presolve_in.find( n )==d_presolve_in.end() ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2c97fd099..77713744b 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -188,8 +188,6 @@ public:
   void registerPattern( std::vector<Node> & pattern);
   /** assert universal quantifier */
   void assertQuantifier( Node q, bool pol );
-  /** get next decision request */
-  Node getNextDecisionRequest( unsigned& priority );
 private:
  /** (context-indepentent) register quantifier internal
   *
-- 
2.30.2