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. --- src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java | 31 +-- src/uk/ac/ox/cs/pagoda/rules/Approximator.java | 62 ----- .../ac/ox/cs/pagoda/rules/DisjunctiveProgram.java | 4 +- .../cs/pagoda/rules/ExistConstantApproximator.java | 2 + .../ac/ox/cs/pagoda/rules/ExistentialProgram.java | 4 +- .../cs/pagoda/rules/ExistentialToDisjunctive.java | 16 +- .../rules/LimitedSkolemisationApproximator.java | 72 ------ .../ac/ox/cs/pagoda/rules/LowerDatalogProgram.java | 31 ++- src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java | 24 -- src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java | 100 -------- src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java | 259 -------------------- .../pagoda/rules/TupleDependentApproximator.java | 16 -- .../ac/ox/cs/pagoda/rules/UpperDatalogProgram.java | 9 +- .../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 ++ 20 files changed, 652 insertions(+), 573 deletions(-) delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/Approximator.java delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java delete mode 100644 src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java 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') diff --git a/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java b/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java index 3b9d6fc..acbf354 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java +++ b/src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java @@ -1,27 +1,22 @@ package uk.ac.ox.cs.pagoda.rules; -import java.util.Collection; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.Map; - import org.semanticweb.HermiT.model.DLClause; import org.semanticweb.owlapi.model.OWLAxiom; import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom; import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom; - import uk.ac.ox.cs.pagoda.owl.OWLHelper; +import uk.ac.ox.cs.pagoda.rules.approximators.Approximator; + +import java.util.*; public abstract class ApproxProgram extends Program { - + + protected Approximator m_approx = null; /** * mapping from over-approximated DLClauses to DLClauses from the original ontology */ Map correspondence = new HashMap(); - protected Approximator m_approx = null; - protected ApproxProgram() { initApproximator(); } protected abstract void initApproximator(); @@ -76,7 +71,7 @@ public abstract class ApproxProgram extends Program { public OWLAxiom getEquivalentAxiom(DLClause clause) { Object obj = correspondence.get(clause); - while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey((DLClause) obj)) + while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey(obj)) obj = correspondence.get(clause); if (obj instanceof OWLAxiom) return (OWLAxiom) obj; @@ -98,14 +93,14 @@ public abstract class ApproxProgram extends Program { class ClauseSet extends HashSet { - public ClauseSet(DLClause first, DLClause second) { - add(first); - add(second); - } - /** - * + * */ private static final long serialVersionUID = 1L; - + + public ClauseSet(DLClause first, DLClause second) { + add(first); + add(second); + } + } \ No newline at end of file diff --git a/src/uk/ac/ox/cs/pagoda/rules/Approximator.java b/src/uk/ac/ox/cs/pagoda/rules/Approximator.java deleted file mode 100644 index 66e676b..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/Approximator.java +++ /dev/null @@ -1,62 +0,0 @@ -package uk.ac.ox.cs.pagoda.rules; - -import org.semanticweb.HermiT.model.AtLeast; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; - -import java.util.Collection; -import java.util.LinkedList; - -public interface Approximator { - - Collection convert(DLClause clause, DLClause originalClause); - -} - -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 IgnoreBoth implements Approximator { - - @Override - public Collection convert(DLClause clause, DLClause originalClause) { - Collection ret = new LinkedList(); - - if (clause.getHeadLength() > 1) return ret; - - if (clause.getHeadLength() > 0) { - DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate(); - - if (predicate 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/DisjunctiveProgram.java b/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java index 6ebe666..d50c2d4 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java +++ b/src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java @@ -1,10 +1,12 @@ package uk.ac.ox.cs.pagoda.rules; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; + public class DisjunctiveProgram extends UpperProgram { @Override protected void initApproximator() { - m_approx = new OverApproxExist(); + m_approx = new OverApproxExist(); } // @Override diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java index 74c531f..7c9562f 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java @@ -2,6 +2,8 @@ package uk.ac.ox.cs.pagoda.rules; import org.semanticweb.HermiT.model.DLClause; import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator; import java.util.Collection; diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java b/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java index 64d018f..e825917 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java +++ b/src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java @@ -1,5 +1,7 @@ package uk.ac.ox.cs.pagoda.rules; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxDisj; + public class ExistentialProgram extends UpperProgram { // @Override @@ -12,7 +14,7 @@ public class ExistentialProgram extends UpperProgram { @Override protected void initApproximator() { - m_approx = new OverApproxDisj(); + m_approx = new OverApproxDisj(); } } diff --git a/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java b/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java index ebe0b7d..2098f73 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java +++ b/src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java @@ -1,19 +1,17 @@ package uk.ac.ox.cs.pagoda.rules; +import org.semanticweb.HermiT.model.*; +import org.semanticweb.owlapi.model.OWLObjectProperty; +import org.semanticweb.owlapi.model.OWLOntology; +import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; +import uk.ac.ox.cs.pagoda.rules.approximators.Approximator; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; + import java.util.Collection; import java.util.HashSet; import java.util.LinkedList; import java.util.Set; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.owlapi.model.OWLObjectProperty; -import org.semanticweb.owlapi.model.OWLOntology; -import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; - public class ExistentialToDisjunctive extends UpperProgram { Set inverseFuncProperties = new HashSet(); diff --git a/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java deleted file mode 100644 index 284edd2..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java +++ /dev/null @@ -1,72 +0,0 @@ -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. - *

- * 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 - 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/LowerDatalogProgram.java b/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java index a664ba1..199d167 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java +++ b/src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java @@ -10,6 +10,7 @@ import uk.ac.ox.cs.pagoda.constraints.UnaryBottom; import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom; import uk.ac.ox.cs.pagoda.multistage.Normalisation; import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication; +import uk.ac.ox.cs.pagoda.rules.approximators.Approximator; import uk.ac.ox.cs.pagoda.util.Timer; import uk.ac.ox.cs.pagoda.util.Utility; @@ -106,7 +107,26 @@ public class LowerDatalogProgram extends ApproxProgram implements IncrementalPro @Override protected void initApproximator() { - m_approx = new IgnoreBoth(); + m_approx = new IgnoreBoth(); + } + + private class IgnoreBoth implements Approximator { + + @Override + public Collection convert(DLClause clause, DLClause originalClause) { + Collection ret = new LinkedList(); + + if (clause.getHeadLength() > 1) return ret; + + if (clause.getHeadLength() > 0) { + DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate(); + + if (predicate instanceof AtLeast) return ret; + } + + ret.add(clause); + return ret; + } } } @@ -116,15 +136,13 @@ class ClassifyThread extends Thread { IncrementalProgram m_program; Collection clauses = new LinkedList(); - Variable X = Variable.create("X"), Y = Variable.create("Y"); - + Variable X = Variable.create("X"), Y = Variable.create("Y"); + Reasoner hermitReasoner; + OWLOntology ontology; ClassifyThread(IncrementalProgram program) { m_program = program; } - Reasoner hermitReasoner; - OWLOntology ontology; - @Override public void run() { ontology = m_program.getOntology(); @@ -215,5 +233,4 @@ class ClassifyThread extends Thread { private Atom getAtom(OWLClass c) { return Atom.create(AtomicConcept.create(c.toStringID()), X); } - } \ No newline at end of file diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java deleted file mode 100644 index 3cc2aba..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java +++ /dev/null @@ -1,24 +0,0 @@ -package uk.ac.ox.cs.pagoda.rules; - -import java.util.Collection; -import java.util.LinkedList; - -import org.semanticweb.HermiT.model.AtLeastDataRange; -import org.semanticweb.HermiT.model.DLClause; - -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/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java deleted file mode 100644 index 5b298e8..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java +++ /dev/null @@ -1,100 +0,0 @@ -package uk.ac.ox.cs.pagoda.rules; - -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/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java deleted file mode 100644 index 1099acf..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java +++ /dev/null @@ -1,259 +0,0 @@ -package uk.ac.ox.cs.pagoda.rules; - -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"); - 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; - } - - public static Individual getNewIndividual(DLClause originalClause, int offset) { - Individual ret; - if (individualNumber.containsKey(originalClause)) { - ret = Individual.create(skolemisedIndividualPrefix + (individualNumber.get(originalClause) + offset)); - } - else { - individualNumber.put(originalClause, individualCounter); - ret = Individual.create(skolemisedIndividualPrefix + (individualCounter + offset)); - 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/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java deleted file mode 100644 index 63057c4..0000000 --- a/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java +++ /dev/null @@ -1,16 +0,0 @@ -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 convert(DLClause clause, - DLClause originalClause, - Collection violationTuples); -} diff --git a/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java b/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java index a4cd790..611e183 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java +++ b/src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java @@ -1,12 +1,13 @@ package uk.ac.ox.cs.pagoda.rules; +import org.semanticweb.HermiT.model.DLClause; +import org.semanticweb.HermiT.model.DLPredicate; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxBoth; + import java.util.Collection; import java.util.HashMap; import java.util.Map; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; - public class UpperDatalogProgram extends UpperProgram { @@ -22,7 +23,7 @@ public class UpperDatalogProgram extends UpperProgram { @Override protected void initApproximator() { - m_approx = new OverApproxBoth(); + m_approx = new OverApproxBoth(); } public int getBottomNumber() { 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