Lkc: Fix smoothing in atom counting nodes
This commit is contained in:
parent
bb68afe91d
commit
a59c152962
@ -592,7 +592,7 @@ LiftedCircuit::tryAtomCounting (
|
|||||||
}
|
}
|
||||||
if (Globals::verbosity > 1) {
|
if (Globals::verbosity > 1) {
|
||||||
backupClauses_ = Clause::copyClauses (clauses);
|
backupClauses_ = Clause::copyClauses (clauses);
|
||||||
}
|
}
|
||||||
for (size_t i = 0; i < clauses.size(); i++) {
|
for (size_t i = 0; i < clauses.size(); i++) {
|
||||||
Literals literals = clauses[i]->literals();
|
Literals literals = clauses[i]->literals();
|
||||||
for (size_t j = 0; j < literals.size(); j++) {
|
for (size_t j = 0; j < literals.size(); j++) {
|
||||||
@ -765,7 +765,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
bool typeFound = false;
|
bool typeFound = false;
|
||||||
for (size_t k = 0; k < propagLits.size(); k++) {
|
for (size_t k = 0; k < propagLits.size(); k++) {
|
||||||
if (litSet[i].first == propagLits[k].lid()
|
if (litSet[i].first == propagLits[k].lid()
|
||||||
&& containsTypes (allTypes[j], propagLits[k].logVarTypes())) {
|
&& containsTypes (propagLits[k].logVarTypes(), allTypes[j])) {
|
||||||
typeFound = true;
|
typeFound = true;
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
@ -776,8 +776,13 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
createSmoothNode (missingLids, casted->follow());
|
createSmoothNode (missingLids, casted->follow());
|
||||||
for (size_t i = 0; i < propagLits.size(); i++) {
|
// setAllFullLogVars() can cause repeated elements in
|
||||||
propagLits[i].setAllFullLogVars();
|
// the set. Fix this by reconstructing the set again
|
||||||
|
LitLvTypesSet copy = propagLits;
|
||||||
|
propagLits.clear();
|
||||||
|
for (size_t i = 0; i < copy.size(); i++) {
|
||||||
|
copy[i].setAllFullLogVars();
|
||||||
|
propagLits.insert (copy[i]);
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
|
Reference in New Issue
Block a user