1 files changed, 12 insertions, 10 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 3f1ed7e..5f6e362 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -3,6 +3,7 @@ package uk.ac.ox.cs.pagoda.rules.approximators;
 import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.multistage.MultiStageUpperProgram;
 import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
+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;
 
@@ -53,12 +54,22 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
     }
 
+    public int getMaxDepth(Tuple<Individual> violationTuple) {
+        int maxDepth = 0;
+        for(Individual individual : violationTuple)
+            maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepthOf(individual));
+
+        return maxDepth;
+    }
+
     private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
         ArrayList<DLClause> result = new ArrayList<>();
 
         for (Tuple<Individual> violationTuple : violationTuples)
-            if (getMaxDepth(violationTuple) > maxTermDepth)
+            if(getMaxDepth(violationTuple) > maxTermDepth) {
                 result.addAll(alternativeApproximator.convert(clause, originalClause, null));
+                Utility.logDebug("Approximating maximal individual by a constant in rule:" + originalClause);
+            }
             else
                 result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple));
 
@@ -138,13 +149,4 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
         // END: copy and paste
     }
-
-
-    public int getMaxDepth(Tuple<Individual> violationTuple) {
-        int maxDepth = 0;
-        for (Individual individual : violationTuple)
-            maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepthOf(individual));
-
-        return maxDepth;
-    }
 }