Implemented SkolemTermsManager.

14 files changed, 259 insertions, 143 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java b/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java
index 22d90c4..a9c127b 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java
@@ -7,7 +7,7 @@ import org.openrdf.model.impl.URIImpl;
 import org.openrdf.rio.RDFHandler;
 import org.openrdf.rio.RDFHandlerException;
 import uk.ac.ox.cs.JRDFox.model.Individual;
-import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 
 import java.util.Collection;
@@ -58,9 +58,9 @@ public class IndividualCollector implements RDFHandler {
 
         public Collection<Individual> getAllIndividuals() {
                 if (!addedSkolemised) {
-                        int number = OverApproxExist.getNumberOfSkolemisedIndividual();
+                        int number = SkolemTermsManager.getInstance().getNumberOfSkolemisedIndividual();
                         for (int i = 0; i < number; ++i)
-                                individuals.add(Individual.create(OverApproxExist.skolemisedIndividualPrefix + i));
+                                individuals.add(Individual.create(SkolemTermsManager.skolemisedIndividualPrefix + i));
                         addedSkolemised = true; 
                 }
                 return individuals; 
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java
index 33ba345..1664c99 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java
@@ -15,6 +15,7 @@ import uk.ac.ox.cs.pagoda.util.Namespace;
 import uk.ac.ox.cs.pagoda.util.SparqlHelper;
 import uk.ac.ox.cs.pagoda.util.Timer;
 import uk.ac.ox.cs.pagoda.util.Utility;
+import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
 
 import java.io.*;
 import java.util.*;
@@ -376,7 +377,7 @@ public abstract class MultiStageUpperProgram {
                 return m_bottom.process(m_approxExist.convert(clause, originalDLClause, null));
         }
 
-        public Collection<DLClause> convertExist(DLClause clause, DLClause originalDLClause, List<AnswerTupleID> violationTuples) {
+        public Collection<DLClause> convertExist(DLClause clause, DLClause originalDLClause, Collection<Tuple<Individual>> violationTuples) {
                 return m_bottom.process(m_approxExist.convert(clause, originalDLClause, violationTuples));
         }
 
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java b/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java
index b31d138..c5482e7 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java
@@ -7,6 +7,7 @@ import uk.ac.ox.cs.pagoda.approx.Clause;
 import uk.ac.ox.cs.pagoda.approx.Clausifier;
 import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
 import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 import uk.ac.ox.cs.pagoda.util.Utility;
 
@@ -102,7 +103,9 @@ public class Normalisation {
                         return ;
                 }
                 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
-                AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0));
+                // TODO test
+//              AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0));
+                AtomicConcept ac = getRightAuxiliaryConcept(alc, SkolemTermsManager.getInstance().getFreshIndividual(clause, 0));
                 DLClause newClause;
                 m_normClauses.add(DLClause.create(new Atom[] {Atom.create(ac, headAtom.getArgument(0)) }, clause.getBodyAtoms()));
                 m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, X)}, new Atom[] {Atom.create(ac, X)}));
@@ -140,7 +143,8 @@ public class Normalisation {
                                         }
                                 } else {
                                         AtLeastConcept alc = toAtLeastConcept((AtLeast) headAtom.getDLPredicate());
-                                        AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0));
+//                                      AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0));
+                                        AtomicConcept ac = getRightAuxiliaryConcept(alc, SkolemTermsManager.getInstance().getFreshIndividual(clause, 0));
                                         newHeadAtoms[index] = Atom.create(ac, headAtom.getArgument(0));
                                         m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, headAtom.getArgument(0))}, new Atom[] {newHeadAtoms[index]}));
                                         exist2original.put(newClause, clause);
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/ViolationTuple.java b/src/uk/ac/ox/cs/pagoda/multistage/ViolationTuple.java
new file mode 100644
index 0000000..129f5dd
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/multistage/ViolationTuple.java
@@ -0,0 +1,19 @@
+package uk.ac.ox.cs.pagoda.multistage;
+
+import org.semanticweb.HermiT.model.Individual;
+
+import java.util.ArrayList;
+
+/**
+ * Just a list of <tt>Individual</tt>s.
+ * */
+public class ViolationTuple extends ArrayList<Individual> {
+
+    public ViolationTuple() {
+        super();
+    }
+
+    public ViolationTuple(int size) {
+        super(size);
+    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java b/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java
index 244eb7a..fefb8b2 100644
--- a/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java
+++ b/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConcept.java
@@ -14,6 +14,8 @@ import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 import uk.ac.ox.cs.pagoda.util.SparqlHelper;
 import uk.ac.ox.cs.pagoda.util.Utility;
+import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
+import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder;
 
 import java.util.*;
 
@@ -99,7 +101,20 @@ public abstract class Pick4NegativeConcept implements Treatment {
                 }
                 else {
                         Set<Atom> headAtoms = new HashSet<Atom>();
-                        for (DLClause clause : program.convertExist(constraint, violation.getClause(), violation.getTuples())) {
+
+                        ArrayList<Tuple<Individual>> violationTuples = new ArrayList<>(violation.getTuples().size());
+                        for (int i = 0; i < violation.getTuples().size(); i++) {
+                                AnswerTupleID answerTupleID = violation.getTuples().get(i);
+                                TupleBuilder<Individual> tupleBuilder = new TupleBuilder<>();
+                                for (int j = 0; j < answerTupleID.getArity(); j++) {
+                                        String rawTerm = tripleManager.getRawTerm(answerTupleID.getTerm(j));
+                                        Individual individual = Individual.create(rawTerm.substring(1, rawTerm.length()-1));
+                                        tupleBuilder.add(individual);
+                                }
+                                violationTuples.add(tupleBuilder.create());
+                        }
+
+                        for (DLClause clause : program.convertExist(constraint, violation.getClause(), violationTuples)) {
 
                                 if (!DLClauseHelper.hasSubsetBodyAtoms(clause, constraint)) {
                                         Utility.logError("There might be an error here... Cannot happen!!!");
diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
index 7c9562f..a7afa2e 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
@@ -1,9 +1,10 @@
 package uk.ac.ox.cs.pagoda.rules;
 
 import org.semanticweb.HermiT.model.DLClause;
-import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import org.semanticweb.HermiT.model.Individual;
 import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
 import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator;
+import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
 
 import java.util.Collection;
 
@@ -19,7 +20,7 @@ public class ExistConstantApproximator implements TupleDependentApproximator {
     }
 
     @Override
-    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
         return overApproxExist.convert(clause, originalClause);
     }
 }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
index 8fc6b77..e53ae49 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -1,8 +1,10 @@
 package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.DLClause;
+import org.semanticweb.HermiT.model.Individual;
 import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
 import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
+import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
 
 import java.util.*;
 
@@ -33,7 +35,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
     }
 
     @Override
-    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
         switch (clause.getHeadLength()) {
             case 1:
                 return overApprox(clause, originalClause, violationTuples);
@@ -48,26 +50,26 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
     }
 
-    private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+    private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
         ArrayList<DLClause> result = new ArrayList<>();
 
-        for (AnswerTupleID violationTuple : violationTuples)
+        for (Tuple<Individual> violationTuple : violationTuples)
             if (getDepth(violationTuple) > maxTermDepth)
                 result.addAll(alternativeApproximator.convert(clause, originalClause, null));
             else
-                result.add(getInstantiatedSkolemisation(clause, originalClause, violationTuple));
+                result.add(getGroundSkolemisation(clause, originalClause, violationTuple));
 
         return result;
     }
 
 
-    private DLClause getInstantiatedSkolemisation(DLClause clause, DLClause originalClause, AnswerTupleID violationTuple) {
+    private DLClause getGroundSkolemisation(DLClause clause, DLClause originalClause, Tuple<Individual> violationTuple) {
         // TODO implement
         // filter the violation tuples appearing on both the sides of the rule
         return null;
     }
 
-    private int getDepth(AnswerTupleID violationTuple) {
+    private int getDepth(Tuple<Individual> violationTuple) {
         if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0;
         return mapIndividualsToDepth.get(violationTuple);
     }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
index e0bafe0..d71c472 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
@@ -2,27 +2,15 @@ package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
-import uk.ac.ox.cs.pagoda.util.Namespace;
 
-import java.util.*;
+import java.util.Collection;
+import java.util.Iterator;
+import java.util.LinkedList;
 
 public class OverApproxExist implements Approximator {
 
         public static final String negativeSuffix = "_neg";
-        public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
         private static final Variable X = Variable.create("X");
-        //DEBUG
-        public static Collection<String> createdIndividualIRIs = new HashSet<>();
-        private static int individualCounter = 0;
-        private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>();
-
-        private static int noOfExistential(DLClause originalClause) {
-                int no = 0;
-                for (Atom atom: originalClause.getHeadAtoms())
-                        if (atom.getDLPredicate() instanceof AtLeast)
-                                no += ((AtLeast) atom.getDLPredicate()).getNumber();
-                return no;
-        }
 
         private static int indexOfExistential(Atom headAtom, DLClause originalClause) {
                 if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
@@ -65,36 +53,6 @@ public class OverApproxExist implements Approximator {
                 return null;
         }
 
-        public static int getNumberOfSkolemisedIndividual() {
-                return individualCounter;
-        }
-        //DEBUG
-
-        public static Individual getNewIndividual(DLClause originalClause, int offset) {
-                Individual ret;
-                int individualID;
-                if (individualNumber.containsKey(originalClause)) {
-                        individualID = individualNumber.get(originalClause) + offset;
-                        ret = Individual.create(skolemisedIndividualPrefix + individualID);
-                }
-                else {
-                        individualNumber.put(originalClause, individualCounter);
-                        individualID = individualCounter + offset;
-                        ret = Individual.create(skolemisedIndividualPrefix + individualID);
-                        individualCounter += noOfExistential(originalClause);
-                }
-                return ret;
-        }
-        
-        public static int indexOfSkolemisedIndividual(Atom atom) {
-                Term t;
-                for (int index = 0; index < atom.getArity(); ++index) {
-                        t = atom.getArgument(index);
-                        if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index;
-                }
-                return -1;
-        }
-
         @Override
         public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
                 Collection<DLClause> ret;
@@ -140,7 +98,8 @@ public class OverApproxExist implements Approximator {
 
                         int card = atLeastConcept.getNumber(); 
                         Individual[] individuals = new Individual[card];
-                        for (int i = 0; i < card; ++i) individuals[i] = getNewIndividual(originalClause, offset + i);
+                        SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
+                        for (int i = 0; i < card; ++i) individuals[i] = termsManager.getFreshIndividual(originalClause, offset + i);
                         
                         for (int i = 0; i < card; ++i) {
                                 if (atomicConcept != null)
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java
deleted file mode 100644
index a920ec5..0000000
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java
+++ /dev/null
@@ -1,74 +0,0 @@
-package uk.ac.ox.cs.pagoda.rules.approximators;
-
-import org.semanticweb.HermiT.model.AtLeast;
-import org.semanticweb.HermiT.model.Atom;
-import org.semanticweb.HermiT.model.DLClause;
-import org.semanticweb.HermiT.model.Individual;
-import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
-import uk.ac.ox.cs.pagoda.util.Namespace;
-
-import java.util.HashMap;
-import java.util.Map;
-
-/**
- * If you need a Skolem term (i.e. fresh individual), ask this class.
- */
-public class SkolemTermsDispenser {
-
-    public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
-    private static SkolemTermsDispenser skolemTermsDispenser;
-    private int individualCounter = 0;
-    private Map<DLClause, Integer> termNumber = new HashMap<>();
-    private Map<SkolemTermId, Integer> mapTermToDepth = new HashMap<>();
-    private int dependenciesCounter = 0;
-    private Map<AnswerTupleID, Integer> mapDependencyToId = new HashMap<>();
-
-    private SkolemTermsDispenser() {
-    }
-
-    public static SkolemTermsDispenser getInstance() {
-        if (skolemTermsDispenser == null) skolemTermsDispenser = new SkolemTermsDispenser();
-        return skolemTermsDispenser;
-    }
-
-    private int getDependencyId(AnswerTupleID answerTupleID) {
-        if (mapDependencyToId.containsKey(answerTupleID)) return mapDependencyToId.get(answerTupleID);
-        else return mapDependencyToId.put(answerTupleID, dependenciesCounter++);
-    }
-
-    public Individual getNewIndividual(DLClause originalClause, int offset, AnswerTupleID dependency) {
-        if (!termNumber.containsKey(originalClause)) {
-            termNumber.put(originalClause, individualCounter);
-            individualCounter += noOfExistential(originalClause);
-        }
-        if (!mapDependencyToId.containsKey(dependency)) {
-            mapDependencyToId.put(dependency, dependenciesCounter++);
-        }
-
-        SkolemTermId termId = new SkolemTermId(termNumber.get(originalClause) + offset, getDependencyId(dependency));
-        return Individual.create(skolemisedIndividualPrefix + termId);
-    }
-
-    private int noOfExistential(DLClause originalClause) {
-        int no = 0;
-        for (Atom atom : originalClause.getHeadAtoms())
-            if (atom.getDLPredicate() instanceof AtLeast)
-                no += ((AtLeast) atom.getDLPredicate()).getNumber();
-        return no;
-    }
-
-    private class SkolemTermId {
-        private final int idBase;
-        private final int idOffset;
-
-        private SkolemTermId(int idBase, int idOffset) {
-            this.idBase = idBase;
-            this.idOffset = idOffset;
-        }
-
-        @Override
-        public String toString() {
-            return idBase + "_" + idOffset;
-        }
-    }
-}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
new file mode 100644
index 0000000..0413e65
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
@@ -0,0 +1,116 @@
+package uk.ac.ox.cs.pagoda.rules.approximators;
+
+import org.semanticweb.HermiT.model.*;
+import uk.ac.ox.cs.pagoda.util.Namespace;
+import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
+
+import java.util.HashMap;
+import java.util.Map;
+
+/**
+ * If you need a Skolem term (i.e. fresh individual), ask this class.
+ */
+public class SkolemTermsManager {
+
+    public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
+
+    private static SkolemTermsManager skolemTermsManager;
+
+    private int individualCounter = 0;
+    private Map<DLClause, Integer> termNumber = new HashMap<>();
+    private Map<Individual, Integer> mapIndividualToDepth = new HashMap<>();
+    private int dependenciesCounter = 0;
+
+    // replace with hashcode. in case of collision you get only a different upper bound model.
+    private Map<Tuple<Individual>, Integer> mapDependencyToId = new HashMap<>();
+
+    /**
+     * Get a fresh Individual, unique for the clause, the offset and the dependency.
+     * */
+    public Individual getFreshIndividual(DLClause originalClause, int offset, Tuple<Individual> dependency) {
+        if (!termNumber.containsKey(originalClause)) {
+            termNumber.put(originalClause, individualCounter);
+            individualCounter += noOfExistential(originalClause);
+        }
+        if (!mapDependencyToId.containsKey(dependency)) {
+            mapDependencyToId.put(dependency, dependenciesCounter++);
+        }
+
+        String termId = termNumber.get(originalClause) + offset + "_" + mapDependencyToId(dependency);
+        Individual newIndividual = Individual.create(skolemisedIndividualPrefix + termId);
+
+        int depth = 0;
+        for (Individual individual : dependency)
+            depth = Integer.max(depth, mapIndividualToDepth(individual));
+        mapIndividualToDepth.put(newIndividual, depth);
+
+        return newIndividual;
+    }
+
+    /**
+     * Get a fresh Individual, unique for the clause and the offset.
+     * */
+    public Individual getFreshIndividual(DLClause originalClause, int offset) {
+        if (!termNumber.containsKey(originalClause)) {
+            termNumber.put(originalClause, individualCounter);
+            individualCounter += noOfExistential(originalClause);
+        }
+
+        String termId = "" + termNumber.get(originalClause) + offset;
+        Individual newIndividual = Individual.create(skolemisedIndividualPrefix + termId);
+        mapIndividualToDepth.put(newIndividual, 0);
+
+        return newIndividual;
+    }
+
+    /**
+     * Get the depth of a term.
+     * <p>
+     * The term must have been generated by this manager.
+     * */
+    public int getDepth(Individual individual) {
+        return mapIndividualToDepth(individual);
+    }
+
+    /**
+     * Get the number of individuals generated by this manager.
+     * */
+    public int getNumberOfSkolemisedIndividual() {
+        return mapIndividualToDepth.keySet().size();
+        }
+
+    public static int indexOfSkolemisedIndividual(Atom atom) {
+        Term t;
+        for (int index = 0; index < atom.getArity(); ++index) {
+            t = atom.getArgument(index);
+            if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index;
+        }
+        return -1;
+    }
+
+    private SkolemTermsManager() {
+    }
+
+    public static SkolemTermsManager getInstance() {
+        if (skolemTermsManager == null) skolemTermsManager = new SkolemTermsManager();
+        return skolemTermsManager;
+    }
+
+    private int mapDependencyToId(Tuple<Individual> dependency) {
+        if (mapDependencyToId.containsKey(dependency)) return mapDependencyToId.get(dependency);
+        else return mapDependencyToId.put(dependency, dependenciesCounter++);
+    }
+
+    private int mapIndividualToDepth(Individual dependency) {
+        if (mapIndividualToDepth.containsKey(dependency)) return mapIndividualToDepth.get(dependency);
+        else return 0;
+    }
+
+    private int noOfExistential(DLClause originalClause) {
+        int no = 0;
+        for (Atom atom : originalClause.getHeadAtoms())
+            if (atom.getDLPredicate() instanceof AtLeast)
+                no += ((AtLeast) atom.getDLPredicate()).getNumber();
+        return no;
+    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
index 1a729e5..c99a1ad 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java
@@ -1,16 +1,19 @@
 package uk.ac.ox.cs.pagoda.rules.approximators;
 
 import org.semanticweb.HermiT.model.DLClause;
-import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+import org.semanticweb.HermiT.model.Individual;
+import uk.ac.ox.cs.pagoda.util.tuples.Tuple;
 
 import java.util.Collection;
 
 /**
- * It approximates rules according to a specific instantiation of the body.
+ * It can approximate clauses according to a collection of tuples of individuals.
+ * <p>
+ * In particular it can be used to approximate rules given some body instantiations.
  */
 public interface TupleDependentApproximator {
 
     Collection<DLClause> convert(DLClause clause,
                                  DLClause originalClause,
-                                 Collection<AnswerTupleID> violationTuples);
+                                 Collection<Tuple<Individual>> individualsTuples);
 }
diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
index 331ad12..b169053 100644
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
+++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java
@@ -4,7 +4,7 @@ import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
 import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
 import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
-import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
+import uk.ac.ox.cs.pagoda.rules.approximators.SkolemTermsManager;
 import uk.ac.ox.cs.pagoda.util.Namespace;
 
 import java.util.*;
@@ -22,8 +22,9 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap
          */
         protected void processDisjunctiveRules() {
                 Map<Atom, Collection<DLClause>> auxiliaryAtoms = new HashMap<Atom, Collection<DLClause>>(); 
-                Map<Individual, Collection<DLClause>> skolemisedAtoms = new HashMap<Individual, Collection<DLClause>>(); 
-                
+                Map<Individual, Collection<DLClause>> skolemisedAtoms = new HashMap<Individual, Collection<DLClause>>();
+                SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
+
                 for (Map.Entry<DLClause, Collection<DLClause>> entry: disjunctiveRules.entrySet()) {
                         DLClause original = entry.getKey();
                         Collection<DLClause> overClauses = entry.getValue(); 
@@ -33,7 +34,7 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap
                                 DLClause subClause = iter.next(); 
                                 if (DLClauseHelper.hasSubsetBodyAtoms(subClause, original)) {
                                         Atom headAtom = subClause.getHeadAtom(0);
-                                        if ((index = OverApproxExist.indexOfSkolemisedIndividual(headAtom)) != -1) {
+                                        if ((index = SkolemTermsManager.indexOfSkolemisedIndividual(headAtom)) != -1) {
                                                 Individual i = (Individual) headAtom.getArgument(index);
                                                 Collection<DLClause> clauses = skolemisedAtoms.get(i);
                                                 if (clauses == null) {
@@ -55,7 +56,7 @@ public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap
                                         Collection<DLClause> clauses = new HashSet<DLClause>();
                                         Individual[] individuals = new Individual[alc.getNumber()]; 
                                         for (int i = 0; i < alc.getNumber(); ++i) {
-                                                individuals[i] = OverApproxExist.getNewIndividual(original, i);
+                                                individuals[i] = termsManager.getFreshIndividual(original, i);
                                                 clauses.addAll(skolemisedAtoms.get(individuals[i])); 
                                         }
                                         auxiliaryAtoms.put(getAuxiliaryAtom(original, headAtom, individuals), clauses);
diff --git a/src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java b/src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java
new file mode 100644
index 0000000..3e72748
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/util/tuples/Tuple.java
@@ -0,0 +1,44 @@
+package uk.ac.ox.cs.pagoda.util.tuples;
+
+import java.util.ArrayList;
+import java.util.Iterator;
+import java.util.Spliterator;
+import java.util.function.Consumer;
+
+public class Tuple<T> implements Iterable<T> {
+
+    final ArrayList<T> elements = new ArrayList<>();
+
+    Tuple() { }
+
+    public Tuple(T... elements) {
+        for(T t: elements) {
+            this.elements.add(t);
+        }
+    }
+    
+    public Tuple(Iterable<T> iterable) {
+        for (T t : iterable) {
+            this.elements.add(t);
+        }
+    }
+
+    public T get(int i) {
+        return elements.get(i);
+    }
+
+    @Override
+    public Iterator<T> iterator() {
+        return elements.iterator();
+    }
+
+    @Override
+    public void forEach(Consumer<? super T> action) {
+        elements.forEach(action);
+    }
+
+    @Override
+    public Spliterator<T> spliterator() {
+        return elements.spliterator();
+    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/util/tuples/TupleBuilder.java b/src/uk/ac/ox/cs/pagoda/util/tuples/TupleBuilder.java
new file mode 100644
index 0000000..aacd15e
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/util/tuples/TupleBuilder.java
@@ -0,0 +1,25 @@
+package uk.ac.ox.cs.pagoda.util.tuples;
+
+/**
+ * Allows to create an immutable <tt>Tuple</tt> in a non-atomic way.
+ * It can create only one <tt>Tuple</tt>.
+ * */
+public class TupleBuilder<T> {
+
+    private Tuple tuple = new Tuple();
+
+    private boolean building = true;
+
+    public boolean add(T t) {
+        if(building) tuple.elements.add(t);
+        return building;
+    }
+
+    public Tuple<T> create() {
+        if(building) {
+            building = false;
+            return tuple;
+        }
+        return null;
+    }
+}