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

8 files changed, 43 insertions, 27 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;
     }
diff --git a/test/resources/BugTests.xml b/test/resources/BugTests.xml
index 1413b5b..4844fbe 100644
--- a/test/resources/BugTests.xml
+++ b/test/resources/BugTests.xml
@@ -6,7 +6,7 @@
     <test name="BugTest">
         <classes>
             <class name="uk.ac.ox.cs.pagoda.global_tests.BugTests"/>
-            <!--<class name="uk.ac.ox.cs.pagoda.endomorph.DependencyGraphTest"/>-->
+            <class name="uk.ac.ox.cs.pagoda.endomorph.DependencyGraphTest"/>
         </classes>
     </test>
 
diff --git a/test/resources/MainTests.xml b/test/resources/MainTests.xml
index 255b68e..43300a1 100644
--- a/test/resources/MainTests.xml
+++ b/test/resources/MainTests.xml
@@ -7,9 +7,9 @@
             <run>
                 <!--<include name="correctness"/>-->
                 <!--<include name="light"/>-->
-                <!--<include name="justExecute"/>-->
+                <include name="justExecute"/>
                 <!--&lt;!&ndash;<include name="heavy"/>&ndash;&gt;-->
-                <include name="nonOriginal"/>
+                <!--<include name="nonOriginal"/>-->
             </run>
         </groups>
         <classes>
diff --git a/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java b/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java
index eec1e8f..a4579a3 100644
--- a/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java
+++ b/test/uk/ac/ox/cs/pagoda/endomorph/DependencyGraphTest.java
@@ -2,6 +2,7 @@ package uk.ac.ox.cs.pagoda.endomorph;
 
 import org.semanticweb.owlapi.apibinding.OWLManager;
 import org.semanticweb.owlapi.model.*;
+import org.testng.Assert;
 import org.testng.annotations.Test;
 import uk.ac.ox.cs.JRDFox.model.GroundTerm;
 import uk.ac.ox.cs.JRDFox.model.Individual;
@@ -54,6 +55,6 @@ public class DependencyGraphTest {
 
         dependencyGraph.build(tuples);
 
-        System.out.println(dependencyGraph.getTopologicalOrder());
+        Assert.assertTrue(dependencyGraph.getTopologicalOrder().size() >= 2);
     }
 }
diff --git a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java
index a7a562d..42f0ac1 100644
--- a/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java
+++ b/test/uk/ac/ox/cs/pagoda/global_tests/TestPagodaFLY.java
@@ -62,7 +62,7 @@ public class TestPagodaFLY {
 //                        .answer(Paths.get("/home/alessandro/Desktop/answers.json"))
                 .classify(false)
                 .hermit(true)
-                .skolem(PagodaProperties.SkolemUpperBoundOptions.AFTER_SUMMARISATION)
+                .skolem(PagodaProperties.SkolemUpperBoundOptions.BEFORE_SUMMARISATION)
                 .build()
                 .run();
     }