diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/OnlyNonLearntBins.cpp')
-rw-r--r-- | src/prop/cryptominisat/Solver/OnlyNonLearntBins.cpp | 84 |
1 files changed, 0 insertions, 84 deletions
diff --git a/src/prop/cryptominisat/Solver/OnlyNonLearntBins.cpp b/src/prop/cryptominisat/Solver/OnlyNonLearntBins.cpp deleted file mode 100644 index 021178b08..000000000 --- a/src/prop/cryptominisat/Solver/OnlyNonLearntBins.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/*********************************************************************** -CryptoMiniSat -- Copyright (c) 2009 Mate Soos - -This program is free software: you can redistribute it and/or modify -it under the terms of the GNU General Public License as published by -the Free Software Foundation, either version 3 of the License, or -(at your option) any later version. - -This program is distributed in the hope that it will be useful, -but WITHOUT ANY WARRANTY; without even the implied warranty of -MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -GNU General Public License for more details. - -You should have received a copy of the GNU General Public License -along with this program. If not, see <http://www.gnu.org/licenses/>. -************************************************************************/ - -#include "OnlyNonLearntBins.h" - -#include <iomanip> -#include "Solver.h" -#include "Clause.h" -#include "VarReplacer.h" -#include "ClauseCleaner.h" -#include "time_mem.h" - -using namespace CMSat; - -OnlyNonLearntBins::OnlyNonLearntBins(Solver& _solver) : - solver(_solver) -{} - -/** -@brief Propagate recursively on non-learnt binaries -*/ -bool OnlyNonLearntBins::propagate() -{ - while (solver.qhead < solver.trail.size()) { - Lit p = solver.trail[solver.qhead++]; - vec<WatchedBin> & wbin = binwatches[p.toInt()]; - solver.propagations += wbin.size()/2 + 2; - for(WatchedBin *k = wbin.getData(), *end = wbin.getDataEnd(); k != end; k++) { - lbool val = solver.value(k->impliedLit); - if (val.isUndef()) { - solver.uncheckedEnqueueLight(k->impliedLit); - } else if (val == l_False) { - return false; - } - } - } - - return true; -} - -/** -@brief Fill internal watchlists with non-binary clauses -*/ -bool OnlyNonLearntBins::fill() -{ - uint32_t numBins = 0; - double myTime = cpuTime(); - binwatches.growTo(solver.nVars()*2); - - uint32_t wsLit = 0; - for (const vec<Watched> *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) { - const vec<Watched>& ws = *it; - for (vec<Watched>::const_iterator it2 = ws.getData(), end2 = ws.getDataEnd(); it2 != end2; it2++) { - if (it2->isBinary() && !it2->getLearnt()) { - binwatches[wsLit].push(WatchedBin(it2->getOtherLit())); - numBins++; - } - } - } - - if (solver.conf.verbosity >= 3) { - std::cout << "c Time to fill non-learnt binary watchlists:" - << std::fixed << std::setprecision(2) << std::setw(5) - << cpuTime() - myTime << " s" - << " num non-learnt bins: " << std::setw(10) << numBins - << std::endl; - } - - return true; -} |