From 9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8 Mon Sep 17 00:00:00 2001 From: yzhou Date: Tue, 21 Apr 2015 10:34:27 +0100 Subject: initial version --- .../tracking/TrackingRuleEncoderDisjVar2.java | 242 +++++++++++++++++++++ 1 file changed, 242 insertions(+) create mode 100644 src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java (limited to 'src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java') diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java new file mode 100644 index 0000000..d257de3 --- /dev/null +++ b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java @@ -0,0 +1,242 @@ +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 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.util.Namespace; + +public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap { + + public TrackingRuleEncoderDisjVar2(UpperDatalogProgram program, BasicQueryEngine store) { + super(program, store); + } + + private Set disjunctiveRules = new HashSet(); + + @Override + public boolean encodingRules() { + if (ruleEncoded) return false; + ruleEncoded = true; + + for (DLClause clause: program.getClauses()) { + encodingRule(clause); + } + + if (disjunctiveRules.isEmpty()) + return true; + + processDisjunctiveRules(); + return false; + } + + @Override + protected void encodingRule(DLClause clause) { + DLClause original = program.getCorrespondingClause(clause); + if (original.getHeadLength() <= 1) { + super.encodingRule(clause); + } + else { + if (!DLClauseHelper.hasSubsetBodyAtoms(clause, original)) + super.encodingRule(clause); + addDisjunctiveRule(original); + } + } + + private void processDisjunctiveRules() { + for (DLClause clause: disjunctiveRules) + encodingDisjunctiveRule(clause); + } + + private Atom getAuxiliaryAtom(Atom headAtom) { + DLPredicate p = headAtom.getDLPredicate(); + if (p instanceof AtLeastConcept) { + return Atom.create(generateAuxiliaryRule((AtLeastConcept) p), 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 Atom getGapAtom(Atom headAtom) { + DLPredicate p = headAtom.getDLPredicate(); + if (p instanceof AtLeastConcept) { + 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)); + if (p instanceof AtomicRole) + return Atom.create(getGapDLPredicate((AtomicRole) 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 null; + } + + private void encodingDisjunctiveRule(DLClause clause) { + int headLength = clause.getHeadLength(); + + Atom[] auxAtoms = new Atom[headLength]; + for (int i = 0; i < headLength; ++i) + auxAtoms[i] = getAuxiliaryAtom(clause.getHeadAtom(i)); + + Atom[] gapAtoms = new Atom[headLength]; + for (int i = 0; i < headLength; ++i) + gapAtoms[i] = getGapAtom(clause.getHeadAtom(i)); + + 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; + for (int j = 0; j < headLength; ++j) { + Atom[] newBodyAtoms = new Atom[headLength + bodyAtoms.length + 1]; + newBodyAtoms[0] = gapAtoms[j]; + + for (int i = 0; i < headLength; ++i) +// newBodyAtoms[i] = auxAtoms[i]; + newBodyAtoms[i + 1] = auxAtoms[i]; + + for (int i = 0; i < bodyAtoms.length; ++i) +// newBodyAtoms[i + headLength] = bodyAtoms[i]; + newBodyAtoms[i + headLength + 1] = bodyAtoms[i]; + + for (Atom atom: newHeadAtoms) { + newClause = DLClause.create(new Atom[] {atom}, newBodyAtoms); + addTrackingClause(newClause); + } + } + } + + private void addTrackingClause(DLClause clause) { + trackingClauses.add(clause); + } + + private void addDisjunctiveRule(DLClause clause) { + disjunctiveRules.add(clause); + } + + protected DLPredicate generateAuxiliaryRule(AtLeastConcept p) { + AtomicConcept ac = AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct(p)); + int num = p.getNumber(); + Variable X = Variable.create("X"); + Variable[] Ys = new Variable[num]; + for (int i = 0; i < num; ++i) Ys[i] = Variable.create("Y" + (i + 1)); + Collection expandedAtom = new LinkedList(); + Collection representativeAtom = new LinkedList(); + if (p.getOnRole() instanceof AtomicRole) { + AtomicRole r = (AtomicRole) p.getOnRole(); + for (int i = 0; i < num; ++i) + expandedAtom.add(Atom.create(r, X, Ys[i])); + representativeAtom.add(Atom.create(r, X, Ys[0])); + } + else { + AtomicRole r = ((InverseRole) p.getOnRole()).getInverseOf(); + for (int i = 0; i < num; ++i) + expandedAtom.add(Atom.create(r, Ys[i], X)); + representativeAtom.add(Atom.create(r, Ys[0], X)); + + } + + if (num > 1) { + representativeAtom.add(Atom.create(Inequality.INSTANCE, Ys[0], Ys[1])); + } + for (int i = 0; i < num; ++i) + for (int j = i + 1; j < num; ++i) + expandedAtom.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j])); + + if (!p.getToConcept().equals(AtomicConcept.THING)) { + AtomicConcept c; + if (p.getToConcept() instanceof AtomicConcept) + c = (AtomicConcept) p.getToConcept(); + else + c = OverApproxExist.getNegationConcept(((AtomicNegationConcept) p.getToConcept()).getNegatedAtomicConcept()); + for (int i = 0; i < num; ++i) + expandedAtom.add(Atom.create(c, Ys[i])); + representativeAtom.add(Atom.create(c, Ys[0])); + } + + DLPredicate auxPredicate = getTrackingDLPredicate(ac); + DLPredicate gapPredicate = getGapDLPredicate(ac); + for (Atom atom: representativeAtom) { + Atom[] bodyAtoms = new Atom[expandedAtom.size() + 1]; + bodyAtoms[0] = getAuxiliaryAtom(atom); + int i = 0; + for (Atom bodyAtom: expandedAtom) + bodyAtoms[++i] = bodyAtom; + addTrackingClause(DLClause.create(new Atom[] {Atom.create(auxPredicate, X)}, bodyAtoms)); + + bodyAtoms = new Atom[expandedAtom.size() + 1]; + if (atom.getArity() == 1) + bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0)); + else + bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0), atom.getArgument(1)); + i = 0; + for (Atom bodyAtom: expandedAtom) + bodyAtoms[++i] = bodyAtom; + addTrackingClause(DLClause.create(new Atom[] {Atom.create(gapPredicate, X)}, bodyAtoms)); + } + + return auxPredicate; + } + + private DLPredicate generateAuxiliaryRule(AtomicConcept p) { + return getTrackingDLPredicate(p); + } + + private DLPredicate generateAuxiliaryRule(AtomicRole p) { + return getTrackingDLPredicate(p); + } + + protected DLPredicate generateAuxiliaryRule(Equality instance) { + return getTrackingDLPredicate(AtomicRole.create(Namespace.EQUALITY)); + } + + protected DLPredicate generateAuxiliaryRule(Inequality instance) { + return getTrackingDLPredicate(AtomicRole.create(Namespace.INEQUALITY)); + } + + @Override + protected void encodingAtomicQuery(QueryRecord[] botQuerRecords) { + encodingAtomicQuery(botQuerRecords, true); + } + +} -- cgit v1.2.3