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. --- .../cs/pagoda/constraints/PredicateDependency.java | 138 ++++---- .../ox/cs/pagoda/multistage/FoldedApplication.java | 8 +- .../cs/pagoda/multistage/IndividualCollector.java | 15 +- .../LimitedSkolemisationApplication.java | 2 +- .../pagoda/multistage/MultiStageUpperProgram.java | 4 +- .../ac/ox/cs/pagoda/multistage/Normalisation.java | 374 +++++++++------------ .../cs/pagoda/multistage/TwoStageApplication.java | 57 +--- .../Pick4NegativeConceptQuerySpecific.java | 20 +- .../reasoner/light/DLPredicateComparator.java | 6 +- 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 + .../pagoda/tracking/TrackingRuleEncoderDisj.java | 24 +- .../pagoda/tracking/TrackingRuleEncoderDisj1.java | 20 +- .../pagoda/tracking/TrackingRuleEncoderDisj2.java | 18 +- .../tracking/TrackingRuleEncoderDisjVar1.java | 42 +-- .../tracking/TrackingRuleEncoderDisjVar2.java | 32 +- 34 files changed, 949 insertions(+), 1036 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') diff --git a/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java b/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java index b201918..70f841f 100644 --- a/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java +++ b/src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java @@ -1,155 +1,135 @@ package uk.ac.ox.cs.pagoda.constraints; -import java.util.Collection; -import java.util.HashMap; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.Map; -import java.util.Queue; -import java.util.Set; - -import org.semanticweb.HermiT.model.AnnotatedEquality; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.AtLeastDataRange; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.Equality; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.InverseRole; - -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; +import org.semanticweb.HermiT.model.*; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.Utility; +import java.util.*; + public class PredicateDependency extends DependencyGraph { - - Collection m_clauses; - Map> edgeLabels = new HashMap>(); - + + private static final DLPredicate equality = AtomicRole.create(Namespace.EQUALITY); + private static final DLPredicate inequality = AtomicRole.create(Namespace.INEQUALITY); + Collection m_clauses; + Map> edgeLabels = new HashMap>(); + Set reachableToBottom = null; + public PredicateDependency(Collection clauses) { m_clauses = clauses; - build(); + build(); } @Override protected void build() { update(m_clauses); - + addLink(equality, AtomicConcept.NOTHING); addLink(inequality, AtomicConcept.NOTHING); } - + private void addEdgeLabel(DLPredicate body, DLPredicate head, DLClause clause) { - PredicatePair key = new PredicatePair(body, head); - LinkedList value; - if ((value = edgeLabels.get(key)) == null) - edgeLabels.put(key, value = new LinkedList()); + PredicatePair key = new PredicatePair(body, head); + LinkedList value; + if ((value = edgeLabels.get(key)) == null) + edgeLabels.put(key, value = new LinkedList()); value.add(clause); } private void addLinks4Negation(AtomicConcept c, DLClause clause) { addLink(c, AtomicConcept.NOTHING); addEdgeLabel(c, AtomicConcept.NOTHING, clause); - String iri = c.getIRI(); + String iri = c.getIRI(); addLink(c = AtomicConcept.create(iri.substring(0, iri.length() - 4)), AtomicConcept.NOTHING); addEdgeLabel(c, AtomicConcept.NOTHING, clause); } public Set collectPredicate(Atom[] atoms) { Set predicates = new HashSet(); - for (Atom atom: atoms) - predicates.addAll(getAtomicPredicates(atom.getDLPredicate())); + for (Atom atom : atoms) + predicates.addAll(getAtomicPredicates(atom.getDLPredicate())); return predicates; } - - private static final DLPredicate equality = AtomicRole.create(Namespace.EQUALITY); - private static final DLPredicate inequality = AtomicRole.create(Namespace.INEQUALITY); private Set getAtomicPredicates(DLPredicate predicate) { - Set predicates = new HashSet(); + Set predicates = new HashSet(); if (predicate instanceof AtLeastConcept) predicates.addAll(getAtomicPredicates((AtLeastConcept) predicate)); else { - if ((predicate = getAtomicPredicate(predicate)) != null) + if ((predicate = getAtomicPredicate(predicate)) != null) predicates.add(predicate); } - return predicates; + return predicates; } private Set getAtomicPredicates(AtLeastConcept alc) { Set set = new HashSet(); - if (alc.getOnRole() instanceof AtomicRole) - set.add((AtomicRole) alc.getOnRole()); - else + if (alc.getOnRole() instanceof AtomicRole) + set.add((AtomicRole) alc.getOnRole()); + else set.add(((InverseRole) alc.getOnRole()).getInverseOf()); - - if (alc.getToConcept() instanceof AtomicConcept) - if (alc.getToConcept().equals(AtomicConcept.THING)); - else set.add((AtomicConcept) alc.getToConcept()); - else + + if (alc.getToConcept() instanceof AtomicConcept) + if (alc.getToConcept().equals(AtomicConcept.THING)) ; + else set.add((AtomicConcept) alc.getToConcept()); + else set.add(OverApproxExist.getNegationConcept(((AtomicNegationConcept) alc.getToConcept()).getNegatedAtomicConcept())); - return set; + return set; } private DLPredicate getAtomicPredicate(DLPredicate p) { if (p instanceof Equality || p instanceof AnnotatedEquality) return equality; if (p instanceof Inequality) - return inequality; + return inequality; if (p instanceof AtomicConcept) - if (p.equals(AtomicConcept.THING)) + if (p.equals(AtomicConcept.THING)) return null; - else return p; + else return p; if (p instanceof AtomicRole) - return p; + return p; if (p instanceof AtLeastDataRange) { - AtLeastDataRange aldr = (AtLeastDataRange) p; - if (aldr.getOnRole() instanceof AtomicRole) - return (AtomicRole) aldr.getOnRole(); - else - return ((InverseRole) aldr.getOnRole()).getInverseOf(); + AtLeastDataRange aldr = (AtLeastDataRange) p; + if (aldr.getOnRole() instanceof AtomicRole) + return (AtomicRole) aldr.getOnRole(); + else + return ((InverseRole) aldr.getOnRole()).getInverseOf(); } Utility.logDebug("Unknown DLPredicate in PredicateDependency: " + p); - return null; + return null; } public Set pathTo(DLPredicate p) { - Set rules = new HashSet(); - Set visited = new HashSet(); - - Queue queue = new LinkedList(); - queue.add(p); + Set rules = new HashSet(); + Set visited = new HashSet(); + + Queue queue = new LinkedList(); + queue.add(p); visited.add(p); - - Set edge; - Collection clauses; - + + Set edge; + Collection clauses; + while (!queue.isEmpty()) { if ((edge = reverseEdges.get(p = queue.poll())) != null) { for (DLPredicate pred: edge) { if (!visited.contains(pred)) { - queue.add(pred); - visited.add(pred); + queue.add(pred); + visited.add(pred); } - clauses = edgeLabelsBetween(pred, p); - if (clauses != null) rules.addAll(clauses); + clauses = edgeLabelsBetween(pred, p); + if (clauses != null) rules.addAll(clauses); } } } - return rules; + return rules; } - + private LinkedList edgeLabelsBetween(DLPredicate p, DLPredicate q) { PredicatePair pair = new PredicatePair(p, q); - return edgeLabels.get(pair); + return edgeLabels.get(pair); } - - Set reachableToBottom = null; public Set pathToBottom(DLPredicate p) { if (reachableToBottom == null) { diff --git a/src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication.java b/src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication.java index 22f1d1d..c75083b 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication.java @@ -1,14 +1,14 @@ package uk.ac.ox.cs.pagoda.multistage; -import java.util.Collection; -import java.util.LinkedList; - import org.semanticweb.HermiT.model.DLClause; import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; -import uk.ac.ox.cs.pagoda.rules.OverApproxDisj; import uk.ac.ox.cs.pagoda.rules.Program; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxDisj; import uk.ac.ox.cs.pagoda.util.Timer; +import java.util.Collection; +import java.util.LinkedList; + public class FoldedApplication extends MultiStageUpperProgram { public FoldedApplication(Program program, BottomStrategy upperBottom) { diff --git a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java b/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java index 3d78f0a..22d90c4 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java @@ -1,20 +1,19 @@ package uk.ac.ox.cs.pagoda.multistage; -import java.util.Collection; -import java.util.HashSet; -import java.util.Set; - import org.openrdf.model.Resource; import org.openrdf.model.Statement; import org.openrdf.model.Value; import org.openrdf.model.impl.URIImpl; import org.openrdf.rio.RDFHandler; import org.openrdf.rio.RDFHandlerException; - import uk.ac.ox.cs.JRDFox.model.Individual; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; +import java.util.Collection; +import java.util.HashSet; +import java.util.Set; + public class IndividualCollector implements RDFHandler { boolean addedSkolemised = false; @@ -43,11 +42,11 @@ public class IndividualCollector implements RDFHandler { public void handleStatement(Statement st) throws RDFHandlerException { Resource sub = st.getSubject(); if (sub instanceof URIImpl) - individuals.add(Individual.create(((URIImpl) sub).toString())); + individuals.add(Individual.create(sub.toString())); if (!st.getPredicate().toString().equals(Namespace.RDF_TYPE)) { Value obj = st.getObject(); if (obj instanceof URIImpl) - individuals.add(Individual.create(((URIImpl) sub).toString())); + individuals.add(Individual.create(sub.toString())); } } diff --git a/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java b/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java index 13752a3..f729158 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java @@ -3,8 +3,8 @@ package uk.ac.ox.cs.pagoda.multistage; import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; -import uk.ac.ox.cs.pagoda.rules.LimitedSkolemisationApproximator; import uk.ac.ox.cs.pagoda.rules.Program; +import uk.ac.ox.cs.pagoda.rules.approximators.LimitedSkolemisationApproximator; public class LimitedSkolemisationApplication extends RestrictedApplication { diff --git a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java index acaf167..33ba345 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java @@ -8,9 +8,9 @@ import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; import uk.ac.ox.cs.pagoda.hermit.RuleHelper; import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager; import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.Program; -import uk.ac.ox.cs.pagoda.rules.TupleDependentApproximator; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator; import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.SparqlHelper; import uk.ac.ox.cs.pagoda.util.Timer; diff --git a/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java b/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java index 4667747..b31d138 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java @@ -1,82 +1,92 @@ package uk.ac.ox.cs.pagoda.multistage; -import java.util.Collection; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.LinkedList; -import java.util.Map; -import java.util.Set; - -import org.semanticweb.HermiT.model.AtLeast; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.AtLeastDataRange; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.Constant; -import org.semanticweb.HermiT.model.ConstantEnumeration; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.Individual; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.InverseRole; -import org.semanticweb.HermiT.model.LiteralConcept; -import org.semanticweb.HermiT.model.Role; -import org.semanticweb.HermiT.model.Variable; -import org.semanticweb.owlapi.model.OWLClass; -import org.semanticweb.owlapi.model.OWLClassExpression; -import org.semanticweb.owlapi.model.OWLDataHasValue; -import org.semanticweb.owlapi.model.OWLDataProperty; -import org.semanticweb.owlapi.model.OWLDataPropertyExpression; -import org.semanticweb.owlapi.model.OWLLiteral; -import org.semanticweb.owlapi.model.OWLObjectHasSelf; -import org.semanticweb.owlapi.model.OWLObjectInverseOf; -import org.semanticweb.owlapi.model.OWLObjectMinCardinality; -import org.semanticweb.owlapi.model.OWLObjectProperty; -import org.semanticweb.owlapi.model.OWLObjectPropertyExpression; -import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom; -import org.semanticweb.owlapi.model.OWLOntology; - +import org.semanticweb.HermiT.model.*; +import org.semanticweb.owlapi.model.*; import uk.ac.ox.cs.pagoda.MyPrefixes; import uk.ac.ox.cs.pagoda.approx.Clause; import uk.ac.ox.cs.pagoda.approx.Clausifier; import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.Utility; +import java.util.*; + public class Normalisation { - -// MultiStageUpperProgram m_program; + + public static final String auxiliaryConceptPrefix = Namespace.PAGODA_AUX + "concept_"; + private static final Variable X = Variable.create("X"), Y = Variable.create("Y"); + // MultiStageUpperProgram m_program; OWLOntology m_ontology; BottomStrategy m_botStrategy; Collection m_rules; Set m_normClauses = new HashSet(); - Map exist2original = new HashMap(); - + Map exist2original = new HashMap(); + Map rightAuxiliaryConcept = new HashMap(); + private Map leftAuxiliaryConcept = new HashMap(); + private Map leftAuxiliaryConcept_inv = new HashMap(); + + public Normalisation(Collection rules, OWLOntology ontology, BottomStrategy botStrategy) { +// m_program = program; + m_ontology = ontology; + m_rules = rules; + m_botStrategy = botStrategy; + } + + public static AtLeastConcept toAtLeastConcept(AtLeast p) { + if (p instanceof AtLeastConcept) return (AtLeastConcept) p; + AtLeastDataRange aldr = (AtLeastDataRange) p; + return AtLeastConcept.create(aldr.getNumber(), aldr.getOnRole(), AtomicConcept.create(MyPrefixes.PAGOdAPrefixes.expandIRI(aldr.getToDataRange().toString()))); + } + + private static String getName(String iri) { + int index = iri.lastIndexOf("#"); + if (index != -1) return iri.substring(index + 1); + index = iri.lastIndexOf("/"); + if (index != -1) return iri.substring(index + 1); + return iri; + } + + public static String getAuxiliaryConcept4Disjunct(AtLeastConcept alc, Individual... individuals) { + Role r = alc.getOnRole(); + LiteralConcept c = alc.getToConcept(); + StringBuilder builder = new StringBuilder(auxiliaryConceptPrefix); + if (r instanceof AtomicRole) + builder.append(getName(((AtomicRole) r).getIRI())); + else + builder.append(getName(((InverseRole) r).getInverseOf().getIRI())).append("_inv"); + + if (alc.getNumber() > 1) + builder.append("_").append(alc.getNumber()); + + if (c instanceof AtomicConcept) { + if (!c.equals(AtomicConcept.THING)) + builder.append("_").append(getName(((AtomicConcept) c).getIRI())); + } else + builder.append("_").append(getName((OverApproxExist.getNegationConcept(((AtomicNegationConcept) c).getNegatedAtomicConcept()).getIRI()))); + + if (individuals.length > 1) + builder.append("_").append(getName(individuals[0].getIRI())); + + builder.append("_exist"); + + return builder.toString(); + } + public Set getNormlisedClauses() { return m_normClauses; } - - public Normalisation(Collection rules, OWLOntology ontology, BottomStrategy botStrategy) { -// m_program = program; - m_ontology = ontology; - m_rules = rules; - m_botStrategy = botStrategy; - } - + public void process() { - for (DLClause clause: m_rules) - if (m_botStrategy.isBottomRule(clause)) + for (DLClause clause : m_rules) + if (m_botStrategy.isBottomRule(clause)) processBottomRule(clause); else if (clause.getHeadLength() == 1) { if (clause.getHeadAtom(0).getDLPredicate() instanceof AtLeast) processExistentialRule(clause); - else + else m_normClauses.add(clause); - } - else + } else processDisjunctiveRule(clause); } @@ -85,75 +95,68 @@ public class Normalisation { m_normClauses.add(clause); return ; } - - Atom headAtom = clause.getHeadAtom(0); + + Atom headAtom = clause.getHeadAtom(0); if (headAtom.getDLPredicate() instanceof AtLeastDataRange) { m_normClauses.add(clause); return ; } - AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); + AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); - DLClause newClause; + DLClause newClause; m_normClauses.add(DLClause.create(new Atom[] {Atom.create(ac, headAtom.getArgument(0)) }, clause.getBodyAtoms())); m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, X)}, new Atom[] {Atom.create(ac, X)})); - exist2original.put(newClause, clause); - } - - public static AtLeastConcept toAtLeastConcept(AtLeast p) { - if (p instanceof AtLeastConcept) return (AtLeastConcept) p; - AtLeastDataRange aldr = (AtLeastDataRange) p; - return AtLeastConcept.create(aldr.getNumber(), aldr.getOnRole(), AtomicConcept.create(MyPrefixes.PAGOdAPrefixes.expandIRI(aldr.getToDataRange().toString()))); + exist2original.put(newClause, clause); } private void processDisjunctiveRule(DLClause clause) { - boolean toNormalise = false; + boolean toNormalise = false; for (Atom atom: clause.getHeadAtoms()) if (!(atom.getDLPredicate() instanceof AtomicConcept)) { toNormalise = true; - break; + break; } - + if (!toNormalise) { m_normClauses.add(clause); - return ; + return; } - + Atom[] newHeadAtoms = new Atom[clause.getHeadLength()]; - Set additionalAtoms = new HashSet(); - int index = 0; - DLClause newClause; + Set additionalAtoms = new HashSet(); + int index = 0; + DLClause newClause; for (Atom headAtom: clause.getHeadAtoms()) { if (headAtom.getDLPredicate() instanceof AtLeast) { AtLeast al = (AtLeast) headAtom.getDLPredicate(); if (al instanceof AtLeastDataRange && ((AtLeastDataRange) al).getToDataRange() instanceof ConstantEnumeration) { ConstantEnumeration ldr = (ConstantEnumeration) ((AtLeastDataRange) al).getToDataRange(); newHeadAtoms[index] = null; - Atom newHeadAtom; + Atom newHeadAtom; for (int i = 0; i < ldr.getNumberOfConstants(); ++i) { - newHeadAtom = Atom.create(AtomicRole.create(((AtomicRole) ((AtLeastDataRange) al).getOnRole()).getIRI()), headAtom.getArgument(0), ldr.getConstant(i)); - if (newHeadAtoms[index] == null) newHeadAtoms[index] = newHeadAtom; + newHeadAtom = Atom.create(AtomicRole.create(((AtomicRole) al.getOnRole()).getIRI()), headAtom.getArgument(0), ldr.getConstant(i)); + if (newHeadAtoms[index] == null) newHeadAtoms[index] = newHeadAtom; else additionalAtoms.add(newHeadAtom); - } + } } else { - AtLeastConcept alc = toAtLeastConcept((AtLeast) headAtom.getDLPredicate()); - AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); + AtLeastConcept alc = toAtLeastConcept((AtLeast) headAtom.getDLPredicate()); + AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); newHeadAtoms[index] = Atom.create(ac, headAtom.getArgument(0)); m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, headAtom.getArgument(0))}, new Atom[] {newHeadAtoms[index]})); - exist2original.put(newClause, clause); + exist2original.put(newClause, clause); } - } - else + } else newHeadAtoms[index] = headAtom; - ++index; + ++index; } - + if (!additionalAtoms.isEmpty()) { - Atom[] tempHeadAtoms = newHeadAtoms; + Atom[] tempHeadAtoms = newHeadAtoms; newHeadAtoms = new Atom[newHeadAtoms.length + additionalAtoms.size()]; - for (int i = 0; i < tempHeadAtoms.length; ++i) + for (int i = 0; i < tempHeadAtoms.length; ++i) newHeadAtoms[i] = tempHeadAtoms[i]; - int tempI = tempHeadAtoms.length; - for (Iterator iter = additionalAtoms.iterator(); iter.hasNext(); ) + int tempI = tempHeadAtoms.length; + for (Iterator iter = additionalAtoms.iterator(); iter.hasNext(); ) newHeadAtoms[tempI++] = iter.next(); additionalAtoms.clear(); } @@ -169,202 +172,157 @@ public class Normalisation { return ; } } - - boolean toNormalise = false; + + boolean toNormalise = false; for (Atom atom: clause.getBodyAtoms()) if (!(atom.getDLPredicate() instanceof AtomicConcept)) - toNormalise = true; - - if (!toNormalise) { - m_normClauses.add(clause); - return ; + toNormalise = true; + + if (!toNormalise) { + m_normClauses.add(clause); + return; } - - Clause myClause = null; + + Clause myClause = null; try { myClause = new Clause(Clausifier.getInstance(m_ontology), clause); } catch (Exception e) { Utility.logError("The clause: " + clause + " cannot be rolled up into GCI."); - m_normClauses.add(clause); - return ; + m_normClauses.add(clause); + return; } - + Atom[] newBodyAtoms = new Atom [myClause.getSubClasses().size()]; - int index = 0; + int index = 0; for (OWLClassExpression clsExp: myClause.getSubClasses()) { - if (clsExp instanceof OWLClass) - newBodyAtoms[index] = Atom.create(AtomicConcept.create(((OWLClass) clsExp).getIRI().toString()), X); + if (clsExp instanceof OWLClass) + newBodyAtoms[index] = Atom.create(AtomicConcept.create(((OWLClass) clsExp).getIRI().toString()), X); else if (clsExp instanceof OWLObjectSomeValuesFrom || clsExp instanceof OWLObjectMinCardinality) { - int number; - OWLObjectPropertyExpression prop; + int number; + OWLObjectPropertyExpression prop; OWLClassExpression filler; if (clsExp instanceof OWLObjectSomeValuesFrom) { OWLObjectSomeValuesFrom owl = (OWLObjectSomeValuesFrom) clsExp; - number = 1; + number = 1; prop = owl.getProperty(); - filler = owl.getFiller(); + filler = owl.getFiller(); } else { - OWLObjectMinCardinality owl = (OWLObjectMinCardinality) clsExp; - number = owl.getCardinality(); - prop = owl.getProperty(); - filler = owl.getFiller(); + OWLObjectMinCardinality owl = (OWLObjectMinCardinality) clsExp; + number = owl.getCardinality(); + prop = owl.getProperty(); + filler = owl.getFiller(); } - - Role r = null; - if (prop instanceof OWLObjectProperty) + + Role r = null; + if (prop instanceof OWLObjectProperty) r = AtomicRole.create(((OWLObjectProperty) prop).getIRI().toString()); - else + else r = InverseRole.create(AtomicRole.create(((OWLObjectProperty) (((OWLObjectInverseOf) prop).getInverse())).getIRI().toString())); - + LiteralConcept c = AtomicConcept.create(((OWLClass) filler).getIRI().toString()); AtomicConcept ac = getLeftAuxiliaryConcept(AtLeastConcept.create(number, r, c), false); - - m_normClauses.add(exists_r_C_implies_A(number, r, c, ac)); + + m_normClauses.add(exists_r_C_implies_A(number, r, c, ac)); newBodyAtoms[index] = Atom.create(ac, X); } // else if (clsExp instanceof OWLDataSomeValuesFrom || clsExp instanceof OWLDataMinCardinality) { -// int number; -// OWLDataPropertyExpression prop; +// int number; +// OWLDataPropertyExpression prop; // OWLDataRange filler; // if (clsExp instanceof OWLDataSomeValuesFrom) { // OWLDataSomeValuesFrom owl = (OWLDataSomeValuesFrom) clsExp; -// number = 1; +// number = 1; // prop = owl.getProperty(); -// filler = owl.getFiller(); +// filler = owl.getFiller(); // } // else { -// OWLDataMinCardinality owl = (OWLDataMinCardinality) clsExp; -// number = owl.getCardinality(); -// prop = owl.getProperty(); -// filler = owl.getFiller(); +// OWLDataMinCardinality owl = (OWLDataMinCardinality) clsExp; +// number = owl.getCardinality(); +// prop = owl.getProperty(); +// filler = owl.getFiller(); // } -// +// // Role r = AtomicRole.create(((OWLDataProperty) prop).getIRI().toString()); -// +// // LiteralConcept c = AtomicConcept.create(((OWLClass) filler).getIRI().toString()); // AtomicConcept ac = getLeftAuxiliaryConcept(AtLeastConcept.create(number, r, c), false); -// -// m_normClauses.add(exists_r_C_implies_A(number, r, c, ac)); +// +// m_normClauses.add(exists_r_C_implies_A(number, r, c, ac)); // newBodyAtoms[index] = Atom.create(ac, X); // } else if (clsExp instanceof OWLObjectHasSelf) { OWLObjectPropertyExpression prop = ((OWLObjectHasSelf) clsExp).getProperty(); - AtomicRole r; - if (prop instanceof OWLObjectProperty) + AtomicRole r; + if (prop instanceof OWLObjectProperty) r = AtomicRole.create(((OWLObjectProperty) prop).getIRI().toString()); - else + else r = AtomicRole.create(((OWLObjectProperty) (((OWLObjectInverseOf) prop).getInverse())).getIRI().toString()); - newBodyAtoms[index] = Atom.create(r, X, X); + newBodyAtoms[index] = Atom.create(r, X, X); } else if (clsExp instanceof OWLDataHasValue) { - OWLDataPropertyExpression prop = ((OWLDataHasValue) clsExp).getProperty(); + OWLDataPropertyExpression prop = ((OWLDataHasValue) clsExp).getProperty(); AtomicRole r = AtomicRole.create(((OWLDataProperty) prop).getIRI().toString()); OWLLiteral l = ((OWLDataHasValue) clsExp).getValue(); if (l.getDatatype().toStringID().equals(Namespace.RDF_PLAIN_LITERAL)) - newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral() + "@" + l.getLang(), Namespace.RDF_PLAIN_LITERAL)); - else - newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral(), l.getDatatype().toStringID())); - } - else { + newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral() + "@" + l.getLang(), Namespace.RDF_PLAIN_LITERAL)); + else + newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral(), l.getDatatype().toStringID())); + } else { newBodyAtoms[index] = null; Utility.logError("counld not translate OWLClassExpression: " + clsExp + " in " + clause); } - ++index; + ++index; } - + m_normClauses.add(DLClause.create(clause.getHeadAtoms(), newBodyAtoms)); } - private static final Variable X = Variable.create("X"), Y = Variable.create("Y"); - private DLClause exists_r_C_implies_A(int n, Role r, LiteralConcept c, AtomicConcept a) { - Variable[] Ys = new Variable[n]; - if (n == 1) Ys[0] = Y; - else + Variable[] Ys = new Variable[n]; + if (n == 1) Ys[0] = Y; + else for (int i = 0; i < n; ++i) Ys[i] = Variable.create("Y" + (i + 1)); - Collection bodyAtoms = new LinkedList(); - + Collection bodyAtoms = new LinkedList(); + for (int i = 0; i < n; ++i) { - Atom rxy = r instanceof AtomicRole ? - Atom.create(((AtomicRole) r), X, Ys[i]) : + Atom rxy = r instanceof AtomicRole ? + Atom.create(((AtomicRole) r), X, Ys[i]) : Atom.create(((InverseRole) r).getInverseOf(), Ys[i], X); - bodyAtoms.add(rxy); + bodyAtoms.add(rxy); if (!c.equals(AtomicConcept.THING)) bodyAtoms.add(Atom.create((AtomicConcept) c, Ys[i])); } - + for (int i = 0; i < n; ++i) for (int j = i + 1; j < n; ++j) - bodyAtoms.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j])); - - return DLClause.create(new Atom[] {Atom.create(a, X)}, bodyAtoms.toArray(new Atom[0])); - } - - private Map leftAuxiliaryConcept = new HashMap(); - private Map leftAuxiliaryConcept_inv = new HashMap(); - - public static final String auxiliaryConceptPrefix = Namespace.PAGODA_AUX + "concept_"; + bodyAtoms.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j])); - private static String getName(String iri) { - int index = iri.lastIndexOf("#"); - if (index != -1) return iri.substring(index + 1); - index = iri.lastIndexOf("/"); - if (index != -1) return iri.substring(index + 1); - return iri; + return DLClause.create(new Atom[]{Atom.create(a, X)}, bodyAtoms.toArray(new Atom[0])); } - + private AtomicConcept getRightAuxiliaryConcept(AtLeastConcept alc, Individual... individuals) { String iri = getAuxiliaryConcept4Disjunct(alc, individuals); - rightAuxiliaryConcept.put(iri, alc); - return AtomicConcept.create(iri); - } - - public static String getAuxiliaryConcept4Disjunct(AtLeastConcept alc, Individual... individuals) { - Role r = alc.getOnRole(); - LiteralConcept c = alc.getToConcept(); - StringBuilder builder = new StringBuilder(auxiliaryConceptPrefix); - if (r instanceof AtomicRole) - builder.append(getName(((AtomicRole) r).getIRI())); - else - builder.append(getName(((InverseRole) r).getInverseOf().getIRI())).append("_inv"); - - if (alc.getNumber() > 1) - builder.append("_").append(alc.getNumber()); - - if (c instanceof AtomicConcept) { - if (!c.equals(AtomicConcept.THING)) - builder.append("_").append(getName(((AtomicConcept) c).getIRI())); - } - else - builder.append("_").append(getName((OverApproxExist.getNegationConcept(((AtomicNegationConcept) c).getNegatedAtomicConcept()).getIRI()))); - - if (individuals.length > 1) - builder.append("_").append(getName(individuals[0].getIRI())); - - builder.append("_exist"); - - return builder.toString(); + rightAuxiliaryConcept.put(iri, alc); + return AtomicConcept.create(iri); } public AtomicConcept getLeftAuxiliaryConcept(AtLeastConcept key, boolean available) { -// AtLeastConcept key = AtLeastConcept.create(1, r, c); - AtomicConcept value = null; - if ((value = leftAuxiliaryConcept.get(key)) != null); +// AtLeastConcept key = AtLeastConcept.create(1, r, c); + AtomicConcept value = null; + if ((value = leftAuxiliaryConcept.get(key)) != null) ; else if (!available) { value = AtomicConcept.create(getAuxiliaryConcept4Disjunct(key)); - leftAuxiliaryConcept.put(key, value); + leftAuxiliaryConcept.put(key, value); leftAuxiliaryConcept_inv.put(value, key); } - return value; + return value; } public AtLeastConcept getLeftAtLeastConcept(AtomicConcept value) { - return leftAuxiliaryConcept_inv.get(value); + return leftAuxiliaryConcept_inv.get(value); } - - Map rightAuxiliaryConcept = new HashMap(); public AtLeastConcept getRightAtLeastConcept(AtomicConcept p) { return rightAuxiliaryConcept.get(p.getIRI()); diff --git a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java index f08bfbd..79627d9 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java @@ -1,26 +1,6 @@ package uk.ac.ox.cs.pagoda.multistage; -import java.util.Collection; -import java.util.HashMap; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.Map; -import java.util.Set; - -import org.semanticweb.HermiT.model.AnnotatedEquality; -import org.semanticweb.HermiT.model.AtLeast; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.AtLeastDataRange; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.Equality; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.Variable; - +import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.JRDFox.JRDFStoreException; import uk.ac.ox.cs.JRDFox.store.TupleIterator; import uk.ac.ox.cs.pagoda.MyPrefixes; @@ -29,38 +9,36 @@ import uk.ac.ox.cs.pagoda.hermit.RuleHelper; import uk.ac.ox.cs.pagoda.query.GapByStore4ID; import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager; import uk.ac.ox.cs.pagoda.rules.DatalogProgram; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.Program; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.SparqlHelper; import uk.ac.ox.cs.pagoda.util.Utility; +import java.util.*; + abstract class TwoStageApplication { + private static final String NAF_suffix = "_NAF"; protected TwoStageQueryEngine engine; protected MyPrefixes prefixes = MyPrefixes.PAGOdAPrefixes; - private GapByStore4ID gap; - - Program lowerProgram; - - boolean m_incrementally = true; - protected Set rules = new HashSet(); - private StringBuilder datalogRuleText = new StringBuilder(); - protected Collection constraints = new LinkedList(); protected BottomStrategy m_bottom; - protected Set toGenerateNAFFacts = new HashSet(); - protected OverApproxExist overExist = new OverApproxExist(); - + Program lowerProgram; + boolean m_incrementally = true; + Set allIndividuals = new HashSet(); + RDFoxTripleManager tripleManager; + private GapByStore4ID gap; + private StringBuilder datalogRuleText = new StringBuilder(); private Map map = new HashMap(); public TwoStageApplication(TwoStageQueryEngine engine, DatalogProgram program, GapByStore4ID gap) { this.engine = engine; tripleManager = new RDFoxTripleManager(engine.getDataStore(), m_incrementally); - this.gap = gap; + this.gap = gap; m_bottom = program.getUpperBottomStrategy(); lowerProgram = program.getLower(); @@ -123,7 +101,7 @@ abstract class TwoStageApplication { for (DLClause clause: lowerProgram.getClauses()) if (!rules.contains(clause)) builder.append(RuleHelper.getText(clause)); - + engine.materialise(builder.toString(), null, false); addAuxiliaryRules(); addAuxiliaryNAFFacts(); @@ -150,7 +128,7 @@ abstract class TwoStageApplication { e.printStackTrace(); } finally { if (tuples != null) tuples.dispose(); - tuples = null; + tuples = null; } } } @@ -171,9 +149,6 @@ abstract class TwoStageApplication { protected abstract void addAuxiliaryRules(); - Set allIndividuals = new HashSet(); - RDFoxTripleManager tripleManager; - private void addAuxiliaryNAFFacts() { for (int id : tripleManager.getResourceIDs(engine.getAllIndividuals())) @@ -203,7 +178,7 @@ abstract class TwoStageApplication { tuples = engine.internal_evaluate(SparqlHelper.getSPARQLQuery( new Atom[] { Atom.create(p, X) }, "X")); for (long multi = tuples.open(); multi != 0; multi = tuples.getNext()) { - ret.remove((int) tuples.getResourceID(0)); + ret.remove(tuples.getResourceID(0)); } } catch (JRDFStoreException e) { // TODO Auto-generated catch block @@ -216,8 +191,6 @@ abstract class TwoStageApplication { protected abstract Collection getInitialClauses(Program program); - private static final String NAF_suffix = "_NAF"; - protected Atom getNAFAtom(Atom atom) { return getNAFAtom(atom, true); } diff --git a/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConceptQuerySpecific.java b/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConceptQuerySpecific.java index ae168cf..10aa22f 100644 --- a/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConceptQuerySpecific.java +++ b/src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConceptQuerySpecific.java @@ -1,18 +1,7 @@ package uk.ac.ox.cs.pagoda.multistage.treatement; -import java.util.Comparator; -import java.util.Set; - -import org.semanticweb.HermiT.model.AnnotatedEquality; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.Equality; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.InverseRole; +import org.semanticweb.HermiT.model.*; +import uk.ac.ox.cs.JRDFox.JRDFStoreException; import uk.ac.ox.cs.pagoda.constraints.PredicateDependency; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine; @@ -20,10 +9,11 @@ import uk.ac.ox.cs.pagoda.multistage.Normalisation; import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication; import uk.ac.ox.cs.pagoda.multistage.Violation; import uk.ac.ox.cs.pagoda.query.QueryRecord; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; -import uk.ac.ox.cs.JRDFox.JRDFStoreException; +import java.util.Comparator; +import java.util.Set; public class Pick4NegativeConceptQuerySpecific extends Pick4NegativeConcept { diff --git a/src/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java b/src/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java index c22902c..05e399e 100644 --- a/src/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java +++ b/src/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java @@ -1,9 +1,9 @@ package uk.ac.ox.cs.pagoda.reasoner.light; -import java.util.Comparator; - import uk.ac.ox.cs.pagoda.multistage.Normalisation; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; + +import java.util.Comparator; public class DLPredicateComparator implements Comparator { 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); +} diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java index cee829f..331ad12 100644 --- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java @@ -1,30 +1,14 @@ package uk.ac.ox.cs.pagoda.tracking; -import java.util.Collection; -import java.util.Collections; -import java.util.HashMap; -import java.util.HashSet; -import java.util.Iterator; -import java.util.LinkedList; -import java.util.Map; - -import org.semanticweb.HermiT.model.AnnotatedEquality; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.Equality; -import org.semanticweb.HermiT.model.Individual; -import org.semanticweb.HermiT.model.Inequality; - +import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; +import java.util.*; + public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap { public TrackingRuleEncoderDisj(UpperDatalogProgram program, BasicQueryEngine store) { diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java index e72ed96..d6b5e8b 100644 --- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java @@ -1,26 +1,14 @@ package uk.ac.ox.cs.pagoda.tracking; -import java.util.LinkedList; - -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.Individual; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.InverseRole; -import org.semanticweb.HermiT.model.Term; -import org.semanticweb.HermiT.model.Variable; - +import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.MyPrefixes; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.multistage.Normalisation; import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; + +import java.util.LinkedList; public class TrackingRuleEncoderDisj1 extends TrackingRuleEncoderDisj { diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java index 6cf239f..8d79090 100644 --- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java @@ -1,24 +1,12 @@ package uk.ac.ox.cs.pagoda.tracking; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.Individual; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.InverseRole; -import org.semanticweb.HermiT.model.Term; -import org.semanticweb.HermiT.model.Variable; - +import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.MyPrefixes; import uk.ac.ox.cs.pagoda.multistage.Normalisation; import uk.ac.ox.cs.pagoda.query.QueryRecord; import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; public class TrackingRuleEncoderDisj2 extends TrackingRuleEncoderDisj { @@ -56,7 +44,7 @@ public class TrackingRuleEncoderDisj2 extends TrackingRuleEncoderDisj { @Override protected DLPredicate generateAuxiliaryRule(AtLeastConcept p, DLClause original, Individual[] individuals) { - DLPredicate ret = AtomicConcept.create(getTrackingPredicate(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p, individuals))); + DLPredicate ret = AtomicConcept.create(getTrackingPredicate(Normalisation.getAuxiliaryConcept4Disjunct(p, individuals))); Atom[] headAtom = new Atom[] {Atom.create(ret, X)}; AtomicRole role = p.getOnRole() instanceof AtomicRole ? diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java index 37116d4..2143b03 100644 --- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java @@ -1,34 +1,20 @@ package uk.ac.ox.cs.pagoda.tracking; -import java.util.Collection; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.Set; - -import org.semanticweb.HermiT.model.AnnotatedEquality; -import org.semanticweb.HermiT.model.AtLeast; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.DatatypeRestriction; -import org.semanticweb.HermiT.model.Equality; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.InverseRole; -import org.semanticweb.HermiT.model.Variable; - +import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.MyPrefixes; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.multistage.Normalisation; import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; import uk.ac.ox.cs.pagoda.util.Utility; +import java.util.Collection; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.Set; + public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap { public TrackingRuleEncoderDisjVar1(UpperDatalogProgram program, BasicQueryEngine store) { @@ -96,13 +82,13 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap { return Atom.create(getTrackingDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); } if (p instanceof AtomicConcept) - return Atom.create(getTrackingDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); + return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0)); if (p instanceof AtomicRole) - return Atom.create(getTrackingDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); + return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); if (p instanceof Equality || p instanceof AnnotatedEquality) return Atom.create(getTrackingDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); if (p instanceof Inequality) - return Atom.create(getTrackingDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); + return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); return null; } @@ -114,15 +100,15 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap { return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); } if (p instanceof AtomicConcept) - return Atom.create(getGapDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); + return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0)); if (p instanceof AtomicRole) - return Atom.create(getGapDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); + return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); if (p instanceof Equality || p instanceof AnnotatedEquality) return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); if (p instanceof Inequality) - return Atom.create(getGapDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); + return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); if (p instanceof DatatypeRestriction) - return Atom.create(getGapDLPredicate((DatatypeRestriction) p), headAtom.getArgument(0)); + return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0)); Utility.logError(p + " is not recognised."); return null; } diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java index d257de3..7311a86 100644 --- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java @@ -1,31 +1,19 @@ package uk.ac.ox.cs.pagoda.tracking; -import java.util.Collection; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.Set; - -import org.semanticweb.HermiT.model.AnnotatedEquality; -import org.semanticweb.HermiT.model.AtLeastConcept; -import org.semanticweb.HermiT.model.Atom; -import org.semanticweb.HermiT.model.AtomicConcept; -import org.semanticweb.HermiT.model.AtomicNegationConcept; -import org.semanticweb.HermiT.model.AtomicRole; -import org.semanticweb.HermiT.model.DLClause; -import org.semanticweb.HermiT.model.DLPredicate; -import org.semanticweb.HermiT.model.Equality; -import org.semanticweb.HermiT.model.Inequality; -import org.semanticweb.HermiT.model.InverseRole; -import org.semanticweb.HermiT.model.Variable; - +import org.semanticweb.HermiT.model.*; import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; import uk.ac.ox.cs.pagoda.multistage.Normalisation; import uk.ac.ox.cs.pagoda.query.QueryRecord; import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; -import uk.ac.ox.cs.pagoda.rules.OverApproxExist; import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; +import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; import uk.ac.ox.cs.pagoda.util.Namespace; +import java.util.Collection; +import java.util.HashSet; +import java.util.LinkedList; +import java.util.Set; + public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap { public TrackingRuleEncoderDisjVar2(UpperDatalogProgram program, BasicQueryEngine store) { @@ -91,13 +79,13 @@ public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap { return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); } if (p instanceof AtomicConcept) - return Atom.create(getGapDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); + return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0)); if (p instanceof AtomicRole) - return Atom.create(getGapDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); + return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); if (p instanceof Equality || p instanceof AnnotatedEquality) return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); if (p instanceof Inequality) - return Atom.create(getGapDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); + return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1)); return null; } -- cgit v1.2.3