aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox
diff options
context:
space:
mode:
authorRncLsn <rnc.lsn@gmail.com>2015-05-13 11:57:06 +0100
committerRncLsn <rnc.lsn@gmail.com>2015-05-13 11:57:06 +0100
commit7e0ecc07285209e65f9d4d022065d06a4997fc86 (patch)
tree3c3faa6684e49444c7078903d2e5762fc44bb3a6 /src/uk/ac/ox
parent0c2726db44b562cbda9bfa87e76d829927c31ec8 (diff)
downloadACQuA-7e0ecc07285209e65f9d4d022065d06a4997fc86.tar.gz
ACQuA-7e0ecc07285209e65f9d4d022065d06a4997fc86.zip
Implementing Limited Skolemisation, in particular SkolemTermsDispenser.
Diffstat (limited to 'src/uk/ac/ox')
-rw-r--r--src/uk/ac/ox/cs/pagoda/constraints/PredicateDependency.java138
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/FoldedApplication.java8
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/IndividualCollector.java15
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/LimitedSkolemisationApplication.java2
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/MultiStageUpperProgram.java4
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/Normalisation.java374
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/TwoStageApplication.java57
-rw-r--r--src/uk/ac/ox/cs/pagoda/multistage/treatement/Pick4NegativeConceptQuerySpecific.java20
-rw-r--r--src/uk/ac/ox/cs/pagoda/reasoner/light/DLPredicateComparator.java6
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/ApproxProgram.java31
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/Approximator.java62
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/DisjunctiveProgram.java4
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/ExistConstantApproximator.java2
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/ExistentialProgram.java4
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/ExistentialToDisjunctive.java16
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/LowerDatalogProgram.java31
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/UpperDatalogProgram.java9
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/Approximator.java42
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/LimitedSkolemisationApproximator.java (renamed from src/uk/ac/ox/cs/pagoda/rules/LimitedSkolemisationApproximator.java)4
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxBoth.java (renamed from src/uk/ac/ox/cs/pagoda/rules/OverApproxBoth.java)8
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxDisj.java (renamed from src/uk/ac/ox/cs/pagoda/rules/OverApproxDisj.java)4
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/OverApproxExist.java (renamed from src/uk/ac/ox/cs/pagoda/rules/OverApproxExist.java)18
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/SkolemTermsDispenser.java74
-rw-r--r--src/uk/ac/ox/cs/pagoda/rules/approximators/TupleDependentApproximator.java (renamed from src/uk/ac/ox/cs/pagoda/rules/TupleDependentApproximator.java)2
-rw-r--r--src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj.java24
-rw-r--r--src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj1.java20
-rw-r--r--src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisj2.java18
-rw-r--r--src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java42
-rw-r--r--src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar2.java32
29 files changed, 492 insertions, 579 deletions
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 @@
1package uk.ac.ox.cs.pagoda.constraints; 1package uk.ac.ox.cs.pagoda.constraints;
2 2
3import java.util.Collection; 3import org.semanticweb.HermiT.model.*;
4import java.util.HashMap; 4import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
5import java.util.HashSet;
6import java.util.LinkedList;
7import java.util.Map;
8import java.util.Queue;
9import java.util.Set;
10
11import org.semanticweb.HermiT.model.AnnotatedEquality;
12import org.semanticweb.HermiT.model.AtLeastConcept;
13import org.semanticweb.HermiT.model.AtLeastDataRange;
14import org.semanticweb.HermiT.model.Atom;
15import org.semanticweb.HermiT.model.AtomicConcept;
16import org.semanticweb.HermiT.model.AtomicNegationConcept;
17import org.semanticweb.HermiT.model.AtomicRole;
18import org.semanticweb.HermiT.model.DLClause;
19import org.semanticweb.HermiT.model.DLPredicate;
20import org.semanticweb.HermiT.model.Equality;
21import org.semanticweb.HermiT.model.Inequality;
22import org.semanticweb.HermiT.model.InverseRole;
23
24import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
25import uk.ac.ox.cs.pagoda.util.Namespace; 5import uk.ac.ox.cs.pagoda.util.Namespace;
26import uk.ac.ox.cs.pagoda.util.Utility; 6import uk.ac.ox.cs.pagoda.util.Utility;
27 7
8import java.util.*;
9
28 10
29public class PredicateDependency extends DependencyGraph<DLPredicate> { 11public class PredicateDependency extends DependencyGraph<DLPredicate> {
30 12
31 Collection<DLClause> m_clauses; 13 private static final DLPredicate equality = AtomicRole.create(Namespace.EQUALITY);
32 Map<PredicatePair, LinkedList<DLClause>> edgeLabels = new HashMap<PredicatePair, LinkedList<DLClause>>(); 14 private static final DLPredicate inequality = AtomicRole.create(Namespace.INEQUALITY);
33 15 Collection<DLClause> m_clauses;
16 Map<PredicatePair, LinkedList<DLClause>> edgeLabels = new HashMap<PredicatePair, LinkedList<DLClause>>();
17 Set<DLPredicate> reachableToBottom = null;
18
34 public PredicateDependency(Collection<DLClause> clauses) { 19 public PredicateDependency(Collection<DLClause> clauses) {
35 m_clauses = clauses; 20 m_clauses = clauses;
36 build(); 21 build();
37 } 22 }
38 23
39 @Override 24 @Override
40 protected void build() { 25 protected void build() {
41 update(m_clauses); 26 update(m_clauses);
42 27
43 addLink(equality, AtomicConcept.NOTHING); 28 addLink(equality, AtomicConcept.NOTHING);
44 addLink(inequality, AtomicConcept.NOTHING); 29 addLink(inequality, AtomicConcept.NOTHING);
45 } 30 }
46 31
47 private void addEdgeLabel(DLPredicate body, DLPredicate head, DLClause clause) { 32 private void addEdgeLabel(DLPredicate body, DLPredicate head, DLClause clause) {
48 PredicatePair key = new PredicatePair(body, head); 33 PredicatePair key = new PredicatePair(body, head);
49 LinkedList<DLClause> value; 34 LinkedList<DLClause> value;
50 if ((value = edgeLabels.get(key)) == null) 35 if ((value = edgeLabels.get(key)) == null)
51 edgeLabels.put(key, value = new LinkedList<DLClause>()); 36 edgeLabels.put(key, value = new LinkedList<DLClause>());
52 value.add(clause); 37 value.add(clause);
53 } 38 }
54 39
55 private void addLinks4Negation(AtomicConcept c, DLClause clause) { 40 private void addLinks4Negation(AtomicConcept c, DLClause clause) {
56 addLink(c, AtomicConcept.NOTHING); 41 addLink(c, AtomicConcept.NOTHING);
57 addEdgeLabel(c, AtomicConcept.NOTHING, clause); 42 addEdgeLabel(c, AtomicConcept.NOTHING, clause);
58 String iri = c.getIRI(); 43 String iri = c.getIRI();
59 addLink(c = AtomicConcept.create(iri.substring(0, iri.length() - 4)), AtomicConcept.NOTHING); 44 addLink(c = AtomicConcept.create(iri.substring(0, iri.length() - 4)), AtomicConcept.NOTHING);
60 addEdgeLabel(c, AtomicConcept.NOTHING, clause); 45 addEdgeLabel(c, AtomicConcept.NOTHING, clause);
61 } 46 }
62 47
63 public Set<DLPredicate> collectPredicate(Atom[] atoms) { 48 public Set<DLPredicate> collectPredicate(Atom[] atoms) {
64 Set<DLPredicate> predicates = new HashSet<DLPredicate>(); 49 Set<DLPredicate> predicates = new HashSet<DLPredicate>();
65 for (Atom atom: atoms) 50 for (Atom atom : atoms)
66 predicates.addAll(getAtomicPredicates(atom.getDLPredicate())); 51 predicates.addAll(getAtomicPredicates(atom.getDLPredicate()));
67 return predicates; 52 return predicates;
68 } 53 }
69
70 private static final DLPredicate equality = AtomicRole.create(Namespace.EQUALITY);
71 private static final DLPredicate inequality = AtomicRole.create(Namespace.INEQUALITY);
72 54
73 private Set<DLPredicate> getAtomicPredicates(DLPredicate predicate) { 55 private Set<DLPredicate> getAtomicPredicates(DLPredicate predicate) {
74 Set<DLPredicate> predicates = new HashSet<DLPredicate>(); 56 Set<DLPredicate> predicates = new HashSet<DLPredicate>();
75 if (predicate instanceof AtLeastConcept) 57 if (predicate instanceof AtLeastConcept)
76 predicates.addAll(getAtomicPredicates((AtLeastConcept) predicate)); 58 predicates.addAll(getAtomicPredicates((AtLeastConcept) predicate));
77 else { 59 else {
78 if ((predicate = getAtomicPredicate(predicate)) != null) 60 if ((predicate = getAtomicPredicate(predicate)) != null)
79 predicates.add(predicate); 61 predicates.add(predicate);
80 } 62 }
81 return predicates; 63 return predicates;
82 } 64 }
83 65
84 private Set<DLPredicate> getAtomicPredicates(AtLeastConcept alc) { 66 private Set<DLPredicate> getAtomicPredicates(AtLeastConcept alc) {
85 Set<DLPredicate> set = new HashSet<DLPredicate>(); 67 Set<DLPredicate> set = new HashSet<DLPredicate>();
86 if (alc.getOnRole() instanceof AtomicRole) 68 if (alc.getOnRole() instanceof AtomicRole)
87 set.add((AtomicRole) alc.getOnRole()); 69 set.add((AtomicRole) alc.getOnRole());
88 else 70 else
89 set.add(((InverseRole) alc.getOnRole()).getInverseOf()); 71 set.add(((InverseRole) alc.getOnRole()).getInverseOf());
90 72
91 if (alc.getToConcept() instanceof AtomicConcept) 73 if (alc.getToConcept() instanceof AtomicConcept)
92 if (alc.getToConcept().equals(AtomicConcept.THING)); 74 if (alc.getToConcept().equals(AtomicConcept.THING)) ;
93 else set.add((AtomicConcept) alc.getToConcept()); 75 else set.add((AtomicConcept) alc.getToConcept());
94 else 76 else
95 set.add(OverApproxExist.getNegationConcept(((AtomicNegationConcept) alc.getToConcept()).getNegatedAtomicConcept())); 77 set.add(OverApproxExist.getNegationConcept(((AtomicNegationConcept) alc.getToConcept()).getNegatedAtomicConcept()));
96 return set; 78 return set;
97 } 79 }
98 80
99 private DLPredicate getAtomicPredicate(DLPredicate p) { 81 private DLPredicate getAtomicPredicate(DLPredicate p) {
100 if (p instanceof Equality || p instanceof AnnotatedEquality) 82 if (p instanceof Equality || p instanceof AnnotatedEquality)
101 return equality; 83 return equality;
102 if (p instanceof Inequality) 84 if (p instanceof Inequality)
103 return inequality; 85 return inequality;
104 if (p instanceof AtomicConcept) 86 if (p instanceof AtomicConcept)
105 if (p.equals(AtomicConcept.THING)) 87 if (p.equals(AtomicConcept.THING))
106 return null; 88 return null;
107 else return p; 89 else return p;
108 if (p instanceof AtomicRole) 90 if (p instanceof AtomicRole)
109 return p; 91 return p;
110 if (p instanceof AtLeastDataRange) { 92 if (p instanceof AtLeastDataRange) {
111 AtLeastDataRange aldr = (AtLeastDataRange) p; 93 AtLeastDataRange aldr = (AtLeastDataRange) p;
112 if (aldr.getOnRole() instanceof AtomicRole) 94 if (aldr.getOnRole() instanceof AtomicRole)
113 return (AtomicRole) aldr.getOnRole(); 95 return (AtomicRole) aldr.getOnRole();
114 else 96 else
115 return ((InverseRole) aldr.getOnRole()).getInverseOf(); 97 return ((InverseRole) aldr.getOnRole()).getInverseOf();
116 } 98 }
117 Utility.logDebug("Unknown DLPredicate in PredicateDependency: " + p); 99 Utility.logDebug("Unknown DLPredicate in PredicateDependency: " + p);
118 return null; 100 return null;
119 } 101 }
120 102
121 public Set<DLClause> pathTo(DLPredicate p) { 103 public Set<DLClause> pathTo(DLPredicate p) {
122 Set<DLClause> rules = new HashSet<DLClause>(); 104 Set<DLClause> rules = new HashSet<DLClause>();
123 Set<DLPredicate> visited = new HashSet<DLPredicate>(); 105 Set<DLPredicate> visited = new HashSet<DLPredicate>();
124 106
125 Queue<DLPredicate> queue = new LinkedList<DLPredicate>(); 107 Queue<DLPredicate> queue = new LinkedList<DLPredicate>();
126 queue.add(p); 108 queue.add(p);
127 visited.add(p); 109 visited.add(p);
128 110
129 Set<DLPredicate> edge; 111 Set<DLPredicate> edge;
130 Collection<DLClause> clauses; 112 Collection<DLClause> clauses;
131 113
132 while (!queue.isEmpty()) { 114 while (!queue.isEmpty()) {
133 if ((edge = reverseEdges.get(p = queue.poll())) != null) { 115 if ((edge = reverseEdges.get(p = queue.poll())) != null) {
134 for (DLPredicate pred: edge) { 116 for (DLPredicate pred: edge) {
135 if (!visited.contains(pred)) { 117 if (!visited.contains(pred)) {
136 queue.add(pred); 118 queue.add(pred);
137 visited.add(pred); 119 visited.add(pred);
138 } 120 }
139 clauses = edgeLabelsBetween(pred, p); 121 clauses = edgeLabelsBetween(pred, p);
140 if (clauses != null) rules.addAll(clauses); 122 if (clauses != null) rules.addAll(clauses);
141 } 123 }
142 } 124 }
143 } 125 }
144 return rules; 126 return rules;
145 } 127 }
146 128
147 private LinkedList<DLClause> edgeLabelsBetween(DLPredicate p, DLPredicate q) { 129 private LinkedList<DLClause> edgeLabelsBetween(DLPredicate p, DLPredicate q) {
148 PredicatePair pair = new PredicatePair(p, q); 130 PredicatePair pair = new PredicatePair(p, q);
149 return edgeLabels.get(pair); 131 return edgeLabels.get(pair);
150 } 132 }
151
152 Set<DLPredicate> reachableToBottom = null;
153 133
154 public Set<DLClause> pathToBottom(DLPredicate p) { 134 public Set<DLClause> pathToBottom(DLPredicate p) {
155 if (reachableToBottom == null) { 135 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 @@
1package uk.ac.ox.cs.pagoda.multistage; 1package uk.ac.ox.cs.pagoda.multistage;
2 2
3import java.util.Collection;
4import java.util.LinkedList;
5
6import org.semanticweb.HermiT.model.DLClause; 3import org.semanticweb.HermiT.model.DLClause;
7import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; 4import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
8import uk.ac.ox.cs.pagoda.rules.OverApproxDisj;
9import uk.ac.ox.cs.pagoda.rules.Program; 5import uk.ac.ox.cs.pagoda.rules.Program;
6import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxDisj;
10import uk.ac.ox.cs.pagoda.util.Timer; 7import uk.ac.ox.cs.pagoda.util.Timer;
11 8
9import java.util.Collection;
10import java.util.LinkedList;
11
12public class FoldedApplication extends MultiStageUpperProgram { 12public class FoldedApplication extends MultiStageUpperProgram {
13 13
14 public FoldedApplication(Program program, BottomStrategy upperBottom) { 14 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 @@
1package uk.ac.ox.cs.pagoda.multistage; 1package uk.ac.ox.cs.pagoda.multistage;
2 2
3import java.util.Collection;
4import java.util.HashSet;
5import java.util.Set;
6
7import org.openrdf.model.Resource; 3import org.openrdf.model.Resource;
8import org.openrdf.model.Statement; 4import org.openrdf.model.Statement;
9import org.openrdf.model.Value; 5import org.openrdf.model.Value;
10import org.openrdf.model.impl.URIImpl; 6import org.openrdf.model.impl.URIImpl;
11import org.openrdf.rio.RDFHandler; 7import org.openrdf.rio.RDFHandler;
12import org.openrdf.rio.RDFHandlerException; 8import org.openrdf.rio.RDFHandlerException;
13
14import uk.ac.ox.cs.JRDFox.model.Individual; 9import uk.ac.ox.cs.JRDFox.model.Individual;
15import uk.ac.ox.cs.pagoda.rules.OverApproxExist; 10import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
16import uk.ac.ox.cs.pagoda.util.Namespace; 11import uk.ac.ox.cs.pagoda.util.Namespace;
17 12
13import java.util.Collection;
14import java.util.HashSet;
15import java.util.Set;
16
18public class IndividualCollector implements RDFHandler { 17public class IndividualCollector implements RDFHandler {
19 18
20 boolean addedSkolemised = false; 19 boolean addedSkolemised = false;
@@ -43,11 +42,11 @@ public class IndividualCollector implements RDFHandler {
43 public void handleStatement(Statement st) throws RDFHandlerException { 42 public void handleStatement(Statement st) throws RDFHandlerException {
44 Resource sub = st.getSubject(); 43 Resource sub = st.getSubject();
45 if (sub instanceof URIImpl) 44 if (sub instanceof URIImpl)
46 individuals.add(Individual.create(((URIImpl) sub).toString())); 45 individuals.add(Individual.create(sub.toString()));
47 if (!st.getPredicate().toString().equals(Namespace.RDF_TYPE)) { 46 if (!st.getPredicate().toString().equals(Namespace.RDF_TYPE)) {
48 Value obj = st.getObject(); 47 Value obj = st.getObject();
49 if (obj instanceof URIImpl) 48 if (obj instanceof URIImpl)
50 individuals.add(Individual.create(((URIImpl) sub).toString())); 49 individuals.add(Individual.create(sub.toString()));
51 } 50 }
52 } 51 }
53 52
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;
3 3
4import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; 4import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
5import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; 5import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
6import uk.ac.ox.cs.pagoda.rules.LimitedSkolemisationApproximator;
7import uk.ac.ox.cs.pagoda.rules.Program; 6import uk.ac.ox.cs.pagoda.rules.Program;
7import uk.ac.ox.cs.pagoda.rules.approximators.LimitedSkolemisationApproximator;
8 8
9public class LimitedSkolemisationApplication extends RestrictedApplication { 9public class LimitedSkolemisationApplication extends RestrictedApplication {
10 10
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;
8import uk.ac.ox.cs.pagoda.hermit.RuleHelper; 8import uk.ac.ox.cs.pagoda.hermit.RuleHelper;
9import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager; 9import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager;
10import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator; 10import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
11import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
12import uk.ac.ox.cs.pagoda.rules.Program; 11import uk.ac.ox.cs.pagoda.rules.Program;
13import uk.ac.ox.cs.pagoda.rules.TupleDependentApproximator; 12import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
13import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator;
14import uk.ac.ox.cs.pagoda.util.Namespace; 14import uk.ac.ox.cs.pagoda.util.Namespace;
15import uk.ac.ox.cs.pagoda.util.SparqlHelper; 15import uk.ac.ox.cs.pagoda.util.SparqlHelper;
16import uk.ac.ox.cs.pagoda.util.Timer; 16import 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 @@
1package uk.ac.ox.cs.pagoda.multistage; 1package uk.ac.ox.cs.pagoda.multistage;
2 2
3import java.util.Collection; 3import org.semanticweb.HermiT.model.*;
4import java.util.HashMap; 4import org.semanticweb.owlapi.model.*;
5import java.util.HashSet;
6import java.util.Iterator;
7import java.util.LinkedList;
8import java.util.Map;
9import java.util.Set;
10
11import org.semanticweb.HermiT.model.AtLeast;
12import org.semanticweb.HermiT.model.AtLeastConcept;
13import org.semanticweb.HermiT.model.AtLeastDataRange;
14import org.semanticweb.HermiT.model.Atom;
15import org.semanticweb.HermiT.model.AtomicConcept;
16import org.semanticweb.HermiT.model.AtomicNegationConcept;
17import org.semanticweb.HermiT.model.AtomicRole;
18import org.semanticweb.HermiT.model.Constant;
19import org.semanticweb.HermiT.model.ConstantEnumeration;
20import org.semanticweb.HermiT.model.DLClause;
21import org.semanticweb.HermiT.model.Individual;
22import org.semanticweb.HermiT.model.Inequality;
23import org.semanticweb.HermiT.model.InverseRole;
24import org.semanticweb.HermiT.model.LiteralConcept;
25import org.semanticweb.HermiT.model.Role;
26import org.semanticweb.HermiT.model.Variable;
27import org.semanticweb.owlapi.model.OWLClass;
28import org.semanticweb.owlapi.model.OWLClassExpression;
29import org.semanticweb.owlapi.model.OWLDataHasValue;
30import org.semanticweb.owlapi.model.OWLDataProperty;
31import org.semanticweb.owlapi.model.OWLDataPropertyExpression;
32import org.semanticweb.owlapi.model.OWLLiteral;
33import org.semanticweb.owlapi.model.OWLObjectHasSelf;
34import org.semanticweb.owlapi.model.OWLObjectInverseOf;
35import org.semanticweb.owlapi.model.OWLObjectMinCardinality;
36import org.semanticweb.owlapi.model.OWLObjectProperty;
37import org.semanticweb.owlapi.model.OWLObjectPropertyExpression;
38import org.semanticweb.owlapi.model.OWLObjectSomeValuesFrom;
39import org.semanticweb.owlapi.model.OWLOntology;
40
41import uk.ac.ox.cs.pagoda.MyPrefixes; 5import uk.ac.ox.cs.pagoda.MyPrefixes;
42import uk.ac.ox.cs.pagoda.approx.Clause; 6import uk.ac.ox.cs.pagoda.approx.Clause;
43import uk.ac.ox.cs.pagoda.approx.Clausifier; 7import uk.ac.ox.cs.pagoda.approx.Clausifier;
44import uk.ac.ox.cs.pagoda.constraints.BottomStrategy; 8import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
45import uk.ac.ox.cs.pagoda.rules.OverApproxExist; 9import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
46import uk.ac.ox.cs.pagoda.util.Namespace; 10import uk.ac.ox.cs.pagoda.util.Namespace;
47import uk.ac.ox.cs.pagoda.util.Utility; 11import uk.ac.ox.cs.pagoda.util.Utility;
48 12
13import java.util.*;
14
49public class Normalisation { 15public class Normalisation {
50 16
51// MultiStageUpperProgram m_program; 17 public static final String auxiliaryConceptPrefix = Namespace.PAGODA_AUX + "concept_";
18 private static final Variable X = Variable.create("X"), Y = Variable.create("Y");
19 // MultiStageUpperProgram m_program;
52 OWLOntology m_ontology; 20 OWLOntology m_ontology;
53 BottomStrategy m_botStrategy; 21 BottomStrategy m_botStrategy;
54 Collection<DLClause> m_rules; 22 Collection<DLClause> m_rules;
55 Set<DLClause> m_normClauses = new HashSet<DLClause>(); 23 Set<DLClause> m_normClauses = new HashSet<DLClause>();
56 Map<DLClause, DLClause> exist2original = new HashMap<DLClause, DLClause>(); 24 Map<DLClause, DLClause> exist2original = new HashMap<DLClause, DLClause>();
57 25 Map<String, AtLeastConcept> rightAuxiliaryConcept = new HashMap<String, AtLeastConcept>();
26 private Map<AtLeastConcept, AtomicConcept> leftAuxiliaryConcept = new HashMap<AtLeastConcept, AtomicConcept>();
27 private Map<AtomicConcept, AtLeastConcept> leftAuxiliaryConcept_inv = new HashMap<AtomicConcept, AtLeastConcept>();
28
29 public Normalisation(Collection<DLClause> rules, OWLOntology ontology, BottomStrategy botStrategy) {
30// m_program = program;
31 m_ontology = ontology;
32 m_rules = rules;
33 m_botStrategy = botStrategy;
34 }
35
36 public static AtLeastConcept toAtLeastConcept(AtLeast p) {
37 if (p instanceof AtLeastConcept) return (AtLeastConcept) p;
38 AtLeastDataRange aldr = (AtLeastDataRange) p;
39 return AtLeastConcept.create(aldr.getNumber(), aldr.getOnRole(), AtomicConcept.create(MyPrefixes.PAGOdAPrefixes.expandIRI(aldr.getToDataRange().toString())));
40 }
41
42 private static String getName(String iri) {
43 int index = iri.lastIndexOf("#");
44 if (index != -1) return iri.substring(index + 1);
45 index = iri.lastIndexOf("/");
46 if (index != -1) return iri.substring(index + 1);
47 return iri;
48 }
49
50 public static String getAuxiliaryConcept4Disjunct(AtLeastConcept alc, Individual... individuals) {
51 Role r = alc.getOnRole();
52 LiteralConcept c = alc.getToConcept();
53 StringBuilder builder = new StringBuilder(auxiliaryConceptPrefix);
54 if (r instanceof AtomicRole)
55 builder.append(getName(((AtomicRole) r).getIRI()));
56 else
57 builder.append(getName(((InverseRole) r).getInverseOf().getIRI())).append("_inv");
58
59 if (alc.getNumber() > 1)
60 builder.append("_").append(alc.getNumber());
61
62 if (c instanceof AtomicConcept) {
63 if (!c.equals(AtomicConcept.THING))
64 builder.append("_").append(getName(((AtomicConcept) c).getIRI()));
65 } else
66 builder.append("_").append(getName((OverApproxExist.getNegationConcept(((AtomicNegationConcept) c).getNegatedAtomicConcept()).getIRI())));
67
68 if (individuals.length > 1)
69 builder.append("_").append(getName(individuals[0].getIRI()));
70
71 builder.append("_exist");
72
73 return builder.toString();
74 }
75
58 public Set<DLClause> getNormlisedClauses() { 76 public Set<DLClause> getNormlisedClauses() {
59 return m_normClauses; 77 return m_normClauses;
60 } 78 }
61 79
62 public Normalisation(Collection<DLClause> rules, OWLOntology ontology, BottomStrategy botStrategy) {
63// m_program = program;
64 m_ontology = ontology;
65 m_rules = rules;
66 m_botStrategy = botStrategy;
67 }
68
69 public void process() { 80 public void process() {
70 for (DLClause clause: m_rules) 81 for (DLClause clause : m_rules)
71 if (m_botStrategy.isBottomRule(clause)) 82 if (m_botStrategy.isBottomRule(clause))
72 processBottomRule(clause); 83 processBottomRule(clause);
73 else if (clause.getHeadLength() == 1) { 84 else if (clause.getHeadLength() == 1) {
74 if (clause.getHeadAtom(0).getDLPredicate() instanceof AtLeast) 85 if (clause.getHeadAtom(0).getDLPredicate() instanceof AtLeast)
75 processExistentialRule(clause); 86 processExistentialRule(clause);
76 else 87 else
77 m_normClauses.add(clause); 88 m_normClauses.add(clause);
78 } 89 } else
79 else
80 processDisjunctiveRule(clause); 90 processDisjunctiveRule(clause);
81 } 91 }
82 92
@@ -85,75 +95,68 @@ public class Normalisation {
85 m_normClauses.add(clause); 95 m_normClauses.add(clause);
86 return ; 96 return ;
87 } 97 }
88 98
89 Atom headAtom = clause.getHeadAtom(0); 99 Atom headAtom = clause.getHeadAtom(0);
90 if (headAtom.getDLPredicate() instanceof AtLeastDataRange) { 100 if (headAtom.getDLPredicate() instanceof AtLeastDataRange) {
91 m_normClauses.add(clause); 101 m_normClauses.add(clause);
92 return ; 102 return ;
93 } 103 }
94 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate(); 104 AtLeastConcept alc = (AtLeastConcept) headAtom.getDLPredicate();
95 AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); 105 AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0));
96 DLClause newClause; 106 DLClause newClause;
97 m_normClauses.add(DLClause.create(new Atom[] {Atom.create(ac, headAtom.getArgument(0)) }, clause.getBodyAtoms())); 107 m_normClauses.add(DLClause.create(new Atom[] {Atom.create(ac, headAtom.getArgument(0)) }, clause.getBodyAtoms()));
98 m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, X)}, new Atom[] {Atom.create(ac, X)})); 108 m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, X)}, new Atom[] {Atom.create(ac, X)}));
99 exist2original.put(newClause, clause); 109 exist2original.put(newClause, clause);
100 }
101
102 public static AtLeastConcept toAtLeastConcept(AtLeast p) {
103 if (p instanceof AtLeastConcept) return (AtLeastConcept) p;
104 AtLeastDataRange aldr = (AtLeastDataRange) p;
105 return AtLeastConcept.create(aldr.getNumber(), aldr.getOnRole(), AtomicConcept.create(MyPrefixes.PAGOdAPrefixes.expandIRI(aldr.getToDataRange().toString())));
106 } 110 }
107 111
108 private void processDisjunctiveRule(DLClause clause) { 112 private void processDisjunctiveRule(DLClause clause) {
109 boolean toNormalise = false; 113 boolean toNormalise = false;
110 for (Atom atom: clause.getHeadAtoms()) 114 for (Atom atom: clause.getHeadAtoms())
111 if (!(atom.getDLPredicate() instanceof AtomicConcept)) { 115 if (!(atom.getDLPredicate() instanceof AtomicConcept)) {
112 toNormalise = true; 116 toNormalise = true;
113 break; 117 break;
114 } 118 }
115 119
116 if (!toNormalise) { 120 if (!toNormalise) {
117 m_normClauses.add(clause); 121 m_normClauses.add(clause);
118 return ; 122 return;
119 } 123 }
120 124
121 Atom[] newHeadAtoms = new Atom[clause.getHeadLength()]; 125 Atom[] newHeadAtoms = new Atom[clause.getHeadLength()];
122 Set<Atom> additionalAtoms = new HashSet<Atom>(); 126 Set<Atom> additionalAtoms = new HashSet<Atom>();
123 int index = 0; 127 int index = 0;
124 DLClause newClause; 128 DLClause newClause;
125 for (Atom headAtom: clause.getHeadAtoms()) { 129 for (Atom headAtom: clause.getHeadAtoms()) {
126 if (headAtom.getDLPredicate() instanceof AtLeast) { 130 if (headAtom.getDLPredicate() instanceof AtLeast) {
127 AtLeast al = (AtLeast) headAtom.getDLPredicate(); 131 AtLeast al = (AtLeast) headAtom.getDLPredicate();
128 if (al instanceof AtLeastDataRange && ((AtLeastDataRange) al).getToDataRange() instanceof ConstantEnumeration) { 132 if (al instanceof AtLeastDataRange && ((AtLeastDataRange) al).getToDataRange() instanceof ConstantEnumeration) {
129 ConstantEnumeration ldr = (ConstantEnumeration) ((AtLeastDataRange) al).getToDataRange(); 133 ConstantEnumeration ldr = (ConstantEnumeration) ((AtLeastDataRange) al).getToDataRange();
130 newHeadAtoms[index] = null; 134 newHeadAtoms[index] = null;
131 Atom newHeadAtom; 135 Atom newHeadAtom;
132 for (int i = 0; i < ldr.getNumberOfConstants(); ++i) { 136 for (int i = 0; i < ldr.getNumberOfConstants(); ++i) {
133 newHeadAtom = Atom.create(AtomicRole.create(((AtomicRole) ((AtLeastDataRange) al).getOnRole()).getIRI()), headAtom.getArgument(0), ldr.getConstant(i)); 137 newHeadAtom = Atom.create(AtomicRole.create(((AtomicRole) al.getOnRole()).getIRI()), headAtom.getArgument(0), ldr.getConstant(i));
134 if (newHeadAtoms[index] == null) newHeadAtoms[index] = newHeadAtom; 138 if (newHeadAtoms[index] == null) newHeadAtoms[index] = newHeadAtom;
135 else additionalAtoms.add(newHeadAtom); 139 else additionalAtoms.add(newHeadAtom);
136 } 140 }
137 } else { 141 } else {
138 AtLeastConcept alc = toAtLeastConcept((AtLeast) headAtom.getDLPredicate()); 142 AtLeastConcept alc = toAtLeastConcept((AtLeast) headAtom.getDLPredicate());
139 AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0)); 143 AtomicConcept ac = getRightAuxiliaryConcept(alc, OverApproxExist.getNewIndividual(clause, 0));
140 newHeadAtoms[index] = Atom.create(ac, headAtom.getArgument(0)); 144 newHeadAtoms[index] = Atom.create(ac, headAtom.getArgument(0));
141 m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, headAtom.getArgument(0))}, new Atom[] {newHeadAtoms[index]})); 145 m_normClauses.add(newClause = DLClause.create(new Atom[] {Atom.create(alc, headAtom.getArgument(0))}, new Atom[] {newHeadAtoms[index]}));
142 exist2original.put(newClause, clause); 146 exist2original.put(newClause, clause);
143 } 147 }
144 } 148 } else
145 else
146 newHeadAtoms[index] = headAtom; 149 newHeadAtoms[index] = headAtom;
147 ++index; 150 ++index;
148 } 151 }
149 152
150 if (!additionalAtoms.isEmpty()) { 153 if (!additionalAtoms.isEmpty()) {
151 Atom[] tempHeadAtoms = newHeadAtoms; 154 Atom[] tempHeadAtoms = newHeadAtoms;
152 newHeadAtoms = new Atom[newHeadAtoms.length + additionalAtoms.size()]; 155 newHeadAtoms = new Atom[newHeadAtoms.length + additionalAtoms.size()];
153 for (int i = 0; i < tempHeadAtoms.length; ++i) 156 for (int i = 0; i < tempHeadAtoms.length; ++i)
154 newHeadAtoms[i] = tempHeadAtoms[i]; 157 newHeadAtoms[i] = tempHeadAtoms[i];
155 int tempI = tempHeadAtoms.length; 158 int tempI = tempHeadAtoms.length;
156 for (Iterator<Atom> iter = additionalAtoms.iterator(); iter.hasNext(); ) 159 for (Iterator<Atom> iter = additionalAtoms.iterator(); iter.hasNext(); )
157 newHeadAtoms[tempI++] = iter.next(); 160 newHeadAtoms[tempI++] = iter.next();
158 additionalAtoms.clear(); 161 additionalAtoms.clear();
159 } 162 }
@@ -169,202 +172,157 @@ public class Normalisation {
169 return ; 172 return ;
170 } 173 }
171 } 174 }
172 175
173 boolean toNormalise = false; 176 boolean toNormalise = false;
174 for (Atom atom: clause.getBodyAtoms()) 177 for (Atom atom: clause.getBodyAtoms())
175 if (!(atom.getDLPredicate() instanceof AtomicConcept)) 178 if (!(atom.getDLPredicate() instanceof AtomicConcept))
176 toNormalise = true; 179 toNormalise = true;
177 180
178 if (!toNormalise) { 181 if (!toNormalise) {
179 m_normClauses.add(clause); 182 m_normClauses.add(clause);
180 return ; 183 return;
181 } 184 }
182 185
183 Clause myClause = null; 186 Clause myClause = null;
184 try { 187 try {
185 myClause = new Clause(Clausifier.getInstance(m_ontology), clause); 188 myClause = new Clause(Clausifier.getInstance(m_ontology), clause);
186 } catch (Exception e) { 189 } catch (Exception e) {
187 Utility.logError("The clause: " + clause + " cannot be rolled up into GCI."); 190 Utility.logError("The clause: " + clause + " cannot be rolled up into GCI.");
188 m_normClauses.add(clause); 191 m_normClauses.add(clause);
189 return ; 192 return;
190 } 193 }
191 194
192 Atom[] newBodyAtoms = new Atom [myClause.getSubClasses().size()]; 195 Atom[] newBodyAtoms = new Atom [myClause.getSubClasses().size()];
193 int index = 0; 196 int index = 0;
194 for (OWLClassExpression clsExp: myClause.getSubClasses()) { 197 for (OWLClassExpression clsExp: myClause.getSubClasses()) {
195 if (clsExp instanceof OWLClass) 198 if (clsExp instanceof OWLClass)
196 newBodyAtoms[index] = Atom.create(AtomicConcept.create(((OWLClass) clsExp).getIRI().toString()), X); 199 newBodyAtoms[index] = Atom.create(AtomicConcept.create(((OWLClass) clsExp).getIRI().toString()), X);
197 else if (clsExp instanceof OWLObjectSomeValuesFrom || clsExp instanceof OWLObjectMinCardinality) { 200 else if (clsExp instanceof OWLObjectSomeValuesFrom || clsExp instanceof OWLObjectMinCardinality) {
198 int number; 201 int number;
199 OWLObjectPropertyExpression prop; 202 OWLObjectPropertyExpression prop;
200 OWLClassExpression filler; 203 OWLClassExpression filler;
201 if (clsExp instanceof OWLObjectSomeValuesFrom) { 204 if (clsExp instanceof OWLObjectSomeValuesFrom) {
202 OWLObjectSomeValuesFrom owl = (OWLObjectSomeValuesFrom) clsExp; 205 OWLObjectSomeValuesFrom owl = (OWLObjectSomeValuesFrom) clsExp;
203 number = 1; 206 number = 1;
204 prop = owl.getProperty(); 207 prop = owl.getProperty();
205 filler = owl.getFiller(); 208 filler = owl.getFiller();
206 } 209 }
207 else { 210 else {
208 OWLObjectMinCardinality owl = (OWLObjectMinCardinality) clsExp; 211 OWLObjectMinCardinality owl = (OWLObjectMinCardinality) clsExp;
209 number = owl.getCardinality(); 212 number = owl.getCardinality();
210 prop = owl.getProperty(); 213 prop = owl.getProperty();
211 filler = owl.getFiller(); 214 filler = owl.getFiller();
212 } 215 }
213 216
214 Role r = null; 217 Role r = null;
215 if (prop instanceof OWLObjectProperty) 218 if (prop instanceof OWLObjectProperty)
216 r = AtomicRole.create(((OWLObjectProperty) prop).getIRI().toString()); 219 r = AtomicRole.create(((OWLObjectProperty) prop).getIRI().toString());
217 else 220 else
218 r = InverseRole.create(AtomicRole.create(((OWLObjectProperty) (((OWLObjectInverseOf) prop).getInverse())).getIRI().toString())); 221 r = InverseRole.create(AtomicRole.create(((OWLObjectProperty) (((OWLObjectInverseOf) prop).getInverse())).getIRI().toString()));
219 222
220 LiteralConcept c = AtomicConcept.create(((OWLClass) filler).getIRI().toString()); 223 LiteralConcept c = AtomicConcept.create(((OWLClass) filler).getIRI().toString());
221 AtomicConcept ac = getLeftAuxiliaryConcept(AtLeastConcept.create(number, r, c), false); 224 AtomicConcept ac = getLeftAuxiliaryConcept(AtLeastConcept.create(number, r, c), false);
222 225
223 m_normClauses.add(exists_r_C_implies_A(number, r, c, ac)); 226 m_normClauses.add(exists_r_C_implies_A(number, r, c, ac));
224 newBodyAtoms[index] = Atom.create(ac, X); 227 newBodyAtoms[index] = Atom.create(ac, X);
225 } 228 }
226// else if (clsExp instanceof OWLDataSomeValuesFrom || clsExp instanceof OWLDataMinCardinality) { 229// else if (clsExp instanceof OWLDataSomeValuesFrom || clsExp instanceof OWLDataMinCardinality) {
227// int number; 230// int number;
228// OWLDataPropertyExpression prop; 231// OWLDataPropertyExpression prop;
229// OWLDataRange filler; 232// OWLDataRange filler;
230// if (clsExp instanceof OWLDataSomeValuesFrom) { 233// if (clsExp instanceof OWLDataSomeValuesFrom) {
231// OWLDataSomeValuesFrom owl = (OWLDataSomeValuesFrom) clsExp; 234// OWLDataSomeValuesFrom owl = (OWLDataSomeValuesFrom) clsExp;
232// number = 1; 235// number = 1;
233// prop = owl.getProperty(); 236// prop = owl.getProperty();
234// filler = owl.getFiller(); 237// filler = owl.getFiller();
235// } 238// }
236// else { 239// else {
237// OWLDataMinCardinality owl = (OWLDataMinCardinality) clsExp; 240// OWLDataMinCardinality owl = (OWLDataMinCardinality) clsExp;
238// number = owl.getCardinality(); 241// number = owl.getCardinality();
239// prop = owl.getProperty(); 242// prop = owl.getProperty();
240// filler = owl.getFiller(); 243// filler = owl.getFiller();
241// } 244// }
242// 245//
243// Role r = AtomicRole.create(((OWLDataProperty) prop).getIRI().toString()); 246// Role r = AtomicRole.create(((OWLDataProperty) prop).getIRI().toString());
244// 247//
245// LiteralConcept c = AtomicConcept.create(((OWLClass) filler).getIRI().toString()); 248// LiteralConcept c = AtomicConcept.create(((OWLClass) filler).getIRI().toString());
246// AtomicConcept ac = getLeftAuxiliaryConcept(AtLeastConcept.create(number, r, c), false); 249// AtomicConcept ac = getLeftAuxiliaryConcept(AtLeastConcept.create(number, r, c), false);
247// 250//
248// m_normClauses.add(exists_r_C_implies_A(number, r, c, ac)); 251// m_normClauses.add(exists_r_C_implies_A(number, r, c, ac));
249// newBodyAtoms[index] = Atom.create(ac, X); 252// newBodyAtoms[index] = Atom.create(ac, X);
250// } 253// }
251 else if (clsExp instanceof OWLObjectHasSelf) { 254 else if (clsExp instanceof OWLObjectHasSelf) {
252 OWLObjectPropertyExpression prop = ((OWLObjectHasSelf) clsExp).getProperty(); 255 OWLObjectPropertyExpression prop = ((OWLObjectHasSelf) clsExp).getProperty();
253 AtomicRole r; 256 AtomicRole r;
254 if (prop instanceof OWLObjectProperty) 257 if (prop instanceof OWLObjectProperty)
255 r = AtomicRole.create(((OWLObjectProperty) prop).getIRI().toString()); 258 r = AtomicRole.create(((OWLObjectProperty) prop).getIRI().toString());
256 else 259 else
257 r = AtomicRole.create(((OWLObjectProperty) (((OWLObjectInverseOf) prop).getInverse())).getIRI().toString()); 260 r = AtomicRole.create(((OWLObjectProperty) (((OWLObjectInverseOf) prop).getInverse())).getIRI().toString());
258 newBodyAtoms[index] = Atom.create(r, X, X); 261 newBodyAtoms[index] = Atom.create(r, X, X);
259 } 262 }
260 else if (clsExp instanceof OWLDataHasValue) { 263 else if (clsExp instanceof OWLDataHasValue) {
261 OWLDataPropertyExpression prop = ((OWLDataHasValue) clsExp).getProperty(); 264 OWLDataPropertyExpression prop = ((OWLDataHasValue) clsExp).getProperty();
262 AtomicRole r = AtomicRole.create(((OWLDataProperty) prop).getIRI().toString()); 265 AtomicRole r = AtomicRole.create(((OWLDataProperty) prop).getIRI().toString());
263 OWLLiteral l = ((OWLDataHasValue) clsExp).getValue(); 266 OWLLiteral l = ((OWLDataHasValue) clsExp).getValue();
264 if (l.getDatatype().toStringID().equals(Namespace.RDF_PLAIN_LITERAL)) 267 if (l.getDatatype().toStringID().equals(Namespace.RDF_PLAIN_LITERAL))
265 newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral() + "@" + l.getLang(), Namespace.RDF_PLAIN_LITERAL)); 268 newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral() + "@" + l.getLang(), Namespace.RDF_PLAIN_LITERAL));
266 else 269 else
267 newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral(), l.getDatatype().toStringID())); 270 newBodyAtoms[index] = Atom.create(r, X, Constant.create(l.getLiteral(), l.getDatatype().toStringID()));
268 } 271 } else {
269 else {
270 newBodyAtoms[index] = null; 272 newBodyAtoms[index] = null;
271 Utility.logError("counld not translate OWLClassExpression: " + clsExp + " in " + clause); 273 Utility.logError("counld not translate OWLClassExpression: " + clsExp + " in " + clause);
272 } 274 }
273 ++index; 275 ++index;
274 } 276 }
275 277
276 m_normClauses.add(DLClause.create(clause.getHeadAtoms(), newBodyAtoms)); 278 m_normClauses.add(DLClause.create(clause.getHeadAtoms(), newBodyAtoms));
277 } 279 }
278 280
279 private static final Variable X = Variable.create("X"), Y = Variable.create("Y");
280
281 private DLClause exists_r_C_implies_A(int n, Role r, LiteralConcept c, AtomicConcept a) { 281 private DLClause exists_r_C_implies_A(int n, Role r, LiteralConcept c, AtomicConcept a) {
282 Variable[] Ys = new Variable[n]; 282 Variable[] Ys = new Variable[n];
283 if (n == 1) Ys[0] = Y; 283 if (n == 1) Ys[0] = Y;
284 else 284 else
285 for (int i = 0; i < n; ++i) 285 for (int i = 0; i < n; ++i)
286 Ys[i] = Variable.create("Y" + (i + 1)); 286 Ys[i] = Variable.create("Y" + (i + 1));
287 Collection<Atom> bodyAtoms = new LinkedList<Atom>(); 287 Collection<Atom> bodyAtoms = new LinkedList<Atom>();
288 288
289 for (int i = 0; i < n; ++i) { 289 for (int i = 0; i < n; ++i) {
290 Atom rxy = r instanceof AtomicRole ? 290 Atom rxy = r instanceof AtomicRole ?
291 Atom.create(((AtomicRole) r), X, Ys[i]) : 291 Atom.create(((AtomicRole) r), X, Ys[i]) :
292 Atom.create(((InverseRole) r).getInverseOf(), Ys[i], X); 292 Atom.create(((InverseRole) r).getInverseOf(), Ys[i], X);
293 bodyAtoms.add(rxy); 293 bodyAtoms.add(rxy);
294 if (!c.equals(AtomicConcept.THING)) 294 if (!c.equals(AtomicConcept.THING))
295 bodyAtoms.add(Atom.create((AtomicConcept) c, Ys[i])); 295 bodyAtoms.add(Atom.create((AtomicConcept) c, Ys[i]));
296 } 296 }
297 297
298 for (int i = 0; i < n; ++i) 298 for (int i = 0; i < n; ++i)
299 for (int j = i + 1; j < n; ++j) 299 for (int j = i + 1; j < n; ++j)
300 bodyAtoms.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j])); 300 bodyAtoms.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j]));
301
302 return DLClause.create(new Atom[] {Atom.create(a, X)}, bodyAtoms.toArray(new Atom[0]));
303 }
304
305 private Map<AtLeastConcept, AtomicConcept> leftAuxiliaryConcept = new HashMap<AtLeastConcept, AtomicConcept>();
306 private Map<AtomicConcept, AtLeastConcept> leftAuxiliaryConcept_inv = new HashMap<AtomicConcept, AtLeastConcept>();
307
308 public static final String auxiliaryConceptPrefix = Namespace.PAGODA_AUX + "concept_";
309 301
310 private static String getName(String iri) { 302 return DLClause.create(new Atom[]{Atom.create(a, X)}, bodyAtoms.toArray(new Atom[0]));
311 int index = iri.lastIndexOf("#");
312 if (index != -1) return iri.substring(index + 1);
313 index = iri.lastIndexOf("/");
314 if (index != -1) return iri.substring(index + 1);
315 return iri;
316 } 303 }
317 304
318 private AtomicConcept getRightAuxiliaryConcept(AtLeastConcept alc, Individual... individuals) { 305 private AtomicConcept getRightAuxiliaryConcept(AtLeastConcept alc, Individual... individuals) {
319 String iri = getAuxiliaryConcept4Disjunct(alc, individuals); 306 String iri = getAuxiliaryConcept4Disjunct(alc, individuals);
320 rightAuxiliaryConcept.put(iri, alc); 307 rightAuxiliaryConcept.put(iri, alc);
321 return AtomicConcept.create(iri); 308 return AtomicConcept.create(iri);
322 }
323
324 public static String getAuxiliaryConcept4Disjunct(AtLeastConcept alc, Individual... individuals) {
325 Role r = alc.getOnRole();
326 LiteralConcept c = alc.getToConcept();
327 StringBuilder builder = new StringBuilder(auxiliaryConceptPrefix);
328 if (r instanceof AtomicRole)
329 builder.append(getName(((AtomicRole) r).getIRI()));
330 else
331 builder.append(getName(((InverseRole) r).getInverseOf().getIRI())).append("_inv");
332
333 if (alc.getNumber() > 1)
334 builder.append("_").append(alc.getNumber());
335
336 if (c instanceof AtomicConcept) {
337 if (!c.equals(AtomicConcept.THING))
338 builder.append("_").append(getName(((AtomicConcept) c).getIRI()));
339 }
340 else
341 builder.append("_").append(getName((OverApproxExist.getNegationConcept(((AtomicNegationConcept) c).getNegatedAtomicConcept()).getIRI())));
342
343 if (individuals.length > 1)
344 builder.append("_").append(getName(individuals[0].getIRI()));
345
346 builder.append("_exist");
347
348 return builder.toString();
349 } 309 }
350 310
351 public AtomicConcept getLeftAuxiliaryConcept(AtLeastConcept key, boolean available) { 311 public AtomicConcept getLeftAuxiliaryConcept(AtLeastConcept key, boolean available) {
352// AtLeastConcept key = AtLeastConcept.create(1, r, c); 312// AtLeastConcept key = AtLeastConcept.create(1, r, c);
353 AtomicConcept value = null; 313 AtomicConcept value = null;
354 if ((value = leftAuxiliaryConcept.get(key)) != null); 314 if ((value = leftAuxiliaryConcept.get(key)) != null) ;
355 else if (!available) { 315 else if (!available) {
356 value = AtomicConcept.create(getAuxiliaryConcept4Disjunct(key)); 316 value = AtomicConcept.create(getAuxiliaryConcept4Disjunct(key));
357 leftAuxiliaryConcept.put(key, value); 317 leftAuxiliaryConcept.put(key, value);
358 leftAuxiliaryConcept_inv.put(value, key); 318 leftAuxiliaryConcept_inv.put(value, key);
359 } 319 }
360 return value; 320 return value;
361 } 321 }
362 322
363 public AtLeastConcept getLeftAtLeastConcept(AtomicConcept value) { 323 public AtLeastConcept getLeftAtLeastConcept(AtomicConcept value) {
364 return leftAuxiliaryConcept_inv.get(value); 324 return leftAuxiliaryConcept_inv.get(value);
365 } 325 }
366
367 Map<String, AtLeastConcept> rightAuxiliaryConcept = new HashMap<String, AtLeastConcept>();
368 326
369 public AtLeastConcept getRightAtLeastConcept(AtomicConcept p) { 327 public AtLeastConcept getRightAtLeastConcept(AtomicConcept p) {
370 return rightAuxiliaryConcept.get(p.getIRI()); 328 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 @@
1package uk.ac.ox.cs.pagoda.multistage; 1package uk.ac.ox.cs.pagoda.multistage;
2 2
3import java.util.Collection; 3import org.semanticweb.HermiT.model.*;
4import java.util.HashMap;
5import java.util.HashSet;
6import java.util.LinkedList;
7import java.util.Map;
8import java.util.Set;
9
10import org.semanticweb.HermiT.model.AnnotatedEquality;
11import org.semanticweb.HermiT.model.AtLeast;
12import org.semanticweb.HermiT.model.AtLeastConcept;
13import org.semanticweb.HermiT.model.AtLeastDataRange;
14import org.semanticweb.HermiT.model.Atom;
15import org.semanticweb.HermiT.model.AtomicConcept;
16import org.semanticweb.HermiT.model.AtomicNegationConcept;
17import org.semanticweb.HermiT.model.AtomicRole;
18import org.semanticweb.HermiT.model.DLClause;
19import org.semanticweb.HermiT.model.DLPredicate;
20import org.semanticweb.HermiT.model.Equality;
21import org.semanticweb.HermiT.model.Inequality;
22import org.semanticweb.HermiT.model.Variable;
23
24import uk.ac.ox.cs.JRDFox.JRDFStoreException; 4import uk.ac.ox.cs.JRDFox.JRDFStoreException;
25import uk.ac.ox.cs.JRDFox.store.TupleIterator; 5import uk.ac.ox.cs.JRDFox.store.TupleIterator;
26import uk.ac.ox.cs.pagoda.MyPrefixes; 6import uk.ac.ox.cs.pagoda.MyPrefixes;
@@ -29,38 +9,36 @@ import uk.ac.ox.cs.pagoda.hermit.RuleHelper;
29import uk.ac.ox.cs.pagoda.query.GapByStore4ID; 9import uk.ac.ox.cs.pagoda.query.GapByStore4ID;
30import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager; 10import uk.ac.ox.cs.pagoda.reasoner.light.RDFoxTripleManager;
31import uk.ac.ox.cs.pagoda.rules.DatalogProgram; 11import uk.ac.ox.cs.pagoda.rules.DatalogProgram;
32import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
33import uk.ac.ox.cs.pagoda.rules.Program; 12import uk.ac.ox.cs.pagoda.rules.Program;
13import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
34import uk.ac.ox.cs.pagoda.util.Namespace; 14import uk.ac.ox.cs.pagoda.util.Namespace;
35import uk.ac.ox.cs.pagoda.util.SparqlHelper; 15import uk.ac.ox.cs.pagoda.util.SparqlHelper;
36import uk.ac.ox.cs.pagoda.util.Utility; 16import uk.ac.ox.cs.pagoda.util.Utility;
37 17
18import java.util.*;
19
38abstract class TwoStageApplication { 20abstract class TwoStageApplication {
39 21
22 private static final String NAF_suffix = "_NAF";
40 protected TwoStageQueryEngine engine; 23 protected TwoStageQueryEngine engine;
41 protected MyPrefixes prefixes = MyPrefixes.PAGOdAPrefixes; 24 protected MyPrefixes prefixes = MyPrefixes.PAGOdAPrefixes;
42 private GapByStore4ID gap;
43
44 Program lowerProgram;
45
46 boolean m_incrementally = true;
47
48 protected Set<DLClause> rules = new HashSet<DLClause>(); 25 protected Set<DLClause> rules = new HashSet<DLClause>();
49 private StringBuilder datalogRuleText = new StringBuilder();
50
51 protected Collection<DLClause> constraints = new LinkedList<DLClause>(); 26 protected Collection<DLClause> constraints = new LinkedList<DLClause>();
52 protected BottomStrategy m_bottom; 27 protected BottomStrategy m_bottom;
53
54 protected Set<Atom> toGenerateNAFFacts = new HashSet<Atom>(); 28 protected Set<Atom> toGenerateNAFFacts = new HashSet<Atom>();
55
56 protected OverApproxExist overExist = new OverApproxExist(); 29 protected OverApproxExist overExist = new OverApproxExist();
57 30 Program lowerProgram;
31 boolean m_incrementally = true;
32 Set<Integer> allIndividuals = new HashSet<Integer>();
33 RDFoxTripleManager tripleManager;
34 private GapByStore4ID gap;
35 private StringBuilder datalogRuleText = new StringBuilder();
58 private Map<DLClause, DLClause> map = new HashMap<DLClause, DLClause>(); 36 private Map<DLClause, DLClause> map = new HashMap<DLClause, DLClause>();
59 37
60 public TwoStageApplication(TwoStageQueryEngine engine, DatalogProgram program, GapByStore4ID gap) { 38 public TwoStageApplication(TwoStageQueryEngine engine, DatalogProgram program, GapByStore4ID gap) {
61 this.engine = engine; 39 this.engine = engine;
62 tripleManager = new RDFoxTripleManager(engine.getDataStore(), m_incrementally); 40 tripleManager = new RDFoxTripleManager(engine.getDataStore(), m_incrementally);
63 this.gap = gap; 41 this.gap = gap;
64 m_bottom = program.getUpperBottomStrategy(); 42 m_bottom = program.getUpperBottomStrategy();
65 lowerProgram = program.getLower(); 43 lowerProgram = program.getLower();
66 44
@@ -123,7 +101,7 @@ abstract class TwoStageApplication {
123 for (DLClause clause: lowerProgram.getClauses()) 101 for (DLClause clause: lowerProgram.getClauses())
124 if (!rules.contains(clause)) 102 if (!rules.contains(clause))
125 builder.append(RuleHelper.getText(clause)); 103 builder.append(RuleHelper.getText(clause));
126 104
127 engine.materialise(builder.toString(), null, false); 105 engine.materialise(builder.toString(), null, false);
128 addAuxiliaryRules(); 106 addAuxiliaryRules();
129 addAuxiliaryNAFFacts(); 107 addAuxiliaryNAFFacts();
@@ -150,7 +128,7 @@ abstract class TwoStageApplication {
150 e.printStackTrace(); 128 e.printStackTrace();
151 } finally { 129 } finally {
152 if (tuples != null) tuples.dispose(); 130 if (tuples != null) tuples.dispose();
153 tuples = null; 131 tuples = null;
154 } 132 }
155 } 133 }
156 } 134 }
@@ -171,9 +149,6 @@ abstract class TwoStageApplication {
171 149
172 protected abstract void addAuxiliaryRules(); 150 protected abstract void addAuxiliaryRules();
173 151
174 Set<Integer> allIndividuals = new HashSet<Integer>();
175 RDFoxTripleManager tripleManager;
176
177 private void addAuxiliaryNAFFacts() { 152 private void addAuxiliaryNAFFacts() {
178 153
179 for (int id : tripleManager.getResourceIDs(engine.getAllIndividuals())) 154 for (int id : tripleManager.getResourceIDs(engine.getAllIndividuals()))
@@ -203,7 +178,7 @@ abstract class TwoStageApplication {
203 tuples = engine.internal_evaluate(SparqlHelper.getSPARQLQuery( 178 tuples = engine.internal_evaluate(SparqlHelper.getSPARQLQuery(
204 new Atom[] { Atom.create(p, X) }, "X")); 179 new Atom[] { Atom.create(p, X) }, "X"));
205 for (long multi = tuples.open(); multi != 0; multi = tuples.getNext()) { 180 for (long multi = tuples.open(); multi != 0; multi = tuples.getNext()) {
206 ret.remove((int) tuples.getResourceID(0)); 181 ret.remove(tuples.getResourceID(0));
207 } 182 }
208 } catch (JRDFStoreException e) { 183 } catch (JRDFStoreException e) {
209 // TODO Auto-generated catch block 184 // TODO Auto-generated catch block
@@ -216,8 +191,6 @@ abstract class TwoStageApplication {
216 191
217 protected abstract Collection<DLClause> getInitialClauses(Program program); 192 protected abstract Collection<DLClause> getInitialClauses(Program program);
218 193
219 private static final String NAF_suffix = "_NAF";
220
221 protected Atom getNAFAtom(Atom atom) { 194 protected Atom getNAFAtom(Atom atom) {
222 return getNAFAtom(atom, true); 195 return getNAFAtom(atom, true);
223 } 196 }
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 @@
1package uk.ac.ox.cs.pagoda.multistage.treatement; 1package uk.ac.ox.cs.pagoda.multistage.treatement;
2 2
3import java.util.Comparator; 3import org.semanticweb.HermiT.model.*;
4import java.util.Set; 4import uk.ac.ox.cs.JRDFox.JRDFStoreException;
5
6import org.semanticweb.HermiT.model.AnnotatedEquality;
7import org.semanticweb.HermiT.model.AtLeastConcept;
8import org.semanticweb.HermiT.model.Atom;
9import org.semanticweb.HermiT.model.AtomicConcept;
10import org.semanticweb.HermiT.model.AtomicNegationConcept;
11import org.semanticweb.HermiT.model.AtomicRole;
12import org.semanticweb.HermiT.model.DLPredicate;
13import org.semanticweb.HermiT.model.Equality;
14import org.semanticweb.HermiT.model.Inequality;
15import org.semanticweb.HermiT.model.InverseRole;
16import uk.ac.ox.cs.pagoda.constraints.PredicateDependency; 5import uk.ac.ox.cs.pagoda.constraints.PredicateDependency;
17import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; 6import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
18import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine; 7import uk.ac.ox.cs.pagoda.multistage.MultiStageQueryEngine;
@@ -20,10 +9,11 @@ import uk.ac.ox.cs.pagoda.multistage.Normalisation;
20import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication; 9import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication;
21import uk.ac.ox.cs.pagoda.multistage.Violation; 10import uk.ac.ox.cs.pagoda.multistage.Violation;
22import uk.ac.ox.cs.pagoda.query.QueryRecord; 11import uk.ac.ox.cs.pagoda.query.QueryRecord;
23import uk.ac.ox.cs.pagoda.rules.OverApproxExist; 12import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
24import uk.ac.ox.cs.pagoda.util.Namespace; 13import uk.ac.ox.cs.pagoda.util.Namespace;
25 14
26import uk.ac.ox.cs.JRDFox.JRDFStoreException; 15import java.util.Comparator;
16import java.util.Set;
27 17
28public class Pick4NegativeConceptQuerySpecific extends Pick4NegativeConcept { 18public class Pick4NegativeConceptQuerySpecific extends Pick4NegativeConcept {
29 19
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 @@
1package uk.ac.ox.cs.pagoda.reasoner.light; 1package uk.ac.ox.cs.pagoda.reasoner.light;
2 2
3import java.util.Comparator;
4
5import uk.ac.ox.cs.pagoda.multistage.Normalisation; 3import uk.ac.ox.cs.pagoda.multistage.Normalisation;
6import uk.ac.ox.cs.pagoda.rules.OverApproxExist; 4import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
5
6import java.util.Comparator;
7 7
8public class DLPredicateComparator implements Comparator<String> { 8public class DLPredicateComparator implements Comparator<String> {
9 9
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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules;
2 2
3import java.util.Collection;
4import java.util.HashMap;
5import java.util.HashSet;
6import java.util.Iterator;
7import java.util.Map;
8
9import org.semanticweb.HermiT.model.DLClause; 3import org.semanticweb.HermiT.model.DLClause;
10import org.semanticweb.owlapi.model.OWLAxiom; 4import org.semanticweb.owlapi.model.OWLAxiom;
11import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom; 5import org.semanticweb.owlapi.model.OWLSubPropertyChainOfAxiom;
12import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom; 6import org.semanticweb.owlapi.model.OWLTransitiveObjectPropertyAxiom;
13
14import uk.ac.ox.cs.pagoda.owl.OWLHelper; 7import uk.ac.ox.cs.pagoda.owl.OWLHelper;
8import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
9
10import java.util.*;
15 11
16public abstract class ApproxProgram extends Program { 12public 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
99class ClauseSet extends HashSet<DLClause> { 94class 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 @@
1package uk.ac.ox.cs.pagoda.rules;
2
3import org.semanticweb.HermiT.model.AtLeast;
4import org.semanticweb.HermiT.model.Atom;
5import org.semanticweb.HermiT.model.DLClause;
6import org.semanticweb.HermiT.model.DLPredicate;
7
8import java.util.Collection;
9import java.util.LinkedList;
10
11public interface Approximator {
12
13 Collection<DLClause> convert(DLClause clause, DLClause originalClause);
14
15}
16
17class 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
34class 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
53class 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules;
2 2
3import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
4
3public class DisjunctiveProgram extends UpperProgram { 5public 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
3import org.semanticweb.HermiT.model.DLClause; 3import org.semanticweb.HermiT.model.DLClause;
4import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; 4import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
5import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
6import uk.ac.ox.cs.pagoda.rules.approximators.TupleDependentApproximator;
5 7
6import java.util.Collection; 8import 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules;
2 2
3import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxDisj;
4
3public class ExistentialProgram extends UpperProgram { 5public 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules;
2 2
3import org.semanticweb.HermiT.model.*;
4import org.semanticweb.owlapi.model.OWLObjectProperty;
5import org.semanticweb.owlapi.model.OWLOntology;
6import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
7import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
8import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
9
3import java.util.Collection; 10import java.util.Collection;
4import java.util.HashSet; 11import java.util.HashSet;
5import java.util.LinkedList; 12import java.util.LinkedList;
6import java.util.Set; 13import java.util.Set;
7 14
8import org.semanticweb.HermiT.model.AtLeastConcept;
9import org.semanticweb.HermiT.model.Atom;
10import org.semanticweb.HermiT.model.AtomicRole;
11import org.semanticweb.HermiT.model.DLClause;
12import org.semanticweb.HermiT.model.DLPredicate;
13import org.semanticweb.owlapi.model.OWLObjectProperty;
14import org.semanticweb.owlapi.model.OWLOntology;
15import uk.ac.ox.cs.pagoda.constraints.BottomStrategy;
16
17public class ExistentialToDisjunctive extends UpperProgram { 15public 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;
10import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom; 10import uk.ac.ox.cs.pagoda.constraints.UpperUnaryBottom;
11import uk.ac.ox.cs.pagoda.multistage.Normalisation; 11import uk.ac.ox.cs.pagoda.multistage.Normalisation;
12import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication; 12import uk.ac.ox.cs.pagoda.multistage.RestrictedApplication;
13import uk.ac.ox.cs.pagoda.rules.approximators.Approximator;
13import uk.ac.ox.cs.pagoda.util.Timer; 14import uk.ac.ox.cs.pagoda.util.Timer;
14import uk.ac.ox.cs.pagoda.util.Utility; 15import 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules;
2 2
3import org.semanticweb.HermiT.model.DLClause;
4import org.semanticweb.HermiT.model.DLPredicate;
5import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxBoth;
6
3import java.util.Collection; 7import java.util.Collection;
4import java.util.HashMap; 8import java.util.HashMap;
5import java.util.Map; 9import java.util.Map;
6 10
7import org.semanticweb.HermiT.model.DLClause;
8import org.semanticweb.HermiT.model.DLPredicate;
9
10 11
11public class UpperDatalogProgram extends UpperProgram { 12public 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 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.DLClause;
4
5import java.util.Collection;
6
7public 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules.approximators;
2 2
3import org.semanticweb.HermiT.model.DLClause; 3import org.semanticweb.HermiT.model.DLClause;
4import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; 4import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
5import uk.ac.ox.cs.pagoda.rules.ExistConstantApproximator;
5 6
6import java.util.*; 7import 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import java.util.Collection;
4import java.util.LinkedList;
5 2
6import org.semanticweb.HermiT.model.AtLeastDataRange; 3import org.semanticweb.HermiT.model.AtLeastDataRange;
7import org.semanticweb.HermiT.model.DLClause; 4import org.semanticweb.HermiT.model.DLClause;
8 5
6import java.util.Collection;
7import java.util.LinkedList;
8
9public class OverApproxBoth implements Approximator { 9public 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules.approximators;
2 2
3import org.semanticweb.HermiT.model.*; 3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; 4import 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules.approximators;
2 2
3import org.semanticweb.HermiT.model.*; 3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; 4import 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 @@
1package uk.ac.ox.cs.pagoda.rules.approximators;
2
3import org.semanticweb.HermiT.model.AtLeast;
4import org.semanticweb.HermiT.model.Atom;
5import org.semanticweb.HermiT.model.DLClause;
6import org.semanticweb.HermiT.model.Individual;
7import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
8import uk.ac.ox.cs.pagoda.util.Namespace;
9
10import java.util.HashMap;
11import java.util.Map;
12
13/**
14 * If you need a Skolem term (i.e. fresh individual), ask this class.
15 */
16public 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 @@
1package uk.ac.ox.cs.pagoda.rules; 1package uk.ac.ox.cs.pagoda.rules.approximators;
2 2
3import org.semanticweb.HermiT.model.DLClause; 3import org.semanticweb.HermiT.model.DLClause;
4import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID; 4import uk.ac.ox.cs.pagoda.multistage.AnswerTupleID;
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 @@
1package uk.ac.ox.cs.pagoda.tracking; 1package uk.ac.ox.cs.pagoda.tracking;
2 2
3import java.util.Collection; 3import org.semanticweb.HermiT.model.*;
4import java.util.Collections;
5import java.util.HashMap;
6import java.util.HashSet;
7import java.util.Iterator;
8import java.util.LinkedList;
9import java.util.Map;
10
11import org.semanticweb.HermiT.model.AnnotatedEquality;
12import org.semanticweb.HermiT.model.AtLeastConcept;
13import org.semanticweb.HermiT.model.Atom;
14import org.semanticweb.HermiT.model.AtomicConcept;
15import org.semanticweb.HermiT.model.AtomicRole;
16import org.semanticweb.HermiT.model.DLClause;
17import org.semanticweb.HermiT.model.DLPredicate;
18import org.semanticweb.HermiT.model.Equality;
19import org.semanticweb.HermiT.model.Individual;
20import org.semanticweb.HermiT.model.Inequality;
21
22import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; 4import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
23import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; 5import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
24import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
25import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; 6import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
7import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
26import uk.ac.ox.cs.pagoda.util.Namespace; 8import uk.ac.ox.cs.pagoda.util.Namespace;
27 9
10import java.util.*;
11
28public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap { 12public abstract class TrackingRuleEncoderDisj extends TrackingRuleEncoderWithGap {
29 13
30 public TrackingRuleEncoderDisj(UpperDatalogProgram program, BasicQueryEngine store) { 14 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 @@
1package uk.ac.ox.cs.pagoda.tracking; 1package uk.ac.ox.cs.pagoda.tracking;
2 2
3import java.util.LinkedList; 3import org.semanticweb.HermiT.model.*;
4
5import org.semanticweb.HermiT.model.AtLeastConcept;
6import org.semanticweb.HermiT.model.Atom;
7import org.semanticweb.HermiT.model.AtomicConcept;
8import org.semanticweb.HermiT.model.AtomicNegationConcept;
9import org.semanticweb.HermiT.model.AtomicRole;
10import org.semanticweb.HermiT.model.DLClause;
11import org.semanticweb.HermiT.model.DLPredicate;
12import org.semanticweb.HermiT.model.Individual;
13import org.semanticweb.HermiT.model.Inequality;
14import org.semanticweb.HermiT.model.InverseRole;
15import org.semanticweb.HermiT.model.Term;
16import org.semanticweb.HermiT.model.Variable;
17
18import uk.ac.ox.cs.pagoda.MyPrefixes; 4import uk.ac.ox.cs.pagoda.MyPrefixes;
19import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; 5import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
20import uk.ac.ox.cs.pagoda.multistage.Normalisation; 6import uk.ac.ox.cs.pagoda.multistage.Normalisation;
21import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; 7import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
22import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
23import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; 8import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
9import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
10
11import java.util.LinkedList;
24 12
25public class TrackingRuleEncoderDisj1 extends TrackingRuleEncoderDisj { 13public class TrackingRuleEncoderDisj1 extends TrackingRuleEncoderDisj {
26 14
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 @@
1package uk.ac.ox.cs.pagoda.tracking; 1package uk.ac.ox.cs.pagoda.tracking;
2 2
3import org.semanticweb.HermiT.model.AtLeastConcept; 3import org.semanticweb.HermiT.model.*;
4import org.semanticweb.HermiT.model.Atom;
5import org.semanticweb.HermiT.model.AtomicConcept;
6import org.semanticweb.HermiT.model.AtomicNegationConcept;
7import org.semanticweb.HermiT.model.AtomicRole;
8import org.semanticweb.HermiT.model.DLClause;
9import org.semanticweb.HermiT.model.DLPredicate;
10import org.semanticweb.HermiT.model.Individual;
11import org.semanticweb.HermiT.model.Inequality;
12import org.semanticweb.HermiT.model.InverseRole;
13import org.semanticweb.HermiT.model.Term;
14import org.semanticweb.HermiT.model.Variable;
15
16import uk.ac.ox.cs.pagoda.MyPrefixes; 4import uk.ac.ox.cs.pagoda.MyPrefixes;
17import uk.ac.ox.cs.pagoda.multistage.Normalisation; 5import uk.ac.ox.cs.pagoda.multistage.Normalisation;
18import uk.ac.ox.cs.pagoda.query.QueryRecord; 6import uk.ac.ox.cs.pagoda.query.QueryRecord;
19import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; 7import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
20import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
21import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; 8import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
9import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
22 10
23public class TrackingRuleEncoderDisj2 extends TrackingRuleEncoderDisj { 11public class TrackingRuleEncoderDisj2 extends TrackingRuleEncoderDisj {
24 12
@@ -56,7 +44,7 @@ public class TrackingRuleEncoderDisj2 extends TrackingRuleEncoderDisj {
56 44
57 @Override 45 @Override
58 protected DLPredicate generateAuxiliaryRule(AtLeastConcept p, DLClause original, Individual[] individuals) { 46 protected DLPredicate generateAuxiliaryRule(AtLeastConcept p, DLClause original, Individual[] individuals) {
59 DLPredicate ret = AtomicConcept.create(getTrackingPredicate(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p, individuals))); 47 DLPredicate ret = AtomicConcept.create(getTrackingPredicate(Normalisation.getAuxiliaryConcept4Disjunct(p, individuals)));
60 Atom[] headAtom = new Atom[] {Atom.create(ret, X)}; 48 Atom[] headAtom = new Atom[] {Atom.create(ret, X)};
61 49
62 AtomicRole role = p.getOnRole() instanceof AtomicRole ? 50 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 @@
1package uk.ac.ox.cs.pagoda.tracking; 1package uk.ac.ox.cs.pagoda.tracking;
2 2
3import java.util.Collection; 3import org.semanticweb.HermiT.model.*;
4import java.util.HashSet;
5import java.util.LinkedList;
6import java.util.Set;
7
8import org.semanticweb.HermiT.model.AnnotatedEquality;
9import org.semanticweb.HermiT.model.AtLeast;
10import org.semanticweb.HermiT.model.AtLeastConcept;
11import org.semanticweb.HermiT.model.Atom;
12import org.semanticweb.HermiT.model.AtomicConcept;
13import org.semanticweb.HermiT.model.AtomicNegationConcept;
14import org.semanticweb.HermiT.model.AtomicRole;
15import org.semanticweb.HermiT.model.DLClause;
16import org.semanticweb.HermiT.model.DLPredicate;
17import org.semanticweb.HermiT.model.DatatypeRestriction;
18import org.semanticweb.HermiT.model.Equality;
19import org.semanticweb.HermiT.model.Inequality;
20import org.semanticweb.HermiT.model.InverseRole;
21import org.semanticweb.HermiT.model.Variable;
22
23import uk.ac.ox.cs.pagoda.MyPrefixes; 4import uk.ac.ox.cs.pagoda.MyPrefixes;
24import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; 5import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
25import uk.ac.ox.cs.pagoda.multistage.Normalisation; 6import uk.ac.ox.cs.pagoda.multistage.Normalisation;
26import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; 7import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
27import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
28import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; 8import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
9import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
29import uk.ac.ox.cs.pagoda.util.Namespace; 10import uk.ac.ox.cs.pagoda.util.Namespace;
30import uk.ac.ox.cs.pagoda.util.Utility; 11import uk.ac.ox.cs.pagoda.util.Utility;
31 12
13import java.util.Collection;
14import java.util.HashSet;
15import java.util.LinkedList;
16import java.util.Set;
17
32public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap { 18public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
33 19
34 public TrackingRuleEncoderDisjVar1(UpperDatalogProgram program, BasicQueryEngine store) { 20 public TrackingRuleEncoderDisjVar1(UpperDatalogProgram program, BasicQueryEngine store) {
@@ -96,13 +82,13 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
96 return Atom.create(getTrackingDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 82 return Atom.create(getTrackingDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0));
97 } 83 }
98 if (p instanceof AtomicConcept) 84 if (p instanceof AtomicConcept)
99 return Atom.create(getTrackingDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); 85 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0));
100 if (p instanceof AtomicRole) 86 if (p instanceof AtomicRole)
101 return Atom.create(getTrackingDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); 87 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
102 if (p instanceof Equality || p instanceof AnnotatedEquality) 88 if (p instanceof Equality || p instanceof AnnotatedEquality)
103 return Atom.create(getTrackingDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 89 return Atom.create(getTrackingDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
104 if (p instanceof Inequality) 90 if (p instanceof Inequality)
105 return Atom.create(getTrackingDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); 91 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
106 92
107 return null; 93 return null;
108 } 94 }
@@ -114,15 +100,15 @@ public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
114 return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 100 return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0));
115 } 101 }
116 if (p instanceof AtomicConcept) 102 if (p instanceof AtomicConcept)
117 return Atom.create(getGapDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); 103 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
118 if (p instanceof AtomicRole) 104 if (p instanceof AtomicRole)
119 return Atom.create(getGapDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); 105 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
120 if (p instanceof Equality || p instanceof AnnotatedEquality) 106 if (p instanceof Equality || p instanceof AnnotatedEquality)
121 return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 107 return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
122 if (p instanceof Inequality) 108 if (p instanceof Inequality)
123 return Atom.create(getGapDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); 109 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
124 if (p instanceof DatatypeRestriction) 110 if (p instanceof DatatypeRestriction)
125 return Atom.create(getGapDLPredicate((DatatypeRestriction) p), headAtom.getArgument(0)); 111 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
126 Utility.logError(p + " is not recognised."); 112 Utility.logError(p + " is not recognised.");
127 return null; 113 return null;
128 } 114 }
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 @@
1package uk.ac.ox.cs.pagoda.tracking; 1package uk.ac.ox.cs.pagoda.tracking;
2 2
3import java.util.Collection; 3import org.semanticweb.HermiT.model.*;
4import java.util.HashSet;
5import java.util.LinkedList;
6import java.util.Set;
7
8import org.semanticweb.HermiT.model.AnnotatedEquality;
9import org.semanticweb.HermiT.model.AtLeastConcept;
10import org.semanticweb.HermiT.model.Atom;
11import org.semanticweb.HermiT.model.AtomicConcept;
12import org.semanticweb.HermiT.model.AtomicNegationConcept;
13import org.semanticweb.HermiT.model.AtomicRole;
14import org.semanticweb.HermiT.model.DLClause;
15import org.semanticweb.HermiT.model.DLPredicate;
16import org.semanticweb.HermiT.model.Equality;
17import org.semanticweb.HermiT.model.Inequality;
18import org.semanticweb.HermiT.model.InverseRole;
19import org.semanticweb.HermiT.model.Variable;
20
21import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper; 4import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
22import uk.ac.ox.cs.pagoda.multistage.Normalisation; 5import uk.ac.ox.cs.pagoda.multistage.Normalisation;
23import uk.ac.ox.cs.pagoda.query.QueryRecord; 6import uk.ac.ox.cs.pagoda.query.QueryRecord;
24import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine; 7import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
25import uk.ac.ox.cs.pagoda.rules.OverApproxExist;
26import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram; 8import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
9import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
27import uk.ac.ox.cs.pagoda.util.Namespace; 10import uk.ac.ox.cs.pagoda.util.Namespace;
28 11
12import java.util.Collection;
13import java.util.HashSet;
14import java.util.LinkedList;
15import java.util.Set;
16
29public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap { 17public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap {
30 18
31 public TrackingRuleEncoderDisjVar2(UpperDatalogProgram program, BasicQueryEngine store) { 19 public TrackingRuleEncoderDisjVar2(UpperDatalogProgram program, BasicQueryEngine store) {
@@ -91,13 +79,13 @@ public class TrackingRuleEncoderDisjVar2 extends TrackingRuleEncoderWithGap {
91 return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0)); 79 return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom.getArgument(0));
92 } 80 }
93 if (p instanceof AtomicConcept) 81 if (p instanceof AtomicConcept)
94 return Atom.create(getGapDLPredicate((AtomicConcept) p), headAtom.getArgument(0)); 82 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
95 if (p instanceof AtomicRole) 83 if (p instanceof AtomicRole)
96 return Atom.create(getGapDLPredicate((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1)); 84 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
97 if (p instanceof Equality || p instanceof AnnotatedEquality) 85 if (p instanceof Equality || p instanceof AnnotatedEquality)
98 return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1)); 86 return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
99 if (p instanceof Inequality) 87 if (p instanceof Inequality)
100 return Atom.create(getGapDLPredicate((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1)); 88 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
101 89
102 return null; 90 return null;
103 } 91 }
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-05 15:58:28 +0000