Added classes for implementing new upper store (Limited Skolemisation).

Started implementation of the new classes.

1 files changed, 72 insertions, 0 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java
new file mode 100644
index 0000000..284edd2
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java
@@ -0,0 +1,72 @@
+package uk.ac.ox.cs.pagoda.rules;
+
+import org.semanticweb.HermiT.model.DLClause;
+import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+
+import java.util.*;
+
+/**
+ * Approximates existential rules by a limited form of Skolemisation.
+ * <p>
+ * Given a rule and a grounding substitution,
+ * 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 final int maxTermDepth;
+    private final TupleDependentApproximator alternativeApproximator;
+
+    private Map<AnswerTupleID, Integer> mapIndividualsToDepth;
+
+    public LimitedSkolemisationApproximator(int maxTermDepth) {
+        this(maxTermDepth, new ExistConstantApproximator());
+    }
+
+    public LimitedSkolemisationApproximator(int maxTermDepth, TupleDependentApproximator alternativeApproximator) {
+        this.maxTermDepth = maxTermDepth;
+        this.alternativeApproximator = alternativeApproximator;
+        this.mapIndividualsToDepth = new HashMap<>();
+    }
+
+    @Override
+    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+        switch (clause.getHeadLength()) {
+            case 1:
+                return overApprox(clause, originalClause, violationTuples);
+            case 0:
+                return Arrays.asList(clause);
+            default:
+                ArrayList<DLClause> result = new ArrayList<>();
+                // TODO implement
+                return result;
+        }
+
+
+    }
+
+    private Collection<DLClause> overApprox(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+        ArrayList<DLClause> result = new ArrayList<>();
+
+        for (AnswerTupleID violationTuple : violationTuples)
+            if (getDepth(violationTuple) > maxTermDepth)
+                result.addAll(alternativeApproximator.convert(clause, originalClause, null));
+            else
+                result.add(getInstantiatedSkolemisation(clause, originalClause, violationTuple));
+
+        return result;
+    }
+
+
+    private DLClause getInstantiatedSkolemisation(DLClause clause, DLClause originalClause, AnswerTupleID violationTuple) {
+        // TODO implement
+        return null;
+    }
+
+    private int getDepth(AnswerTupleID violationTuple) {
+        if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0;
+        return mapIndividualsToDepth.get(violationTuple);
+    }
+}