Implemented SkolemTermsManager.

5 files changed, 135 insertions, 129 deletions

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);
 }