IncExc: check if log vars are count normalized

This commit is contained in:
Tiago Gomes 2012-11-14 14:43:56 +00:00
parent f5c85ffcc9
commit 9202e286f8
2 changed files with 14 additions and 9 deletions

View File

@ -37,14 +37,15 @@ SetOrNode::weight (void) const
double w = std::log (Util::nrCombinations (nrGroundings_, i));
weightSum = Util::logSum (weightSum, w + follow_->weight());
} else {
cout << endl;
cout << "nr groundings = " << nrGroundings_ << endl;
cout << "nr positives = " << nrPositives() << endl;
cout << "nr negatives = " << nrNegatives() << endl;
cout << "i = " << i << endl;
cout << "nr combos = " << Util::nrCombinations (nrGroundings_, i) << endl;
// cout << endl;
// cout << "nr groundings = " << nrGroundings_ << endl;
// cout << "nr positives = " << nrPositives() << endl;
// cout << "nr negatives = " << nrNegatives() << endl;
// cout << "i = " << i << endl;
// cout << "nr combos = " ;
// cout << Util::nrCombinations (nrGroundings_, i) << endl;
double w = follow_->weight();
cout << "weight = " << w << endl;
// cout << "weight = " << w << endl;
weightSum += Util::nrCombinations (nrGroundings_, i) * w;
}
}
@ -411,15 +412,20 @@ LiftedCircuit::tryInclusionExclusion (
}
}
if (indepLits.empty() == false) {
// TODO this should be have to be count normalized too
LogVarSet lvs1;
for (size_t j = 0; j < depLits.size(); j++) {
lvs1 |= depLits[j].logVarSet();
}
if (clauses[i].constr().isCountNormalized (lvs1) == false) {
break;
}
LogVarSet lvs2;
for (size_t j = 0; j < indepLits.size(); j++) {
lvs2 |= indepLits[j].logVarSet();
}
if (clauses[i].constr().isCountNormalized (lvs2) == false) {
break;
}
Clause c1 (clauses[i].constr().projectedCopy (lvs1));
for (size_t j = 0; j < depLits.size(); j++) {
c1.addLiteral (depLits[j]);

View File

@ -269,4 +269,3 @@ LiftedOperations::absorve (
return absorvedPfs;
}