Remove support for flipDecision (#2319)

diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
index 0e09033885c4ee35b0a0aeace3986b1a05269c9a..1489e83bd7923a2e4c4db6cfb76e0f0994c17231 100644 (file)
--- a/src/proof/proof_output_channel.cpp
+++ b/src/proof/proof_output_channel.cpp
@@ -71,12 +71,6 @@ void ProofOutputChannel::requirePhase(TNode n, bool b) {
   Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl;
 }
 
-bool ProofOutputChannel::flipDecision() {
-  Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl;
-  AlwaysAssert(false);
-  return false;
-}
-
 void ProofOutputChannel::setIncomplete() {
   Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl;
   AlwaysAssert(false);

diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index 6c4d8e4891e6a5801457d487b1763c05e00fca11..8be434f50b80f39dd739188781803042fe62ef58 100644 (file)
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -41,7 +41,6 @@ class ProofOutputChannel : public theory::OutputChannel {
   theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override;
   theory::LemmaStatus splitLemma(TNode, bool) override;
   void requirePhase(TNode n, bool b) override;
-  bool flipDecision() override;
   void setIncomplete() override;
 
   /** Has conflict() has been called? */

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 62496df2fb287a90609d800f0fda002e43fe0387..dbe417dbc8c090484cea4e16446742db42c55867 100644 (file)
--- 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 c27d8a18b72c5634d2c9b754683cc0d8a2ab80c5..b6da9b9c800173ff9378cfcfa20f537d7bccf30e 100644 (file)
--- 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 2c511df4a59dfacceb3d8f1edcf92cd4482f5c2a..3c11d5ad8d494f81ec31a1bc9f7e38e5409f19ff 100644 (file)
--- 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 8395fddf0d449959b5de34cae08a22d19c961f96..dc42066d779665055647f5ef8ebf0fa910716580 100644 (file)
--- 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:

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 0a8e8ade6591ca317d112ca7ee264b4752140758..e1200c7e5a799560d02d773dde79810d80edd7c5 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -148,11 +148,6 @@ void PropEngine::requirePhase(TNode n, bool phase) {
   d_satSolver->requirePhase(phase ? lit : ~lit);
 }
 
-bool PropEngine::flipDecision() {
-  Debug("prop") << "flipDecision()" << endl;
-  return d_satSolver->flipDecision();
-}
-
 bool PropEngine::isDecision(Node lit) const {
   Assert(isSatLiteral(lit));
   return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable());

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index cfeb30fe4b7b842f4411b5c551f8342120525749..2ff862d18955c08ada1dfed632c6ea8e0b1a5969 100644 (file)
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -147,19 +147,6 @@ public:
    */
   void requirePhase(TNode n, bool phase);
 
-  /**
-   * Backtracks to and flips the most recent unflipped decision, and
-   * returns TRUE.  If the decision stack is nonempty but all
-   * decisions have been flipped already, the state is backtracked to
-   * the root decision, which is re-flipped to the original phase (and
-   * FALSE is returned).  If the decision stack is empty, the state is
-   * unchanged and FALSE is returned.
-   *
-   * @return true if a decision was flipped as requested; false if the
-   * root decision was reflipped, or if no decisions are on the stack.
-   */
-  bool flipDecision();
-
   /**
    * Return whether the given literal is a SAT decision.  Either phase
    * is permitted; that is, if "lit" is a SAT decision, this function

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index add73eebe903b625a2d91223fab7d5e989ea739d..5222af200b034048df6b72d75df4c0494b7b6e3b 100644 (file)
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -164,8 +164,6 @@ public:
 
   virtual void requirePhase(SatLiteral lit) = 0;
 
-  virtual bool flipDecision() = 0;
-
   virtual bool isDecision(SatVariable decn) const = 0;
 };/* class DPLLSatSolverInterface */
 

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index fb0a92cc2fb464b50874e4b76763722a6b97b686..bb8103891ceb2f2b8d3a0b0a886c773693e112ac 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -155,48 +155,6 @@ class OutputChannel {
    */
   virtual void requirePhase(TNode n, bool phase) = 0;
 
-  /**
-   * Flips the most recent unflipped decision to the other phase and
-   * returns true.  If all decisions have been flipped, the root
-   * decision is re-flipped and flipDecision() returns false.  If no
-   * decisions (flipped nor unflipped) are on the decision stack, the
-   * state is not affected and flipDecision() returns false.
-   *
-   * For example, if l1, l2, and l3 are all decision literals, and
-   * have been decided in positive phase, a series of flipDecision()
-   * calls has the following effects:
-   *
-   * l1 l2 l3 <br/>
-   * l1 l2 ~l3 <br/>
-   * l1 ~l2 <br/>
-   * ~l1 <br/>
-   * l1 (and flipDecision() returns false)
-   *
-   * Naturally, flipDecision() might be interleaved with search.  For example:
-   *
-   * l1 l2 l3 <br/>
-   * flipDecision() <br/>
-   * l1 l2 ~l3 <br/>
-   * flipDecision() <br/>
-   * l1 ~l2 <br/>
-   * SAT decides l3 <br/>
-   * l1 ~l2 l3 <br/>
-   * flipDecision() <br/>
-   * l1 ~l2 ~l3 <br/>
-   * flipDecision() <br/>
-   * ~l1 <br/>
-   * SAT decides l2 <br/>
-   * ~l1 l2 <br/>
-   * flipDecision() <br/>
-   * ~l1 ~l2 <br/>
-   * flipDecision() returns FALSE<br/>
-   * l1
-   *
-   * @return true if a decision was flipped; false if no decision
-   * could be flipped, or if the root decision was re-flipped
-   */
-  virtual bool flipDecision() = 0;
-
   /**
    * Notification from a theory that it realizes it is incomplete at
    * this context level.  If SAT is later determined by the

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0ccce95c99dfd1dfb35ac8317e4b3e4ab61aaf0c..f5341b38bf74c3589bd72b2ccdb3f700bfdef980 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2393,14 +2393,12 @@ TheoryEngine::Statistics::Statistics(theory::TheoryId theory):
     propagations(getStatsPrefix(theory) + "::propagations", 0),
     lemmas(getStatsPrefix(theory) + "::lemmas", 0),
     requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
-    flipDecision(getStatsPrefix(theory) + "::flipDecision", 0),
     restartDemands(getStatsPrefix(theory) + "::restartDemands", 0)
 {
   smtStatisticsRegistry()->registerStat(&conflicts);
   smtStatisticsRegistry()->registerStat(&propagations);
   smtStatisticsRegistry()->registerStat(&lemmas);
   smtStatisticsRegistry()->registerStat(&requirePhase);
-  smtStatisticsRegistry()->registerStat(&flipDecision);
   smtStatisticsRegistry()->registerStat(&restartDemands);
 }
 
@@ -2409,7 +2407,6 @@ TheoryEngine::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&propagations);
   smtStatisticsRegistry()->unregisterStat(&lemmas);
   smtStatisticsRegistry()->unregisterStat(&requirePhase);
-  smtStatisticsRegistry()->unregisterStat(&flipDecision);
   smtStatisticsRegistry()->unregisterStat(&restartDemands);
 }
 

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9eafe259885b5037ba6858688690def0323837ca..5763114caa8091a55b67dd528b945805ea586ad0 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -247,9 +247,8 @@ class TheoryEngine {
       return ss.str();
     }
 
-  public:
-
-    IntStat conflicts, propagations, lemmas, requirePhase, flipDecision, restartDemands;
+   public:
+    IntStat conflicts, propagations, lemmas, requirePhase, restartDemands;
 
     Statistics(theory::TheoryId theory);
     ~Statistics();
@@ -316,12 +315,6 @@ class TheoryEngine {
       d_engine->d_propEngine->requirePhase(n, phase);
     }
 
-    bool flipDecision() override {
-      Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl;
-      ++d_statistics.flipDecision;
-      return d_engine->d_propEngine->flipDecision();
-    }
-
     void setIncomplete() override {
       Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
       d_engine->setIncomplete(d_theory);

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 8ebb367ab25be4d0fad8bca7ace070a214526b92..e0db2fdeb6a81dbcaf4e5de53322c7600c7ccafd 100644 (file)
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -86,7 +86,6 @@ public:
   }
 
   void requirePhase(TNode, bool) override {}
-  bool flipDecision() override { return true; }
   void setIncomplete() override {}
   void handleUserAttribute(const char* attr, theory::Theory* t) override {}
 

diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 290f0d4527003f40f77b67a0f5f369c86461af3e..620fcd92ef05f6640a889ee844539d0d7022d34f 100644 (file)
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -64,7 +64,6 @@ class FakeOutputChannel : public OutputChannel {
     Unimplemented();
   }
   void requirePhase(TNode, bool) override { Unimplemented(); }
-  bool flipDecision() override { Unimplemented(); }
   void setIncomplete() override { Unimplemented(); }
   void handleUserAttribute(const char* attr, Theory* t) override {
     Unimplemented();

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index bb227d2bb9cda4c25ae4780862c4ec129aeb6baf..0fbf9c1d6900e4122699f14eca2222424be6014e 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -68,7 +68,6 @@ class TestOutputChannel : public OutputChannel {
   }
 
   void requirePhase(TNode, bool) override { Unreachable(); }
-  bool flipDecision() override { Unreachable(); }
   void setIncomplete() override { Unreachable(); }
 
   void clear() { d_callHistory.clear(); }