The LimitedSkolemisation now employs a fixed-depth term instead of a constant. Performed some testing before merging with master.

4 files changed, 37 insertions, 22 deletions

diff --git a/src/resources/pagoda.properties b/src/resources/pagoda.properties
index 07a0eac..e6aa503 100644
--- a/src/resources/pagoda.properties
+++ b/src/resources/pagoda.properties
@@ -1,9 +1,9 @@
 debug=true
 useAlwaysSimpleUpperBound=false
 skolemUpperBound=DISABLED
-skolemDepth=1
 #skolemUpperBound=BEFORE_SUMMARISATION
 #skolemUpperBound=AFTER_SUMMARISATION
+skolemDepth=1
 toCallHermit=true
 
 statisticsDir=/home/alessandro/Dropbox/Oxford/PAGOdA/statistics
\ No newline at end of file
diff --git a/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java b/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java
index 320af09..0f215ad 100644
--- a/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java
+++ b/src/uk/ac/ox/cs/pagoda/endomorph/DependencyGraph.java
@@ -241,7 +241,6 @@ public class DependencyGraph {
                 ++homomorphismCheckCounter; 
                 homomorphismChecker.setMapping(u, v);
 
-                // TODO recently added, test it
                 if(!homomorphismChecker.isMappingTo(u, v))
                         return false;
 
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 2c8e23d..7d29c74 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -2,7 +2,6 @@ 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.tuples.Tuple;
 import uk.ac.ox.cs.pagoda.util.tuples.TupleBuilder;
 
@@ -23,16 +22,10 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
     private static final Atom[] EMPTY_BODY = new Atom[0];
     private static final Variable X = Variable.create("X");
     private final int maxTermDepth;
-    private final TupleDependentApproximator alternativeApproximator;
     private final SkolemTermsManager skolemTermsManager;
 
     public LimitedSkolemisationApproximator(int maxTermDepth) {
-        this(maxTermDepth, new ExistConstantApproximator());
-    }
-
-    public LimitedSkolemisationApproximator(int maxTermDepth, TupleDependentApproximator alternativeApproximator) {
         this.maxTermDepth = maxTermDepth;
-        this.alternativeApproximator = alternativeApproximator;
         this.skolemTermsManager = SkolemTermsManager.getInstance();
     }
 
@@ -64,10 +57,8 @@ 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) {
-            if(getMaxDepth(violationTuple) < maxTermDepth)
-                result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple));
-            else
-                result.addAll(alternativeApproximator.convert(clause, originalClause, null));
+                result.addAll(getGroundSkolemisation(clause,
+                        originalClause, violationTuple, getMaxDepth(violationTuple) >= maxTermDepth));
         }
 
         return result;
@@ -75,7 +66,8 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
 
     private Collection<DLClause> getGroundSkolemisation(DLClause clause,
                                                         DLClause originalClause,
-                                                        Tuple<Individual> violationTuple) {
+                                                        Tuple<Individual> violationTuple,
+                                                        boolean useClauseUniqueIndividual) {
 
         String[] commonVars = MultiStageUpperProgram.getCommonVars(clause);
 
@@ -100,7 +92,6 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
             AtomicConcept atomicConcept;
 
             if(concept instanceof AtomicNegationConcept) {
-                // TODO CHECK: is this already in MultiStageUpperProgram?
                 Atom atom1 =
                         Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
                 Atom atom2 = Atom.create(atomicConcept = OverApproxExist.getNegationConcept(atomicConcept), X);
@@ -116,9 +107,14 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
             Individual[] individuals = new Individual[card];
             SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
             for(int i = 0; i < card; ++i)
-                individuals[i] = termsManager.getFreshIndividual(originalClause,
-                                                                 offset + i,
-                                                                 commonIndividuals);
+                if(useClauseUniqueIndividual)
+                    individuals[i] = termsManager.getFreshIndividual(originalClause,
+                                                                     offset + i,
+                                                                     maxTermDepth + 1);
+                else
+                    individuals[i] = termsManager.getFreshIndividual(originalClause,
+                                                                     offset + i,
+                                                                     commonIndividuals);
 
             for(int i = 0; i < card; ++i) {
                 if(atomicConcept != null)
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 a78aabe..ed93d0e 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsManager.java
@@ -13,6 +13,7 @@ import java.util.Map;
 public class SkolemTermsManager {
 
     public static final String SKOLEMISED_INDIVIDUAL_PREFIX = Namespace.PAGODA_ANONY + "individual";
+    public static final String RULE_UNIQUE_SKOLEMISED_INDIVIDUAL_PREFIX = SKOLEMISED_INDIVIDUAL_PREFIX + "_unique";
 
     private static SkolemTermsManager skolemTermsManager;
 
@@ -54,10 +55,29 @@ public class SkolemTermsManager {
                 + "_" + mapDependencyToId(dependency);
         Individual newIndividual = Individual.create(SKOLEMISED_INDIVIDUAL_PREFIX + termId);
 
-        int depth = 0;
-        for(Individual individual : dependency)
-            depth = Integer.max(depth, getDepthOf(individual));
-        individualToDepth_map.put(newIndividual, depth + 1);
+        if(!individualToDepth_map.containsKey(newIndividual)) {
+            int depth = 0;
+            for (Individual individual : dependency)
+                depth = Integer.max(depth, getDepthOf(individual));
+            individualToDepth_map.put(newIndividual, depth + 1);
+        }
+
+        return newIndividual;
+    }
+
+    /***
+     * Create a term of a given depth, unique for the clause and the depth.
+     *
+     * @param originalClause
+     * @param offset
+     * @param depth
+     * @return
+     */
+    public Individual getFreshIndividual(DLClause originalClause, int offset, int depth) {
+        String termId = Integer.toString(mapClauseToId(originalClause) + offset) + "_depth_" + depth;
+        Individual newIndividual = Individual.create(RULE_UNIQUE_SKOLEMISED_INDIVIDUAL_PREFIX + termId);
+
+        individualToDepth_map.putIfAbsent(newIndividual, depth);
 
         return newIndividual;
     }