}
// -- use this function instead:
- friend Clause* Clause_new(const vec<Lit>& ps, const uint group, const bool learnt = false);
- friend Clause* Clause_new(const vector<Lit>& ps, const uint group, const bool learnt = false);
+ template<class T>
+ friend Clause* Clause_new(const T& ps, const uint group, const bool learnt = false);
uint size () const {
return size_etc >> 16;
// -- use this function instead:
template<class V>
- friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group) {
- void* mem = malloc(sizeof(XorClause) + sizeof(Lit)*(ps.size()));
- XorClause* real= new (mem) XorClause(ps, inverted, group);
- return real;
- }
+ friend XorClause* XorClause_new(const V& ps, const bool inverted, const uint group);
inline bool xor_clause_inverted() const
{
Clause* real= new (mem) Clause(ps, group, learnt);
return real;
}
-//Clause* Clause_new(const vector<Lit>& ps, const uint group, const bool learnt);
+
+template<class T>
+XorClause* XorClause_new(const T& ps, const bool inverted, const uint group)
+{
+ void* mem = malloc(sizeof(XorClause) + sizeof(Lit)*(ps.size()));
+ XorClause* real= new (mem) XorClause(ps, inverted, group);
+ return real;
+}
/*_________________________________________________________________________________________________
|
#include <utility>
#include <algorithm>
+using std::make_pair;
//#define VERBOSE_DEBUG
using std::endl;
#endif
-using std::make_pair;
namespace MINISAT
{
S(_S)
{}
+Conglomerate::~Conglomerate()
+{
+ for(uint i = 0; i < calcAtFinish.size(); i++)
+ free(calcAtFinish[i]);
+}
+
const vec<XorClause*>& Conglomerate::getCalcAtFinish() const
{
return calcAtFinish;
for (Lit* it = &(S->trail[0]), *end = it + S->trail.size(); it != end; it++)
blocked[it->var()] = true;
+ const vec<Clause*>& tmp = S->toReplace->getToRemove();
+ for (Clause *const*it = tmp.getData(), *const*end = it + tmp.size(); it != end; it++) {
+ const Clause& c = **it;
+ for (const Lit* a = &c[0], *end = a + c.size(); a != end; a++) {
+ blocked[a->var()] = true;
+ }
+ }
+
uint i = 0;
for (XorClause* const* it = S->xorclauses.getData(), *const*end = it + S->xorclauses.size(); it != end; it++, i++) {
const XorClause& c = **it;
varToXor[a->var()].push_back(make_pair(*it, i));
}
}
-
- const vector<Lit>& replaceTable = S->toReplace->getReplaceTable();
- for (uint i = 0; i < replaceTable.size(); i++) {
- if (replaceTable[i] != Lit(i, false)) {
- blocked[i] = true;
- blocked[replaceTable[i].var()] = true;
- }
- }
}
void Conglomerate::process_clause(XorClause& x, const uint num, uint var, vec<Lit>& vars) {
{
if (S->xorclauses.size() == 0)
return 0;
+ toRemove.clear();
toRemove.resize(S->xorclauses.size(), false);
#ifdef VERBOSE_DEBUG
cout << "Finding conglomerate xors started" << endl;
#endif
+ S->removeSatisfied(S->xorclauses);
+ S->cleanClauses(S->xorclauses);
+
fillVarToXor();
uint found = 0;
#endif
S->xorclauses.push(newX);
- S->xorclauses_tofree.push(newX);
toRemove.push_back(false);
S->attachClause(*newX);
for (const Lit * a = &((*newX)[0]), *end = a + newX->size(); a != end; a++) {
}
}
+void Conglomerate::addRemovedClauses()
+{
+ #ifdef VERBOSE_DEBUG
+ cout << "Executing addRemovedClauses" << endl;
+ #endif
+
+ char tmp[100];
+ tmp[0] = '\0';
+ vec<Lit> ps;
+ for(uint i = 0; i < calcAtFinish.size(); i++)
+ {
+ XorClause& c = *calcAtFinish[i];
+ #ifdef VERBOSE_DEBUG
+ cout << "readding already removed (conglomerated) clause: ";
+ c.plain_print();
+ #endif
+
+ ps.clear();
+ for(uint i2 = 0; i2 != c.size() ; i2++) {
+ ps.push(c[i2]);
+ S->setDecisionVar(c[i2].var(), true);
+ }
+ S->addXorClause(ps, c.xor_clause_inverted(), c.group, tmp);
+ free(&c);
+ }
+ calcAtFinish.clear();
+}
+
};
{
public:
Conglomerate(Solver *S);
+ ~Conglomerate();
uint conglomerateXors(); ///<Conglomerate XOR-s that are attached using a variable
+ void addRemovedClauses(); ///<Add clauses that have been removed. Used if solve() is called multiple times
void doCalcAtFinish(); ///<Calculate variables removed during conglomeration
const vec<XorClause*>& getCalcAtFinish() const;
vec<XorClause*>& getCalcAtFinish();
#include <iomanip>
#include "Clause.h"
#include <algorithm>
+using std::ostream;
+using std::cout;
+using std::endl;
#ifdef VERBOSE_DEBUG
#include <iterator>
{
using namespace MINISAT;
-using std::ostream;
-using std::cout;
-using std::endl;
-
ostream& operator << (ostream& os, const vec<Lit>& v)
{
for (int i = 0; i < v.size(); i++) {
if (name.length() == 0) return;
+ if (name == "Noname" || name == "") return;
+
if (groupnames[group] == "Noname") {
groupnames[group] = name;
} else if (groupnames[group] != name) {
//=================================================================================================
// Constructor/Destructor:
+
Solver::Solver() :
// Parameters: (formerly in 'SearchParams')
var_decay(1 / 0.95), random_var_freq(0.02)
, restrictedPickBranch(0)
, useRealUnknowns (false)
, xorFinder (true)
+ , performReplace (true)
, greedyUnbound (false)
// Statistics: (formerly in 'SolverStats')
for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_learnts[i]);
for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
- for (int i = 0; i < xorclauses_tofree.size(); i++) free(xorclauses_tofree[i]);
+ for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[i]);
for (uint i = 0; i < gauss_matrixes.size(); i++) delete gauss_matrixes[i];
gauss_matrixes.clear();
delete toReplace;
Lit p;
int i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- //ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+ ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
xor_clause_inverted ^= ps[i].sign();
ps[i] ^= ps[i].sign();
XorClause* c = XorClause_new(ps, xor_clause_inverted, group);
xorclauses.push(c);
- xorclauses_tofree.push(c);
attachClause(*c);
toReplace->newClause();
break;
Lit p;
int i, j;
for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
- //ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
+ ps[i] = toReplace->getReplaceTable()[ps[i].var()] ^ ps[i].sign();
if (value(ps[i]) == l_True || ps[i] == ~p)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
#endif
}
-//Permutates the clauses in the solver. Very useful to calcuate the average time it takes the solver to solve the prolbem
-void Solver::permutateClauses()
-{
- for (int i = 0; i < clauses.size(); i++) {
- int j = mtrand.randInt(i);
- Clause* tmp = clauses[i];
- clauses[i] = clauses[j];
- clauses[j] = tmp;
- }
-
- for (int i = 0; i < xorclauses.size(); i++) {
- int j = mtrand.randInt(i);
- XorClause* tmp = xorclauses[i];
- xorclauses[i] = xorclauses[j];
- xorclauses[j] = tmp;
- }
-}
-
void Solver::setRealUnknown(const uint var)
{
if (realUnknowns.size() < var+1)
nbclausesbeforereduce = (nClauses() * learntsize_factor)/2;
}
- //toReplace->performReplace();
- //if (!ok) return l_False;
+ conglomerate->addRemovedClauses();
+
+ if (performReplace) {
+ toReplace->performReplace();
+ if (!ok) return l_False;
+ }
if (xorFinder) {
double time;
uint sumLengths = 0;
XorFinder xorFinder(this, clauses);
uint foundXors = xorFinder.doNoPart(sumLengths, 2, 10);
+ if (!ok) return l_False;
if (verbosity >=1)
printf("| Finding XORs: %5.2lf s (found: %7d, avg size: %3.1lf) |\n", cpuTime()-time, foundXors, (double)sumLengths/(double)foundXors);
- if (!ok) return l_False;
+
+ if (performReplace) {
+ toReplace->performReplace();
+ if (!ok) return l_False;
+ }
}
if (xorclauses.size() > 1) {
}
time = cpuTime();
- removeSatisfied(xorclauses);
- cleanClauses(xorclauses);
uint foundCong = conglomerate->conglomerateXors();
if (verbosity >=1)
printf("| Conglomerating XORs: %4.2lf s (removed %6d vars) |\n", cpuTime()-time, foundCong);
printf("| Sum xclauses before: %8d, after: %12d |\n", orig_num_cls, new_num_cls);
printf("| Sum xlits before: %11d, after: %12d |\n", orig_total, new_total);
}
+
+ if (performReplace) {
+ toReplace->performReplace();
+ if (!ok) return l_False;
+ }
}
}
- //toReplace->performReplace();
- //if (!ok) return l_False;
-
if (gaussconfig.decision_until > 0 && xorclauses.size() > 1 && xorclauses.size() < 20000) {
removeSatisfied(xorclauses);
cleanClauses(xorclauses);
if (verbosity >=1)
printf("| Finding matrixes : %4.2lf s (found %5d) |\n", cpuTime()-time, numMatrixes);
}
+
if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) {
printf("============================[ Search Statistics ]========================================\n");
bool final = c.xor_clause_inverted();
#ifdef VERBOSE_DEBUG
- std::sort(&c[0], &c[0] + c.size());
- c.plain_print();
+ XorClause* c2 = XorClause_new(c, c.xor_clause_inverted(), c.group);
+ std::sort(c2->getData(), c2->getData()+ c2->size());
+ c2->plain_print();
+ free(c2);
#endif
for (uint j = 0; j < c.size(); j++) {
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
void setSeed (const uint32_t seed); // Sets the seed to be the given number
- void permutateClauses(); // Permutates the clauses using the seed. It updates the seed in mtrand
void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown
void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on)
void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value
bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE)
int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false)
int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0)
- uint restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all])
+ Var restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all])
bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true
vector<bool> realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable
bool xorFinder; // Automatically find xor-clauses and convert them
+ bool performReplace; // Should var-replacing be performed?
friend class FindUndef;
bool greedyUnbound; //If set to TRUE, then we will greedily unbound variables (set them to l_Undef)
void set_gaussian_decision_until(const uint to);
//
bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
vec<Clause*> clauses; // List of problem clauses.
- vec<XorClause*> xorclauses; // List of problem xor-clauses. Will not be freed
- vec<XorClause*> xorclauses_tofree;// List of problem xor-clauses. Will be freed
+ vec<XorClause*> xorclauses; // List of problem xor-clauses. Will be freed
vec<Clause*> learnts; // List of learnt clauses.
vec<Clause*> unitary_learnts; // List of learnt clauses.
vec<double> activity; // A heuristic measurement of the activity of a variable.
CryptoMiniSat
-SVN revision: 504
-GIT revision: 4f460459f42a5fd33d971a19f9c206985a73c40d
+SVN revision: 519
+GIT revision: 0426e61b02a00a073a87fdffc0282820875fad61
return replacingVars;
}
+const vec<Clause*>& VarReplacer::getToRemove() const
+{
+ return toRemove;
+}
+
void VarReplacer::extendModel() const
{
uint i = 0;
const uint getNumReplacedVars() const;
const vector<Var> getReplacingVars() const;
const vector<Lit>& getReplaceTable() const;
+ const vec<Clause*>& getToRemove() const;
void newClause();
void newVar();
default: {
XorClause* x = XorClause_new(lits, impair, old_group);
S->xorclauses.push(x);
- S->xorclauses_tofree.push(x);
S->attachClause(*x);
#ifdef VERBOSE_DEBUG
projects / francis / stp.git / commitdiff