From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 2 Aug 2018 18:01:50 +0000 (-0500)
Subject:  Remove references to deprecated propagate as decision feature (#2258)
X-Git-Tag: cvc5-1.0.0~4828
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a84b54ea155251af6254237816e449589591b33c;p=cvc5.git

 Remove references to deprecated propagate as decision feature (#2258)
---

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index c312ac146..62496df2f 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -603,15 +603,21 @@ Lit Solver::pickBranchLit()
     nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
     while (nextLit != lit_Undef) {
       if(value(var(nextLit)) == l_Undef) {
-        Debug("propagateAsDecision") << "propagateAsDecision(): now deciding on " << nextLit << std::endl;
+        Debug("theoryDecision")
+            << "getNextTheoryDecisionRequest(): now deciding on " << nextLit
+            << std::endl;
         decisions++;
         return nextLit;
       } else {
-        Debug("propagateAsDecision") << "propagateAsDecision(): would decide on " << nextLit << " but it already has an assignment" << std::endl;
+        Debug("theoryDecision")
+            << "getNextTheoryDecisionRequest(): would decide on " << nextLit
+            << " but it already has an assignment" << std::endl;
       }
       nextLit = MinisatSatSolver::toMinisatLit(proxy->getNextTheoryDecisionRequest());
     }
-    Debug("propagateAsDecision") << "propagateAsDecision(): decide on another literal" << std::endl;
+    Debug("theoryDecision")
+        << "getNextTheoryDecisionRequest(): decide on another literal"
+        << std::endl;
 
     // DE requests
     bool stopSearch = false;
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 25520c1cc..9eafe2598 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -413,12 +413,6 @@ class TheoryEngine {
    */
   void propagate(theory::Theory::Effort effort);
 
-  /**
-   * Called by the output channel to request decisions "as soon as
-   * possible."
-   */
-  void propagateAsDecision(TNode literal, theory::TheoryId theory);
-
   /**
    * A variable to mark if we added any lemmas.
    */
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 6161710f2..65f7238c9 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1172,9 +1172,6 @@ void SortModel::allocateCardinality( OutputChannel* out ){
     }
     //require phase
     out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true );
-    //add the appropriate lemma, propagate as decision
-    //Trace("uf-ss-prop-as-dec") << "Propagate as decision " << lem[0] << " " << d_type << std::endl;
-    //out->propagateAsDecision( lem[0] );
     d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality );
 
     if( applyTotality( d_aloc_cardinality ) ){