aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java
blob: 284edd2993e0e76d41213a33bbfd210fa03fdea8 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
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);
    }
}