diff --git a/packages/CLPBN/horus/LiftedCircuit.cpp b/packages/CLPBN/horus/LiftedCircuit.cpp index f185c5212..eb8d4fe33 100644 --- a/packages/CLPBN/horus/LiftedCircuit.cpp +++ b/packages/CLPBN/horus/LiftedCircuit.cpp @@ -110,6 +110,17 @@ TrueNode::weight (void) const +double +CompilationFailedNode::weight (void) const +{ + // we should not perform model counting + // in compilation failed nodes + abort(); + return 0.0; +} + + + LiftedCircuit::LiftedCircuit (const LiftedWCNF* lwcnf) : lwcnf_(lwcnf) { @@ -217,7 +228,7 @@ LiftedCircuit::compile ( } // assert (false); - *follow = new FailNode (clauses); + *follow = new CompilationFailedNode (clauses); } @@ -237,14 +248,10 @@ LiftedCircuit::tryUnitPropagation ( if (clauses[i].literals()[0].isPositive()) { if (clauses[j].containsPositiveLiteral (lid) == false) { Clause newClause = clauses[j]; - //cout << "new j : " << clauses[j] << endl; - //cout << "new clause: " << newClause << endl; - //cout << "clvs: " << clauses[j].constr()->logVars() << endl; newClause.removeNegativeLiterals (lid); newClauses.push_back (newClause); } } else if (clauses[i].literals()[0].isNegative()) { - //cout << "unit prop of = " << clauses[i].literals()[0] << endl; if (clauses[j].containsNegativeLiteral (lid) == false) { Clause newClause = clauses[j]; newClause.removePositiveLiterals (lid); @@ -254,7 +261,6 @@ LiftedCircuit::tryUnitPropagation ( } } stringstream explanation; - explanation << " UP of " << clauses[i]; AndNode* andNode = new AndNode (clauses, explanation.str()); Clauses leftClauses = {clauses[i]}; compile (andNode->leftBranch(), leftClauses); @@ -551,7 +557,7 @@ LiftedCircuit::smoothCircuit (CircuitNode* node) // case CircuitNodeType::SMOOTH_NODE: // case CircuitNodeType::TRUE_NODE: - // case CircuitNodeType::FAIL_NODE: + // case CircuitNodeType::COMPILATION_FAILED_NODE: default: break; @@ -571,8 +577,6 @@ LiftedCircuit::getCircuitNodeType (const CircuitNode* node) const } else if (dynamic_cast(node) != 0) { type = CircuitNodeType::AND_NODE; } else if (dynamic_cast(node) != 0) { - // TODO - assert (false); type = CircuitNodeType::SET_OR_NODE; } else if (dynamic_cast(node) != 0) { type = CircuitNodeType::SET_AND_NODE; @@ -584,8 +588,8 @@ LiftedCircuit::getCircuitNodeType (const CircuitNode* node) const type = CircuitNodeType::SMOOTH_NODE; } else if (dynamic_cast(node) != 0) { type = CircuitNodeType::TRUE_NODE; - } else if (dynamic_cast(node) != 0) { - type = CircuitNodeType::FAIL_NODE; + } else if (dynamic_cast(node) != 0) { + type = CircuitNodeType::COMPILATION_FAILED_NODE; } else { assert (false); } @@ -778,7 +782,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os) break; } - case FAIL_NODE: { + case COMPILATION_FAILED_NODE: { os << escapeNode (node); os << " [shape=box,style=filled,fillcolor=brown1,label=\"" ; const Clauses& clauses = node->clauses(); diff --git a/packages/CLPBN/horus/LiftedCircuit.h b/packages/CLPBN/horus/LiftedCircuit.h index 98ce61086..35bd794ec 100644 --- a/packages/CLPBN/horus/LiftedCircuit.h +++ b/packages/CLPBN/horus/LiftedCircuit.h @@ -13,7 +13,7 @@ enum CircuitNodeType { LEAF_NODE, SMOOTH_NODE, TRUE_NODE, - FAIL_NODE + COMPILATION_FAILED_NODE }; @@ -28,7 +28,7 @@ class CircuitNode Clauses clauses (void) { return clauses_; } - virtual double weight (void) const { return 0; } + virtual double weight (void) const = 0; string explanation (void) const { return explanation_; } @@ -128,6 +128,8 @@ class IncExcNode : public CircuitNode IncExcNode (const Clauses& clauses) : CircuitNode (clauses), plus1Branch_(0), plus2Branch_(0), minusBranch_(0) { } + + double weight (void) const; CircuitNode** plus1Branch (void) { return &plus1Branch_; } CircuitNode** plus2Branch (void) { return &plus2Branch_; } @@ -171,10 +173,12 @@ class TrueNode : public CircuitNode -class FailNode : public CircuitNode +class CompilationFailedNode : public CircuitNode { public: - FailNode (const Clauses& clauses) : CircuitNode (clauses) { } + CompilationFailedNode (const Clauses& clauses) : CircuitNode (clauses) { } + + double weight (void) const; };