Clean remaining references to getNextDecisionRequest in quantifiers. (#2484)

4 files changed, 1 insertions, 11 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