Remove support for flipDecision (#2319)

4 files changed, 0 insertions, 45 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 62496df2f..dbe417dbc 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1703,43 +1703,6 @@ void Solver::pop()
   trail_ok.pop();
 }
 
-bool Solver::flipDecision() {
-  Debug("flipdec") << "FLIP: decision level is " << decisionLevel() << std::endl;
-  if(decisionLevel() == 0) {
-    Debug("flipdec") << "FLIP: no decisions, returning false" << std::endl;
-    return false;
-  }
-
-  // find the level to cancel until
-  int level = trail_lim.size() - 1;
-  Debug("flipdec") << "FLIP: looking at level " << level << " dec is " << trail[trail_lim[level]] << " flippable?" << ((polarity[var(trail[trail_lim[level]])] & 0x2) == 0 ? 1 : 0) << " flipped?" << flipped[level] << std::endl;
-  while(level > 0 && (flipped[level] || /* phase-locked */ (polarity[var(trail[trail_lim[level]])] & 0x2) != 0)) {
-    --level;
-    Debug("flipdec") << "FLIP: looking at level " << level << " dec is " << trail[trail_lim[level]] << " flippable?" << ((polarity[var(trail[trail_lim[level]])] & 0x2) == 0 ? 2 : 0) << " flipped?" << flipped[level] << std::endl;
-  }
-  if(level < 0) {
-    Lit l = trail[trail_lim[0]];
-    Debug("flipdec") << "FLIP: canceling everything, flipping root decision " << l << std::endl;
-    cancelUntil(0);
-    newDecisionLevel();
-    Debug("flipdec") << "FLIP: enqueuing " << ~l << std::endl;
-    uncheckedEnqueue(~l);
-    flipped[0] = true;
-    Debug("flipdec") << "FLIP: returning false" << std::endl;
-    return false;
-  }
-  Lit l = trail[trail_lim[level]];
-  Debug("flipdec") << "FLIP: canceling to level " << level << ", flipping decision " << l << std::endl;
-  cancelUntil(level);
-  newDecisionLevel();
-  Debug("flipdec") << "FLIP: enqueuing " << ~l << std::endl;
-  uncheckedEnqueue(~l);
-  flipped[level] = true;
-  Debug("flipdec") << "FLIP: returning true" << std::endl;
-  return true;
-}
-
-
 CRef Solver::updateLemmas() {
 
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index c27d8a18b..b6da9b9c8 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -211,7 +211,6 @@ public:
     void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
     void    freezePolarity (Var v, bool b); // Declare which polarity the decision heuristic MUST ALWAYS use for a variable. Requires mode 'polarity_user'.
     void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
-    bool    flipDecision   ();              // Backtrack and flip most recent decision
 
     // Read state:
     //
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 2c511df4a..3c11d5ad8 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -209,11 +209,6 @@ void MinisatSatSolver::requirePhase(SatLiteral lit) {
   d_minisat->freezePolarity(v, lit.isNegated());
 }
 
-bool MinisatSatSolver::flipDecision() {
-  Debug("minisat") << "flipDecision()" << std::endl;
-  return d_minisat->flipDecision();
-}
-
 bool MinisatSatSolver::isDecision(SatVariable decn) const {
   return d_minisat->isDecision( decn );
 }
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 8395fddf0..dc42066d7 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -78,8 +78,6 @@ public:
 
   void requirePhase(SatLiteral lit) override;
 
-  bool flipDecision() override;
-
   bool isDecision(SatVariable decn) const override;
 
  private: