InxExc: improve the code

packages/CLPBN/horus/LiftedCircuit.cpp

@@ -341,7 +341,7 @@ LiftedCircuit::tryIndependence (
   while (finish == false) {
     finish = true;
     for (size_t i = 0; i < indepClauses.size(); i++) {
-      if (isIndependentClause (indepClauses[i], depClauses) == false) {
+      if (independentClause (indepClauses[i], depClauses) == false) {
         depClauses.push_back (indepClauses[i]);
         indepClauses.erase (indepClauses.begin() + i);
         finish = false;
@@ -402,44 +402,58 @@ LiftedCircuit::tryInclusionExclusion (
     CircuitNode** follow,
     Clauses& clauses)
 {
-  // TODO compare all subsets with all subsets
   for (size_t i = 0; i < clauses.size(); i++) {
-    const Literals& literals = clauses[i].literals();
+    Literals depLits = { clauses[i].literals().front() };
-    for (size_t j = 0; j < literals.size(); j++) {
+    Literals indepLits (clauses[i].literals().begin() + 1,
-      bool indep = true;
+        clauses[i].literals().end());
-      for (size_t k = 0; k < literals.size(); k++) {
+    bool finish = false;
-        LogVarSet intersect = literals[j].logVarSet()
+    while (finish == false) {
-            & literals[k].logVarSet();
+      finish = true;
-        if (j != k && intersect.empty() == false) {
+      for (size_t j = 0; j < indepLits.size(); j++) {
-          indep = false;
+        if (independentLiteral (indepLits[j], depLits) == false) {
+          depLits.push_back (indepLits[j]);
+          indepLits.erase (indepLits.begin() + j);
+          finish = false;
           break;
         }
       }
-      if (indep) {
+    }
-        // TODO this should be have to be count normalized too
+    if (indepLits.empty() == false) {
-        ConstraintTree really = clauses[i].constr();
+      // TODO this should be have to be count normalized too
-        Clause c1 (really.projectedCopy (
+      LogVarSet lvs1;
-            literals[j].logVars()));
+      for (size_t j = 0; j < depLits.size(); j++) {
-        c1.addLiteral (literals[j]);
+        lvs1 |= depLits[j].logVarSet();
-        Clause c2 = clauses[i];
-        c2.removeLiteral (j);
-        Clauses plus1Clauses = clauses;
-        Clauses plus2Clauses = clauses;
-        Clauses minusClauses = clauses;
-        plus1Clauses.erase (plus1Clauses.begin() + i);
-        plus2Clauses.erase (plus2Clauses.begin() + i);
-        minusClauses.erase (minusClauses.begin() + i);
-        plus1Clauses.push_back (c1);
-        plus2Clauses.push_back (c2);
-        minusClauses.push_back (c1);
-        minusClauses.push_back (c2);
-        IncExcNode* ieNode = new IncExcNode (clauses);
-        compile (ieNode->plus1Branch(), plus1Clauses);
-        compile (ieNode->plus2Branch(), plus2Clauses);
-        compile (ieNode->minusBranch(), minusClauses);
-        *follow = ieNode;
-        return true;
       }
+      LogVarSet lvs2;
+      for (size_t j = 0; j < indepLits.size(); j++) {
+        lvs2 |= indepLits[j].logVarSet();
+      }
+      Clause c1 (clauses[i].constr().projectedCopy (lvs1));
+      for (size_t j = 0; j < depLits.size(); j++) {
+        c1.addLiteral (depLits[j]);
+      }
+      Clause c2 (clauses[i].constr().projectedCopy (lvs2));
+      for (size_t j = 0; j < indepLits.size(); j++) {
+        c2.addLiteral (indepLits[j]);
+      }
+      Clauses plus1Clauses = clauses;
+      Clauses plus2Clauses = clauses;
+      Clauses minusClauses = clauses;
+      plus1Clauses.erase (plus1Clauses.begin() + i);
+      plus2Clauses.erase (plus2Clauses.begin() + i);
+      minusClauses.erase (minusClauses.begin() + i);
+      plus1Clauses.push_back (c1);
+      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());
+      compile (ieNode->plus1Branch(), plus1Clauses);
+      compile (ieNode->plus2Branch(), plus2Clauses);
+      compile (ieNode->minusBranch(), minusClauses);
+      *follow = ieNode;
+      return true;
     }
   }
   return false;
@@ -651,7 +665,7 @@ LiftedCircuit::shatterCountedLogVarsAux (
 
 
 bool
-LiftedCircuit::isIndependentClause (
+LiftedCircuit::independentClause (
     Clause& clause,
     Clauses& otherClauses) const
 {
@@ -665,6 +679,22 @@ LiftedCircuit::isIndependentClause (
 
 
 
+bool
+LiftedCircuit::independentLiteral (
+    const Literal& lit,
+    const Literals& otherLits) const
+{
+  for (size_t i = 0; i < otherLits.size(); i++) {
+    if (lit.lid() == otherLits[i].lid()
+        || (lit.logVarSet() & otherLits[i].logVarSet()).empty() == false) {
+      return false;
+    }
+  }
+  return true;
+}
+
+
+
 LitLvTypesSet
 LiftedCircuit::smoothCircuit (CircuitNode* node)
 {
@@ -882,7 +912,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
   ss << "n" << nrAuxNodes;
   string auxNode = ss.str();
   nrAuxNodes ++;
-
+  string opStyle = "shape=circle,width=0.7,margin=\"0.0,0.0\"," ;
 
   switch (getCircuitNodeType (node)) {
   
@@ -890,7 +920,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
       OrNode* casted = dynamic_cast<OrNode*>(node);
       printClauses (casted, os);
 
-      os << auxNode << " [label=\"∨\"]" << endl;
+      os << auxNode << " [" << opStyle << "label=\"∨\"]" << endl;
       os << escapeNode (node) << " -> " << auxNode;
       os << " [label=\"" << node->explanation() << "\"]" ;
       os << endl;
@@ -914,7 +944,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
       AndNode* casted = dynamic_cast<AndNode*>(node);
       printClauses (casted, os);
 
-      os << auxNode << " [label=\"∧\"]" << endl;
+      os << auxNode << " [" << opStyle << "label=\"∧\"]" << endl;
       os << escapeNode (node) << " -> " << auxNode;
       os << " [label=\"" << node->explanation() << "\"]" ;
       os << endl;
@@ -938,7 +968,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
       SetOrNode* casted = dynamic_cast<SetOrNode*>(node);
       printClauses (casted, os);
 
-      os << auxNode << " [label=\"∨(X)\"]" << endl;
+      os << auxNode << " [" << opStyle << "label=\"∨(X)\"]" << endl;
       os << escapeNode (node) << " -> " << auxNode;
       os << " [label=\"" << node->explanation() << "\"]" ;
       os << endl;
@@ -956,7 +986,7 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
       SetAndNode* casted = dynamic_cast<SetAndNode*>(node);
       printClauses (casted, os);
 
-      os << auxNode << " [label=\"∧(X)\"]" << endl;
+      os << auxNode << " [" << opStyle << "label=\"∧(X)\"]" << endl;
       os << escapeNode (node) << " -> " << auxNode;
       os << " [label=\"" << node->explanation() << "\"]" ;
       os << endl;
@@ -974,7 +1004,8 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
       IncExcNode* casted = dynamic_cast<IncExcNode*>(node);
       printClauses (casted, os);
 
-      os << auxNode << " [label=\"IncExc\"]" << endl;
+      os << auxNode << " [" << opStyle << "label=\"+ - +\"]" ;
+      os << endl;
       os << escapeNode (node) << " -> " << auxNode;
       os << " [label=\"" << node->explanation() << "\"]" ;
       os << endl;
@@ -983,17 +1014,17 @@ LiftedCircuit::exportToGraphViz (CircuitNode* node, ofstream& os)
       os << escapeNode (*casted->plus1Branch());
       os << " [label=\" " << (*casted->plus1Branch())->weight() << "\"]" ;
       os << endl;
+      
+      os << auxNode << " -> " ;
+      os << escapeNode (*casted->minusBranch()) << endl;
+      os << " [label=\" " << (*casted->minusBranch())->weight() << "\"]" ;
+      os << endl;      
 
       os << auxNode << " -> " ;
       os << escapeNode (*casted->plus2Branch());
       os << " [label=\" " << (*casted->plus2Branch())->weight() << "\"]" ;
       os << endl;
 
-      os << auxNode << " -> " ;
-      os << escapeNode (*casted->minusBranch()) << endl;
-      os << " [label=\" " << (*casted->minusBranch())->weight() << "\"]" ;
-      os << endl;
-
       exportToGraphViz (*casted->plus1Branch(), os);
       exportToGraphViz (*casted->plus2Branch(), os);
       exportToGraphViz (*casted->minusBranch(), os);

packages/CLPBN/horus/LiftedCircuit.h

@@ -54,8 +54,8 @@ class OrNode : public CircuitNode
     double weight (void) const;
 
   private:
-    CircuitNode* leftBranch_;
+    CircuitNode*  leftBranch_;
-    CircuitNode* rightBranch_;
+    CircuitNode*  rightBranch_;
 };
 
 
@@ -88,8 +88,8 @@ class AndNode : public CircuitNode
     double weight (void) const;
     
   private:
-    CircuitNode* leftBranch_;
+    CircuitNode*  leftBranch_;
-    CircuitNode* rightBranch_;
+    CircuitNode*  rightBranch_;
 };
 
 
@@ -139,8 +139,8 @@ class SetAndNode : public CircuitNode
 class IncExcNode : public CircuitNode
 {
   public:
-    IncExcNode (const Clauses& clauses)
+    IncExcNode (const Clauses& clauses, string explanation)
-        : CircuitNode (clauses), plus1Branch_(0),
+        : CircuitNode (clauses, explanation), plus1Branch_(0),
         plus2Branch_(0), minusBranch_(0) { }
 
     CircuitNode** plus1Branch (void) { return &plus1Branch_; }
@@ -150,9 +150,9 @@ class IncExcNode : public CircuitNode
     double weight (void) const;    
 
   private:
-    CircuitNode* plus1Branch_;
+    CircuitNode*  plus1Branch_;
-    CircuitNode* plus2Branch_;
+    CircuitNode*  plus2Branch_;
-    CircuitNode* minusBranch_;
+    CircuitNode*  minusBranch_;
 };
 
 
@@ -198,7 +198,8 @@ class TrueNode : public CircuitNode
 class CompilationFailedNode : public CircuitNode
 {
   public:
-    CompilationFailedNode (const Clauses& clauses) : CircuitNode (clauses) { }
+    CompilationFailedNode (const Clauses& clauses)
+        : CircuitNode (clauses) { }
     
     double weight (void) const;
 };
@@ -243,7 +244,10 @@ class LiftedCircuit
 
     bool shatterCountedLogVarsAux (Clauses& clauses, size_t idx1, size_t idx2);
     
-    bool isIndependentClause (Clause& clause, Clauses& otherClauses) const;
+    bool independentClause (Clause& clause, Clauses& otherClauses) const;
+    
+    bool independentLiteral (const Literal& lit,
+        const Literals& otherLits) const;
 
     LitLvTypesSet smoothCircuit (CircuitNode* node);
     

packages/CLPBN/horus/LiftedWCNF.cpp

@@ -377,22 +377,24 @@ LiftedWCNF::LiftedWCNF (const ParfactorList& pfList)
   */
   
   Literal lit1 (0, {0});
-  Literal lit2 (1, {});
+  Literal lit2 (1, {0});
-  Literal lit3 (2, {});
+  Literal lit3 (2, {1});
-  Literal lit4 (3, {});
+  Literal lit4 (3, {1});
   
-  vector<vector<string>> names = {{"p1"},{"p2"}};
+  vector<vector<string>> names = {{"p1","p2"},{"p3","p4"}};
   Clause c1 (names);
   c1.addLiteral (lit1);
   c1.addLiteral (lit2);
-  c1.addPosCountedLogVar (0);
+  c1.addLiteral (lit3);
+  c1.addLiteral (lit4);
+  //c1.addPosCountedLogVar (0);
   clauses_.push_back (c1);
 
   Clause c2 (names);
   c2.addLiteral (lit1);
   c2.addLiteral (lit3);
   c2.addNegCountedLogVar (0);
-  clauses_.push_back (c2);
+  //clauses_.push_back (c2);
   /*
   Clause c3;
   c3.addLiteral (lit3);