aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
diff options
context:
space:
mode:
Diffstat (limited to 'src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java')
-rw-r--r--src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java425
1 files changed, 0 insertions, 425 deletions
diff --git a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java b/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
deleted file mode 100644
index d96c747..0000000
--- a/src/uk/ac/ox/cs/pagoda/tracking/TrackingRuleEncoderDisjVar1.java
+++ /dev/null
@@ -1,425 +0,0 @@
1package uk.ac.ox.cs.pagoda.tracking;
2
3import org.semanticweb.HermiT.model.*;
4import uk.ac.ox.cs.pagoda.MyPrefixes;
5import uk.ac.ox.cs.pagoda.hermit.DLClauseHelper;
6import uk.ac.ox.cs.pagoda.multistage.Normalisation;
7import uk.ac.ox.cs.pagoda.reasoner.light.BasicQueryEngine;
8import uk.ac.ox.cs.pagoda.rules.UpperDatalogProgram;
9import uk.ac.ox.cs.pagoda.rules.approximators.OverApproxExist;
10import uk.ac.ox.cs.pagoda.util.Namespace;
11import uk.ac.ox.cs.pagoda.util.Utility;
12
13import java.util.Collection;
14import java.util.HashSet;
15import java.util.LinkedList;
16import java.util.Set;
17
18public class TrackingRuleEncoderDisjVar1 extends TrackingRuleEncoderWithGap {
19
20 private Set<DLClause> disjunctiveRules = new HashSet<DLClause>();
21 private Variable X = Variable.create("X"), Y = Variable.create("Y");
22 private String bottomTrackingProgram = null;
23
24 public TrackingRuleEncoderDisjVar1(UpperDatalogProgram program, BasicQueryEngine store) {
25 super(program, store);
26 }
27
28 @Override
29 public boolean encodingRules() {
30 if (super.encodingRules()) {
31 processDisjunctiveRules();
32 return true;
33 }
34 return false;
35 }
36
37 @Override
38 protected void encodingRule(DLClause clause) {
39 if (currentQuery.isBottom()) {
40// super.encodingRule(clause);
41 encodingBottomQueryClause(clause);
42 return;
43 }
44
45 DLClause original = program.getCorrespondingClause(clause);
46 if (original.getHeadLength() <= 1) {
47 super.encodingRule(clause);
48 }
49 else {
50 if (!DLClauseHelper.hasSubsetBodyAtoms(clause, original))
51 super.encodingRule(clause);
52 addDisjunctiveRule(original);
53 }
54
55 }
56
57 private void processDisjunctiveRules() {
58 for (DLClause clause: disjunctiveRules)
59 encodingDisjunctiveRule(clause);
60 }
61
62 private Atom getAuxiliaryAtom(Atom headAtom) {
63 DLPredicate p = headAtom.getDLPredicate();
64 if (p instanceof AtLeast || p instanceof AtLeast) {
65 return Atom.create(generateAuxiliaryRule((AtLeast) p, true), headAtom.getArgument(0));
66 }
67 if(p instanceof AtomicConcept)
68 return Atom.create(generateAuxiliaryRule((AtomicConcept) p), headAtom.getArgument(0));
69 if(p instanceof AtomicRole)
70 return Atom.create(generateAuxiliaryRule((AtomicRole) p), headAtom.getArgument(0), headAtom.getArgument(1));
71 if(p instanceof Equality || p instanceof AnnotatedEquality)
72 return Atom.create(generateAuxiliaryRule(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
73 if(p instanceof Inequality)
74 return Atom.create(generateAuxiliaryRule((Inequality) p), headAtom.getArgument(0), headAtom.getArgument(1));
75
76 return null;
77 }
78
79 private Atom getTrackingAtom(Atom headAtom) {
80 DLPredicate p = headAtom.getDLPredicate();
81 if (p instanceof AtLeast) {
82 p = Normalisation.toAtLeastConcept((AtLeast) p);
83 return Atom.create(getTrackingDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom
84 .getArgument(0));
85 }
86 if(p instanceof AtomicConcept)
87 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0));
88 if(p instanceof AtomicRole)
89 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
90 if(p instanceof Equality || p instanceof AnnotatedEquality)
91 return Atom.create(getTrackingDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
92 if(p instanceof Inequality)
93 return Atom.create(getTrackingDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
94
95 return null;
96 }
97
98 private Atom getGapAtom(Atom headAtom) {
99 DLPredicate p = headAtom.getDLPredicate();
100 if (p instanceof AtLeast) {
101 p = Normalisation.toAtLeastConcept((AtLeast) p);
102 return Atom.create(getGapDLPredicate(AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p))), headAtom
103 .getArgument(0));
104 }
105 if(p instanceof AtomicConcept)
106 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
107 if(p instanceof AtomicRole)
108 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
109 if(p instanceof Equality || p instanceof AnnotatedEquality)
110 return Atom.create(getGapDLPredicate(Equality.INSTANCE), headAtom.getArgument(0), headAtom.getArgument(1));
111 if(p instanceof Inequality)
112 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0), headAtom.getArgument(1));
113 if (p instanceof DatatypeRestriction)
114 return Atom.create(getGapDLPredicate(p), headAtom.getArgument(0));
115 Utility.logError(p + " is not recognised.");
116 return null;
117 }
118
119 private void encodingDisjunctiveRule(DLClause clause) {
120 int headLength = clause.getHeadLength();
121
122 Atom[] auxAtoms = new Atom[headLength];
123 for (int i = 0; i < headLength; ++i)
124 auxAtoms[i] = getAuxiliaryAtom(clause.getHeadAtom(i));
125
126 Atom[] trackingAtoms = new Atom[headLength];
127 for (int i = 0; i < headLength; ++i)
128 trackingAtoms[i] = getTrackingAtom(clause.getHeadAtom(i));
129
130 Atom[] gapAtoms = new Atom[headLength];
131 for (int i = 0; i < headLength; ++i)
132 gapAtoms[i] = getGapAtom(clause.getHeadAtom(i));
133
134 Atom[] bodyAtoms = clause.getBodyAtoms();
135
136 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
137 DLPredicate selected = AtomicConcept.create(getSelectedPredicate());
138 newHeadAtoms.add(Atom.create(selected, getIndividual4GeneralRule(clause)));
139
140 for (Atom atom: bodyAtoms) {
141 Atom newAtom = Atom.create(
142 getTrackingDLPredicate(atom.getDLPredicate()),
143 DLClauseHelper.getArguments(atom));
144 newHeadAtoms.add(newAtom);
145 }
146
147 DLClause newClause;
148 int index;
149 for (int j = 0; j < headLength; ++j) {
150 Atom[] newBodyAtoms = new Atom[headLength * 2 + bodyAtoms.length];
151 index = 0;
152 for (int i = 0; i < headLength; ++i, ++index)
153 newBodyAtoms[index] = gapAtoms[i];
154 for (int i = 0; i < headLength; ++i, ++index)
155 if (i != j)
156 newBodyAtoms[index] = auxAtoms[i];
157 else
158 newBodyAtoms[index] = trackingAtoms[i];
159
160 for (int i = 0; i < bodyAtoms.length; ++i, ++index)
161 newBodyAtoms[index] = bodyAtoms[i];
162
163 for (Atom atom: newHeadAtoms) {
164 newClause = DLClause.create(new Atom[]{atom}, newBodyAtoms);
165 addTrackingClause(newClause);
166 }
167 }
168 }
169
170 private void addTrackingClause(DLClause clause) {
171 trackingClauses.add(clause);
172 }
173
174 private void addDisjunctiveRule(DLClause clause) {
175 disjunctiveRules.add(clause);
176 }
177
178 private DLPredicate getAuxPredicate(DLPredicate p) {
179 if (p instanceof AtLeastConcept) {
180 StringBuilder builder = new StringBuilder(
181 Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p));
182 builder.append("_AUXa").append(currentQuery.getQueryID());
183 return AtomicConcept.create(builder.toString());
184 }
185
186 return getDLPredicate(p, "_AUXa" + currentQuery.getQueryID());
187 }
188
189 private DLPredicate getTrackingBottomDLPredicate(DLPredicate p) {
190 return getDLPredicate(p, getTrackingSuffix("0"));
191 }
192
193 private DLPredicate generateAuxiliaryRule(AtLeast p1, boolean withAux) {
194 AtLeastConcept p = Normalisation.toAtLeastConcept(p1);
195
196 int num = p.getNumber();
197 Variable[] Ys = new Variable[num];
198 if (num > 1)
199 for(int i = 0; i < num; ++i)
200 Ys[i] = Variable.create("Y" + (i + 1));
201 else
202 Ys[0] = Y;
203
204 Collection<Atom> expandedAtom = new LinkedList<Atom>();
205 Collection<Atom> representativeAtom = new LinkedList<Atom>();
206 if (p.getOnRole() instanceof AtomicRole) {
207 AtomicRole r = (AtomicRole) p.getOnRole();
208 for(int i = 0; i < num; ++i)
209 expandedAtom.add(Atom.create(r, X, Ys[i]));
210 representativeAtom.add(Atom.create(r, X, Ys[0]));
211 }
212 else {
213 AtomicRole r = ((InverseRole) p.getOnRole()).getInverseOf();
214 for(int i = 0; i < num; ++i)
215 expandedAtom.add(Atom.create(r, Ys[i], X));
216 representativeAtom.add(Atom.create(r, Ys[0], X));
217 }
218
219 if (num > 1) {
220 representativeAtom.add(Atom.create(Inequality.INSTANCE, Ys[0], Ys[1]));
221 }
222 for (int i = 0; i < num; ++i)
223 for (int j = i + 1; j < num; ++j)
224 expandedAtom.add(Atom.create(Inequality.INSTANCE, Ys[i], Ys[j]));
225
226 if (!p.getToConcept().equals(AtomicConcept.THING)) {
227 AtomicConcept c;
228 if(p.getToConcept() instanceof AtomicConcept)
229 c = (AtomicConcept) p.getToConcept();
230 else {
231 c = OverApproxExist.getNegationConcept(((AtomicNegationConcept) p.getToConcept()).getNegatedAtomicConcept());
232 }
233 for (int i = 0; i < num; ++i)
234 expandedAtom.add(Atom.create(c, Ys[i]));
235 representativeAtom.add(Atom.create(c, Ys[0]));
236 }
237
238 AtomicConcept ac = AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct(p));
239 DLPredicate trackingPredicate = getTrackingDLPredicate(ac);
240 DLPredicate gapPredicate = getGapDLPredicate(ac);
241 DLPredicate auxPredicate = withAux ? getAuxPredicate(p) : null;
242
243 for (Atom atom: representativeAtom) {
244 Atom[] bodyAtoms = new Atom[expandedAtom.size() + 1];
245 if (atom.getArity() == 1)
246 bodyAtoms[0] = Atom.create(getTrackingDLPredicate(atom.getDLPredicate()), atom.getArgument(0));
247 else
248 bodyAtoms[0] = Atom.create(getTrackingDLPredicate(atom.getDLPredicate()), atom.getArgument(0), atom.getArgument(1));
249 int i = 0;
250 for (Atom bodyAtom: expandedAtom)
251 bodyAtoms[++i] = bodyAtom;
252 addTrackingClause(DLClause.create(new Atom[] {Atom.create(trackingPredicate, X)}, bodyAtoms));
253
254 bodyAtoms = new Atom[expandedAtom.size() + 1];
255 if (atom.getArity() == 1)
256 bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0));
257 else
258 bodyAtoms[0] = Atom.create(getGapDLPredicate(atom.getDLPredicate()), atom.getArgument(0), atom.getArgument(1));
259 i = 0;
260 for (Atom bodyAtom: expandedAtom)
261 bodyAtoms[++i] = bodyAtom;
262 addTrackingClause(DLClause.create(new Atom[] {Atom.create(gapPredicate, X)}, bodyAtoms));
263
264 if (withAux) {
265 bodyAtoms = new Atom[expandedAtom.size() + 1];
266 bodyAtoms[0] = getAuxiliaryAtom(atom);
267 i = 0;
268 for (Atom bodyAtom: expandedAtom)
269 bodyAtoms[++i] = bodyAtom;
270 addTrackingClause(DLClause.create(new Atom[] {Atom.create(auxPredicate, X)}, bodyAtoms));
271 }
272 }
273
274 return withAux ? auxPredicate : trackingPredicate;
275 }
276
277 private DLPredicate generateAuxiliaryRule(AtomicRole p) {
278 if(currentQuery.isBottom())
279 return getTrackingDLPredicate(p);
280
281 DLPredicate ret = getAuxPredicate(p);
282 Atom[] headAtom = new Atom[] {Atom.create(ret, X, Y)};
283
284 addTrackingClause(
285 DLClause.create(headAtom, new Atom[]{Atom.create(getTrackingDLPredicate(p), X, Y)}));
286 addTrackingClause(
287 DLClause.create(headAtom, new Atom[]{Atom.create(getTrackingBottomDLPredicate(p), X, Y)}));
288
289 return ret;
290 }
291
292 private DLPredicate generateAuxiliaryRule(AtomicConcept p) {
293 if (currentQuery.isBottom())
294 return getTrackingDLPredicate(p);
295
296 DLPredicate ret = getAuxPredicate(p);
297 Atom[] headAtom = new Atom[]{Atom.create(ret, X)};
298 addTrackingClause(
299 DLClause.create(headAtom,
300 new Atom[]{Atom.create(getTrackingDLPredicate(p), X)}));
301 addTrackingClause(
302 DLClause.create(headAtom,
303 new Atom[] { Atom.create(getTrackingBottomDLPredicate(p), X)}));
304
305 return ret;
306 }
307
308 private DLPredicate generateAuxiliaryRule(Equality instance) {
309 return generateAuxiliaryRule(AtomicRole.create(Namespace.EQUALITY));
310 }
311
312 private DLPredicate generateAuxiliaryRule(Inequality instance) {
313 return generateAuxiliaryRule(AtomicRole.create(Namespace.INEQUALITY));
314 }
315
316 @Override
317 public String getTrackingProgram() {
318 StringBuilder sb = getTrackingProgramBody();
319 if (currentQuery.isBottom())
320 sb.append(getBottomTrackingProgram());
321 sb.insert(0, MyPrefixes.PAGOdAPrefixes.prefixesText());
322 return sb.toString();
323 }
324
325 private String getBottomTrackingProgram() {
326 if (bottomTrackingProgram != null) return bottomTrackingProgram.replace("_tn", getTrackingPredicate(""));
327
328 String bottomSuffix = getTrackingSuffix("0");
329 LinkedList<DLClause> clauses = new LinkedList<DLClause>();
330 Variable X = Variable.create("X");
331 for (String concept: unaryPredicates)
332 clauses.add(DLClause.create(new Atom[] {Atom.create(AtomicConcept.create(concept + bottomSuffix) , X)},
333 new Atom[] {Atom.create(AtomicConcept.create(concept + "_tn"), X)}));
334 Variable Y = Variable.create("Y");
335 for (String role: binaryPredicates)
336 clauses.add(DLClause.create(new Atom[] {Atom.create(AtomicRole.create(role + bottomSuffix) , X, Y)},
337 new Atom[] {Atom.create(AtomicRole.create(role + "_tn"), X, Y) }));
338
339 StringBuilder builder = new StringBuilder(DLClauseHelper.toString(clauses));
340 bottomTrackingProgram = builder.toString();
341 return bottomTrackingProgram.replace("_tn", getTrackingPredicate(""));
342 }
343
344 private void encodingBottomQueryClause(DLClause clause) {
345 if (!clause.toString().contains("owl:Nothing"))
346 clause = program.getCorrespondingClause(clause);
347
348// Term t;
349// for (Atom tAtom: clause.getHeadAtoms()) {
350// for (int i = 0; i < tAtom.getArity(); ++i)
351// if ((t = tAtom.getArgument(i)) instanceof Individual)
352// if (((Individual) t).getIRI().startsWith(OverApproxExist.SKOLEMISED_INDIVIDUAL_PREFIX))
353// clause = program.getCorrespondingClause(clause);
354// }
355
356 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
357 Atom selectAtom = Atom.create(selected, getIndividual4GeneralRule(program.getCorrespondingClause(clause)));
358
359 for (Atom atom: clause.getBodyAtoms()) {
360 atom = Atom.create(
361 getTrackingDLPredicate(atom.getDLPredicate()),
362 DLClauseHelper.getArguments(atom));
363 newHeadAtoms.add(atom);
364 }
365
366 DLClause newClause;
367
368 boolean botInHead = clause.getBodyLength() == 1 && clause.getBodyAtom(0).getDLPredicate().toString().contains("owl:Nothing");
369
370 DLPredicate[] trackingPredicates = new DLPredicate[clause.getHeadLength()];
371 DLPredicate[] predicates = new DLPredicate[clause.getHeadLength()];
372 int headIndex = 0;
373 DLPredicate trackingPredicate, p;
374 for (Atom headAtom: clause.getHeadAtoms()) {
375 if ((p = headAtom.getDLPredicate()) instanceof AtLeastConcept) {
376 trackingPredicate = generateAuxiliaryRule((AtLeastConcept) p, false);
377 p = AtomicConcept.create(Normalisation.getAuxiliaryConcept4Disjunct((AtLeastConcept) p));
378 trackingClauses.add(DLClause.create(
379 new Atom[] { Atom.create(getDLPredicate(p, getTrackingSuffix("0")), X) },
380 new Atom[] { Atom.create(trackingPredicate, X) }));
381 }
382 else
383 trackingPredicate = getTrackingDLPredicate(p);
384
385 trackingPredicates[headIndex] = trackingPredicate;
386 predicates[headIndex] = p;
387 ++headIndex;
388 }
389
390 headIndex = 0;
391 int headLength = clause.getHeadLength();
392 Atom[] gapAtoms = new Atom[headLength];
393 for (int i = 0; i < headLength; ++i)
394 gapAtoms[i] = getGapAtom(clause.getHeadAtom(i));
395// Atom.create(getGapDLPredicate(predicates[headIndex]), DLClauseHelper.getArguments(clause.getHeadAtom(i)));
396 int index, selectIndex;
397 for (Atom headAtom: clause.getHeadAtoms()) {
398 index = 0; selectIndex = 0;
399 Atom[] newBodyAtoms = new Atom[clause.getBodyLength() + 1 + headLength - 1 + (botInHead ? 0 : headLength)];
400 Atom[] selectBodyAtoms = new Atom[clause.getBodyLength() + 1 + (botInHead ? 0 : headLength)];
401 newBodyAtoms[index++] = selectBodyAtoms[selectIndex++] = Atom.create(trackingPredicates[headIndex], DLClauseHelper.getArguments(headAtom));
402
403 if (!botInHead) {
404 for (int i = 0; i < headLength; ++i)
405 newBodyAtoms[index++] = selectBodyAtoms[selectIndex++] = gapAtoms[i];
406 }
407
408 for (int i = 0; i < headLength; ++i)
409 if (i != headIndex) {
410 newBodyAtoms[index++] = Atom.create(getDLPredicate(predicates[i], getTrackingSuffix("0")), DLClauseHelper.getArguments(clause.getHeadAtom(i)));
411 }
412
413 for (int i = 0; i < clause.getBodyLength(); ++i)
414 newBodyAtoms[index++] = selectBodyAtoms[selectIndex++] = clause.getBodyAtom(i);
415
416 for (Atom atom: newHeadAtoms) {
417 newClause = DLClause.create(new Atom[] {atom}, newBodyAtoms);
418 trackingClauses.add(newClause);
419 }
420 trackingClauses.add(DLClause.create(new Atom[] {selectAtom}, selectBodyAtoms));
421 ++headIndex;
422 }
423 }
424
425}
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-06 09:28:59 +0000