From 9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8 Mon Sep 17 00:00:00 2001 From: yzhou Date: Tue, 21 Apr 2015 10:34:27 +0100 Subject: initial version --- .../pagoda/tracking/TrackingRuleEncoderDisj.java | 178 +++++++++++++++++++++ 1 file changed, 178 insertions(+) create mode 100644 src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java (limited to 'src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java') diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java new file mode 100644 index 0000000..cee829f --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java @@ -0,0 +1,178 @@ +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 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.util.Namespace; + +public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap { + + public TrackingRuleEncoderDisj(UpperDatalogProgram program, BasicQueryEngine store) { + super(program, store); + } + + protected Map> disjunctiveRules = new HashMap>(); + + /** + * + */ + protected void processDisjunctiveRules() { + Map> auxiliaryAtoms = new HashMap>(); + Map> skolemisedAtoms = new HashMap>(); + + for (Map.Entry> entry: disjunctiveRules.entrySet()) { + DLClause original = entry.getKey(); + Collection overClauses = entry.getValue(); + + int index = 0; + for (Iterator iter = overClauses.iterator(); iter.hasNext();) { + DLClause subClause = iter.next(); + if (DLClauseHelper.hasSubsetBodyAtoms(subClause, original)) { + Atom headAtom = subClause.getHeadAtom(0); + if ((index = OverApproxExist.indexOfSkolemisedIndividual(headAtom)) != -1) { + Individual i = (Individual) headAtom.getArgument(index); + Collection clauses = skolemisedAtoms.get(i); + if (clauses == null) { + clauses = new HashSet(); + skolemisedAtoms.put(i, clauses); + } + clauses.add(subClause); + } + else + auxiliaryAtoms.put(getAuxiliaryAtom(original, subClause.getHeadAtom(0)), Collections.singleton(subClause)); + } + else + super.encodingRule(subClause); + } + + for (Atom headAtom: original.getHeadAtoms()) + if (headAtom.getDLPredicate() instanceof AtLeastConcept) { + AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); + Collection clauses = new HashSet(); + Individual[] individuals = new Individual[alc.getNumber()]; + for (int i = 0; i < alc.getNumber(); ++i) { + individuals[i] = OverApproxExist.getNewIndividual(original, i); + clauses.addAll(skolemisedAtoms.get(individuals[i])); + } + auxiliaryAtoms.put(getAuxiliaryAtom(original, headAtom, individuals), clauses); + } + + index = 0; + Atom[] auxAtoms = auxiliaryAtoms.keySet().toArray(new Atom[0]); + for (Atom atom: auxAtoms) { + for (DLClause subClause: auxiliaryAtoms.get(atom)) + encodingDisjunctiveRule(subClause, index, auxAtoms); + index++; + } + + auxiliaryAtoms.clear(); + } + } + + private Atom getAuxiliaryAtom(DLClause original, Atom headAtom, Individual... individuals) { + DLPredicate p = headAtom.getDLPredicate(); + if (p instanceof AtLeastConcept) { +// AtLeastConcept alc = (AtLeastConcept) p; +// Individual[] individuals = new Individual[alc.getNumber()]; +// for (int i = 0; i < alc.getNumber(); ++i) +// individuals[i] = OverApproxExist.getNewIndividual(original, i); + return Atom.create(generateAuxiliaryRule((AtLeastConcept) p, original, individuals), headAtom.getArgument(0)); + } + if (p instanceof AtomicConcept) + return Atom.create(generateAuxiliaryRule((AtomicConcept) p), headAtom.getArgument(0)); + if (p instanceof AtomicRole) + return Atom.create(generateAuxiliaryRule((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); + if (p instanceof Equality || p instanceof AnnotatedEquality) + return Atom.create(generateAuxiliaryRule(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); + if (p instanceof Inequality) + return Atom.create(generateAuxiliaryRule((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); + + return null; + } + + private void encodingDisjunctiveRule(DLClause clause, int index, Atom[] auxAtoms) { + int validHeadLength = auxAtoms.length; + Atom headAtom = clause.getHeadAtom(0); + Atom[] bodyAtoms = clause.getBodyAtoms(); + + LinkedList newHeadAtoms = new LinkedList(); + DLPredicate selected = AtomicConcept.create(getSelectedPredicate()); + newHeadAtoms.add(Atom.create(selected, getIndividual4GeneralRule(clause))); + + for (Atom atom: bodyAtoms) { + Atom newAtom = Atom.create( + getTrackingDLPredicate(atom.getDLPredicate()), + DLClauseHelper.getArguments(atom)); + newHeadAtoms.add(newAtom); + } + + DLClause newClause; + Atom[] newBodyAtoms = new Atom[bodyAtoms.length + validHeadLength + 1]; + + newBodyAtoms[0] = Atom.create( + getTrackingDLPredicate(headAtom.getDLPredicate()), + DLClauseHelper.getArguments(headAtom)); + + newBodyAtoms[1] = Atom.create( + getGapDLPredicate(headAtom.getDLPredicate()), + DLClauseHelper.getArguments(headAtom)); + + for (int i = 0; i < validHeadLength; ++i) + if (i != index) + newBodyAtoms[i + (i < index ? 2 : 1)] = auxAtoms[i]; + + for (int i = 0; i < bodyAtoms.length; ++i) + newBodyAtoms[i + validHeadLength + 1] = bodyAtoms[i]; + + for (Atom atom: newHeadAtoms) { + newClause = DLClause.create(new Atom[] {atom}, newBodyAtoms); + addTrackingClause(newClause); + } + } + + protected void addTrackingClause(DLClause clause) { + trackingClauses.add(clause); + } + + protected void addDisjunctiveRule(DLClause key, DLClause clause) { + Collection value = disjunctiveRules.get(key); + if (value == null) { + value = new LinkedList(); + disjunctiveRules.put(key, value); + } + value.add(clause); + } + + protected abstract DLPredicate generateAuxiliaryRule(AtLeastConcept p, DLClause original, Individual[] individuals); + + protected abstract DLPredicate generateAuxiliaryRule(AtomicRole p); + + protected abstract DLPredicate generateAuxiliaryRule(AtomicConcept p); + + protected DLPredicate generateAuxiliaryRule(Equality instance) { + return generateAuxiliaryRule(AtomicRole.create(Namespace.EQUALITY)); + } + + protected abstract DLPredicate generateAuxiliaryRule(Inequality instance); + +} -- cgit v1.2.3