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

diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index b03c4ad3be84f47617402694b86d95d6f0b52c4e..dc11ed56287541551b03dc8a893a6edb78886f10 100644 (file)
--- 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 bb3bd68e37b61debd246d35790f5b28356c8ce19..e324bc36f8036531e3baf444cf08bd5cd1741824 100644 (file)
--- 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 2ab45aa96c810c962451f6de573c2c3b4e7848e2..6f647aeb12a922d518664cddf2a23bb7c704ace0 100644 (file)
--- 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 074e288c69f5e344d81ddb0533444db57f806ff0..55047fe2bc8bd13876d6d062ab04434a729596f6 100644 (file)
--- 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 516f31efc13f2146dd20c56b995d74f406bbf7be..7a5652e2f06d767c419291f1bc5ba4c4870ca795 100644 (file)
--- 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 2c97fd09989fa58685d297ae51bdaabaeb23ab4e..77713744b9971229161b6be4b1773c44d721acf4 100644 (file)
--- 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
   *