From 7e0ecc07285209e65f9d4d022065d06a4997fc86 Mon Sep 17 00:00:00 2001 From: RncLsn Date: Wed, 13 May 2015 11:57:06 +0100 Subject: Implementing Limited Skolemisation, in particular SkolemTermsDispenser. --- .../pagoda/tracking/TrackingRuleEncoderDisj.java | 24 +++---------- .../pagoda/tracking/TrackingRuleEncoderDisj1.java | 20 +++-------- .../pagoda/tracking/TrackingRuleEncoderDisj2.java | 18 ++-------- .../tracking/TrackingRuleEncoderDisjVar1.java | 42 ++++++++-------------- .../tracking/TrackingRuleEncoderDisjVar2.java | 32 ++++++----------- 5 files changed, 35 insertions(+), 101 deletions(-) (limited to 'src/uk/ac/ox/cs/pagoda/tracking') 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