diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/UselessBinRemover.h')
-rw-r--r-- | src/prop/cryptominisat/Solver/UselessBinRemover.h | 85 |
1 files changed, 0 insertions, 85 deletions
diff --git a/src/prop/cryptominisat/Solver/UselessBinRemover.h b/src/prop/cryptominisat/Solver/UselessBinRemover.h deleted file mode 100644 index 37944b431..000000000 --- a/src/prop/cryptominisat/Solver/UselessBinRemover.h +++ /dev/null @@ -1,85 +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/>. -**************************************************************************************************/ - -#ifndef USELESSBINREMOVER_H -#define USELESSBINREMOVER_H - -#include "Vec.h" -#include "Solver.h" -#ifdef _MSC_VER -#include <msvc/stdint.h> -#else -#include <stdint.h> -#endif //_MSC_VER - -namespace CMSat { - -/** -@brief Removes binary clauses that are effectively useless to have - -These binary clauses are useless, because for example clauses: -a V b --b V c - -exist, so the binary clause: -a V c - -is useless in every possible way. Here, we remove such claues. Unfortunately, -currently we only remove useless non-learnt binary clauses. Learnt useless -binary clauses are not removed. - -\todo Extend such that it removes learnt useless binary clauses as well -*/ -class UselessBinRemover { - public: - UselessBinRemover(Solver& solver); - bool removeUslessBinFull(); - - private: - bool failed; ///<Has the previous propagation failed? (=conflict) - uint32_t extraTime; ///<Time that cannot be meausured in bogoprops (~propagation time) - - //Remove useless binaries - bool fillBinImpliesMinusLast(const Lit origLit, const Lit lit, vec<Lit>& wrong); - bool removeUselessBinaries(const Lit lit); - void removeBin(const Lit lit1, const Lit lit2); - /** - @brief Don't delete the same binary twice, and don't assume that deleted binaries still exist - - Not deleting the same binary twice is easy to understand. He hard part - is the second thought. Basically, once we set "a->b" to be deleted, for - instance, we should not check whether any one-hop neighbours of "a" can - be reached from "b", since the binary clause leading to "b" has already - been deleted (and, by the way, checked, since the place where we can - reach "b" from already checked for all places we can visit from "b") - */ - vec<char> toDeleteSet; - vec<Lit> oneHopAway; ///<Lits that are one hop away from selected lit (sometimes called origLit) - /** - @brief Binary clauses to be removed are gathered here - - We only gather the second lit, the one we can reach from selected lit - (calld origLit some places) see fillBinImpliesMinusLast() for details - */ - vec<Lit> wrong; - - Solver& solver; ///<The solver class e want to remove useless binary clauses from -}; - -} - -#endif //USELESSBINREMOVER_H |