From ee4004505fa7f086872880d2d693c0608af29050 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Aug 2018 15:09:05 -0500
Subject: Remove support for flipDecision (#2319)

---
 src/theory/output_channel.h    | 42 ------------------------------------------
 src/theory/theory_engine.cpp   |  3 ---
 src/theory/theory_engine.h     | 11 ++---------
 src/theory/theory_test_utils.h |  1 -
 4 files changed, 2 insertions(+), 55 deletions(-)

(limited to 'src/theory')

diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index fb0a92cc2..bb8103891 100644
--- 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 0ccce95c9..f5341b38b 100644
--- 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 9eafe2598..5763114ca 100644
--- 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 8ebb367ab..e0db2fdeb 100644
--- 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 {}
 
-- 
cgit v1.2.3