#ifdef _MSC_VER
#include <msvc/stdint.h>
#else
+#include "SmallPtr.h"
#include <stdint.h>
#endif //_MSC_VER
#include <cstdio>
return ret;
}*/
-//typedef sptr<Clause> ClausePtr;
-//typedef sptr<XorClause> XorClausePtr;
+#ifdef _MSC_VER
typedef Clause* ClausePtr;
typedef XorClause* XorClausePtr;
+#else
+typedef sptr<Clause> ClausePtr;
+typedef sptr<XorClause> XorClausePtr;
+#endif //_MSC_VER
#pragma pack(push)
#pragma pack(1)
else
*j++ = *i;
}
- cs.shrink_(i - j);
+ cs.shrink(i - j);
lastNumUnitarySat[type] = solver.get_unitary_learnts_num();
}
#include "VarReplacer.h"
#include "ClauseCleaner.h"
+#ifdef _MSC_VER
+#define __builtin_prefetch(a,b,c)
+#endif //_MSC_VER
+
//#define VERBOSE_DEUBUG
namespace MINISAT
return;
string name;
- if (name_tmp == NULL)
- name = "";
- else
- name = name_tmp;
+ if (name_tmp == NULL) return;
+ else name = name_tmp;
new_group(group);
cut_name_to_size(name);
-
- if (name.length() == 0) return;
- if (name == "Noname" || name == "") return;
+ if (name == "Noname") return;
if (groupnames[group] == "Noname") {
groupnames[group] = name;
} else if (groupnames[group] != name) {
- printf("Error! Group no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", group, groupnames[group].c_str(), name.c_str());
+ std::cout << "Error! Group no. " << group << "has been named twice. First, as '" << groupnames[group] << "', then second as '" << name << "'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line" << std::endl;
exit(-1);
}
}
MTL = mtl
MTRAND = MTRand
-SOURCES = Logger.cpp Solver.cpp PackedRow.cpp XorFinder.cpp Conglomerate.cpp VarReplacer.cpp FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp Clause.cpp FailedVarSearcher.cpp PartFinder.cpp Subsumer.cpp PartHandler.cpp XorSubsumer.cpp
+SOURCES = Logger.cpp Solver.cpp PackedRow.cpp XorFinder.cpp Conglomerate.cpp VarReplacer.cpp FindUndef.cpp ClauseCleaner.cpp RestartTypeChooser.cpp Clause.cpp FailedVarSearcher.cpp PartFinder.cpp Subsumer.cpp PartHandler.cpp XorSubsumer.cpp SmallPtr.cpp
OBJECTS = $(SOURCES:.cpp=.o)
LIB = libminisat.a
CFLAGS += -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
Solver::Solver() :
// Parameters: (formerly in 'SearchParams')
random_var_freq(0.02)
+ , clause_decay (1 / 0.999)
, restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1)
// More parameters:
}
qhead = trail_lim[level];
trail.shrink(trail.size() - trail_lim[level]);
- trail_lim.shrink_(trail_lim.size() - level);
+ trail_lim.shrink(trail_lim.size() - level);
}
#ifdef VERBOSE_DEBUG
FoundWatch:
;
}
- ws.shrink_(i - j);
+ ws.shrink(i - j);
//Finally, propagate XOR-clauses
if (xorclauses.size() > 0 && !confl) confl = propagate_xors(p);
for (; i < learnts.size(); i++) {
learnts[j++] = learnts[i];
}
- learnts.shrink_(i - j);
+ learnts.shrink(i - j);
}
const vec<Clause*>& Solver::get_learnts() const
if (ok == false)
return l_False;
- XorFinder xorFinder(this, binaryClauses, ClauseCleaner::binaryClauses);
+ XorFinder xorFinder(*this, binaryClauses, ClauseCleaner::binaryClauses);
if (xorFinder.doNoPart(2, 2) == false)
return l_False;
}
varDecayActivity();
+ if (update && restartType == static_restart) claDecayActivity();
return l_Nothing;
}
}
}
+ /*if (findNormalXors && xorclauses.size() > 200 && clauses.size() < MAX_CLAUSENUM_XORFIND/8) {
+ XorFinder xorFinder(*this, clauses, ClauseCleaner::clauses);
+ if (!xorFinder.doNoPart(3, 7)) {
+ status = l_False;
+ goto end;
+ }
+ } else*/ if (xorclauses.size() <= 200 && xorclauses.size() > 0 && nClauses() > 10000) {
+ XorFinder x(*this, clauses, ClauseCleaner::clauses);
+ x.addAllXorAsNorm();
+ }
+
end:
random_var_freq = backup_random_var_freq;
if (verbosity >= 2)
return;
if (findBinaryXors && binaryClauses.size() < MAX_CLAUSENUM_XORFIND) {
- XorFinder xorFinder(this, binaryClauses, ClauseCleaner::binaryClauses);
+ XorFinder xorFinder(*this, binaryClauses, ClauseCleaner::binaryClauses);
if (!xorFinder.doNoPart(2, 2)) return;
if (performReplace && !varReplacer->performReplace(true)) return;
}
if (findNormalXors && clauses.size() < MAX_CLAUSENUM_XORFIND) {
- XorFinder xorFinder(this, clauses, ClauseCleaner::clauses);
+ XorFinder xorFinder(*this, clauses, ClauseCleaner::clauses);
if (!xorFinder.doNoPart(3, 7)) return;
}
// Mode of operation:
//
double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02)
+ double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999)
int restart_first; // The initial restart limit. (default 100)
double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5)
double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)
bool doSubsume1; // Perform clause contraction through resolution
bool failedVarSearch; // Should search for failed vars and doulbly propagated vars
bool libraryUsage; // Set true if not used as a library
- bool sateliteUsed; // whether satielite was used on CNF before calling
friend class FindUndef;
bool greedyUnbound; //If set, then variables will be greedily unbounded (set to l_Undef)
RestartType fixRestartType; // If set, the solver will always choose the given restart strategy
cla_inc *= 1e-20;
}
}
-
+
+inline void Solver::claDecayActivity()
+{
+ cla_inc *= clause_decay;
+}
inline bool Solver::enqueue (Lit p, Clause* from)
{
vec<Lit> tmp;
typedef map<Var, vector<vector<Lit> > > elimType;
elimType::iterator it = elimedOutVar.find(var);
- assert(it != elimedOutVar.end());
solver.setDecisionVar(var, true);
var_elimed[var] = false;
numElimed--;
+
+ //If the variable was removed because of
+ //pure literal removal (by blocked clause
+ //elimination, there are no clauses to re-insert
+ if (it == elimedOutVar.end()) return solver.ok;
+
FILE* backup_libraryCNFfile = solver.libraryCNFFile;
solver.libraryCNFFile = NULL;
for (vector<vector<Lit> >::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
solver.libraryCNFFile = backup_libraryCNFfile;
elimedOutVar.erase(it);
- if (!solver.ok) return false;
- return true;
+ return solver.ok;
}
bool selfSubset(uint32_t A, uint32_t B)
#ifdef VERBOSE_DEBUG
cout << "subsume0 orig clause:";
ps.plainPrint();
- cout << "pointer:" << &ps << endl;
#endif
vec<ClauseSimp> subs;
registerIteration(s1);
#ifdef BIT_MORE_VERBOSITY
- printf(" FIXED-POINT\n");
+ printf("c FIXED-POINT\n");
#endif
// Fixed-point for 1-subsumption:
assert(solver.qhead == solver.trail.size());
#ifdef BIT_MORE_VERBOSITY
- printf("s1.size()=%d cl_touched.size()=%d\n", s1.size(), cl_touched.size());
+ printf("c s1.size()=%d cl_touched.size()=%d\n", s1.size(), cl_touched.size());
#endif
for (CSet::iterator it = s1.begin(), end = s1.end(); it != end; ++it) {
Clause** a = cs.getData();
Clause** b = a;
for (Clause** end = a + cs.size(); a != end; a++) {
- if (numMaxSubsume0 == 0) break;
- if (!(*a)->subsume0IsFinished()) {
+ if (numMaxSubsume0 > 0 && !(*a)->subsume0IsFinished()) {
numMaxSubsume0--;
uint32_t index = subsume0(**a, calcAbstraction(**a));
if (index != std::numeric_limits<uint32_t>::max()) {
clauses.push(c);
subsume1(c);
numMaxSubsume1--;
- if (!solver.ok)
+ if (!solver.ok) {
+ for (; a != end; a++)
+ *b++ = *a;
+ cs.shrink(a-b);
return;
+ }
assert(clauses[c.index].clause != NULL);
clauses.pop();
clauseID--;
else
fullSubsume = false;
+ //For debugging post-c32s-gcdm16-22.cnf --- an instance that is turned SAT to UNSAT if a bug is in the code
+ //numMaxBlockToVisit = std::numeric_limits<int64_t>::max();
+ //numMaxElim = std::numeric_limits<uint32_t>::max();
+ //numMaxSubsume0 = std::numeric_limits<uint32_t>::max();
+ //numMaxSubsume1 = std::numeric_limits<uint32_t>::max();
+ //numMaxBlockVars = std::numeric_limits<uint32_t>::max();
+
#ifdef BIT_MORE_VERBOSITY
std::cout << "c num clauses:" << clauses.size() << std::endl;
std::cout << "c time to link in:" << cpuTime()-myTime << std::endl;
#endif
if (clauses.size() > 10000000) goto endSimplifyBySubsumption;
-
+ if (solver.doBlockedClause && numCalls % 3 == 1) blockedClauseRemoval();
do{
- if (solver.doBlockedClause && numCalls % 3 == 1) blockedClauseRemoval();
-
#ifdef BIT_MORE_VERBOSITY
std::cout << "c time before the start of almost_all/smaller: " << cpuTime() - myTime << std::endl;
#endif
const Var var = touched_list[i];
if (!var_elimed[var] && !cannot_eliminate[var] && solver.decision_var[var] && solver.assigns[var] == l_Undef) {
order.push(touched_list[i]);
- touched[touched_list[i]] = 0;
}
+ touched[var] = 0;
}
touched_list.clear();
}
std::cout << "c time until the end of varelim: " << cpuTime() - myTime << std::endl;
#endif
}
- }while (cl_added.size() > 100);
+ }while (cl_added.size() > 100 && numMaxElim > 0);
endSimplifyBySubsumption:
if (!solver.ok) return false;
return false;
}
- #ifndef DNDEBUG
+ #ifndef NDEBUG
verifyIntegrity();
#endif
addBackToSolver();
solver.nbCompensateSubsumer += origNLearnts-solver.learnts.size();
- if (solver.findNormalXors && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/8) {
- XorFinder xorFinder(&solver, solver.clauses, ClauseCleaner::clauses);
- if (!xorFinder.doNoPart(3, 7)) return false;
- }
if (solver.verbosity >= 1) {
std::cout << "c | lits-rem: " << std::setw(9) << literals_removed
return returnVal;
}
-void Subsumer::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.verbosity >= 1) {
- std::cout << "c | Added XOR as norm:" << added << std::endl;
- }
-}
-
-void Subsumer::addXorAsNormal3(XorClause& c)
-{
- assert(c.size() == 3);
- Clause *tmp;
- vec<Var> vars;
- vec<Lit> vars2(c.size());
- const bool inverted = c.xor_clause_inverted();
-
- 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);
- tmp = solver.addClauseInt(vars2, c.getGroup());
- 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);
- tmp = solver.addClauseInt(vars2, c.getGroup());
- 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);
- tmp = solver.addClauseInt(vars2, c.getGroup());
- 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);
- tmp = solver.addClauseInt(vars2, c.getGroup());
- if (tmp) solver.clauses.push(tmp);
-}
-
-void Subsumer::addXorAsNormal4(XorClause& c)
-{
- assert(c.size() == 4);
- Clause *tmp;
- vec<Var> vars;
- vec<Lit> vars2(c.size());
- const bool inverted = !c.xor_clause_inverted();
-
- 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, c.getGroup());
- 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, c.getGroup());
- 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, c.getGroup());
- 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, c.getGroup());
- 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, c.getGroup());
- 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, c.getGroup());
- 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, c.getGroup());
- 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, c.getGroup());
- if (tmp) solver.clauses.push(tmp);
-}
-
/*vector<char> Subsumer::merge()
{
vector<char> var_merged(solver.nVars(), false);
CryptoMiniSat
-GIT revision: 9653102935b2e707c0aae731704e28809c4b548d
+GIT revision: 36df8dc9098df142071729c19f78002311987863
assert(solver.order_heap.heapProperty());
if (solver.verbosity >= 2)
- std::cout << "c | Replacing " << std::setw(8) << replacedVars-lastReplacedVars << " vars";
+ std::cout << "c | Replacing " << std::setw(8) << replacedVars-lastReplacedVars << " vars" << std::flush;
lastReplacedVars = replacedVars;
clauses.clear();
if (solver.verbosity >= 2) {
- std::cout << "c | Replaced " << std::setw(8) << replacedLits<< " lits"
- << " Time: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime()-time << " s "
- << std::setw(12) << " |" << std::endl;
+ std::cout << " Replaced " << std::setw(8) << replacedLits<< " lits"
+ << " Time: " << std::setw(8) << std::fixed << std::setprecision(2) << cpuTime()-time << " s "
+ << std::setw(10) << " |" << std::endl;
}
replacedLits = 0;
using std::make_pair;
-XorFinder::XorFinder(Solver* _s, vec<Clause*>& _cls, ClauseCleaner::ClauseSetType _type) :
+XorFinder::XorFinder(Solver& _solver, vec<Clause*>& _cls, ClauseCleaner::ClauseSetType _type) :
cls(_cls)
, type(_type)
- , S(_s)
+ , solver(_solver)
{
}
uint sumLengths = 0;
double time = cpuTime();
foundXors = 0;
- S->clauseCleaner->cleanClauses(cls, type);
- if (S->ok == false)
+ solver.clauseCleaner->cleanClauses(cls, type);
+ if (solver.ok == false)
return false;
toRemove.clear();
if (!sorted) break;
}
if (!sorted) {
- S->detachClause(c);
+ solver.detachClause(c);
std::sort(c.getData(), c.getData()+c.size());
- S->attachClause(c);
+ solver.attachClause(c);
}
} else {
std::sort(c.getData(), c.getData()+c.size());
#endif //DEBUG_XORFIND
if (findXors(sumLengths) == false) goto end;
- S->ok = (S->propagate() == NULL);
+ solver.ok = (solver.propagate() == NULL);
end:
- if (S->verbosity >= 2) {
- if (minSize == maxSize && minSize == 2)
+ if (minSize == maxSize && minSize == 2) {
+ if (solver.verbosity >= 2 || (solver.conflicts == 0 && solver.verbosity >= 1)) {
printf("c | Finding binary XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
- else
+ }
+ } else {
+ if (solver.verbosity >= 2 || (solver.verbosity >= 1 && foundXors > 0)) {
printf("c | Finding non-binary XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
+ }
}
i = 0;
}
cls.shrink(i-j);
- return S->ok;
+ return solver.ok;
}
const bool XorFinder::findXors(uint& sumLengths)
it->first->plainPrint();
#endif
toRemove[it->second] = true;
- S->removeClause(*it->first);
+ solver.removeClause(*it->first);
}
switch(lits.size()) {
case 2: {
- S->varReplacer->replace(lits, impair, old_group);
+ solver.varReplacer->replace(lits, impair, old_group);
#ifdef VERBOSE_DEBUG
XorClause* x = XorClause_new(lits, impair, old_group);
}
default: {
XorClause* x = XorClause_new(lits, impair, old_group);
- S->xorclauses.push(x);
- S->attachClause(*x);
+ solver.xorclauses.push(x);
+ solver.attachClause(*x);
#ifdef VERBOSE_DEBUG
cout << "- Final xor-clause: ";
sumLengths += lits.size();
}
- return S->ok;
+ return solver.ok;
}
void XorFinder::clearToRemove()
}
}
+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.verbosity >= 1) {
+ std::cout << "c | Added XOR as norm:" << added << std::endl;
+ }
+}
+
+void XorFinder::addXorAsNormal3(XorClause& c)
+{
+ assert(c.size() == 3);
+ Clause *tmp;
+ vec<Var> vars;
+ vec<Lit> vars2(c.size());
+ const bool inverted = c.xor_clause_inverted();
+
+ 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);
+ tmp = solver.addClauseInt(vars2, c.getGroup());
+ 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);
+ tmp = solver.addClauseInt(vars2, c.getGroup());
+ 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);
+ tmp = solver.addClauseInt(vars2, c.getGroup());
+ 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);
+ tmp = solver.addClauseInt(vars2, c.getGroup());
+ if (tmp) solver.clauses.push(tmp);
+}
+
+void XorFinder::addXorAsNormal4(XorClause& c)
+{
+ assert(c.size() == 4);
+ Clause *tmp;
+ vec<Var> vars;
+ vec<Lit> vars2(c.size());
+ const bool inverted = !c.xor_clause_inverted();
+
+ 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, c.getGroup());
+ 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, c.getGroup());
+ 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, c.getGroup());
+ 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, c.getGroup());
+ 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, c.getGroup());
+ 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, c.getGroup());
+ 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, c.getGroup());
+ 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, c.getGroup());
+ if (tmp) solver.clauses.push(tmp);
+}
+
+
}; //NAMESPACE MINISAT
{
public:
- XorFinder(Solver* S, vec<Clause*>& cls, ClauseCleaner::ClauseSetType _type);
+ XorFinder(Solver& _solver, vec<Clause*>& cls, ClauseCleaner::ClauseSetType _type);
const bool doNoPart(const uint minSize, const uint maxSize);
+ void addAllXorAsNorm();
private:
typedef vector<pair<Clause*, uint> > ClauseTable;
void clearToRemove();
uint32_t foundXors;
+ //For adding xor as norm
+ void addXorAsNormal3(XorClause& c);
+ void addXorAsNormal4(XorClause& c);
+
vec<Clause*>& cls;
ClauseCleaner::ClauseSetType type;
void countImpairs(const ClauseTable::iterator& begin, const ClauseTable::iterator& end, uint& numImpair, uint& numPair) const;
bool isXor(const uint32_t size, const ClauseTable::iterator& begin, const ClauseTable::iterator& end, bool& impair);
- Solver* S;
+ Solver& solver;
};
}; //NAMESPACE MINISAT
projects / francis / stp.git / commitdiff