Restored fixed SkolemTermsManager (went lost in some revert).

4 files changed, 52 insertions, 54 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
index dee2966..7f02741 100644
--- a/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
+++ b/src/uk/ac/ox/cs/pagoda/query/QueryRecord.java
@@ -707,7 +707,7 @@ public class QueryRecord extends Disposable {
         UPPER_BOUND,
         SIMPLE_UPPER_BOUND,
         LAZY_UPPER_BOUND,
-        L_SKOLEM_UPPER_BOUND,
+        SKOLEM_UPPER_BOUND,
         EL_LOWER_BOUND,
         FRAGMENT,
         FRAGMENT_REFINEMENT,
diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
index ed6589a..123bd5e 100644
--- a/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
+++ b/src/uk/ac/ox/cs/pagoda/reasoner/MyQueryReasoner.java
@@ -370,10 +370,10 @@ class MyQueryReasoner extends QueryReasoner {
 
         relevantStore.importDataFromABoxOf(relevantSubset);
 
-        int queryDependentMaxTermDepth = 10; // TODO make it dynamic
+        int queryDependentMaxTermDepth = 1; // TODO make it dynamic
         int materialisationTag = relevantStore.materialiseSkolemly(relevantProgram, null,
                                                                    queryDependentMaxTermDepth);
-        queryRecord.addProcessingTime(Step.L_SKOLEM_UPPER_BOUND, t.duration());
+        queryRecord.addProcessingTime(Step.SKOLEM_UPPER_BOUND, t.duration());
         if(materialisationTag == -1) {
             throw new Error("A consistent ontology has turned out to be " +
                                     "inconsistent in the Skolemises-relevant-upper-store");
@@ -385,7 +385,7 @@ class MyQueryReasoner extends QueryReasoner {
 
         boolean isFullyProcessed = queryUpperStore(relevantStore, queryRecord,
                                                    queryRecord.getExtendedQueryText(),
-                                                   Step.L_SKOLEM_UPPER_BOUND);
+                                                   Step.SKOLEM_UPPER_BOUND);
         Utility.logInfo("Semi-Skolemised relevant upper store has been evaluated");
         return isFullyProcessed;
     }
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 5f6e362..dc2ba8a 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -18,7 +18,7 @@ import java.util.Collection;
  * it Skolemises the rule
  * if all the terms in the substitution have depth less than a given depth,
  * otherwise it approximates using an alternative <tt>TupleDependentApproximator</tt>.
- * */
+ */
 public class LimitedSkolemisationApproximator implements TupleDependentApproximator {
 
     private static final Atom[] EMPTY_BODY = new Atom[0];
@@ -41,7 +41,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
     public Collection<DLClause> convert(DLClause clause,
                                         DLClause originalClause,
                                         Collection<Tuple<Individual>> violationTuples) {
-        switch (clause.getHeadLength()) {
+        switch(clause.getHeadLength()) {
             case 1:
                 return overApprox(clause, originalClause, violationTuples);
             case 0:
@@ -65,7 +65,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
     private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
         ArrayList<DLClause> result = new ArrayList<>();
 
-        for (Tuple<Individual> violationTuple : violationTuples)
+        for(Tuple<Individual> violationTuple : violationTuples)
             if(getMaxDepth(violationTuple) > maxTermDepth) {
                 result.addAll(alternativeApproximator.convert(clause, originalClause, null));
                 Utility.logDebug("Approximating maximal individual by a constant in rule:" + originalClause);
@@ -84,7 +84,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
         // TODO check: strong assumption, the first tuples are the common ones
         TupleBuilder<Individual> commonIndividualsBuilder = new TupleBuilder<>();
-        for (int i = 0; i < commonVars.length; i++)
+        for(int i = 0; i < commonVars.length; i++)
             commonIndividualsBuilder.append(violationTuple.get(i));
         Tuple<Individual> commonIndividuals = commonIndividualsBuilder.build();
 
@@ -96,54 +96,55 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
         // BEGIN: copy and paste
         ArrayList<DLClause> ret = new ArrayList<>();
         DLPredicate predicate = headAtom.getDLPredicate();
-        if (predicate instanceof AtLeastConcept) {
+        if(predicate instanceof AtLeastConcept) {
             AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
             LiteralConcept concept = atLeastConcept.getToConcept();
             Role role = atLeastConcept.getOnRole();
             AtomicConcept atomicConcept;
 
-            if (concept instanceof AtomicNegationConcept) {
+            if(concept instanceof AtomicNegationConcept) {
                 // TODO CHECK: is this already in MultiStageUpperProgram?
-                Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
+                Atom atom1 =
+                        Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
                 Atom atom2 = Atom.create(atomicConcept = OverApproxExist.getNegationConcept(atomicConcept), X);
-                ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2}));
+                ret.add(DLClause.create(new Atom[0], new Atom[]{atom1, atom2}));
             }
             else {
                 atomicConcept = (AtomicConcept) concept;
-                if (atomicConcept.equals(AtomicConcept.THING))
+                if(atomicConcept.equals(AtomicConcept.THING))
                     atomicConcept = null;
             }
 
             int card = atLeastConcept.getNumber();
             Individual[] individuals = new Individual[card];
             SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
-            for (int i = 0; i < card; ++i)
+            for(int i = 0; i < card; ++i)
                 individuals[i] = termsManager.getFreshIndividual(originalClause,
                                                                  offset + i,
                                                                  commonIndividuals);
 
-            for (int i = 0; i < card; ++i) {
-                if (atomicConcept != null)
-                    ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY));
+            for(int i = 0; i < card; ++i) {
+                if(atomicConcept != null)
+                    ret.add(DLClause.create(new Atom[]{Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY));
 
                 Atom atom = role instanceof AtomicRole ?
                         Atom.create((AtomicRole) role, commonIndividuals.get(0), individuals[i]) :
                         Atom.create(((InverseRole) role).getInverseOf(), individuals[i], commonIndividuals.get(0));
 
-                ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY));
+                ret.add(DLClause.create(new Atom[]{atom}, EMPTY_BODY));
             }
 
-            for (int i = 0; i < card; ++i)
-                for (int j = i + 1; j < card; ++j)
+            for(int i = 0; i < card; ++i)
+                for(int j = i + 1; j < card; ++j)
                     // TODO to be checked ... different as
-                    ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, EMPTY_BODY));
+                    ret.add(DLClause.create(new Atom[]{Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, EMPTY_BODY));
 
         }
-        else if (predicate instanceof AtLeastDataRange) {
+        else if(predicate instanceof AtLeastDataRange) {
             // TODO to be implemented ...
         }
         else
-            ret.add(DLClause.create(new Atom[] {headAtom}, EMPTY_BODY));
+            ret.add(DLClause.create(new Atom[]{headAtom}, EMPTY_BODY));
 
         return ret;
 
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
index 368c014..07ad1f9 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
@@ -17,13 +17,12 @@ public class SkolemTermsManager {
     private static SkolemTermsManager skolemTermsManager;
 
     private int termsCounter = 0;
-    private Map<DLClause, Integer> mapClauseToId = new HashMap<>();
-    private Map<Individual, Integer> mapTermToDepth = new HashMap<>();
+    private Map<DLClause, Integer> clauseToId_map = new HashMap<>();
+    private Map<Individual, Integer> individualToDepth_map = new HashMap<>();
     private int dependenciesCounter = 0;
 
-    // TODO replace with hashcode. in case of collision you get only a different upper bound model.
-    // TODO you can use a cash.
-    private Map<Tuple<Individual>, Integer> mapDependencyToId = new HashMap<>();
+    // TODO replace with hashcode. in case of collision you would get only a different upper bound model.
+    private Map<Tuple<Individual>, Integer> dependencyToId_map = new HashMap<>();
 
     private SkolemTermsManager() {
     }
@@ -38,6 +37,11 @@ public class SkolemTermsManager {
         return -1;
     }
 
+    /**
+     * Returns the existing unique <tt>SkolemTermsManager</tt> or a new one.
+     * <p>
+     * Indeed the <tt>SkolemTermsManager</tt> is a singleton.
+     */
     public static SkolemTermsManager getInstance() {
         if(skolemTermsManager == null) skolemTermsManager = new SkolemTermsManager();
         return skolemTermsManager;
@@ -47,21 +51,14 @@ public class SkolemTermsManager {
      * Get a fresh Individual, unique for the clause, the offset and the dependency.
      * */
     public Individual getFreshIndividual(DLClause originalClause, int offset, Tuple<Individual> dependency) {
-        if(!mapClauseToId.containsKey(originalClause)) {
-            mapClauseToId.put(originalClause, termsCounter);
-            termsCounter += noOfExistential(originalClause);
-        }
-        if (!mapDependencyToId.containsKey(dependency)) {
-            mapDependencyToId.put(dependency, dependenciesCounter++);
-        }
-
-        String termId = mapClauseToId.get(originalClause) + offset + "_" + mapDependencyToId(dependency);
+        String termId = Integer.toString(mapClauseToId(originalClause) + offset)
+                + "_" + mapDependencyToId(dependency);
         Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId);
 
         int depth = 0;
         for (Individual individual : dependency)
-            depth = Integer.max(depth, mapIndividualToDepth(individual));
-        mapTermToDepth.put(newIndividual, depth);
+            depth = Integer.max(depth, getDepthOf(individual));
+        individualToDepth_map.put(newIndividual, depth);
 
         return newIndividual;
     }
@@ -70,14 +67,9 @@ public class SkolemTermsManager {
      * Get a fresh Individual, unique for the clause and the offset.
      * */
     public Individual getFreshIndividual(DLClause originalClause, int offset) {
-        if(!mapClauseToId.containsKey(originalClause)) {
-            mapClauseToId.put(originalClause, termsCounter);
-            termsCounter += noOfExistential(originalClause);
-        }
-
-        String termId = "" + mapClauseToId.get(originalClause) + offset;
+        String termId = Integer.toString(mapClauseToId(originalClause) + offset);
         Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId);
-        mapTermToDepth.put(newIndividual, 0);
+//        individualToDepth_map.put(newIndividual, 0); // TODO REMOVE
 
         return newIndividual;
     }
@@ -88,24 +80,29 @@ public class SkolemTermsManager {
      * The term must have been generated by this manager.
      * */
     public int getDepthOf(Individual individual) {
-        return mapIndividualToDepth(individual);
+        if(individualToDepth_map.containsKey(individual)) return individualToDepth_map.get(individual);
+        else return 0;
     }
 
     /**
      * Get the number of individuals generated by this manager.
      * */
     public int getNumberOfSkolemisedIndividual() {
-        return mapTermToDepth.keySet().size();
+        return individualToDepth_map.keySet().size();
     }
 
-    private int mapDependencyToId(Tuple<Individual> dependency) {
-        if (mapDependencyToId.containsKey(dependency)) return mapDependencyToId.get(dependency);
-        else return mapDependencyToId.put(dependency, dependenciesCounter++);
+    private int mapClauseToId(DLClause clause) {
+        if(!clauseToId_map.containsKey(clause)) {
+            clauseToId_map.put(clause, termsCounter);
+            termsCounter += noOfExistential(clause);
+        }
+        return clauseToId_map.get(clause);
     }
 
-    private int mapIndividualToDepth(Individual dependency) {
-        if(mapTermToDepth.containsKey(dependency)) return mapTermToDepth.get(dependency);
-        else return 0;
+    private int mapDependencyToId(Tuple<Individual> dependency) {
+        if(!dependencyToId_map.containsKey(dependency))
+            dependencyToId_map.put(dependency, dependenciesCounter++);
+        return dependencyToId_map.get(dependency);
     }
 
     private int noOfExistential(DLClause originalClause) {