diff options
Diffstat (limited to 'src/prop/cryptominisat/Solver/XorFinder.cpp')
-rw-r--r-- | src/prop/cryptominisat/Solver/XorFinder.cpp | 462 |
1 files changed, 0 insertions, 462 deletions
diff --git a/src/prop/cryptominisat/Solver/XorFinder.cpp b/src/prop/cryptominisat/Solver/XorFinder.cpp deleted file mode 100644 index 1b82430e9..000000000 --- a/src/prop/cryptominisat/Solver/XorFinder.cpp +++ /dev/null @@ -1,462 +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 "XorFinder.h" - -#include <algorithm> -#include <utility> -#include <iostream> -#include "Solver.h" -#include "VarReplacer.h" -#include "ClauseCleaner.h" -#include "time_mem.h" - -//#define VERBOSE_DEBUG - -using namespace CMSat; -using std::make_pair; - -XorFinder::XorFinder(Solver& _solver, vec<Clause*>& _cls) : - cls(_cls) - , solver(_solver) -{ -} - -bool XorFinder::fullFindXors(const uint32_t minSize, const uint32_t maxSize) -{ - uint32_t sumLengths = 0; - double time = cpuTime(); - foundXors = 0; - solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses); - if (!solver.ok) return false; - - toRemove.clear(); - toRemove.resize(cls.size(), false); - toLeaveInPlace.clear(); - toLeaveInPlace.resize(cls.size(), false); - - table.clear(); - table.reserve(cls.size()); - - for (Clause **it = cls.getData(), **end = cls.getDataEnd(); it != end; it ++) { - if (it+1 != end) __builtin_prefetch(*(it+1)); - Clause& c = (**it); - assert((*it)->size() > 2); - bool sorted = true; - for (uint32_t i = 0, size = c.size(); i+1 < size ; i++) { - sorted = (c[i].var() <= c[i+1].var()); - if (!sorted) break; - } - if (!sorted) { - solver.detachClause(c); - std::sort(c.getData(), c.getDataEnd()); - solver.attachClause(c); - } - } - - uint32_t i = 0; - for (Clause **it = cls.getData(), **end = cls.getDataEnd(); it != end; it++, i++) { - const uint32_t size = (*it)->size(); - if ( size > maxSize || size < minSize) { - toLeaveInPlace[i] = true; - continue; - } - table.push_back(make_pair(*it, i)); - } - std::sort(table.begin(), table.end(), clause_sorter_primary()); - - if (!findXors(sumLengths)) goto end; - solver.ok = (solver.propagate<true>().isNULL()); - -end: - - if (solver.conf.verbosity >= 1 || (solver.conf.verbosity >= 1 && foundXors > 0)) { - printf("c Finding non-binary XORs: %5.2f s (found: %7d, avg size: %3.1f)\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors); - } - - i = 0; - uint32_t j = 0; - uint32_t toSkip = 0; - for (uint32_t end = cls.size(); i != end; i++) { - if (toLeaveInPlace[i]) { - cls[j] = cls[i]; - j++; - toSkip++; - continue; - } - if (!toRemove[table[i-toSkip].second]) { - cls[j] = table[i-toSkip].first; - j++; - } - } - cls.shrink(i-j); - - return solver.ok; -} - - -/** -@brief Finds xors in clauseTable -- datastructures must already be set up - -Identifies sets of clauses of the same length and variable content, and then -tries to merge them into an XOR. -*/ -bool XorFinder::findXors(uint32_t& sumLengths) -{ - #ifdef VERBOSE_DEBUG - cout << "Finding Xors started" << endl; - #endif - - sumLengths = 0; - - ClauseTable::iterator begin = table.begin(); - ClauseTable::iterator end = table.begin(); - vec<Lit> lits; - bool impair; - while (getNextXor(begin, end, impair)) { - const Clause& c = *(begin->first); - lits.clear(); - for (const Lit *it = &c[0], *cend = it+c.size() ; it != cend; it++) { - lits.push(Lit(it->var(), false)); - } - - #ifdef VERBOSE_DEBUG - cout << "- Found clauses:" << endl; - #endif - - for (ClauseTable::iterator it = begin; it != end; it++) { - //This clause belongs to the xor we found? - //(i.e. does it have the correct number of inverted literals?) - if (impairSigns(*it->first) == impair){ - #ifdef VERBOSE_DEBUG - it->first->plainPrint(); - #endif - toRemove[it->second] = true; - solver.removeClause(*it->first); - } - } - - assert(lits.size() > 2); - XorClause* x = solver.addXorClauseInt(lits, impair); - if (x != NULL) solver.xorclauses.push(x); - if (!solver.ok) return false; - - #ifdef VERBOSE_DEBUG - cout << "- Final xor-clause: " << x << std::endl;; - #endif - - foundXors++; - sumLengths += lits.size(); - } - - return solver.ok; -} - -/** -@brief Moves to the next set of begin&end pointers that contain an xor - -@p begin[inout] start searching here in XorFinder::table -@p end[inout] end iterator of XorFinder::table until which the xor spans -*/ -bool XorFinder::getNextXor(ClauseTable::iterator& begin, ClauseTable::iterator& end, bool& impair) -{ - ClauseTable::iterator tableEnd = table.end(); - - while(begin != tableEnd && end != tableEnd) { - begin = end; - end++; - uint32_t size = (end == tableEnd ? 0:1); - while(end != tableEnd && clause_vareq(begin->first, end->first)) { - size++; - end++; - } - if (size > 0 && isXor(size, begin, end, impair)) - return true; - } - - return false; -} - -/** -@brief Returns if the two clauses are equal - -NOTE: assumes that the clauses are of equal lenght AND contain the same -variables (but the invertedness of the literals might differ) -*/ -bool XorFinder::clauseEqual(const Clause& c1, const Clause& c2) const -{ - assert(c1.size() == c2.size()); - for (uint32_t i = 0, size = c1.size(); i < size; i++) - if (c1[i].sign() != c2[i].sign()) return false; - - return true; -} - -/** -@brief Returns whether the number of inverted literals in the clause is pair or impair -*/ -bool XorFinder::impairSigns(const Clause& c) const -{ - uint32_t num = 0; - for (const Lit *it = &c[0], *end = it + c.size(); it != end; it++) - num += it->sign(); - - return num % 2; -} - -/** -@brief Gets as input a set of clauses of equal size and variable content, decides if there is an XOR in them - -@param impair If there is an XOR, this tells if that XOR contains an impair -number of inverted literal or not -@return True, if ther is an XOR, and False if not -*/ -bool XorFinder::isXor(const uint32_t size, const ClauseTable::iterator& begin, const ClauseTable::iterator& end, bool& impair) -{ - const uint32_t requiredSize = 1 << (begin->first->size()-1); - - //Note: "size" can be larger than requiredSize, since there might be - //a mix of imparied and paired num. inverted literals, and furthermore, - //clauses might be repeated - if (size < requiredSize) return false; - - #ifdef DEBUG_XORFIND2 - { - vec<Var> vars; - Clause& c = *begin->first; - for (uint32_t i = 0; i < c.size(); i++) - vars.push(c[i].var()); - for (ClauseTable::iterator it = begin; it != end; it++) { - Clause& c = *it->first; - for (uint32_t i = 0; i < c.size(); i++) - assert(vars[i] == c[i].var()); - } - clause_sorter_primary sorter; - - for (ClauseTable::iterator it = begin; it != end; it++) { - ClauseTable::iterator it2 = it; - it2++; - if (it2 == end) break; - assert(!sorter(*it2, *it)); - } - } - #endif //DEBUG_XORFIND - - //We now sort them according to literal content - std::sort(begin, end, clause_sorter_secondary()); - - uint32_t numPair = 0; - uint32_t numImpair = 0; - countImpairs(begin, end, numImpair, numPair); - - //if there are two XORs with equal variable sets, but different invertedness - //that leads to direct UNSAT result. - if (numImpair == requiredSize && numPair == requiredSize) { - solver.ok = false; - impair = true; - return true; - } - - if (numImpair == requiredSize) { - impair = true; - return true; - } - - if (numPair == requiredSize) { - impair = false; - return true; - } - - return false; -} - -/** -@brief Counts number of negations in the literals in clauses between begin&end, and returns the number of clauses with pair, and impair literals -*/ -void XorFinder::countImpairs(const ClauseTable::iterator& begin, const ClauseTable::iterator& end, uint32_t& numImpair, uint32_t& numPair) const -{ - numImpair = 0; - numPair = 0; - - ClauseTable::const_iterator it = begin; - ClauseTable::const_iterator it2 = begin; - it2++; - - bool impair = impairSigns(*it->first); - numImpair += impair; - numPair += !impair; - - for (; it2 != end;) { - if (!clauseEqual(*it->first, *it2->first)) { - bool impair = impairSigns(*it2->first); - numImpair += impair; - numPair += !impair; - } - it++; - it2++; - } -} - -/** -@brief Converts all xor clauses to normal clauses - -Sometimes it's not worth the hassle of having xor clauses and normal clauses. -This function converts xor clauses to normal clauses, and removes the normal -clauses. - -\todo It currently only works for 3- and 4-long clauses. Larger clauses should -also be handled. -*/ -void XorFinder::addAllXorAsNorm() -{ - uint32_t added = 0; - XorClause **i = solver.xorclauses.getData(), **j = i; - for (XorClause **end = solver.xorclauses.getDataEnd(); i != end; i++) { - if ((*i)->size() > 3) { - *j++ = *i; - continue; - } - added++; - if ((*i)->size() == 3) addXorAsNormal3(**i); - //if ((*i)->size() == 4) addXorAsNormal4(**i); - solver.removeClause(**i); - } - solver.xorclauses.shrink(i-j); - if (solver.conf.verbosity >= 1) { - std::cout << "c Added XOR as norm:" << added << std::endl; - } -} - -/** -@brief Utility function for addAllXorAsNorm() for converting 3-long xor clauses to normal clauses - -\todo clean this up, it's ugly -*/ -void XorFinder::addXorAsNormal3(XorClause& c) -{ - assert(c.size() == 3); - Clause *tmp; - vec<Var> vars; - const bool inverted = c.xorEqualFalse(); - - for (uint32_t i = 0; i < c.size(); i++) { - vars.push(c[i].var()); - } - - vec<Lit> vars2; - vars2.growTo(3); - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2.growTo(3); - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2.growTo(3); - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2.growTo(3); - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); -} - -/** -@brief Utility function for addAllXorAsNorm() for converting 4-long xor clauses to normal clauses - -\todo clean this up, it's ugly -*/ -void XorFinder::addXorAsNormal4(XorClause& c) -{ - assert(c.size() == 4); - Clause *tmp; - vec<Var> vars; - vec<Lit> vars2(c.size()); - const bool inverted = !c.xorEqualFalse(); - - for (uint32_t i = 0; i < c.size(); i++) { - vars.push(c[i].var()); - } - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], false ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], false ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], false ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], false ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], false ^ inverted); - vars2[3] = Lit(vars[3], true ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); - - vars2[0] = Lit(vars[0], true ^ inverted); - vars2[1] = Lit(vars[1], true ^ inverted); - vars2[2] = Lit(vars[2], true ^ inverted); - vars2[3] = Lit(vars[3], false ^ inverted); - tmp = solver.addClauseInt(vars2); - if (tmp) solver.clauses.push(tmp); -} |