diff options
| author | RncLsn <rnc.lsn@gmail.com> | 2015-05-13 11:57:06 +0100 |
|---|---|---|
| committer | RncLsn <rnc.lsn@gmail.com> | 2015-05-13 11:57:06 +0100 |
| commit | 7e0ecc07285209e65f9d4d022065d06a4997fc86 (patch) | |
| tree | 3c3faa6684e49444c7078903d2e5762fc44bb3a6 /src/uk/ac/ox/cs/pagoda/rules | |
| parent | 0c2726db44b562cbda9bfa87e76d829927c31ec8 (diff) | |
| download | ACQuA-7e0ecc07285209e65f9d4d022065d06a4997fc86.tar.gz ACQuA-7e0ecc07285209e65f9d4d022065d06a4997fc86.zip | |
Implementing Limited Skolemisation, in particular SkolemTermsDispenser.
Diffstat (limited to 'src/uk/ac/ox/cs/pagoda/rules')
15 files changed, 195 insertions, 116 deletions
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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules; |
| 2 | 2 | ||
| 3 | import java.util.Collection; | ||
| 4 | import java.util.HashMap; | ||
| 5 | import java.util.HashSet; | ||
| 6 | import java.util.Iterator; | ||
| 7 | import java.util.Map; | ||
| 8 | |||
| 9 | import org.semanticweb.HermiT.model.DLClause; | 3 | import org.semanticweb.HermiT.model.DLClause; |
| 10 | import org.semanticweb.owlapi.model.OWLAxiom; | 4 | import org.semanticweb.owlapi.model.OWLAxiom; |
| 11 | import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom; | 5 | import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom; |
| 12 | import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom; | 6 | import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom; |
| 13 | |||
| 14 | import uk.ac.ox.cs.pagoda.owl.OWLHelper; | 7 | import uk.ac.ox.cs.pagoda.owl.OWLHelper; |
| 8 | import uk.ac.ox.cs.pagoda.rules.approximators.Approximator; | ||
| 9 | |||
| 10 | import java.util.*; | ||
| 15 | 11 | ||
| 16 | public abstract class ApproxProgram extends Program { | 12 | public abstract class ApproxProgram extends Program { |
| 17 | 13 | ||
| 14 | protected Approximator m_approx = null; | ||
| 18 | /** | 15 | /** |
| 19 | * mapping from over-approximated DLClauses to DLClauses from the original ontology | 16 | * mapping from over-approximated DLClauses to DLClauses from the original ontology |
| 20 | */ | 17 | */ |
| 21 | Map<DLClause, Object> correspondence = new HashMap<DLClause, Object>(); | 18 | Map<DLClause, Object> correspondence = new HashMap<DLClause, Object>(); |
| 22 | 19 | ||
| 23 | protected Approximator m_approx = null; | ||
| 24 | |||
| 25 | protected ApproxProgram() { initApproximator(); } | 20 | protected ApproxProgram() { initApproximator(); } |
| 26 | 21 | ||
| 27 | protected abstract void initApproximator(); | 22 | protected abstract void initApproximator(); |
| @@ -76,7 +71,7 @@ public abstract class ApproxProgram extends Program { | |||
| 76 | 71 | ||
| 77 | public OWLAxiom getEquivalentAxiom(DLClause clause) { | 72 | public OWLAxiom getEquivalentAxiom(DLClause clause) { |
| 78 | Object obj = correspondence.get(clause); | 73 | Object obj = correspondence.get(clause); |
| 79 | while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey((DLClause) obj)) | 74 | while (obj != null && obj instanceof DLClause && !obj.equals(clause) && correspondence.containsKey(obj)) |
| 80 | obj = correspondence.get(clause); | 75 | obj = correspondence.get(clause); |
| 81 | if (obj instanceof OWLAxiom) | 76 | if (obj instanceof OWLAxiom) |
| 82 | return (OWLAxiom) obj; | 77 | return (OWLAxiom) obj; |
| @@ -98,14 +93,14 @@ public abstract class ApproxProgram extends Program { | |||
| 98 | 93 | ||
| 99 | class ClauseSet extends HashSet<DLClause> { | 94 | class ClauseSet extends HashSet<DLClause> { |
| 100 | 95 | ||
| 101 | public ClauseSet(DLClause first, DLClause second) { | ||
| 102 | add(first); | ||
| 103 | add(second); | ||
| 104 | } | ||
| 105 | |||
| 106 | /** | 96 | /** |
| 107 | * | 97 | * |
| 108 | */ | 98 | */ |
| 109 | private static final long serialVersionUID = 1L; | 99 | private static final long serialVersionUID = 1L; |
| 110 | 100 | ||
| 101 | public ClauseSet(DLClause first, DLClause second) { | ||
| 102 | add(first); | ||
| 103 | add(second); | ||
| 104 | } | ||
| 105 | |||
| 111 | } \ No newline at end of file | 106 | } \ 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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | ||
| 2 | |||
| 3 | import org.semanticweb.HermiT.model.AtLeast; | ||
| 4 | import org.semanticweb.HermiT.model.Atom; | ||
| 5 | import org.semanticweb.HermiT.model.DLClause; | ||
| 6 | import org.semanticweb.HermiT.model.DLPredicate; | ||
| 7 | |||
| 8 | import java.util.Collection; | ||
| 9 | import java.util.LinkedList; | ||
| 10 | |||
| 11 | public interface Approximator { | ||
| 12 | |||
| 13 | Collection<DLClause> convert(DLClause clause, DLClause originalClause); | ||
| 14 | |||
| 15 | } | ||
| 16 | |||
| 17 | class IgnoreExist implements Approximator { | ||
| 18 | |||
| 19 | @Override | ||
| 20 | public Collection<DLClause> convert(DLClause clause, DLClause originalClause) { | ||
| 21 | Collection<DLClause> ret = new LinkedList<DLClause>(); | ||
| 22 | DLPredicate p; | ||
| 23 | for (Atom headAtom: clause.getHeadAtoms()) { | ||
| 24 | p = headAtom.getDLPredicate(); | ||
| 25 | if (p instanceof AtLeast) return ret; | ||
| 26 | } | ||
| 27 | |||
| 28 | ret.add(clause); | ||
| 29 | return ret; | ||
| 30 | } | ||
| 31 | |||
| 32 | } | ||
| 33 | |||
| 34 | class IgnoreBoth implements Approximator { | ||
| 35 | |||
| 36 | @Override | ||
| 37 | public Collection<DLClause> convert(DLClause clause, DLClause originalClause) { | ||
| 38 | Collection<DLClause> ret = new LinkedList<DLClause>(); | ||
| 39 | |||
| 40 | if (clause.getHeadLength() > 1) return ret; | ||
| 41 | |||
| 42 | if (clause.getHeadLength() > 0) { | ||
| 43 | DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate(); | ||
| 44 | |||
| 45 | if (predicate instanceof AtLeast) return ret; | ||
| 46 | } | ||
| 47 | |||
| 48 | ret.add(clause); | ||
| 49 | return ret; | ||
| 50 | } | ||
| 51 | } | ||
| 52 | |||
| 53 | class IgnoreDisj implements Approximator { | ||
| 54 | |||
| 55 | @Override | ||
| 56 | public Collection<DLClause> convert(DLClause clause, DLClause originalClause) { | ||
| 57 | Collection<DLClause> ret = new LinkedList<DLClause>(); | ||
| 58 | if (clause.getHeadLength() > 1) return ret; | ||
| 59 | ret.add(clause); | ||
| 60 | return ret; | ||
| 61 | } | ||
| 62 | } | ||
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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules; |
| 2 | 2 | ||
| 3 | import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; | ||
| 4 | |||
| 3 | public class DisjunctiveProgram extends UpperProgram { | 5 | public class DisjunctiveProgram extends UpperProgram { |
| 4 | 6 | ||
| 5 | @Override | 7 | @Override |
| 6 | protected void initApproximator() { | 8 | protected void initApproximator() { |
| 7 | m_approx = new OverApproxExist(); | 9 | m_approx = new OverApproxExist(); |
| 8 | } | 10 | } |
| 9 | 11 | ||
| 10 | // @Override | 12 | // @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; | |||
| 2 | 2 | ||
| 3 | import org.semanticweb.HermiT.model.DLClause; | 3 | import org.semanticweb.HermiT.model.DLClause; |
| 4 | import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; | 4 | import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; |
| 5 | import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; | ||
| 6 | import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator; | ||
| 5 | 7 | ||
| 6 | import java.util.Collection; | 8 | import java.util.Collection; |
| 7 | 9 | ||
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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules; |
| 2 | 2 | ||
| 3 | import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxDisj; | ||
| 4 | |||
| 3 | public class ExistentialProgram extends UpperProgram { | 5 | public class ExistentialProgram extends UpperProgram { |
| 4 | 6 | ||
| 5 | // @Override | 7 | // @Override |
| @@ -12,7 +14,7 @@ public class ExistentialProgram extends UpperProgram { | |||
| 12 | 14 | ||
| 13 | @Override | 15 | @Override |
| 14 | protected void initApproximator() { | 16 | protected void initApproximator() { |
| 15 | m_approx = new OverApproxDisj(); | 17 | m_approx = new OverApproxDisj(); |
| 16 | } | 18 | } |
| 17 | 19 | ||
| 18 | } | 20 | } |
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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules; |
| 2 | 2 | ||
| 3 | import org.semanticweb.HermiT.model.*; | ||
| 4 | import org.semanticweb.owlapi.model.OWLObjectProperty; | ||
| 5 | import org.semanticweb.owlapi.model.OWLOntology; | ||
| 6 | import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; | ||
| 7 | import uk.ac.ox.cs.pagoda.rules.approximators.Approximator; | ||
| 8 | import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist; | ||
| 9 | |||
| 3 | import java.util.Collection; | 10 | import java.util.Collection; |
| 4 | import java.util.HashSet; | 11 | import java.util.HashSet; |
| 5 | import java.util.LinkedList; | 12 | import java.util.LinkedList; |
| 6 | import java.util.Set; | 13 | import java.util.Set; |
| 7 | 14 | ||
| 8 | import org.semanticweb.HermiT.model.AtLeastConcept; | ||
| 9 | import org.semanticweb.HermiT.model.Atom; | ||
| 10 | import org.semanticweb.HermiT.model.AtomicRole; | ||
| 11 | import org.semanticweb.HermiT.model.DLClause; | ||
| 12 | import org.semanticweb.HermiT.model.DLPredicate; | ||
| 13 | import org.semanticweb.owlapi.model.OWLObjectProperty; | ||
| 14 | import org.semanticweb.owlapi.model.OWLOntology; | ||
| 15 | import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; | ||
| 16 | |||
| 17 | public class ExistentialToDisjunctive extends UpperProgram { | 15 | public class ExistentialToDisjunctive extends UpperProgram { |
| 18 | 16 | ||
| 19 | Set<String> inverseFuncProperties = new HashSet<String>(); | 17 | Set<String> inverseFuncProperties = new HashSet<String>(); |
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; | |||
| 10 | import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom; | 10 | import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom; |
| 11 | import uk.ac.ox.cs.pagoda.multistage.Normalisation; | 11 | import uk.ac.ox.cs.pagoda.multistage.Normalisation; |
| 12 | import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication; | 12 | import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication; |
| 13 | import uk.ac.ox.cs.pagoda.rules.approximators.Approximator; | ||
| 13 | import uk.ac.ox.cs.pagoda.util.Timer; | 14 | import uk.ac.ox.cs.pagoda.util.Timer; |
| 14 | import uk.ac.ox.cs.pagoda.util.Utility; | 15 | import uk.ac.ox.cs.pagoda.util.Utility; |
| 15 | 16 | ||
| @@ -106,7 +107,26 @@ public class LowerDatalogProgram extends ApproxProgram implements IncrementalPro | |||
| 106 | 107 | ||
| 107 | @Override | 108 | @Override |
| 108 | protected void initApproximator() { | 109 | protected void initApproximator() { |
| 109 | m_approx = new IgnoreBoth(); | 110 | m_approx = new IgnoreBoth(); |
| 111 | } | ||
| 112 | |||
| 113 | private class IgnoreBoth implements Approximator { | ||
| 114 | |||
| 115 | @Override | ||
| 116 | public Collection<DLClause> convert(DLClause clause, DLClause originalClause) { | ||
| 117 | Collection<DLClause> ret = new LinkedList<DLClause>(); | ||
| 118 | |||
| 119 | if (clause.getHeadLength() > 1) return ret; | ||
| 120 | |||
| 121 | if (clause.getHeadLength() > 0) { | ||
| 122 | DLPredicate predicate = clause.getHeadAtom(0).getDLPredicate(); | ||
| 123 | |||
| 124 | if (predicate instanceof AtLeast) return ret; | ||
| 125 | } | ||
| 126 | |||
| 127 | ret.add(clause); | ||
| 128 | return ret; | ||
| 129 | } | ||
| 110 | } | 130 | } |
| 111 | 131 | ||
| 112 | } | 132 | } |
| @@ -116,15 +136,13 @@ class ClassifyThread extends Thread { | |||
| 116 | IncrementalProgram m_program; | 136 | IncrementalProgram m_program; |
| 117 | Collection<DLClause> clauses = new LinkedList<DLClause>(); | 137 | Collection<DLClause> clauses = new LinkedList<DLClause>(); |
| 118 | 138 | ||
| 119 | Variable X = Variable.create("X"), Y = Variable.create("Y"); | 139 | Variable X = Variable.create("X"), Y = Variable.create("Y"); |
| 120 | 140 | Reasoner hermitReasoner; | |
| 141 | OWLOntology ontology; | ||
| 121 | ClassifyThread(IncrementalProgram program) { | 142 | ClassifyThread(IncrementalProgram program) { |
| 122 | m_program = program; | 143 | m_program = program; |
| 123 | } | 144 | } |
| 124 | 145 | ||
| 125 | Reasoner hermitReasoner; | ||
| 126 | OWLOntology ontology; | ||
| 127 | |||
| 128 | @Override | 146 | @Override |
| 129 | public void run() { | 147 | public void run() { |
| 130 | ontology = m_program.getOntology(); | 148 | ontology = m_program.getOntology(); |
| @@ -215,5 +233,4 @@ class ClassifyThread extends Thread { | |||
| 215 | private Atom getAtom(OWLClass c) { | 233 | private Atom getAtom(OWLClass c) { |
| 216 | return Atom.create(AtomicConcept.create(c.toStringID()), X); | 234 | return Atom.create(AtomicConcept.create(c.toStringID()), X); |
| 217 | } | 235 | } |
| 218 | |||
| 219 | } \ No newline at end of file | 236 | } \ No newline at end of file |
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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules; |
| 2 | 2 | ||
| 3 | import org.semanticweb.HermiT.model.DLClause; | ||
| 4 | import org.semanticweb.HermiT.model.DLPredicate; | ||
| 5 | import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxBoth; | ||
| 6 | |||
| 3 | import java.util.Collection; | 7 | import java.util.Collection; |
| 4 | import java.util.HashMap; | 8 | import java.util.HashMap; |
| 5 | import java.util.Map; | 9 | import java.util.Map; |
| 6 | 10 | ||
| 7 | import org.semanticweb.HermiT.model.DLClause; | ||
| 8 | import org.semanticweb.HermiT.model.DLPredicate; | ||
| 9 | |||
| 10 | 11 | ||
| 11 | public class UpperDatalogProgram extends UpperProgram { | 12 | public class UpperDatalogProgram extends UpperProgram { |
| 12 | 13 | ||
| @@ -22,7 +23,7 @@ public class UpperDatalogProgram extends UpperProgram { | |||
| 22 | 23 | ||
| 23 | @Override | 24 | @Override |
| 24 | protected void initApproximator() { | 25 | protected void initApproximator() { |
| 25 | m_approx = new OverApproxBoth(); | 26 | m_approx = new OverApproxBoth(); |
| 26 | } | 27 | } |
| 27 | 28 | ||
| 28 | public int getBottomNumber() { | 29 | 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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules.approximators; | ||
| 2 | |||
| 3 | import org.semanticweb.HermiT.model.DLClause; | ||
| 4 | |||
| 5 | import java.util.Collection; | ||
| 6 | |||
| 7 | public interface Approximator { | ||
| 8 | |||
| 9 | Collection<DLClause> convert(DLClause clause, DLClause originalClause); | ||
| 10 | |||
| 11 | } | ||
| 12 | |||
| 13 | // TODO remove | ||
| 14 | //class IgnoreExist implements Approximator { | ||
| 15 | // | ||
| 16 | // @Override | ||
| 17 | // public Collection<DLClause> convert(DLClause clause, DLClause originalClause) { | ||
| 18 | // Collection<DLClause> ret = new LinkedList<DLClause>(); | ||
| 19 | // DLPredicate p; | ||
| 20 | // for (Atom headAtom: clause.getHeadAtoms()) { | ||
| 21 | // p = headAtom.getDLPredicate(); | ||
| 22 | // if (p instanceof AtLeast) return ret; | ||
| 23 | // } | ||
| 24 | // | ||
| 25 | // ret.add(clause); | ||
| 26 | // return ret; | ||
| 27 | // } | ||
| 28 | // | ||
| 29 | //} | ||
| 30 | // | ||
| 31 | // | ||
| 32 | // | ||
| 33 | //class IgnoreDisj implements Approximator { | ||
| 34 | // | ||
| 35 | // @Override | ||
| 36 | // public Collection<DLClause> convert(DLClause clause, DLClause originalClause) { | ||
| 37 | // Collection<DLClause> ret = new LinkedList<DLClause>(); | ||
| 38 | // if (clause.getHeadLength() > 1) return ret; | ||
| 39 | // ret.add(clause); | ||
| 40 | // return ret; | ||
| 41 | // } | ||
| 42 | //} | ||
diff --git a/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java index 284edd2..8fc6b77 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java | |||
| @@ -1,7 +1,8 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules.approximators; |
| 2 | 2 | ||
| 3 | import org.semanticweb.HermiT.model.DLClause; | 3 | import org.semanticweb.HermiT.model.DLClause; |
| 4 | import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; | 4 | import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; |
| 5 | import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; | ||
| 5 | 6 | ||
| 6 | import java.util.*; | 7 | import java.util.*; |
| 7 | 8 | ||
| @@ -62,6 +63,7 @@ public class LimitedSkolemisationApproximator implements TupleDependentApproxima | |||
| 62 | 63 | ||
| 63 | private DLClause getInstantiatedSkolemisation(DLClause clause, DLClause originalClause, AnswerTupleID violationTuple) { | 64 | private DLClause getInstantiatedSkolemisation(DLClause clause, DLClause originalClause, AnswerTupleID violationTuple) { |
| 64 | // TODO implement | 65 | // TODO implement |
| 66 | // filter the violation tuples appearing on both the sides of the rule | ||
| 65 | return null; | 67 | return null; |
| 66 | } | 68 | } |
| 67 | 69 | ||
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java index 3cc2aba..ae2a2cf 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java | |||
| @@ -1,11 +1,11 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules.approximators; |
| 2 | |||
| 3 | import java.util.Collection; | ||
| 4 | import java.util.LinkedList; | ||
| 5 | 2 | ||
| 6 | import org.semanticweb.HermiT.model.AtLeastDataRange; | 3 | import org.semanticweb.HermiT.model.AtLeastDataRange; |
| 7 | import org.semanticweb.HermiT.model.DLClause; | 4 | import org.semanticweb.HermiT.model.DLClause; |
| 8 | 5 | ||
| 6 | import java.util.Collection; | ||
| 7 | import java.util.LinkedList; | ||
| 8 | |||
| 9 | public class OverApproxBoth implements Approximator { | 9 | public class OverApproxBoth implements Approximator { |
| 10 | 10 | ||
| 11 | Approximator approxDist = new OverApproxDisj(), approxExist = new OverApproxExist(); | 11 | Approximator approxDist = new OverApproxDisj(), approxExist = new OverApproxExist(); |
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java index 5b298e8..05d9442 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java | |||
| @@ -1,4 +1,4 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules.approximators; |
| 2 | 2 | ||
| 3 | import org.semanticweb.HermiT.model.*; | 3 | import org.semanticweb.HermiT.model.*; |
| 4 | import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; | 4 | import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; |
| @@ -88,7 +88,7 @@ public class OverApproxDisj implements Approximator { | |||
| 88 | arguments[i] = rename(atom.getArgument(i), unifier); | 88 | arguments[i] = rename(atom.getArgument(i), unifier); |
| 89 | return Atom.create(atom.getDLPredicate(), arguments); | 89 | return Atom.create(atom.getDLPredicate(), arguments); |
| 90 | } | 90 | } |
| 91 | 91 | ||
| 92 | public static Term rename(Term argument, Map<Variable, Term> unifier) { | 92 | public static Term rename(Term argument, Map<Variable, Term> unifier) { |
| 93 | Term newArg; | 93 | Term newArg; |
| 94 | while ((newArg = unifier.get(argument)) != null) | 94 | while ((newArg = unifier.get(argument)) != null) |
diff --git a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java index 1099acf..e0bafe0 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java | |||
| @@ -1,4 +1,4 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules.approximators; |
| 2 | 2 | ||
| 3 | import org.semanticweb.HermiT.model.*; | 3 | import org.semanticweb.HermiT.model.*; |
| 4 | import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; | 4 | import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; |
| @@ -11,9 +11,11 @@ public class OverApproxExist implements Approximator { | |||
| 11 | public static final String negativeSuffix = "_neg"; | 11 | public static final String negativeSuffix = "_neg"; |
| 12 | public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; | 12 | public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; |
| 13 | private static final Variable X = Variable.create("X"); | 13 | private static final Variable X = Variable.create("X"); |
| 14 | //DEBUG | ||
| 15 | public static Collection<String> createdIndividualIRIs = new HashSet<>(); | ||
| 14 | private static int individualCounter = 0; | 16 | private static int individualCounter = 0; |
| 15 | private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>(); | 17 | private static Map<DLClause, Integer> individualNumber = new HashMap<DLClause, Integer>(); |
| 16 | 18 | ||
| 17 | private static int noOfExistential(DLClause originalClause) { | 19 | private static int noOfExistential(DLClause originalClause) { |
| 18 | int no = 0; | 20 | int no = 0; |
| 19 | for (Atom atom: originalClause.getHeadAtoms()) | 21 | for (Atom atom: originalClause.getHeadAtoms()) |
| @@ -42,7 +44,7 @@ public class OverApproxExist implements Approximator { | |||
| 42 | } | 44 | } |
| 43 | return -1; | 45 | return -1; |
| 44 | } | 46 | } |
| 45 | 47 | ||
| 46 | public static AtomicConcept getNegationConcept(DLPredicate p) { | 48 | public static AtomicConcept getNegationConcept(DLPredicate p) { |
| 47 | if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING; | 49 | if (p.equals(AtomicConcept.THING)) return AtomicConcept.NOTHING; |
| 48 | if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING; | 50 | if (p.equals(AtomicConcept.NOTHING)) return AtomicConcept.THING; |
| @@ -66,15 +68,19 @@ public class OverApproxExist implements Approximator { | |||
| 66 | public static int getNumberOfSkolemisedIndividual() { | 68 | public static int getNumberOfSkolemisedIndividual() { |
| 67 | return individualCounter; | 69 | return individualCounter; |
| 68 | } | 70 | } |
| 69 | 71 | //DEBUG | |
| 72 | |||
| 70 | public static Individual getNewIndividual(DLClause originalClause, int offset) { | 73 | public static Individual getNewIndividual(DLClause originalClause, int offset) { |
| 71 | Individual ret; | 74 | Individual ret; |
| 75 | int individualID; | ||
| 72 | if (individualNumber.containsKey(originalClause)) { | 76 | if (individualNumber.containsKey(originalClause)) { |
| 73 | ret = Individual.create(skolemisedIndividualPrefix + (individualNumber.get(originalClause) + offset)); | 77 | individualID = individualNumber.get(originalClause) + offset; |
| 78 | ret = Individual.create(skolemisedIndividualPrefix + individualID); | ||
| 74 | } | 79 | } |
| 75 | else { | 80 | else { |
| 76 | individualNumber.put(originalClause, individualCounter); | 81 | individualNumber.put(originalClause, individualCounter); |
| 77 | ret = Individual.create(skolemisedIndividualPrefix + (individualCounter + offset)); | 82 | individualID = individualCounter + offset; |
| 83 | ret = Individual.create(skolemisedIndividualPrefix + individualID); | ||
| 78 | individualCounter += noOfExistential(originalClause); | 84 | individualCounter += noOfExistential(originalClause); |
| 79 | } | 85 | } |
| 80 | return ret; | 86 | return ret; |
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 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules.approximators; | ||
| 2 | |||
| 3 | import org.semanticweb.HermiT.model.AtLeast; | ||
| 4 | import org.semanticweb.HermiT.model.Atom; | ||
| 5 | import org.semanticweb.HermiT.model.DLClause; | ||
| 6 | import org.semanticweb.HermiT.model.Individual; | ||
| 7 | import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; | ||
| 8 | import uk.ac.ox.cs.pagoda.util.Namespace; | ||
| 9 | |||
| 10 | import java.util.HashMap; | ||
| 11 | import java.util.Map; | ||
| 12 | |||
| 13 | /** | ||
| 14 | * If you need a Skolem term (i.e. fresh individual), ask this class. | ||
| 15 | */ | ||
| 16 | public class SkolemTermsDispenser { | ||
| 17 | |||
| 18 | public static final String skolemisedIndividualPrefix = Namespace.PAGODA_ANONY + "individual"; | ||
| 19 | private static SkolemTermsDispenser skolemTermsDispenser; | ||
| 20 | private int individualCounter = 0; | ||
| 21 | private Map<DLClause, Integer> termNumber = new HashMap<>(); | ||
| 22 | private Map<SkolemTermId, Integer> mapTermToDepth = new HashMap<>(); | ||
| 23 | private int dependenciesCounter = 0; | ||
| 24 | private Map<AnswerTupleID, Integer> mapDependencyToId = new HashMap<>(); | ||
| 25 | |||
| 26 | private SkolemTermsDispenser() { | ||
| 27 | } | ||
| 28 | |||
| 29 | public static SkolemTermsDispenser getInstance() { | ||
| 30 | if (skolemTermsDispenser == null) skolemTermsDispenser = new SkolemTermsDispenser(); | ||
| 31 | return skolemTermsDispenser; | ||
| 32 | } | ||
| 33 | |||
| 34 | private int getDependencyId(AnswerTupleID answerTupleID) { | ||
| 35 | if (mapDependencyToId.containsKey(answerTupleID)) return mapDependencyToId.get(answerTupleID); | ||
| 36 | else return mapDependencyToId.put(answerTupleID, dependenciesCounter++); | ||
| 37 | } | ||
| 38 | |||
| 39 | public Individual getNewIndividual(DLClause originalClause, int offset, AnswerTupleID dependency) { | ||
| 40 | if (!termNumber.containsKey(originalClause)) { | ||
| 41 | termNumber.put(originalClause, individualCounter); | ||
| 42 | individualCounter += noOfExistential(originalClause); | ||
| 43 | } | ||
| 44 | if (!mapDependencyToId.containsKey(dependency)) { | ||
| 45 | mapDependencyToId.put(dependency, dependenciesCounter++); | ||
| 46 | } | ||
| 47 | |||
| 48 | SkolemTermId termId = new SkolemTermId(termNumber.get(originalClause) + offset, getDependencyId(dependency)); | ||
| 49 | return Individual.create(skolemisedIndividualPrefix + termId); | ||
| 50 | } | ||
| 51 | |||
| 52 | private int noOfExistential(DLClause originalClause) { | ||
| 53 | int no = 0; | ||
| 54 | for (Atom atom : originalClause.getHeadAtoms()) | ||
| 55 | if (atom.getDLPredicate() instanceof AtLeast) | ||
| 56 | no += ((AtLeast) atom.getDLPredicate()).getNumber(); | ||
| 57 | return no; | ||
| 58 | } | ||
| 59 | |||
| 60 | private class SkolemTermId { | ||
| 61 | private final int idBase; | ||
| 62 | private final int idOffset; | ||
| 63 | |||
| 64 | private SkolemTermId(int idBase, int idOffset) { | ||
| 65 | this.idBase = idBase; | ||
| 66 | this.idOffset = idOffset; | ||
| 67 | } | ||
| 68 | |||
| 69 | @Override | ||
| 70 | public String toString() { | ||
| 71 | return idBase + "_" + idOffset; | ||
| 72 | } | ||
| 73 | } | ||
| 74 | } | ||
diff --git a/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java index 63057c4..1a729e5 100644 --- a/src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java +++ b/src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java | |||
| @@ -1,4 +1,4 @@ | |||
| 1 | package uk.ac.ox.cs.pagoda.rules; | 1 | package uk.ac.ox.cs.pagoda.rules.approximators; |
| 2 | 2 | ||
| 3 | import org.semanticweb.HermiT.model.DLClause; | 3 | import org.semanticweb.HermiT.model.DLClause; |
| 4 | import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; | 4 | import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; |
