diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-17 15:09:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-17 15:09:05 -0500 |
commit | ee4004505fa7f086872880d2d693c0608af29050 (patch) | |
tree | 3c1f155debe7367c3ece51e8a6c5af87c75cbcac /src/prop | |
parent | 6d65aa41a7e218469e99f476259cccb08c4c46c1 (diff) |
Remove support for flipDecision (#2319)
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 37 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 1 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 5 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 2 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 5 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 13 | ||||
-rw-r--r-- | src/prop/sat_solver.h | 2 |
7 files changed, 0 insertions, 65 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: diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 0a8e8ade6..e1200c7e5 100644 --- 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 cfeb30fe4..2ff862d18 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -148,19 +148,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 * returns true for both lit and the negation of lit. diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index add73eebe..5222af200 100644 --- 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 */ |