4 files changed, 162 insertions, 53 deletions

diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
new file mode 100644
index 0000000..74c531f
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java
@@ -0,0 +1,23 @@
+package uk.ac.ox.cs.pagoda.rules;
+
+import org.semanticweb.HermiT.model.DLClause;
+import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+
+import java.util.Collection;
+
+/**
+ * A wrapper for <tt>OverApproxExist</tt>.
+ * */
+public class ExistConstantApproximator implements TupleDependentApproximator {
+
+    private final OverApproxExist overApproxExist;
+
+    public ExistConstantApproximator() {
+        overApproxExist = new OverApproxExist();
+    }
+
+    @Override
+    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<AnswerTupleID> violationTuples) {
+        return overApproxExist.convert(clause, originalClause);
+    }
+}
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);
+    }
+}
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java
index 2ff1673..1099acf 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java
@@ -8,87 +8,67 @@ import java.util.*;
 
 public class OverApproxExist implements Approximator {
 
-        @Override
-        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
-                Collection<DLClause> ret;
-                switch (clause.getHeadLength()) {
-                case 1:
-                        return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause);
-                case 0:
-                        ret = new LinkedList<DLClause>();
-                        ret.add(clause); 
-                        return ret; 
-                default:
-                        ret = new LinkedList<DLClause>();
-                        for (Iterator<DLClause> iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); )
-                                ret.add(iter.next());
-                        return ret;
-                }
-        }
-
+        public static final String negativeSuffix = "_neg";
+        public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual";
+        private static final Variable X = Variable.create("X");
+        private static int individualCounter = 0;
+        private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>();
+        
         private static int noOfExistential(DLClause originalClause) {
-                int no = 0; 
+                int no = 0;
                 for (Atom atom: originalClause.getHeadAtoms())
                         if (atom.getDLPredicate() instanceof AtLeast)
-                                no += ((AtLeast) atom.getDLPredicate()).getNumber(); 
-                return no; 
+                                no += ((AtLeast) atom.getDLPredicate()).getNumber();
+                return no;
         }
 
         private static int indexOfExistential(Atom headAtom, DLClause originalClause) {
-                if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1; 
+                if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
                 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
                 if (alc.getToConcept() instanceof AtomicConcept) {
-                        AtomicConcept ac = (AtomicConcept) alc.getToConcept(); 
+                        AtomicConcept ac = (AtomicConcept) alc.getToConcept();
                         if (ac.getIRI().endsWith(negativeSuffix)) {
                                 alc = AtLeastConcept.create(alc.getNumber(), alc.getOnRole(), AtomicNegationConcept.create(getNegationConcept(ac)));
-                                headAtom = Atom.create(alc, headAtom.getArgument(0)); 
+                                headAtom = Atom.create(alc, headAtom.getArgument(0));
                         }
                 }
-                
-                int index = 0; 
+
+                int index = 0;
                 for (Atom atom: originalClause.getHeadAtoms()) {
-                        if (atom.equals(headAtom)) 
-                                return index; 
+                        if (atom.equals(headAtom))
+                                return index;
                         if (atom.getDLPredicate() instanceof AtLeast)
-                                index += ((AtLeast) atom.getDLPredicate()).getNumber(); 
+                                index += ((AtLeast) atom.getDLPredicate()).getNumber();
                 }
-                return -1; 
+                return -1;
         }
-
-        private static final Variable X = Variable.create("X"); 
-        public static final String negativeSuffix = "_neg"; 
         
         public static AtomicConcept getNegationConcept(DLPredicate p) {
                 if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING;
-                if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING; 
-                
+                if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING;
+
                 if (p instanceof AtomicConcept) {
                         String iri = ((AtomicConcept) p).getIRI();
-                        if (iri.endsWith(negativeSuffix)) 
+                        if (iri.endsWith(negativeSuffix))
                                 iri = iri.substring(0, iri.length() - 4);
-                        else 
-                                iri += negativeSuffix; 
+                        else
+                                iri += negativeSuffix;
 
                         return AtomicConcept.create(iri);
                 }
                 if (p instanceof AtLeastConcept) {
                         // FIXME !!! here
-                        return null; 
+                        return null;
                 }
-                return null; 
-        }       
-        
-        public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; 
-        
-        private static int individualCounter = 0;
-        private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>();
-        
+                return null;
+        }
+
         public static int getNumberOfSkolemisedIndividual() {
-                return individualCounter; 
+                return individualCounter;
         }
         
         public static Individual getNewIndividual(DLClause originalClause, int offset) {
-                Individual ret; 
+                Individual ret;
                 if (individualNumber.containsKey(originalClause)) {
                         ret = Individual.create(skolemisedIndividualPrefix + (individualNumber.get(originalClause) + offset));
                 }
@@ -97,16 +77,34 @@ public class OverApproxExist implements Approximator {
                         ret = Individual.create(skolemisedIndividualPrefix + (individualCounter + offset));
                         individualCounter += noOfExistential(originalClause);
                 }
-                return ret;  
+                return ret;
         }
         
         public static int indexOfSkolemisedIndividual(Atom atom) {
-                Term t; 
+                Term t;
                 for (int index = 0; index < atom.getArity(); ++index) {
                         t = atom.getArgument(index);
                         if (t instanceof Individual && ((Individual) t).getIRI().contains(skolemisedIndividualPrefix)) return index;
                 }
-                return -1; 
+                return -1;
+        }
+
+        @Override
+        public Collection<DLClause> convert(DLClause clause, DLClause originalClause) {
+                Collection<DLClause> ret;
+                switch (clause.getHeadLength()) {
+                        case 1:
+                                return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause);
+                        case 0:
+                                ret = new LinkedList<DLClause>();
+                                ret.add(clause);
+                                return ret;
+                        default:
+                                ret = new LinkedList<DLClause>();
+                                for (Iterator<DLClause> iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); )
+                                        ret.add(iter.next());
+                                return ret;
+                }
         }
         
         public Collection<DLClause> overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause) {
@@ -123,7 +121,7 @@ public class OverApproxExist implements Approximator {
                         AtomicConcept atomicConcept = null;
                         
                         if (concept instanceof AtomicNegationConcept) {
-                                // is this already in MultiStageUpperProgram?
+                                // TODO CHECK: is this already in MultiStageUpperProgram?
                                 Atom atom1 = Atom.create(atomicConcept = ((AtomicNegationConcept) concept).getNegatedAtomicConcept(), X);
                                 Atom atom2 = Atom.create(atomicConcept = getNegationConcept(atomicConcept), X);
                                 ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2})); 
diff --git a/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java
new file mode 100644
index 0000000..63057c4
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java
@@ -0,0 +1,16 @@
+package uk.ac.ox.cs.pagoda.rules;
+
+import org.semanticweb.HermiT.model.DLClause;
+import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+
+import java.util.Collection;
+
+/**
+ * It approximates rules according to a specific instantiation of the body.
+ */
+public interface TupleDependentApproximator {
+
+    Collection<DLClause> convert(DLClause clause,
+                                 DLClause originalClause,
+                                 Collection<AnswerTupleID> violationTuples);
+}