From 06a59ad6590b9771788cab23bbf946fe3e76b2c3 Mon Sep 17 00:00:00 2001
From: Tiago Gomes <tgomes@fc.up.pt>
Date: Tue, 6 Nov 2012 23:35:14 +0000
Subject: [PATCH] IPG: verify that the root log vars appear in the same
 positions

---
 packages/CLPBN/horus/LiftedCircuit.cpp | 56 ++++++++++++++++----------
 packages/CLPBN/horus/LiftedCircuit.h   |  2 +-
 packages/CLPBN/horus/LiftedWCNF.cpp    | 16 ++++++--
 packages/CLPBN/horus/LiftedWCNF.h      |  4 ++
 4 files changed, 52 insertions(+), 26 deletions(-)

diff --git a/packages/CLPBN/horus/LiftedCircuit.cpp b/packages/CLPBN/horus/LiftedCircuit.cpp
index d2a2ab4bc..763d8aae1 100644
--- a/packages/CLPBN/horus/LiftedCircuit.cpp
+++ b/packages/CLPBN/horus/LiftedCircuit.cpp
@@ -264,9 +264,9 @@ LiftedCircuit::compile (
     return;
   }
   
-  //if (tryIndepPartialGrounding (follow, clauses)) {
-  //  return;
-  //}
+  if (tryIndepPartialGrounding (follow, clauses)) {
+    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();
-    lvIndices.push_back (i);
-    ConstraintTree ct = clauses[0].constr();
-    ct.project ({lvs[i]});
-    if (tryIndepPartialGroundingAux (clauses, ct, lvIndices)) {
+    rootLogVars.clear();
+    rootLogVars.push_back (lvs[i]);
+    ConstraintTree ct = clauses[0].constr().projectedCopy ({lvs[i]});
+    if (tryIndepPartialGroundingAux (clauses, ct, rootLogVars)) {
       Clauses newClauses = clauses;
-      for (size_t i = 0; i < clauses.size(); i++) {
-        LogVar lv = clauses[i].ipgCandidates()[lvIndices[i]];
-        newClauses[i].addIpgLogVar (lv);
+      for (size_t j = 0; j < clauses.size(); j++) {
+        newClauses[j].addIpgLogVar (rootLogVars[j]);
       }
       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 j = 1; j < clauses.size(); j++) {
-    LogVarSet lvs2 = clauses[j].ipgCandidates();
-    for (size_t k = 0; k < lvs2.size(); k++) {
-      ConstraintTree ct2 = clauses[j].constr();
-      ct2.project ({lvs2[k]});
+  for (size_t i = 1; i < clauses.size(); i++) {
+    LogVarSet lvs = clauses[i].ipgCandidates();
+    for (size_t j = 0; j < lvs.size(); j++) {
+      ConstraintTree ct2 = clauses[i].constr().projectedCopy ({lvs[j]});
       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;
 }
 
diff --git a/packages/CLPBN/horus/LiftedCircuit.h b/packages/CLPBN/horus/LiftedCircuit.h
index 903b9e73f..cfa3a713b 100644
--- a/packages/CLPBN/horus/LiftedCircuit.h
+++ b/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);
     
diff --git a/packages/CLPBN/horus/LiftedWCNF.cpp b/packages/CLPBN/horus/LiftedWCNF.cpp
index 0dac99a06..07595a22f 100644
--- a/packages/CLPBN/horus/LiftedWCNF.cpp
+++ b/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,
@@ -344,17 +352,17 @@ LiftedWCNF::LiftedWCNF (const ParfactorList& pfList)
   c1.addLiteral (Literal (0, LogVars() = {0}));
   c1.addLiteralNegated (Literal (1, {0,1}));
   clauses_.push_back(c1);
-    
+
   Clause c2 (names);
   c2.addLiteral (Literal (0, LogVars()={0}));
   c2.addLiteralNegated (Literal (1, {1,0}));
   clauses_.push_back(c2);
-  
+
   addWeight (0, 3.0, 4.0);
   addWeight (1, 2.0, 5.0);
-  
+
   freeLiteralId_ = 2;
-  
+
   cout << "FORMULA INDICATORS:" << endl;
   // printFormulaIndicators();
   cout << endl;
diff --git a/packages/CLPBN/horus/LiftedWCNF.h b/packages/CLPBN/horus/LiftedWCNF.h
index a5b7547bc..7220b0823 100644
--- a/packages/CLPBN/horus/LiftedWCNF.h
+++ b/packages/CLPBN/horus/LiftedWCNF.h
@@ -34,6 +34,8 @@ class Literal
     LogVars logVars (void) const { return logVars_; }
 
     LogVarSet logVarSet (void) const { return LogVarSet (logVars_); }
+    
+    size_t nrLogVars (void) const { return logVars_.size(); }
 
     void negate (void) { negated_ = !negated_; }
 
@@ -42,6 +44,8 @@ class Literal
     bool isNegative (void) const { return negated_; }
     
     bool isGround (ConstraintTree constr, LogVarSet ipgLogVars) const;
+    
+    size_t indexOfLogVar (LogVar X) const;
 
     string toString (LogVarSet ipgLogVars = LogVarSet(),
       LogVarSet posCountedLvs = LogVarSet(),