refactor exportToGraphViz

This commit is contained in:
Tiago Gomes 2012-10-30 14:31:52 +00:00
parent a75799b34f
commit b31a047635
2 changed files with 37 additions and 61 deletions

View File

@ -261,6 +261,7 @@ LiftedCircuit::tryUnitPropagation (
} }
} }
stringstream explanation; stringstream explanation;
explanation << " UP on" << clauses[i].literals()[0];
AndNode* andNode = new AndNode (clauses, explanation.str()); AndNode* andNode = new AndNode (clauses, explanation.str());
Clauses leftClauses = {clauses[i]}; Clauses leftClauses = {clauses[i]};
compile (andNode->leftBranch(), leftClauses); compile (andNode->leftBranch(), leftClauses);
@ -282,12 +283,13 @@ LiftedCircuit::tryIndependence (
if (clauses.size() == 1) { if (clauses.size() == 1) {
return false; return false;
} }
// TODO this independence is a little weak
for (size_t i = 0; i < clauses.size(); i++) { for (size_t i = 0; i < clauses.size(); i++) {
bool indep = true; bool indep = true;
TinySet<LiteralId> lids1 = clauses[i].lidSet(); TinySet<LiteralId> lids1 = clauses[i].lidSet();
for (size_t j = 0; j < clauses.size(); j++) { for (size_t j = 0; j < clauses.size(); j++) {
TinySet<LiteralId> lids2 = clauses[j].lidSet(); TinySet<LiteralId> lids2 = clauses[j].lidSet();
if (((lids1 & lids2).empty() == false) && i != j) { if (i != j && ((lids1 & lids2).empty() == false)) {
indep = false; indep = false;
break; break;
} }
@ -296,7 +298,7 @@ LiftedCircuit::tryIndependence (
Clauses newClauses = clauses; Clauses newClauses = clauses;
newClauses.erase (newClauses.begin() + i); newClauses.erase (newClauses.begin() + i);
stringstream explanation; stringstream explanation;
explanation << " independence" ; explanation << " Independence on clause Nº " << i ;
AndNode* andNode = new AndNode (clauses, explanation.str()); AndNode* andNode = new AndNode (clauses, explanation.str());
Clauses indepClause = {clauses[i]}; Clauses indepClause = {clauses[i]};
compile (andNode->leftBranch(), indepClause); compile (andNode->leftBranch(), indepClause);
@ -506,7 +508,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
SmoothNode* smoothNode = new SmoothNode (clauses); SmoothNode* smoothNode = new SmoothNode (clauses);
CircuitNode** prev = casted->leftBranch(); CircuitNode** prev = casted->leftBranch();
AndNode* andNode = new AndNode ((*prev)->clauses(), AndNode* andNode = new AndNode ((*prev)->clauses(),
smoothNode, *prev, " smoothing"); smoothNode, *prev, " Smoothing");
*prev = andNode; *prev = andNode;
} }
if (missingRight.empty() == false) { if (missingRight.empty() == false) {
@ -519,7 +521,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node)
SmoothNode* smoothNode = new SmoothNode (clauses); SmoothNode* smoothNode = new SmoothNode (clauses);
CircuitNode** prev = casted->rightBranch(); CircuitNode** prev = casted->rightBranch();
AndNode* andNode = new AndNode ((*prev)->clauses(), smoothNode, AndNode* andNode = new AndNode ((*prev)->clauses(), smoothNode,
*prev, " smoothing"); *prev, " Smoothing");
*prev = andNode; *prev = andNode;
} }
propagatingLids |= lids1; propagatingLids |= lids1;
@ -624,16 +626,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
case OR_NODE: { case OR_NODE: {
OrNode* casted = dynamic_cast<OrNode*>(node); OrNode* casted = dynamic_cast<OrNode*>(node);
const Clauses& clauses = node->clauses(); printClauses (casted, os);
if (clauses.empty() == false) {
os << escapeNode (node) << " [shape=box,label=\"" ;
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << clauses[i];
}
os << "\"]" ;
os << endl;
}
os << auxNode << " [label=\"\"]" << endl; os << auxNode << " [label=\"\"]" << endl;
os << escapeNode (node) << " -> " << auxNode; os << escapeNode (node) << " -> " << auxNode;
@ -657,14 +650,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
case AND_NODE: { case AND_NODE: {
AndNode* casted = dynamic_cast<AndNode*>(node); AndNode* casted = dynamic_cast<AndNode*>(node);
const Clauses& clauses = node->clauses(); printClauses (casted, os);
os << escapeNode (node) << " [shape=box,label=\"" ;
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << clauses[i];
}
os << "\"]" ;
os << endl;
os << auxNode << " [label=\"\"]" << endl; os << auxNode << " [label=\"\"]" << endl;
os << escapeNode (node) << " -> " << auxNode; os << escapeNode (node) << " -> " << auxNode;
@ -693,14 +679,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
case SET_AND_NODE: { case SET_AND_NODE: {
SetAndNode* casted = dynamic_cast<SetAndNode*>(node); SetAndNode* casted = dynamic_cast<SetAndNode*>(node);
const Clauses& clauses = node->clauses(); printClauses (casted, os);
os << escapeNode (node) << " [shape=box,label=\"" ;
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << clauses[i];
}
os << "\"]" ;
os << endl;
os << auxNode << " [label=\"∧(X)\"]" << endl; os << auxNode << " [label=\"∧(X)\"]" << endl;
os << escapeNode (node) << " -> " << auxNode; os << escapeNode (node) << " -> " << auxNode;
@ -718,14 +697,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
case INC_EXC_NODE: { case INC_EXC_NODE: {
IncExcNode* casted = dynamic_cast<IncExcNode*>(node); IncExcNode* casted = dynamic_cast<IncExcNode*>(node);
const Clauses& clauses = node->clauses(); printClauses (casted, os);
os << escapeNode (node) << " [shape=box,label=\"" ;
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << clauses[i];
}
os << "\"]" ;
os << endl;
os << auxNode << " [label=\"IncExc\"]" << endl; os << auxNode << " [label=\"IncExc\"]" << endl;
os << escapeNode (node) << " -> " << auxNode; os << escapeNode (node) << " -> " << auxNode;
@ -754,24 +726,12 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
} }
case LEAF_NODE: { case LEAF_NODE: {
os << escapeNode (node); printClauses (node, os);
os << " [shape=box,label=\"" ;
os << node->clauses()[0];
os << "\"]" ;
os << endl;
break; break;
} }
case SMOOTH_NODE: { case SMOOTH_NODE: {
os << escapeNode (node); printClauses (node, os, "style=filled,fillcolor=chartreuse,");
os << " [shape=box,style=filled,fillcolor=chartreuse,label=\"" ;
const Clauses& clauses = node->clauses();
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << clauses[i];
}
os << "\"]" ;
os << endl;
break; break;
} }
@ -783,15 +743,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
} }
case COMPILATION_FAILED_NODE: { case COMPILATION_FAILED_NODE: {
os << escapeNode (node); printClauses (node, os, "style=filled,fillcolor=brown1,");
os << " [shape=box,style=filled,fillcolor=brown1,label=\"" ;
const Clauses& clauses = node->clauses();
for (size_t i = 0; i < clauses.size(); i++) {
if (i != 0) os << "\\n" ;
os << clauses[i];
}
os << "\"]" ;
os << endl;
break; break;
} }
@ -800,3 +752,24 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
} }
} }
void
LiftedCircuit::printClauses (
const CircuitNode* node,
ofstream& os,
string extraOptions)
{
const Clauses& clauses = node->clauses();
if (node->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

@ -214,6 +214,9 @@ class LiftedCircuit
string escapeNode (const CircuitNode* node) const; string escapeNode (const CircuitNode* node) const;
void exportToGraphViz (CircuitNode* node, ofstream&); void exportToGraphViz (CircuitNode* node, ofstream&);
void printClauses (const CircuitNode* node, ofstream&,
string extraOptions = "");
CircuitNode* root_; CircuitNode* root_;
const LiftedWCNF* lwcnf_; const LiftedWCNF* lwcnf_;