From 7e0ecc07285209e65f9d4d022065d06a4997fc86 Mon Sep 17 00:00:00 2001 From: RncLsn Date: Wed, 13 May 2015 11:57:06 +0100 Subject: Implementing Limited Skolemisation, in particular SkolemTermsDispenser. --- .../pagoda/rules/approximators/Approximator.java | 42 ++++ .../LimitedSkolemisationApproximator.java | 74 ++++++ .../pagoda/rules/approximators/OverApproxBoth.java | 24 ++ .../pagoda/rules/approximators/OverApproxDisj.java | 100 ++++++++ .../rules/approximators/OverApproxExist.java | 265 +++++++++++++++++++++ .../rules/approximators/SkolemTermsDispenser.java | 74 ++++++ .../approximators/TupleDependentApproximator.java | 16 ++ 7 files changed, 595 insertions(+) create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java create mode 100644 src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java (limited to 'src/uk/ac/ox/cs/pagoda/rules/approximators') diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java new file mode 100644 index 0000000..f910c64 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java @@ -0,0 +1,42 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +import org.semanticweb.HermiT.model.DLClause; + +import java.util.Collection; + +public interface Approximator { + + Collection convert(DLClause clause, DLClause originalClause); + +} + +// TODO remove +//class IgnoreExist implements Approximator { +// +// @Override +// public Collection convert(DLClause clause, DLClause originalClause) { +// Collection ret = new LinkedList(); +// DLPredicate p; +// for (Atom headAtom: clause.getHeadAtoms()) { +// p = headAtom.getDLPredicate(); +// if (p instanceof AtLeast) return ret; +// } +// +// ret.add(clause); +// return ret; +// } +// +//} +// +// +// +//class IgnoreDisj implements Approximator { +// +// @Override +// public Collection convert(DLClause clause, DLClause originalClause) { +// Collection ret = new LinkedList(); +// if (clause.getHeadLength() > 1) return ret; +// ret.add(clause); +// return ret; +// } +//} diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java new file mode 100644 index 0000000..8fc6b77 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java @@ -0,0 +1,74 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +import org.semanticweb.HermiT.model.DLClause; +import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; +import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; + +import java.util.*; + +/** + * Approximates existential rules by 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, + * otherwise it approximates using an alternative TupleDependentApproximator. + * + * */ +public class LimitedSkolemisationApproximator implements TupleDependentApproximator { + + private final int maxTermDepth; + private final TupleDependentApproximator alternativeApproximator; + + private Map 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 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; + } + + + } + + private Collection overApprox(DLClause clause, DLClause originalClause, Collection violationTuples) { + ArrayList 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 + // filter the violation tuples appearing on both the sides of the rule + 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/approximators/OverApproxBoth.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java new file mode 100644 index 0000000..ae2a2cf --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java @@ -0,0 +1,24 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +import org.semanticweb.HermiT.model.AtLeastDataRange; +import org.semanticweb.HermiT.model.DLClause; + +import java.util.Collection; +import java.util.LinkedList; + +public class OverApproxBoth implements Approximator { + + Approximator approxDist = new OverApproxDisj(), approxExist = new OverApproxExist(); + + @Override + public Collection convert(DLClause clause, DLClause originalClause) { + Collection ret = new LinkedList(); + for (DLClause tClause: approxDist.convert(clause, originalClause)) { + if (tClause.getHeadLength() > 0 && tClause.getHeadAtom(0).getDLPredicate() instanceof AtLeastDataRange) + continue; + ret.addAll(approxExist.convert(tClause, originalClause)); + } + return ret; + } + +} diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java new file mode 100644 index 0000000..05d9442 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java @@ -0,0 +1,100 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +import org.semanticweb.HermiT.model.*; +import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; + +import java.util.*; + +public class OverApproxDisj implements Approximator { + + /** + * Splits a disjunctive rule into a bunch of rules. + *

+ * It returns a collection containing a rule for each atom in the head of the input rule. + * Each rule has the same body of the input rule, + * and the relative head atom as head. + * */ + @Override + public Collection convert(DLClause clause, DLClause originalClause) { + LinkedList distincts = new LinkedList(); + Atom[] headAtoms = clause.getHeadAtoms(), bodyAtoms = clause.getBodyAtoms(); + LinkedList newClauses = new LinkedList(); + DLClause newClause; + if (headAtoms.length > 1) { + for (Atom headAtom: headAtoms) { + newClause = DLClause.create(new Atom[] {headAtom}, bodyAtoms); + newClauses.add(newClause); +// distincts.add(newClause); + } + + for (DLClause cls: newClauses) { + newClause = DLClauseHelper.simplified(cls); + if (!isSubsumedBy(newClause, distincts)) + distincts.add(newClause); + } + } + else distincts.add(clause); + + return distincts; + } + + public static boolean isSubsumedBy(DLClause newClause, Collection distinctClauses) { + Map unifier; + Set bodyAtoms = new HashSet(); + for (DLClause clause: distinctClauses) { + if (newClause.getHeadLength() > 0 && clause.getHeadLength() > 0 && + (unifier = isSubsumedBy(newClause.getHeadAtom(0), clause.getHeadAtom(0))) == null) + continue; + else + unifier = new HashMap(); + + for (Atom atom: clause.getBodyAtoms()) + bodyAtoms.add(rename(atom, unifier)); + unifier.clear(); + + for (Atom atom: newClause.getBodyAtoms()) + if (!bodyAtoms.contains(atom)) + continue; + + return true; + } + + return false; + } + + public static Map isSubsumedBy(Atom atom1, Atom atom2) { + DLPredicate predicate = atom1.getDLPredicate(); + if (!predicate.equals(atom2.getDLPredicate())) + return null; + + Map unifier = new HashMap(); + Term term1, term2; + for (int index = 0; index < predicate.getArity(); ++index) { + term1 = rename(atom1.getArgument(index), unifier); + term2 = rename(atom2.getArgument(index), unifier); + + if (term1.equals(term2)); + else if (term1 instanceof Variable) + unifier.put((Variable) term1, term2); + else + return null; + } + return unifier; + } + + public static Atom rename(Atom atom, Map unifier) { + Term[] arguments = new Term[atom.getArity()]; + for (int i = 0; i < atom.getArity(); ++i) + arguments[i] = rename(atom.getArgument(i), unifier); + return Atom.create(atom.getDLPredicate(), arguments); + } + + public static Term rename(Term argument, Map unifier) { + Term newArg; + while ((newArg = unifier.get(argument)) != null) + return newArg; + return argument; + } + + +} diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java new file mode 100644 index 0000000..e0bafe0 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java @@ -0,0 +1,265 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +import org.semanticweb.HermiT.model.*; +import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; +import uk.ac.ox.cs.pagoda.util.Namespace; + +import java.util.*; + +public class OverApproxExist implements Approximator { + + public static final String negativeSuffix = "_neg"; + public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; + private static final Variable X = Variable.create("X"); + //DEBUG + public static Collection createdIndividualIRIs = new HashSet<>(); + private static int individualCounter = 0; + private static Map individualNumber = new HashMap(); + + private static int noOfExistential(DLClause originalClause) { + int no = 0; + for (Atom atom: originalClause.getHeadAtoms()) + if (atom.getDLPredicate() instanceof AtLeast) + no += ((AtLeast) atom.getDLPredicate()).getNumber(); + return no; + } + + private static int indexOfExistential(Atom headAtom, DLClause originalClause) { + if (!(headAtom.getDLPredicate() instanceof AtLeast)) return -1; + AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); + if (alc.getToConcept() instanceof AtomicConcept) { + 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)); + } + } + + int index = 0; + for (Atom atom: originalClause.getHeadAtoms()) { + if (atom.equals(headAtom)) + return index; + if (atom.getDLPredicate() instanceof AtLeast) + index += ((AtLeast) atom.getDLPredicate()).getNumber(); + } + return -1; + } + + public static AtomicConcept getNegationConcept(DLPredicate p) { + if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING; + if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING; + + if (p instanceof AtomicConcept) { + String iri = ((AtomicConcept) p).getIRI(); + if (iri.endsWith(negativeSuffix)) + iri = iri.substring(0, iri.length() - 4); + else + iri += negativeSuffix; + + return AtomicConcept.create(iri); + } + if (p instanceof AtLeastConcept) { + // FIXME !!! here + return null; + } + return null; + } + + public static int getNumberOfSkolemisedIndividual() { + return individualCounter; + } + //DEBUG + + public static Individual getNewIndividual(DLClause originalClause, int offset) { + Individual ret; + int individualID; + if (individualNumber.containsKey(originalClause)) { + individualID = individualNumber.get(originalClause) + offset; + ret = Individual.create(skolemisedIndividualPrefix + individualID); + } + else { + individualNumber.put(originalClause, individualCounter); + individualID = individualCounter + offset; + ret = Individual.create(skolemisedIndividualPrefix + individualID); + individualCounter += noOfExistential(originalClause); + } + return ret; + } + + public static int indexOfSkolemisedIndividual(Atom atom) { + 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; + } + + @Override + public Collection convert(DLClause clause, DLClause originalClause) { + Collection ret; + switch (clause.getHeadLength()) { + case 1: + return overApprox(clause.getHeadAtom(0), clause.getBodyAtoms(), originalClause); + case 0: + ret = new LinkedList(); + ret.add(clause); + return ret; + default: + ret = new LinkedList(); + for (Iterator iter = new DisjunctiveHeads(clause, originalClause); iter.hasNext(); ) + ret.add(iter.next()); + return ret; + } + } + + public Collection overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause) { + return overApprox(headAtom, bodyAtoms, originalClause, indexOfExistential(headAtom, originalClause)); + } + + public Collection overApprox(Atom headAtom, Atom[] bodyAtoms, DLClause originalClause, int offset) { + Collection ret = new LinkedList(); + DLPredicate predicate = headAtom.getDLPredicate(); + if (predicate instanceof AtLeastConcept) { + AtLeastConcept atLeastConcept = (AtLeastConcept) predicate; + LiteralConcept concept = atLeastConcept.getToConcept(); + Role role = atLeastConcept.getOnRole(); + AtomicConcept atomicConcept = null; + + 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 = 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]; + for (int i = 0; i < card; ++i) individuals[i] = getNewIndividual(originalClause, offset + i); + + for (int i = 0; i < card; ++i) { + if (atomicConcept != null) + ret.add(DLClause.create(new Atom[] {Atom.create(atomicConcept, individuals[i])}, bodyAtoms)); + + 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}, bodyAtoms)); + } + + 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])}, bodyAtoms)); + //DLClauseHelper.contructor_differentAs(individuals[i], individuals[j])); + + } + else if (predicate instanceof AtLeastDataRange) { + // TODO to be implemented ... + } + else + ret.add(DLClause.create(new Atom[] {headAtom}, bodyAtoms)); + + return ret; + } + + class DisjunctiveHeads implements Iterator { + + Atom[] bodyAtoms; + Atom[][] disjunctHeadAtoms; + int[] pointer; + int length, l; + LinkedList auxiliaryClauses = new LinkedList(); + + public DisjunctiveHeads(DLClause clause, DLClause originalClause) { + length = clause.getHeadLength(); + + bodyAtoms = clause.getBodyAtoms(); + disjunctHeadAtoms = new Atom[length][]; + pointer = new int[length]; + if (length > 0) l = length - 1; + else length = 0; + + int index = 0, offset = 0; + Collection datalogRules; + DLClause newClause; + for (Atom headAtom: clause.getHeadAtoms()) { + pointer[index] = 0; + + datalogRules = overApprox(headAtom, bodyAtoms, originalClause, offset); + + if (datalogRules.isEmpty()) { + l = -1; + auxiliaryClauses.clear(); + return ; + } + + for (Iterator iter = datalogRules.iterator(); iter.hasNext(); ) { + newClause = iter.next(); + if (!DLClauseHelper.hasSubsetBodyAtoms(newClause, clause)) { + auxiliaryClauses.add(newClause); + iter.remove(); + } + } + + disjunctHeadAtoms[index] = new Atom[datalogRules.size()]; + + int j = 0; + for (DLClause disjunct: datalogRules) { + disjunctHeadAtoms[index][j++] = disjunct.getHeadAtom(0); + } + + ++index; + if (headAtom.getDLPredicate() instanceof AtLeast) + offset += ((AtLeast) headAtom.getDLPredicate()).getNumber(); + + } + + } + + @Override + public boolean hasNext() { + return l != -1 || !auxiliaryClauses.isEmpty(); + } + + @Override + public DLClause next() { + if (l == -1) + return auxiliaryClauses.removeFirst(); + + if (length > 0) { + Atom[] headAtoms = new Atom[length]; + for (int i = 0; i < length; ++i) + headAtoms[i] = disjunctHeadAtoms[i][pointer[i]]; + + ++pointer[l]; + while (l >= 0 && pointer[l] >= disjunctHeadAtoms[l].length) { + pointer[l] = 0; + --l; + if (l >= 0) + ++pointer[l]; + } + + if (l >= 0) l = length - 1; + + return DLClauseHelper.simplified(DLClause.create(headAtoms, bodyAtoms)); +// return DLClause.create(headAtoms, bodyAtoms); + } + else { + --l; + return DLClauseHelper.simplified(DLClause.create(new Atom[0], bodyAtoms)); +// return DLClause.create(new Atom[0], bodyAtoms); + } + } + + @Override + public void remove() { } + + } +} diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java new file mode 100644 index 0000000..a920ec5 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java @@ -0,0 +1,74 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +import org.semanticweb.HermiT.model.AtLeast; +import org.semanticweb.HermiT.model.Atom; +import org.semanticweb.HermiT.model.DLClause; +import org.semanticweb.HermiT.model.Individual; +import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; +import uk.ac.ox.cs.pagoda.util.Namespace; + +import java.util.HashMap; +import java.util.Map; + +/** + * If you need a Skolem term (i.e. fresh individual), ask this class. + */ +public class SkolemTermsDispenser { + + public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; + private static SkolemTermsDispenser skolemTermsDispenser; + private int individualCounter = 0; + private Map termNumber = new HashMap<>(); + private Map mapTermToDepth = new HashMap<>(); + private int dependenciesCounter = 0; + private Map mapDependencyToId = new HashMap<>(); + + private SkolemTermsDispenser() { + } + + public static SkolemTermsDispenser getInstance() { + if (skolemTermsDispenser == null) skolemTermsDispenser = new SkolemTermsDispenser(); + return skolemTermsDispenser; + } + + private int getDependencyId(AnswerTupleID answerTupleID) { + if (mapDependencyToId.containsKey(answerTupleID)) return mapDependencyToId.get(answerTupleID); + else return mapDependencyToId.put(answerTupleID, dependenciesCounter++); + } + + public Individual getNewIndividual(DLClause originalClause, int offset, AnswerTupleID dependency) { + if (!termNumber.containsKey(originalClause)) { + termNumber.put(originalClause, individualCounter); + individualCounter += noOfExistential(originalClause); + } + if (!mapDependencyToId.containsKey(dependency)) { + mapDependencyToId.put(dependency, dependenciesCounter++); + } + + SkolemTermId termId = new SkolemTermId(termNumber.get(originalClause) + offset, getDependencyId(dependency)); + return Individual.create(skolemisedIndividualPrefix + termId); + } + + private int noOfExistential(DLClause originalClause) { + int no = 0; + for (Atom atom : originalClause.getHeadAtoms()) + if (atom.getDLPredicate() instanceof AtLeast) + no += ((AtLeast) atom.getDLPredicate()).getNumber(); + return no; + } + + private class SkolemTermId { + private final int idBase; + private final int idOffset; + + private SkolemTermId(int idBase, int idOffset) { + this.idBase = idBase; + this.idOffset = idOffset; + } + + @Override + public String toString() { + return idBase + "_" + idOffset; + } + } +} diff --git a/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java new file mode 100644 index 0000000..1a729e5 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java @@ -0,0 +1,16 @@ +package uk.ac.ox.cs.pagoda.rules.approximators; + +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 convert(DLClause clause, + DLClause originalClause, + Collection violationTuples); +} -- cgit v1.2.3