From 6fd8b21066852cbc21e247e7cf0a2f423ebc1658 Mon Sep 17 00:00:00 2001 From: RncLsn Date: Wed, 13 May 2015 19:22:07 +0100 Subject: Fast implementation of all the other things to get something working, but it doesn't. --- .../LimitedSkolemisationApproximator.java | 116 +++++++++++++++++---- .../rules/approximators/OverApproxExist.java | 2 +- 2 files changed, 97 insertions(+), 21 deletions(-) (limited to 'src/uk/ac/ox/cs/pagoda/rules') 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. *

- * 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 TupleDependentApproximator. - * * */ 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 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 convert(DLClause clause, DLClause originalClause, Collection> violationTuples) { + public Collection convert(DLClause clause, + DLClause originalClause, + Collection> violationTuples) { switch (clause.getHeadLength()) { case 1: return overApprox(clause, originalClause, violationTuples); case 0: return Arrays.asList(clause); default: - ArrayList 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 result = new ArrayList<>(); for (Tuple 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 getGroundSkolemisation(DLClause clause, + DLClause originalClause, + Tuple violationTuple) { + + String[] commonVars = MultiStageUpperProgram.getCommonVars(clause); + + // TODO check: strong assumption, the first tuples are the common ones + TupleBuilder 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 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 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 violationTuple) { - if (!mapIndividualsToDepth.containsKey(violationTuple)) return 0; - return mapIndividualsToDepth.get(violationTuple); + + public int getMaxDepth(Tuple 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) { -- cgit v1.2.3