diff --git a/packages/CLPBN/horus/LiftedCircuit.cpp b/packages/CLPBN/horus/LiftedCircuit.cpp index dd021bffb..5f2e9db8c 100644 --- a/packages/CLPBN/horus/LiftedCircuit.cpp +++ b/packages/CLPBN/horus/LiftedCircuit.cpp @@ -77,9 +77,8 @@ IncExcNode::weight (void) const double LeafNode::weight (void) const { - assert (clauses().size() == 1); - assert (clauses()[0].isUnit()); - Clause c = clauses()[0]; + assert (clause_.isUnit()); + Clause c = clause_; double weight = c.literals()[0].isPositive() ? lwcnf_.posWeight (c.literals().front().lid()) : lwcnf_.negWeight (c.literals().front().lid()); @@ -261,7 +260,11 @@ LiftedCircuit::compile ( return; } - *follow = new CompilationFailedNode (clauses); + *follow = new CompilationFailedNode(); + if (Globals::verbosity > 1) { + originClausesMap_[*follow] = clauses; + explanationMap_[*follow] = "" ; + } compilationSucceeded_ = false; } @@ -272,6 +275,9 @@ LiftedCircuit::tryUnitPropagation ( CircuitNode** follow, Clauses& clauses) { + if (Globals::verbosity > 1) { + backupClauses_ = clauses; + } for (size_t i = 0; i < clauses.size(); i++) { if (clauses[i].isUnit()) { Clauses newClauses; @@ -294,9 +300,13 @@ LiftedCircuit::tryUnitPropagation ( } } } - stringstream explanation; - explanation << " UP on" << clauses[i].literals()[0]; - AndNode* andNode = new AndNode (clauses, explanation.str()); + AndNode* andNode = new AndNode(); + if (Globals::verbosity > 1) { + originClausesMap_[andNode] = backupClauses_; + stringstream explanation; + explanation << " UP on>" << clauses[i].literals()[0]; + explanationMap_[andNode] = explanation.str(); + } Clauses leftClauses = {clauses[i]}; compile (andNode->leftBranch(), leftClauses); compile (andNode->rightBranch(), newClauses); @@ -317,6 +327,9 @@ LiftedCircuit::tryIndependence ( if (clauses.size() == 1) { return false; } + if (Globals::verbosity > 1) { + backupClauses_ = clauses; + } Clauses depClauses = { clauses[0] }; Clauses indepClauses (clauses.begin() + 1, clauses.end()); bool finish = false; @@ -332,7 +345,11 @@ LiftedCircuit::tryIndependence ( } } if (indepClauses.empty() == false) { - AndNode* andNode = new AndNode (clauses, " Independence"); + AndNode* andNode = new AndNode (); + if (Globals::verbosity > 1) { + originClausesMap_[andNode] = backupClauses_; + explanationMap_[andNode] = " Independence" ; + } compile (andNode->leftBranch(), depClauses); compile (andNode->rightBranch(), indepClauses); (*follow) = andNode; @@ -348,6 +365,9 @@ LiftedCircuit::tryShannonDecomp ( CircuitNode** follow, Clauses& clauses) { + if (Globals::verbosity > 1) { + backupClauses_ = clauses; + } for (size_t i = 0; i < clauses.size(); i++) { const Literals& literals = clauses[i].literals(); for (size_t j = 0; j < literals.size(); j++) { @@ -364,9 +384,13 @@ LiftedCircuit::tryShannonDecomp ( Clauses rightClauses = { c2 }; leftClauses.insert (leftClauses.end(), clauses.begin(), clauses.end()); rightClauses.insert (rightClauses.end(), clauses.begin(), clauses.end()); - stringstream explanation; - explanation << " SD on " << literals[j]; - OrNode* orNode = new OrNode (clauses, explanation.str()); + OrNode* orNode = new OrNode(); + if (Globals::verbosity > 1) { + originClausesMap_[orNode] = backupClauses_; + stringstream explanation; + explanation << " SD on " << literals[j]; + explanationMap_[orNode] = explanation.str(); + } compile (orNode->leftBranch(), leftClauses); compile (orNode->rightBranch(), rightClauses); (*follow) = orNode; @@ -384,6 +408,9 @@ LiftedCircuit::tryInclusionExclusion ( CircuitNode** follow, Clauses& clauses) { + if (Globals::verbosity > 1) { + backupClauses_ = clauses; + } for (size_t i = 0; i < clauses.size(); i++) { Literals depLits = { clauses[i].literals().front() }; Literals indepLits (clauses[i].literals().begin() + 1, @@ -433,9 +460,13 @@ LiftedCircuit::tryInclusionExclusion ( plus2Clauses.push_back (c2); minusClauses.push_back (c1); minusClauses.push_back (c2); - stringstream explanation; - explanation << " IncExc on clause nº " << i + 1; - IncExcNode* ieNode = new IncExcNode (clauses, explanation.str()); + IncExcNode* ieNode = new IncExcNode(); + if (Globals::verbosity > 1) { + originClausesMap_[ieNode] = backupClauses_; + stringstream explanation; + explanation << " IncExc on clause nº " << i + 1; + explanationMap_[ieNode] = explanation.str(); + } compile (ieNode->plus1Branch(), plus1Clauses); compile (ieNode->plus2Branch(), plus2Clauses); compile (ieNode->minusBranch(), minusClauses); @@ -455,6 +486,9 @@ LiftedCircuit::tryIndepPartialGrounding ( { // assumes that all literals have logical variables // else, shannon decomp was possible + if (Globals::verbosity > 1) { + backupClauses_ = clauses; + } LogVars rootLogVars; LogVarSet lvs = clauses[0].ipgCandidates(); for (size_t i = 0; i < lvs.size(); i++) { @@ -466,9 +500,13 @@ LiftedCircuit::tryIndepPartialGrounding ( for (size_t j = 0; j < clauses.size(); j++) { newClauses[j].addIpgLogVar (rootLogVars[j]); } - SetAndNode* node = new SetAndNode (ct.size(), clauses); - *follow = node; - compile (node->follow(), newClauses); + SetAndNode* setAndNode = new SetAndNode (ct.size()); + if (Globals::verbosity > 1) { + originClausesMap_[setAndNode] = backupClauses_; + explanationMap_[setAndNode] = " IPG" ; + } + *follow = setAndNode; + compile (setAndNode->follow(), newClauses); return true; } } @@ -531,6 +569,9 @@ LiftedCircuit::tryAtomCounting ( return false; } } + if (Globals::verbosity > 1) { + backupClauses_ = clauses; + } for (size_t i = 0; i < clauses.size(); i++) { Literals literals = clauses[i].literals(); for (size_t j = 0; j < literals.size(); j++) { @@ -539,7 +580,11 @@ LiftedCircuit::tryAtomCounting ( && ! clauses[i].isCountedLogVar (literals[j].logVars().front())) { unsigned nrGroundings = clauses[i].constr().projectedCopy ( literals[j].logVars()).size(); - SetOrNode* setOrNode = new SetOrNode (nrGroundings, clauses); + SetOrNode* setOrNode = new SetOrNode (nrGroundings); + if (Globals::verbosity > 1) { + originClausesMap_[setOrNode] = backupClauses_; + explanationMap_[setOrNode] = " AC" ; + } Clause c1 (clauses[i].constr().projectedCopy (literals[j].logVars())); Clause c2 (clauses[i].constr().projectedCopy (literals[j].logVars())); c1.addLiteral (literals[j]); @@ -734,9 +779,10 @@ LiftedCircuit::smoothCircuit (CircuitNode* node) } case CircuitNodeType::LEAF_NODE: { + LeafNode* casted = dynamic_cast(node); propagLits.insert (LitLvTypes ( - node->clauses()[0].literals()[0].lid(), - node->clauses()[0].logVarTypes(0))); + casted->clause().literals()[0].lid(), + casted->clause().logVarTypes(0))); } default: @@ -754,6 +800,10 @@ LiftedCircuit::createSmoothNode ( CircuitNode** prev) { if (missingLits.empty() == false) { + if (Globals::verbosity > 1) { + // assert (Util::contains (originClausesMap_, prev)); + backupClauses_ = originClausesMap_[*prev]; + } Clauses clauses; for (size_t i = 0; i < missingLits.size(); i++) { LiteralId lid = missingLits[i].lid(); @@ -771,8 +821,11 @@ LiftedCircuit::createSmoothNode ( clauses.push_back (c); } SmoothNode* smoothNode = new SmoothNode (clauses, *lwcnf_); - *prev = new AndNode ((*prev)->clauses(), smoothNode, - *prev, " Smoothing"); + *prev = new AndNode (smoothNode, *prev); + if (Globals::verbosity > 1) { + originClausesMap_[*prev] = backupClauses_; + explanationMap_[*prev] = " Smoothing" ; + } } } @@ -879,7 +932,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) os << auxNode << " [" << opStyle << "label=\"∨\"]" << endl; os << escapeNode (node) << " -> " << auxNode; - os << " [label=\"" << node->explanation() << "\"]" ; + os << " [label=\"" << getExplanationString (node) << "\"]" ; os << endl; os << auxNode << " -> " ; @@ -903,7 +956,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) os << auxNode << " [" << opStyle << "label=\"∧\"]" << endl; os << escapeNode (node) << " -> " << auxNode; - os << " [label=\"" << node->explanation() << "\"]" ; + os << " [label=\"" << getExplanationString (node) << "\"]" ; os << endl; os << auxNode << " -> " ; @@ -927,7 +980,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) os << auxNode << " [" << opStyle << "label=\"∨(X)\"]" << endl; os << escapeNode (node) << " -> " << auxNode; - os << " [label=\"" << node->explanation() << "\"]" ; + os << " [label=\"" << getExplanationString (node) << "\"]" ; os << endl; os << auxNode << " -> " ; @@ -945,7 +998,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) os << auxNode << " [" << opStyle << "label=\"∧(X)\"]" << endl; os << escapeNode (node) << " -> " << auxNode; - os << " [label=\"" << node->explanation() << "\"]" ; + os << " [label=\"" << getExplanationString (node) << "\"]" ; os << endl; os << auxNode << " -> " ; @@ -964,7 +1017,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) os << auxNode << " [" << opStyle << "label=\"+ - +\"]" ; os << endl; os << escapeNode (node) << " -> " << auxNode; - os << " [label=\"" << node->explanation() << "\"]" ; + os << " [label=\"" << getExplanationString (node) << "\"]" ; os << endl; os << auxNode << " -> " ; @@ -1027,14 +1080,31 @@ LiftedCircuit::escapeNode (const CircuitNode* node) const +string +LiftedCircuit::getExplanationString (CircuitNode* node) +{ + return Util::contains (explanationMap_, node) + ? explanationMap_[node] + : "" ; +} + + + void LiftedCircuit::printClauses ( - const CircuitNode* node, + CircuitNode* node, ofstream& os, string extraOptions) { - const Clauses& clauses = node->clauses(); - if (node->clauses().empty() == false) { + Clauses clauses; + if (Util::contains (originClausesMap_, node)) { + clauses = originClausesMap_[node]; + } else if (getCircuitNodeType (node) == CircuitNodeType::LEAF_NODE) { + clauses = { (dynamic_cast(node))->clause() } ; + } else if (getCircuitNodeType (node) == CircuitNodeType::SMOOTH_NODE) { + clauses = (dynamic_cast(node))->clauses(); + } + if (clauses.empty() == false) { os << escapeNode (node); os << " [shape=box," << extraOptions << "label=\"" ; for (size_t i = 0; i < clauses.size(); i++) { @@ -1043,6 +1113,8 @@ LiftedCircuit::printClauses ( } os << "\"]" ; os << endl; + } else { + os << " [shape=box]" << endl; } } diff --git a/packages/CLPBN/horus/LiftedCircuit.h b/packages/CLPBN/horus/LiftedCircuit.h index cc0263d52..979896b3a 100644 --- a/packages/CLPBN/horus/LiftedCircuit.h +++ b/packages/CLPBN/horus/LiftedCircuit.h @@ -23,20 +23,9 @@ enum CircuitNodeType { class CircuitNode { public: - CircuitNode (const Clauses& clauses, string explanation = "") - : clauses_(clauses), explanation_(explanation) { } - - const Clauses& clauses (void) const { return clauses_; } - - Clauses clauses (void) { return clauses_; } + CircuitNode (void) { } virtual double weight (void) const = 0; - - string explanation (void) const { return explanation_; } - - private: - Clauses clauses_; - string explanation_; }; @@ -44,9 +33,7 @@ class CircuitNode class OrNode : public CircuitNode { public: - OrNode (const Clauses& clauses, string explanation = "") - : CircuitNode (clauses, explanation), - leftBranch_(0), rightBranch_(0) { } + OrNode (void) : CircuitNode(), leftBranch_(0), rightBranch_(0) { } CircuitNode** leftBranch (void) { return &leftBranch_; } CircuitNode** rightBranch (void) { return &rightBranch_; } @@ -63,24 +50,10 @@ class OrNode : public CircuitNode class AndNode : public CircuitNode { public: - AndNode (const Clauses& clauses, string explanation = "") - : CircuitNode (clauses, explanation), - leftBranch_(0), rightBranch_(0) { } - - AndNode ( - const Clauses& clauses, - CircuitNode* leftBranch, - CircuitNode* rightBranch, - string explanation = "") - : CircuitNode (clauses, explanation), - leftBranch_(leftBranch), rightBranch_(rightBranch) { } - - AndNode ( - CircuitNode* leftBranch, - CircuitNode* rightBranch, - string explanation = "") - : CircuitNode ({}, explanation), - leftBranch_(leftBranch), rightBranch_(rightBranch) { } + AndNode (void) : CircuitNode(), leftBranch_(0), rightBranch_(0) { } + + AndNode (CircuitNode* leftBranch, CircuitNode* rightBranch) + : CircuitNode(), leftBranch_(leftBranch), rightBranch_(rightBranch) { } CircuitNode** leftBranch (void) { return &leftBranch_; } CircuitNode** rightBranch (void) { return &rightBranch_; } @@ -97,9 +70,8 @@ class AndNode : public CircuitNode class SetOrNode : public CircuitNode { public: - SetOrNode (unsigned nrGroundings, const Clauses& clauses) - : CircuitNode (clauses, " AC"), follow_(0), - nrGroundings_(nrGroundings) { } + SetOrNode (unsigned nrGroundings) + : CircuitNode(), follow_(0), nrGroundings_(nrGroundings) { } CircuitNode** follow (void) { return &follow_; } @@ -121,9 +93,8 @@ class SetOrNode : public CircuitNode class SetAndNode : public CircuitNode { public: - SetAndNode (unsigned nrGroundings, const Clauses& clauses) - : CircuitNode (clauses, " IPG"), follow_(0), - nrGroundings_(nrGroundings) { } + SetAndNode (unsigned nrGroundings) + : CircuitNode(), follow_(0), nrGroundings_(nrGroundings) { } CircuitNode** follow (void) { return &follow_; } @@ -139,9 +110,8 @@ class SetAndNode : public CircuitNode class IncExcNode : public CircuitNode { public: - IncExcNode (const Clauses& clauses, string explanation) - : CircuitNode (clauses, explanation), plus1Branch_(0), - plus2Branch_(0), minusBranch_(0) { } + IncExcNode (void) + : CircuitNode(), plus1Branch_(0), plus2Branch_(0), minusBranch_(0) { } CircuitNode** plus1Branch (void) { return &plus1Branch_; } CircuitNode** plus2Branch (void) { return &plus2Branch_; } @@ -161,11 +131,16 @@ class LeafNode : public CircuitNode { public: LeafNode (const Clause& clause, const LiftedWCNF& lwcnf) - : CircuitNode (Clauses() = {clause}), lwcnf_(lwcnf) { } + : CircuitNode(), clause_(clause), lwcnf_(lwcnf) { } + + const Clause& clause (void) const { return clause_; } + + Clause& clause (void) { return clause_; } double weight (void) const; private: + Clause clause_; const LiftedWCNF& lwcnf_; }; @@ -175,11 +150,16 @@ class SmoothNode : public CircuitNode { public: SmoothNode (const Clauses& clauses, const LiftedWCNF& lwcnf) - : CircuitNode (clauses), lwcnf_(lwcnf) { } - - double weight (void) const; + : CircuitNode(), clauses_(clauses), lwcnf_(lwcnf) { } + + const Clauses& clauses (void) const { return clauses_; } + Clauses clauses (void) { return clauses_; } + + double weight (void) const; + private: + Clauses clauses_; const LiftedWCNF& lwcnf_; }; @@ -188,7 +168,7 @@ class SmoothNode : public CircuitNode class TrueNode : public CircuitNode { public: - TrueNode (void) : CircuitNode ({}) { } + TrueNode (void) : CircuitNode() { } double weight (void) const; }; @@ -198,8 +178,7 @@ class TrueNode : public CircuitNode class CompilationFailedNode : public CircuitNode { public: - CompilationFailedNode (const Clauses& clauses) - : CircuitNode (clauses) { } + CompilationFailedNode (void) : CircuitNode() { } double weight (void) const; }; @@ -261,13 +240,19 @@ class LiftedCircuit void exportToGraphViz (CircuitNode* node, ofstream&); - void printClauses (const CircuitNode* node, ofstream&, + void printClauses (CircuitNode* node, ofstream&, string extraOptions = ""); string escapeNode (const CircuitNode* node) const; + + string getExplanationString (CircuitNode* node); CircuitNode* root_; const LiftedWCNF* lwcnf_; + + Clauses backupClauses_; + unordered_map originClausesMap_; + unordered_map explanationMap_; bool compilationSucceeded_; };