some reorders

This commit is contained in:
Tiago Gomes 2012-11-01 13:56:12 +00:00
parent bfa9648067
commit d4912ea219
2 changed files with 74 additions and 60 deletions

View File

@ -218,64 +218,6 @@ LiftedCircuit::compile (
bool
shatterCountedLogVars (Clauses& clauses, size_t idx1, size_t idx2)
{
Literals lits1 = clauses[idx1].literals();
Literals lits2 = clauses[idx2].literals();
for (size_t i = 0; i < lits1.size(); i++) {
for (size_t j = 0; j < lits2.size(); j++) {
if (lits1[i].lid() == lits2[j].lid()) {
LogVars lvs1 = lits1[i].logVars();
LogVars lvs2 = lits2[j].logVars();
for (size_t k = 0; k < lvs1.size(); k++) {
if (clauses[idx1].isCountedLogVar (lvs1[k])
&& clauses[idx2].isCountedLogVar (lvs2[k]) == false) {
clauses.push_back (clauses[idx2]);
clauses[idx2].addPositiveCountedLogVar (lvs2[k]);
clauses.back().addNegativeCountedLogVar (lvs2[k]);
return true;
}
if (clauses[idx2].isCountedLogVar (lvs2[k])
&& clauses[idx1].isCountedLogVar (lvs1[k]) == false) {
clauses.push_back (clauses[idx1]);
clauses[idx1].addPositiveCountedLogVar (lvs1[k]);
clauses.back().addNegativeCountedLogVar (lvs1[k]);
return true;
}
}
}
}
}
return false;
}
bool
shatterCountedLogVarsAux (Clauses& clauses)
{
for (size_t i = 0; i < clauses.size() - 1; i++) {
for (size_t j = i + 1; j < clauses.size(); j++) {
bool splitedSome = shatterCountedLogVars (clauses, i, j);
if (splitedSome) {
return true;
}
}
}
return false;
}
void
shatterCountedLogVars (Clauses& clauses)
{
while (shatterCountedLogVarsAux (clauses)) ;
}
bool
LiftedCircuit::tryUnitPropagation (
CircuitNode** follow,
@ -562,6 +504,67 @@ LiftedCircuit::tryGrounding (
void
LiftedCircuit::shatterCountedLogVars (Clauses& clauses)
{
while (shatterCountedLogVarsAux (clauses)) ;
}
bool
LiftedCircuit::shatterCountedLogVarsAux (Clauses& clauses)
{
for (size_t i = 0; i < clauses.size() - 1; i++) {
for (size_t j = i + 1; j < clauses.size(); j++) {
bool splitedSome = shatterCountedLogVarsAux (clauses, i, j);
if (splitedSome) {
return true;
}
}
}
return false;
}
bool
LiftedCircuit::shatterCountedLogVarsAux (
Clauses& clauses,
size_t idx1,
size_t idx2)
{
Literals lits1 = clauses[idx1].literals();
Literals lits2 = clauses[idx2].literals();
for (size_t i = 0; i < lits1.size(); i++) {
for (size_t j = 0; j < lits2.size(); j++) {
if (lits1[i].lid() == lits2[j].lid()) {
LogVars lvs1 = lits1[i].logVars();
LogVars lvs2 = lits2[j].logVars();
for (size_t k = 0; k < lvs1.size(); k++) {
if (clauses[idx1].isCountedLogVar (lvs1[k])
&& clauses[idx2].isCountedLogVar (lvs2[k]) == false) {
clauses.push_back (clauses[idx2]);
clauses[idx2].addPositiveCountedLogVar (lvs2[k]);
clauses.back().addNegativeCountedLogVar (lvs2[k]);
return true;
}
if (clauses[idx2].isCountedLogVar (lvs2[k])
&& clauses[idx1].isCountedLogVar (lvs1[k]) == false) {
clauses.push_back (clauses[idx1]);
clauses[idx1].addPositiveCountedLogVar (lvs1[k]);
clauses.back().addNegativeCountedLogVar (lvs1[k]);
return true;
}
}
}
}
}
return false;
}
TinySet<LiteralId>
LiftedCircuit::smoothCircuit (CircuitNode* node)
{

View File

@ -199,16 +199,27 @@ class LiftedCircuit
void compile (CircuitNode** follow, Clauses& clauses);
bool tryUnitPropagation (CircuitNode** follow, Clauses& clauses);
bool tryIndependence (CircuitNode** follow, Clauses& clauses);
bool tryShannonDecomp (CircuitNode** follow, Clauses& clauses);
bool tryInclusionExclusion (CircuitNode** follow, Clauses& clauses);
bool tryIndepPartialGrounding (CircuitNode** follow, Clauses& clauses);
bool tryIndepPartialGroundingAux (Clauses& clauses, ConstraintTree& ct,
vector<unsigned>& indices);
bool tryAtomCounting (CircuitNode** follow, Clauses& clauses);
bool tryGrounding (CircuitNode** follow, Clauses& clauses);
void propagate (const Clause& c, const Clause& uc, Clauses& newClauses);
bool tryAtomCounting (CircuitNode** follow, Clauses& clauses);
bool tryGrounding (CircuitNode** follow, Clauses& clauses);
void shatterCountedLogVars (Clauses& clauses);
bool shatterCountedLogVarsAux (Clauses& clauses);
bool shatterCountedLogVarsAux (Clauses& clauses, size_t idx1, size_t idx2);
TinySet<LiteralId> smoothCircuit (CircuitNode* node);