2 files changed, 97 insertions, 21 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 e53ae49..4444c00 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java
@@ -1,26 +1,29 @@
 package uk.ac.ox.cs.pagoda.rules.approximators;
 
-import org.semanticweb.HermiT.model.DLClause;
-import org.semanticweb.HermiT.model.Individual;
+import org.semanticweb.HermiT.model.*;
 import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
+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;
 
 import java.util.*;
 
 /**
- * Approximates existential rules by a limited form of Skolemisation.
+ * Approximates existential rules through 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,
+ * Given a rule and a ground 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 static final Atom[] EMPTY_BODY = new Atom[0];
+
     private final int maxTermDepth;
     private final TupleDependentApproximator alternativeApproximator;
+    private final SkolemTermsManager skolemTermsManager;
 
     private Map<AnswerTupleID, Integer> mapIndividualsToDepth;
 
@@ -32,19 +35,21 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
         this.maxTermDepth = maxTermDepth;
         this.alternativeApproximator = alternativeApproximator;
         this.mapIndividualsToDepth = new HashMap<>();
+        this.skolemTermsManager = SkolemTermsManager.getInstance();
     }
 
     @Override
-    public Collection<DLClause> convert(DLClause clause, DLClause originalClause, Collection<Tuple<Individual>> violationTuples) {
+    public Collection<DLClause> convert(DLClause clause,
+                                        DLClause originalClause,
+                                        Collection<Tuple<Individual>> 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;
+                throw new IllegalArgumentException(
+                        "Expected clause with head length < 1, but it is " + clause.getHeadLength());
         }
 
 
@@ -54,23 +59,94 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima
         ArrayList<DLClause> result = new ArrayList<>();
 
         for (Tuple<Individual> violationTuple : violationTuples)
-            if (getDepth(violationTuple) > maxTermDepth)
+            if (getMaxDepth(violationTuple) > maxTermDepth)
                 result.addAll(alternativeApproximator.convert(clause, originalClause, null));
             else
-                result.add(getGroundSkolemisation(clause, originalClause, violationTuple));
+                result.addAll(getGroundSkolemisation(clause, originalClause, violationTuple));
 
         return result;
     }
 
+    private static final Variable X = Variable.create("X");
+
+    private Collection<DLClause> getGroundSkolemisation(DLClause clause,
+                                                        DLClause originalClause,
+                                                        Tuple<Individual> violationTuple) {
+
+        String[] commonVars = MultiStageUpperProgram.getCommonVars(clause);
+
+        // TODO check: strong assumption, the first tuples are the common ones
+        TupleBuilder<Individual> commonIndividualsBuilder = new TupleBuilder<>();
+        for (int i = 0; i < commonVars.length; i++)
+            commonIndividualsBuilder.add(violationTuple.get(i));
+
+        Atom headAtom = clause.getHeadAtom(0);
+        Atom[] bodyAtoms = clause.getBodyAtoms();
+        int offset = OverApproxExist.indexOfExistential(headAtom, originalClause);
+
+        // BEGIN: copy and paste
+        ArrayList<DLClause> ret = new ArrayList<>();
+        DLPredicate predicate = headAtom.getDLPredicate();
+        if (predicate instanceof AtLeastConcept) {
+            AtLeastConcept atLeastConcept = (AtLeastConcept) predicate;
+            LiteralConcept concept = atLeastConcept.getToConcept();
+            Role role = atLeastConcept.getOnRole();
+            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);
+                ret.add(DLClause.create(new Atom[0], new Atom[] {atom1, atom2}));
+            }
+            else {
+                atomicConcept = (AtomicConcept) concept;
+                if (atomicConcept.equals(AtomicConcept.THING))
+                    atomicConcept = null;
+            }
+
+            int card = atLeastConcept.getNumber();
+            Individual[] individuals = new Individual[card];
+            SkolemTermsManager termsManager = SkolemTermsManager.getInstance();
+            for (int i = 0; i < card; ++i)
+                individuals[i] = termsManager.getFreshIndividual(originalClause,
+                                                                 offset + i,
+                                                                 commonIndividualsBuilder.create());
+
+            for (int i = 0; i < card; ++i) {
+                if (atomicConcept != null)
+                    ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, EMPTY_BODY));
+
+                Atom atom = role instanceof AtomicRole ?
+                        Atom.create((AtomicRole) role, X, individuals[i]) :
+                        Atom.create(((InverseRole) role).getInverseOf(), individuals[i], X);
+
+                ret.add(DLClause.create(new Atom[] {atom}, EMPTY_BODY));
+            }
+
+            for (int i = 0; i < card; ++i)
+                for (int j = i + 1; j < card; ++j)
+                    // TODO to be checked ... different as
+                    ret.add(DLClause.create(new Atom[] {Atom.create(Inequality.INSTANCE, individuals[i], individuals[j])}, EMPTY_BODY));
+
+        }
+        else if (predicate instanceof AtLeastDataRange) {
+            // TODO to be implemented ...
+        }
+        else
+            ret.add(DLClause.create(new Atom[] {headAtom}, EMPTY_BODY));
 
-    private DLClause getGroundSkolemisation(DLClause clause, DLClause originalClause, Tuple<Individual> violationTuple) {
-        // TODO implement
-        // filter the violation tuples appearing on both the sides of the rule
-        return null;
+        return ret;
+
+        // END: copy and paste
     }
 
-    private int getDepth(Tuple<Individual> violationTuple) {
-        if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0;
-        return mapIndividualsToDepth.get(violationTuple);
+
+    public int getMaxDepth(Tuple<Individual> violationTuple) {
+        int maxDepth = 0;
+        for (Individual individual : violationTuple)
+            maxDepth = Integer.max(maxDepth, skolemTermsManager.getDepth(individual));
+
+        return maxDepth;
     }
 }
diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
index d71c472..028568c 100644
--- a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
+++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java
@@ -12,7 +12,7 @@ public class OverApproxExist implements Approximator {
         public static final String negativeSuffix = "_neg";
         private static final Variable X = Variable.create("X");
 
-        private static int indexOfExistential(Atom headAtom, DLClause originalClause) {
+        static int indexOfExistential(Atom headAtom, DLClause originalClause) {
                 if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1;
                 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
                 if (alc.getToConcept() instanceof AtomicConcept) {