some clean ups

This commit is contained in:
Tiago Gomes 2012-12-09 22:13:58 +00:00
parent e46d2177b7
commit 90736156ae
2 changed files with 38 additions and 49 deletions

View File

@ -101,9 +101,7 @@ LeafNode::weight (void) const
lvs -= clause_->negCountedLogVars();
unsigned nrGroundings = 1;
if (lvs.empty() == false) {
ConstraintTree ct = clause_->constr();
ct.project (lvs);
nrGroundings = ct.size();
nrGroundings = clause_->constr().projectedCopy (lvs).size();
}
if (clause_->posCountedLogVars().empty() == false) {
nrGroundings *= std::pow (SetOrNode::nrPositives(),
@ -113,7 +111,7 @@ LeafNode::weight (void) const
nrGroundings *= std::pow (SetOrNode::nrNegatives(),
clause_->nrNegCountedLogVars());
}
return Globals::logDomain
return Globals::logDomain
? weight * nrGroundings
: std::pow (weight, nrGroundings);
}
@ -134,9 +132,7 @@ SmoothNode::weight (void) const
lvs -= cs[i]->negCountedLogVars();
unsigned nrGroundings = 1;
if (lvs.empty() == false) {
ConstraintTree ct = cs[i]->constr();
ct.project (lvs);
nrGroundings = ct.size();
nrGroundings = cs[i]->constr().projectedCopy (lvs).size();
}
if (cs[i]->posCountedLogVars().empty() == false) {
nrGroundings *= std::pow (SetOrNode::nrPositives(),
@ -169,7 +165,7 @@ double
CompilationFailedNode::weight (void) const
{
// weighted model counting in compilation
// failed nodes should give nan
// failed nodes should give NaN
return 0.0 / 0.0;
}
@ -474,13 +470,11 @@ LiftedCircuit::tryInclusionExclusion (
for (size_t j = 0; j < indepLits.size(); j++) {
c2->addLiteral (indepLits[j]);
}
clauses.erase (clauses.begin() + i);
Clauses plus1Clauses = Clause::copyClauses (clauses);
Clauses plus2Clauses = Clause::copyClauses (clauses);
plus1Clauses.erase (plus1Clauses.begin() + i);
plus2Clauses.erase (plus2Clauses.begin() + i);
clauses.erase (clauses.begin() + i);
plus1Clauses.push_back (c1);
plus2Clauses.push_back (c2);
clauses.push_back (c1);
@ -744,7 +738,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
propagLits |= lids2;
break;
}
case CircuitNodeType::AND_NODE: {
AndNode* casted = dynamic_cast<AndNode*>(node);
LitLvTypesSet lids1 = smoothCircuit (*casted->leftBranch());
@ -785,13 +779,13 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
}
break;
}
case CircuitNodeType::SET_AND_NODE: {
SetAndNode* casted = dynamic_cast<SetAndNode*>(node);
propagLits = smoothCircuit (*casted->follow());
break;
}
case CircuitNodeType::INC_EXC_NODE: {
IncExcNode* casted = dynamic_cast<IncExcNode*>(node);
LitLvTypesSet lids1 = smoothCircuit (*casted->plus1Branch());
@ -804,18 +798,18 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
propagLits |= lids2;
break;
}
case CircuitNodeType::LEAF_NODE: {
LeafNode* casted = dynamic_cast<LeafNode*>(node);
propagLits.insert (LitLvTypes (
casted->clause()->literals()[0].lid(),
casted->clause()->logVarTypes(0)));
}
default:
break;
}
return propagLits;
}
@ -828,9 +822,14 @@ LiftedCircuit::createSmoothNode (
{
if (missingLits.empty() == false) {
if (Globals::verbosity > 1) {
// assert (Util::contains (originClausesMap_, prev));
backupClauses_ = originClausesMap_[*prev]; // TODO Clause::copyClauses ?
}
unordered_map<CircuitNode*, Clauses>::iterator it;
it = originClausesMap_.find (*prev);
if (it != originClausesMap_.end()) {
backupClauses_ = it->second;
} else {
backupClauses_ = { ((dynamic_cast<LeafNode*>(*prev))->clause()) };
}
}
Clauses clauses;
for (size_t i = 0; i < missingLits.size(); i++) {
LiteralId lid = missingLits[i].lid();
@ -1127,21 +1126,18 @@ LiftedCircuit::printClauses (
if (Util::contains (originClausesMap_, node)) {
clauses = originClausesMap_[node];
} else if (getCircuitNodeType (node) == CircuitNodeType::LEAF_NODE) {
clauses = { (dynamic_cast<LeafNode*>(node))->clause() } ;
clauses = { (dynamic_cast<LeafNode*>(node))->clause() } ;
} else if (getCircuitNodeType (node) == CircuitNodeType::SMOOTH_NODE) {
clauses = (dynamic_cast<SmoothNode*>(node))->clauses();
clauses = (dynamic_cast<SmoothNode*>(node))->clauses();
}
if (clauses.empty() == false) {
os << escapeNode (node);
os << " [shape=box," << extraOptions << "label=\"" ;
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << *clauses[i];
}
os << "\"]" ;
os << endl;
} else {
os << " [shape=box]" << endl;
assert (clauses.empty() == false);
os << escapeNode (node);
os << " [shape=box," << extraOptions << "label=\"" ;
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << *clauses[i];
}
os << "\"]" ;
os << endl;
}

View File

@ -33,11 +33,6 @@ Literal::toString (
{
stringstream ss;
negated_ ? ss << "¬" : ss << "" ;
// if (negated_ == false) {
// posWeight_ < 0.0 ? ss << "λ" : ss << "Θ" ;
// } else {
// negWeight_ < 0.0 ? ss << "λ" : ss << "Θ" ;
// }
ss << "λ" ;
ss << lid_ ;
if (logVars_.empty() == false) {
@ -480,16 +475,14 @@ LiftedWCNF::createClause (LiteralId lid) const
const Literals& literals = clauses_[i]->literals();
for (size_t j = 0; j < literals.size(); j++) {
if (literals[j].lid() == lid) {
// TODO projectedCopy ?
ConstraintTree ct = clauses_[i]->constr();
ct.project (literals[j].logVars());
ConstraintTree ct = clauses_[i]->constr().projectedCopy (
literals[j].logVars());
Clause* c = new Clause (ct);
c->addLiteral (literals[j]);
return c;
}
}
}
abort(); // we should not reach this point
return 0;
}
@ -512,8 +505,8 @@ LiftedWCNF::addIndicatorClauses (const ParfactorList& pfList)
const ProbFormulas& formulas = (*it)->arguments();
for (size_t i = 0; i < formulas.size(); i++) {
if (Util::contains (map_, formulas[i].group()) == false) {
ConstraintTree tempConstr = *(*it)->constr();
tempConstr.project (formulas[i].logVars());
ConstraintTree tempConstr = (*it)->constr()->projectedCopy(
formulas[i].logVars());
Clause* clause = new Clause (tempConstr);
vector<LiteralId> lids;
for (size_t j = 0; j < formulas[i].range(); j++) {
@ -524,8 +517,8 @@ LiftedWCNF::addIndicatorClauses (const ParfactorList& pfList)
clauses_.push_back (clause);
for (size_t j = 0; j < formulas[i].range() - 1; j++) {
for (size_t k = j + 1; k < formulas[i].range(); k++) {
ConstraintTree tempConstr2 = *(*it)->constr();
tempConstr2.project (formulas[i].logVars());
ConstraintTree tempConstr2 = (*it)->constr()->projectedCopy (
formulas[i].logVars());
Clause* clause2 = new Clause (tempConstr2);
clause2->addLiteralComplemented (Literal (clause->literals()[j]));
clause2->addLiteralComplemented (Literal (clause->literals()[k]));
@ -598,8 +591,8 @@ LiftedWCNF::printFormulaIndicators (void) const
if (Util::contains (allGroups, formulas[i].group()) == false) {
allGroups.insert (formulas[i].group());
cout << formulas[i] << " | " ;
ConstraintTree tempCt = *(*it)->constr();
tempCt.project (formulas[i].logVars());
ConstraintTree tempCt = (*it)->constr()->projectedCopy (
formulas[i].logVars());
cout << tempCt.tupleSet();
cout << " indicators => " ;
vector<LiteralId> indicators =