IPG: verify that the root log vars appear in the same positions

packages/CLPBN/horus/LiftedCircuit.cpp

@@ -264,9 +264,9 @@ LiftedCircuit::compile (
     return;
   }
   
-  //if (tryIndepPartialGrounding (follow, clauses)) {
+  if (tryIndepPartialGrounding (follow, clauses)) {
-  //  return;
+    return;
-  //}
+  }
   
   if (tryAtomCounting (follow, clauses)) {
     return;
@@ -457,18 +457,16 @@ LiftedCircuit::tryIndepPartialGrounding (
 { 
   // assumes that all literals have logical variables
   // else, shannon decomp was possible
-  vector<unsigned> lvIndices;
+  LogVars rootLogVars;
   LogVarSet lvs = clauses[0].ipgCandidates();
   for (size_t i = 0; i < lvs.size(); i++) {
-    lvIndices.clear();
+    rootLogVars.clear();
-    lvIndices.push_back (i);
+    rootLogVars.push_back (lvs[i]);
-    ConstraintTree ct = clauses[0].constr();
+    ConstraintTree ct = clauses[0].constr().projectedCopy ({lvs[i]});
-    ct.project ({lvs[i]});
+    if (tryIndepPartialGroundingAux (clauses, ct, rootLogVars)) {
-    if (tryIndepPartialGroundingAux (clauses, ct, lvIndices)) {
       Clauses newClauses = clauses;
-      for (size_t i = 0; i < clauses.size(); i++) {
+      for (size_t j = 0; j < clauses.size(); j++) {
-        LogVar lv = clauses[i].ipgCandidates()[lvIndices[i]];
+        newClauses[j].addIpgLogVar (rootLogVars[j]);
-        newClauses[i].addIpgLogVar (lv);
       }
       SetAndNode* node = new SetAndNode (ct.size(), clauses);
       *follow = node;
@@ -485,23 +483,39 @@ bool
 LiftedCircuit::tryIndepPartialGroundingAux (
     Clauses& clauses,
     ConstraintTree& ct,
-    vector<unsigned>& lvIndices)
+    LogVars& rootLogVars)
 {
-  // TODO check if the ipg log vars appears in the same positions
+  for (size_t i = 1; i < clauses.size(); i++) {
-  for (size_t j = 1; j < clauses.size(); j++) {
+    LogVarSet lvs = clauses[i].ipgCandidates();
-    LogVarSet lvs2 = clauses[j].ipgCandidates();
+    for (size_t j = 0; j < lvs.size(); j++) {
-    for (size_t k = 0; k < lvs2.size(); k++) {
+      ConstraintTree ct2 = clauses[i].constr().projectedCopy ({lvs[j]});
-      ConstraintTree ct2 = clauses[j].constr();
-      ct2.project ({lvs2[k]});
       if (ct.tupleSet() == ct2.tupleSet()) {
-        lvIndices.push_back (k);
+        rootLogVars.push_back (lvs[j]);
         break;
       }
     }
-    if (lvIndices.size() != j+1) {
+    if (rootLogVars.size() != i + 1) {
       return false;
     }
   }
+  // verifies if the IPG logical vars appear in the same positions
+  unordered_map<LiteralId, size_t> positions;
+  for (size_t i = 0; i < clauses.size(); i++) {
+    const Literals& literals = clauses[i].literals();
+    for (size_t j = 0; j < literals.size(); j++) {
+      size_t idx = literals[j].indexOfLogVar (rootLogVars[i]);
+      assert (idx != literals[j].nrLogVars());
+      unordered_map<LiteralId, size_t>::iterator it;
+      it = positions.find (literals[j].lid());
+      if (it != positions.end()) {
+        if (it->second != idx) {
+          return false;
+        }
+      } else {
+        positions[literals[j].lid()] = idx;
+      }
+    }
+  }
   return true;
 }
 

packages/CLPBN/horus/LiftedCircuit.h

@@ -230,7 +230,7 @@ class LiftedCircuit
     bool tryIndepPartialGrounding (CircuitNode** follow, Clauses& clauses);
     
     bool tryIndepPartialGroundingAux (Clauses& clauses, ConstraintTree& ct,
-        vector<unsigned>& indices);
+        LogVars& rootLogVars);
         
     bool tryAtomCounting (CircuitNode** follow, Clauses& clauses);
     

packages/CLPBN/horus/LiftedWCNF.cpp

@@ -17,6 +17,14 @@ Literal::isGround (ConstraintTree constr, LogVarSet ipgLogVars) const
 
 
 
+size_t
+Literal::indexOfLogVar (LogVar X) const
+{
+  return Util::indexOf (logVars_, X);
+}
+
+
+
 string
 Literal::toString (
     LogVarSet ipgLogVars,

packages/CLPBN/horus/LiftedWCNF.h

@@ -35,6 +35,8 @@ class Literal
 
     LogVarSet logVarSet (void) const { return LogVarSet (logVars_); }
     
+    size_t nrLogVars (void) const { return logVars_.size(); }
+
     void negate (void) { negated_ = !negated_; }
 
     bool isPositive (void) const { return negated_ == false; }
@@ -43,6 +45,8 @@ class Literal
     
     bool isGround (ConstraintTree constr, LogVarSet ipgLogVars) const;
     
+    size_t indexOfLogVar (LogVar X) const;
+
     string toString (LogVarSet ipgLogVars = LogVarSet(),
       LogVarSet posCountedLvs = LogVarSet(),
       LogVarSet negCountedLvs = LogVarSet()) const;