+
+class NewGateData
+{
+ public:
+ NewGateData(const Lit _lit1, const Lit _lit2, const uint32_t _numLitRem, const uint32_t _numClRem) :
+ lit1(_lit1)
+ , lit2(_lit2)
+ , numLitRem(_numLitRem)
+ , numClRem(_numClRem)
+ {}
+ const bool operator<(const NewGateData& n2) const
+ {
+ uint32_t value1 = numClRem*ANDGATEUSEFUL + numLitRem;
+ uint32_t value2 = n2.numClRem*ANDGATEUSEFUL + n2.numLitRem;
+ if (value1 != value2) return(value1 > value2);
+ if (lit1 != n2.lit1) return(lit1 > n2.lit1);
+ if (lit2 != n2.lit2) return(lit2 > n2.lit2);
+ return false;
+ }
+ const bool operator==(const NewGateData& n2) const
+ {
+ return(lit1 == n2.lit1
+ && lit2 == n2.lit2
+ && numLitRem == n2.numLitRem
+ && numClRem == n2.numClRem);
+ }
+ Lit lit1;
+ Lit lit2;
+ uint32_t numLitRem;
+ uint32_t numClRem;
+};
+
+struct SecondSorter
+{
+ const bool operator() (const std::pair<Var, uint32_t> p1, const std::pair<Var, uint32_t> p2)
+ {
+ return p1.second > p2.second;
+ }
+};
+
+void Subsumer::createNewVar()
+{
+ double myTime = cpuTime();
+ vector<NewGateData> newGates;
+ vec<Lit> lits;
+ vec<ClauseSimp> subs;
+ numMaxSubsume0 = 300*1000*1000;
+ uint64_t numOp = 0;
+
+ if (solver.negPosDist.size() == 0) return;
+ uint32_t size = std::min((uint32_t)solver.negPosDist.size()-1, 400U);
+
+
+ uint32_t tries = 0;
+ for (; tries < std::min(100000U, size*size/2); tries++) {
+ Var var1, var2;
+ var1 = solver.negPosDist[solver.mtrand.randInt(size)].var;
+ var2 = solver.negPosDist[solver.mtrand.randInt(size)].var;
+ if (var1 == var2) continue;
+
+ if (solver.value(var1) != l_Undef
+ || solver.subsumer->getVarElimed()[var1]
+ || solver.xorSubsumer->getVarElimed()[var1]
+ || solver.partHandler->getSavedState()[var1] != l_Undef
+ ) continue;
+
+ if (solver.value(var2) != l_Undef
+ || solver.subsumer->getVarElimed()[var2]
+ || solver.xorSubsumer->getVarElimed()[var2]
+ || solver.partHandler->getSavedState()[var2] != l_Undef
+ ) continue;
+
+ Lit lit1 = Lit(var1, solver.mtrand.randInt(1));
+ Lit lit2 = Lit(var2, solver.mtrand.randInt(1));
+ if (lit1 > lit2) std::swap(lit1, lit2);
+
+ lits.clear();
+ lits.push(lit1);
+ lits.push(lit2);
+
+ subs.clear();
+ findSubsumed(lits, calcAbstraction(lits), subs);
+
+ uint32_t potential = 0;
+ if (numOp < 100*1000*1000) {
+ OrGate gate;
+ gate.eqLit = Lit(0,false);
+ gate.lits.push_back(lit1);
+ gate.lits.push_back(lit2);
+ treatAndGate(gate, false, potential, numOp);
+ }
+
+ if (potential > 5 || subs.size() > 100
+ || (potential > 1 && subs.size() > 50)) {
+ newGates.push_back(NewGateData(lit1, lit2, subs.size(), potential));
+ }
+ }
+
+ std::sort(newGates.begin(), newGates.end());
+ newGates.erase(std::unique(newGates.begin(), newGates.end() ), newGates.end() );
+
+ uint32_t addedNum = 0;
+ for (uint32_t i = 0; i < newGates.size(); i++) {
+ const NewGateData& n = newGates[i];
+ if ((i > 50 && n.numLitRem < 1000 && n.numClRem < 25)
+ || i > ((double)solver.order_heap.size()*0.01)
+ || i > 100) break;
+
+ const Var newVar = solver.newVar();
+ dontElim[newVar] = true;
+ const Lit newLit = Lit(newVar, false);
+ OrGate orGate;
+ orGate.eqLit = newLit;
+ orGate.lits.push_back(n.lit1);
+ orGate.lits.push_back(n.lit2);
+ orGates.push_back(orGate);
+
+ lits.clear();
+ lits.push(newLit);
+ lits.push(~n.lit1);
+ Clause* cl = solver.addClauseInt(lits, 0);
+ assert(cl == NULL);
+ assert(solver.ok);
+
+ lits.clear();
+ lits.push(newLit);
+ lits.push(~n.lit2);
+ cl = solver.addClauseInt(lits, 0);
+ assert(cl == NULL);
+ assert(solver.ok);
+
+ lits.clear();
+ lits.push(~newLit);
+ lits.push(n.lit1);
+ lits.push(n.lit2);
+ cl = solver.addClauseInt(lits, 0, false, 0, false, false);
+ assert(cl != NULL);
+ assert(solver.ok);
+ ClauseSimp c = linkInClause(*cl);
+ defOfOrGate[c.index] = true;
+
+ addedNum++;
+ numERVars++;
+ }
+ finishedAddingVars = true;
+
+ if (solver.conf.verbosity >= 1) {
+ std::cout << "c Added " << addedNum << " vars "
+ << " tried: " << tries
+ << " time: " << (cpuTime() - myTime) << std::endl;
+ }
+ //std::cout << "c Added " << addedNum << " vars "
+ //<< " time: " << (cpuTime() - myTime) << " numThread: " << solver.threadNum << std::endl;
+}
+
+const bool Subsumer::findOrGatesAndTreat()
+{
+ assert(solver.ok);
+ uint32_t old_clauses_subsumed = clauses_subsumed;
+
+ double myTime = cpuTime();
+ orGates.clear();
+ for (size_t i = 0; i < gateOcc.size(); i++) gateOcc[i].clear();
+
+ totalOrGateSize = 0;
+ uint32_t oldNumVarToReplace = solver.varReplacer->getNewToReplaceVars();
+ uint32_t oldNumBins = solver.numBins;
+ gateLitsRemoved = 0;
+ numOrGateReplaced = 0;
+
+ findOrGates(false);
+ doAllOptimisationWithGates();
+
+ if (solver.conf.verbosity >= 1) {
+ std::cout << "c ORs : " << std::setw(6) << orGates.size()
+ << " avg-s: " << std::fixed << std::setw(4) << std::setprecision(1) << ((double)totalOrGateSize/(double)orGates.size())
+ << " cl-sh: " << std::setw(5) << numOrGateReplaced
+ << " l-rem: " << std::setw(6) << gateLitsRemoved
+ << " b-add: " << std::setw(6) << (solver.numBins - oldNumBins)
+ << " v-rep: " << std::setw(3) << (solver.varReplacer->getNewToReplaceVars() - oldNumVarToReplace)
+ << " cl-rem: " << andGateNumFound
+ << " avg s: " << ((double)andGateTotalSize/(double)andGateNumFound)
+ << " T: " << std::fixed << std::setw(7) << std::setprecision(2) << (cpuTime() - myTime) << std::endl;
+ }
+ if (!solver.ok) return false;
+
+ bool cannotDoER;
+ #pragma omp critical (ERSync)
+ cannotDoER = (solver.threadNum != solver.dataSync->getThreadAddingVars()
+ || solver.dataSync->getEREnded());
+
+
+ if (solver.conf.doER && !cannotDoER) {
+ vector<OrGate> backupOrGates = orGates;
+ if (!carryOutER()) return false;
+ for (vector<OrGate>::const_iterator it = backupOrGates.begin(), end = backupOrGates.end(); it != end; it++) {
+ orGates.push_back(*it);
+ }
+ }
+
+ for (vector<OrGate>::iterator it = orGates.begin(), end = orGates.end(); it != end; it++) {
+ OrGate& gate = *it;
+ for (uint32_t i = 0; i < gate.lits.size(); i++) {
+ Lit lit = gate.lits[i];
+ gateOcc[lit.toInt()].push_back(&(*it));
+ }
+ }
+
+ clauses_subsumed = old_clauses_subsumed;
+
+ return solver.ok;
+}
+
+const bool Subsumer::carryOutER()
+{
+ double myTime = cpuTime();
+ orGates.clear();
+ totalOrGateSize = 0;
+ uint32_t oldNumVarToReplace = solver.varReplacer->getNewToReplaceVars();
+ uint32_t oldNumBins = solver.numBins;
+ gateLitsRemoved = 0;
+ numOrGateReplaced = 0;
+ defOfOrGate.clear();
+ defOfOrGate.growTo(clauses.size(), false);
+
+ createNewVar();
+ doAllOptimisationWithGates();
+
+ if (solver.conf.verbosity >= 1) {
+ std::cout << "c ORs : " << std::setw(6) << orGates.size()
+ << " avg-s: " << std::fixed << std::setw(4) << std::setprecision(1) << ((double)totalOrGateSize/(double)orGates.size())
+ << " cl-sh: " << std::setw(5) << numOrGateReplaced
+ << " l-rem: " << std::setw(6) << gateLitsRemoved
+ << " b-add: " << std::setw(6) << (solver.numBins - oldNumBins)
+ << " v-rep: " << std::setw(3) << (solver.varReplacer->getNewToReplaceVars() - oldNumVarToReplace)
+ << " cl-rem: " << andGateNumFound
+ << " avg s: " << ((double)andGateTotalSize/(double)andGateNumFound)
+ << " T: " << std::fixed << std::setw(7) << std::setprecision(2) << (cpuTime() - myTime) << std::endl;
+ }
+ return solver.ok;
+}
+
+const bool Subsumer::doAllOptimisationWithGates()
+{
+ assert(solver.ok);
+ for (uint32_t i = 0; i < orGates.size(); i++) {
+ std::sort(orGates[i].lits.begin(), orGates[i].lits.end());
+ }
+ std::sort(orGates.begin(), orGates.end(), OrGateSorter2());
+
+ for (vector<OrGate>::const_iterator it = orGates.begin(), end = orGates.end(); it != end; it++) {
+ if (!shortenWithOrGate(*it)) return false;
+ }
+
+ if (!treatAndGates()) return false;
+ if (!findEqOrGates()) return false;
+
+ return true;
+}
+
+const bool Subsumer::findEqOrGates()
+{
+ assert(solver.ok);
+
+ vec<Lit> tmp(2);
+ for (uint32_t i = 1; i < orGates.size(); i++) {
+ const OrGate& gate1 = orGates[i-1];
+ const OrGate& gate2 = orGates[i];
+ if (gate1.lits == gate2.lits
+ && gate1.eqLit.var() != gate2.eqLit.var()
+ ) {
+ tmp[0] = gate1.eqLit.unsign();
+ tmp[1] = gate2.eqLit.unsign();
+ const bool sign = true ^ gate1.eqLit.sign() ^ gate2.eqLit.sign();
+ Clause *c = solver.addXorClauseInt(tmp, sign, 0);
+ tmp.clear();
+ tmp.growTo(2);
+ assert(c == NULL);
+ if (!solver.ok) return false;
+ }
+ }
+
+ return true;
+}
+
+void Subsumer::findOrGates(const bool learntGatesToo)
+{
+ for (const ClauseSimp *it = clauses.getData(), *end = clauses.getDataEnd(); it != end; it++) {
+ if (it->clause == NULL) continue;
+ const Clause& cl = *it->clause;
+ if (!learntGatesToo && cl.learnt()) continue;
+
+ uint8_t numSizeZeroCache = 0;
+ Lit which = lit_Undef;
+ for (const Lit *l = cl.getData(), *end2 = cl.getDataEnd(); l != end2; l++) {
+ Lit lit = *l;
+ const vector<LitExtra>& cache = solver.transOTFCache[(~lit).toInt()].lits;
+
+ if (cache.size() == 0) {
+ numSizeZeroCache++;
+ if (numSizeZeroCache > 1) break;
+ which = lit;
+ }
+ }
+ if (numSizeZeroCache > 1) continue;
+
+ if (numSizeZeroCache == 1) {
+ findOrGate(~which, *it, learntGatesToo);
+ } else {
+ for (const Lit *l = cl.getData(), *end2 = cl.getDataEnd(); l != end2; l++)
+ findOrGate(~*l, *it, learntGatesToo);
+ }
+ }
+}
+
+void Subsumer::findOrGate(const Lit eqLit, const ClauseSimp& c, const bool learntGatesToo)
+{
+ Clause& cl = *c.clause;
+ bool isEqual = true;
+ for (const Lit *l2 = cl.getData(), *end3 = cl.getDataEnd(); l2 != end3; l2++) {
+ if (*l2 == ~eqLit) continue;
+ Lit otherLit = *l2;
+ const vector<LitExtra>& cache = solver.transOTFCache[(~otherLit).toInt()].lits;
+
+ bool OK = false;
+ for (vector<LitExtra>::const_iterator cacheLit = cache.begin(), endCache = cache.end(); cacheLit != endCache; cacheLit++) {
+ if ((learntGatesToo || cacheLit->getOnlyNLBin()) &&
+ cacheLit->getLit() == eqLit) {
+ OK = true;
+ break;
+ }
+ }
+ if (!OK) {
+ isEqual = false;
+ break;
+ }
+ }
+
+ if (isEqual) {
+ OrGate gate;
+ for (const Lit *l2 = cl.getData(), *end3 = cl.getDataEnd(); l2 != end3; l2++) {
+ if (*l2 == ~eqLit) continue;
+ gate.lits.push_back(*l2);
+ }
+ //std::sort(gate.lits.begin(), gate.lits.end());
+ gate.eqLit = eqLit;
+ //gate.num = orGates.size();
+ orGates.push_back(gate);
+ totalOrGateSize += gate.lits.size();
+ defOfOrGate[c.index] = true;
+
+ #ifdef VERBOSE_ORGATE_REPLACE
+ std::cout << "Found gate : " << gate << std::endl;
+ #endif
+ }
+}
+
+const bool Subsumer::shortenWithOrGate(const OrGate& gate)
+{
+ assert(solver.ok);
+
+ vec<ClauseSimp> subs;
+ findSubsumed(gate.lits, calcAbstraction(gate.lits), subs);
+ for (uint32_t i = 0; i < subs.size(); i++) {
+ ClauseSimp c = subs[i];
+ Clause* cl = subs[i].clause;
+
+ if (defOfOrGate[c.index]) continue;
+
+ bool inside = false;
+ for (Lit *l = cl->getData(), *end = cl->getDataEnd(); l != end; l++) {
+ if (gate.eqLit.var() == l->var()) {
+ inside = true;
+ break;
+ }
+ }
+ if (inside) continue;
+
+ #ifdef VERBOSE_ORGATE_REPLACE
+ std::cout << "OR gate-based cl-shortening" << std::endl;
+ std::cout << "Gate used: " << gate << std::endl;
+ std::cout << "orig Clause: " << *cl << std::endl;
+ #endif
+
+ numOrGateReplaced++;
+
+ for (vector<Lit>::const_iterator it = gate.lits.begin(), end = gate.lits.end(); it != end; it++) {
+ gateLitsRemoved++;
+ cl->strengthen(*it);
+ maybeRemove(occur[it->toInt()], cl);
+ #ifndef TOUCH_LESS
+ touch(*it, cl->learnt());
+ #endif
+ }
+
+ gateLitsRemoved--;
+ cl->add(gate.eqLit); //we can add, because we removed above. Otherwise this is segfault
+ occur[gate.eqLit.toInt()].push(c);
+
+ #ifdef VERBOSE_ORGATE_REPLACE
+ std::cout << "new Clause : " << *cl << std::endl;
+ std::cout << "-----------" << std::endl;
+ #endif
+
+ if (!handleUpdatedClause(c)) return false;
+ if (c.clause != NULL && !cl->learnt()) {
+ for (Lit *i2 = cl->getData(), *end2 = cl->getDataEnd(); i2 != end2; i2++)
+ touchChangeVars(*i2);
+ }
+ }
+
+ return solver.ok;
+}
+
+const bool Subsumer::subsumeNonExist()
+{
+ double myTime = cpuTime();
+
+ clauses_subsumed = 0;
+ for (const ClauseSimp *it = clauses.getData(), *end = clauses.getDataEnd(); it != end; it++) {
+ if (it->clause == NULL) continue;
+ const Clause& cl = *it->clause;
+
+
+ for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) {
+ seen_tmp[l->toInt()] = true;
+ }
+
+ bool toRemove = false;
+ for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) {
+ const vector<LitExtra>& cache = solver.transOTFCache[l->toInt()].lits;
+ for (vector<LitExtra>::const_iterator cacheLit = cache.begin(), endCache = cache.end(); cacheLit != endCache; cacheLit++) {
+ if (cacheLit->getOnlyNLBin() && seen_tmp[cacheLit->getLit().toInt()]) {
+ toRemove = true;
+ break;
+ }
+ }
+ if (toRemove) break;
+ }
+
+ for (const Lit *l = cl.getData(), *end = cl.getDataEnd(); l != end; l++) {
+ seen_tmp[l->toInt()] = false;
+ }
+
+ if (toRemove) unlinkClause(*it);
+ }
+
+ if (solver.conf.verbosity >= 1) {
+ std::cout << "c Subs w/ non-existent bins: " << std::setw(6) << clauses_subsumed
+ << " time: " << std::fixed << std::setprecision(2) << std::setw(5) << (cpuTime() - myTime) << " s"
+ << std::endl;
+ }
+ totalTime += cpuTime() - myTime;
+
+ return true;
+}
+
+
+const bool Subsumer::treatAndGates()
+{
+ assert(solver.ok);
+
+ andGateNumFound = 0;
+ vec<Lit> lits;
+ andGateTotalSize = 0;
+ uint32_t foundPotential;
+ //double myTime = cpuTime();
+ uint64_t numOp = 0;
+
+ for (vector<OrGate>::const_iterator it = orGates.begin(), end = orGates.end(); it != end; it++) {
+ const OrGate& gate = *it;
+ if (gate.lits.size() > 2) continue;
+ if (!treatAndGate(gate, true, foundPotential, numOp)) return false;
+ }
+
+ //std::cout << "c andgate time : " << (cpuTime() - myTime) << std::endl;
+
+ return true;
+}
+
+const bool Subsumer::treatAndGate(const OrGate& gate, const bool reallyRemove, uint32_t& foundPotential, uint64_t& numOp)
+{
+ assert(gate.lits.size() == 2);
+ std::set<uint32_t> clToUnlink;
+ ClauseSimp other;
+ foundPotential = 0;
+
+ if (occur[(~(gate.lits[0])).toInt()].empty() || occur[(~(gate.lits[1])).toInt()].empty())
+ return true;
+
+ for (uint32_t i = 0; i < sizeSortedOcc.size(); i++)
+ sizeSortedOcc[i].clear();
+
+ const vec<ClauseSimp>& csOther = occur[(~(gate.lits[1])).toInt()];
+ //std::cout << "csother: " << csOther.size() << std::endl;
+ uint32_t abstraction = 0;
+ uint32_t maxSize = 0;
+ for (const ClauseSimp *it2 = csOther.getData(), *end2 = csOther.getDataEnd(); it2 != end2; it2++) {
+ const Clause& cl = *it2->clause;
+ numOp += cl.size();
+ if (defOfOrGate[it2->index]) continue;
+
+ maxSize = std::max(maxSize, cl.size());
+ if (sizeSortedOcc.size() < maxSize+1) sizeSortedOcc.resize(maxSize+1);
+ sizeSortedOcc[cl.size()].push_back(*it2);
+
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ seen_tmp2[cl[i].toInt()] = true;
+ abstraction |= 1 << (cl[i].var() & 31);
+ }
+ }
+ abstraction |= 1 << (gate.lits[0].var() & 31);
+
+ vec<ClauseSimp>& cs = occur[(~(gate.lits[0])).toInt()];
+ //std::cout << "cs: " << cs.size() << std::endl;
+ for (ClauseSimp *it2 = cs.getData(), *end2 = cs.getDataEnd(); it2 != end2; it2++) {
+ const Clause& cl = *it2->clause;
+ if (defOfOrGate[it2->index]
+ || (cl.getAbst() | abstraction) != abstraction
+ || cl.size() > maxSize
+ || sizeSortedOcc[cl.size()].empty()) continue;
+ numOp += cl.size();
+
+ bool OK = true;
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ if (cl[i] == ~(gate.lits[0])) continue;
+ if ( cl[i].var() == ~(gate.lits[1].var())
+ || cl[i].var() == gate.eqLit.var()
+ || !seen_tmp2[cl[i].toInt()]
+ ) {
+ OK = false;
+ break;
+ }
+ }
+ if (!OK) continue;
+
+ uint32_t abst2 = 0;
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ if (cl[i] == ~(gate.lits[0])) continue;
+ seen_tmp[cl[i].toInt()] = true;
+ abst2 |= 1 << (cl[i].var() & 31);
+ }
+ abst2 |= 1 << ((~(gate.lits[1])).var() & 31);
+
+ numOp += sizeSortedOcc[cl.size()].size()*5;
+ const bool foundOther = findAndGateOtherCl(sizeSortedOcc[cl.size()], ~(gate.lits[1]), abst2, other);
+ foundPotential += foundOther;
+ if (reallyRemove && foundOther) {
+ assert(other.index != it2->index);
+ clToUnlink.insert(other.index);
+ clToUnlink.insert(it2->index);
+ if (!treatAndGateClause(other, gate, cl)) return false;
+ }
+
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ seen_tmp[cl[i].toInt()] = false;
+ }
+ }
+
+ std::fill(seen_tmp2.getData(), seen_tmp2.getDataEnd(), 0);
+
+ for(std::set<uint32_t>::const_iterator it2 = clToUnlink.begin(), end2 = clToUnlink.end(); it2 != end2; it2++) {
+ unlinkClause(clauses[*it2]);
+ }
+ clToUnlink.clear();
+
+ return true;
+}
+
+const bool Subsumer::treatAndGateClause(const ClauseSimp& other, const OrGate& gate, const Clause& cl)
+{
+ vec<Lit> lits;
+
+ #ifdef VERBOSE_ORGATE_REPLACE
+ std::cout << "AND gate-based cl rem" << std::endl;
+ std::cout << "clause 1: " << cl << std::endl;
+ std::cout << "clause 2: " << *other.clause << std::endl;
+ std::cout << "gate : " << gate << std::endl;
+ #endif
+
+ lits.clear();
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ if (cl[i] != ~(gate.lits[0])) lits.push(cl[i]);
+
+ assert(cl[i].var() != gate.eqLit.var());
+ }
+ andGateNumFound++;
+ andGateTotalSize += cl.size();
+
+ lits.push(~(gate.eqLit));
+ bool learnt = other.clause->learnt() && cl.learnt();
+ uint32_t glue;
+ if (!learnt) glue = 0;
+ else glue = std::min(other.clause->getGlue(), cl.getGlue());
+
+ #ifdef VERBOSE_ORGATE_REPLACE
+ std::cout << "new clause:" << lits << std::endl;
+ std::cout << "-----------" << std::endl;
+ #endif
+
+ Clause* c = solver.addClauseInt(lits, cl.getGroup(), learnt, glue, false, false);
+ if (c != NULL) linkInClause(*c);
+ if (!solver.ok) return false;
+
+ return true;
+}
+
+inline const bool Subsumer::findAndGateOtherCl(const vector<ClauseSimp>& sizeSortedOcc, const Lit lit, const uint32_t abst2, ClauseSimp& other)
+{
+ for (vector<ClauseSimp>::const_iterator it = sizeSortedOcc.begin(), end = sizeSortedOcc.end(); it != end; it++) {
+ const Clause& cl = *it->clause;
+ if (defOfOrGate[it->index]
+ || cl.getAbst() != abst2) continue;
+
+ for (uint32_t i = 0; i < cl.size(); i++) {
+ if (cl[i] == lit) continue;
+ if (!seen_tmp[cl[i].toInt()]) goto next;
+ }
+ other = *it;
+ return true;
+
+ next:;
+ }
+
+ return false;
+}
+
+void Subsumer::makeAllBinsNonLearnt()
+{
+ uint32_t changedHalfToNonLearnt = 0;
+ uint32_t wsLit = 0;
+ for (vec<Watched> *it = solver.watches.getData(), *end = solver.watches.getDataEnd(); it != end; it++, wsLit++) {
+ Lit lit = ~Lit::toLit(wsLit);
+ vec<Watched>& ws = *it;
+
+ for (Watched *i = ws.getData(), *end2 = ws.getDataEnd(); i != end2; i++) {
+ if (i->isBinary() && i->getLearnt()) {
+ i->setLearnt(false);
+ changedHalfToNonLearnt++;
+ }
+ }
+ }
+
+ assert(changedHalfToNonLearnt % 2 == 0);
+ solver.learnts_literals -= changedHalfToNonLearnt;
+ solver.clauses_literals += changedHalfToNonLearnt;
+}
projects / francis / stp.git / commitdiff