aboutsummaryrefslogtreecommitdiff
path: root/src/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java
diff options
context:
space:
mode:
authoryzhou <yujiao.zhou@gmail.com>2015-04-21 10:34:27 +0100
committeryzhou <yujiao.zhou@gmail.com>2015-04-21 10:34:27 +0100
commit9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8 (patch)
tree47511c0fb89dccff0db4b5990522e04f294d795b /src/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java
parentb1ac207612ee8b045244253fb94b866104bc34f2 (diff)
downloadACQuA-9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8.tar.gz
ACQuA-9ce65c5a963b03ee97fe9cb6c5aa65a3c04a80a8.zip
initial version
Diffstat (limited to 'src/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java')
-rw-r--r--src/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java480
1 files changed, 480 insertions, 0 deletions
diff --git a/src/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java b/src/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java
new file mode 100644
index 0000000..c3f7a2a
--- /dev/null
+++ b/src/uk/ac/ox/cs/pagoda/hermit/DLClauseHelper.java
@@ -0,0 +1,480 @@
1package uk.ac.ox.cs.pagoda.hermit;
2
3import java.util.Collection;
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.Prefixes;
11import org.semanticweb.HermiT.model.AnnotatedEquality;
12import org.semanticweb.HermiT.model.AtLeastDataRange;
13import org.semanticweb.HermiT.model.Atom;
14import org.semanticweb.HermiT.model.AtomicConcept;
15import org.semanticweb.HermiT.model.AtomicDataRange;
16import org.semanticweb.HermiT.model.AtomicNegationDataRange;
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.DLPredicate;
22import org.semanticweb.HermiT.model.Equality;
23import org.semanticweb.HermiT.model.Individual;
24import org.semanticweb.HermiT.model.Inequality;
25import org.semanticweb.HermiT.model.Term;
26import org.semanticweb.HermiT.model.Variable;
27
28import uk.ac.ox.cs.pagoda.owl.OWLHelper;
29import uk.ac.ox.cs.pagoda.util.Namespace;
30import uk.ac.ox.cs.pagoda.util.SparqlHelper;
31import uk.ac.ox.cs.pagoda.util.Utility;
32
33public class DLClauseHelper {
34
35 public static String getIRI4Nominal(DLPredicate predicate) {
36 return ((AtomicConcept) predicate).getIRI().replace("internal:nom#", "");
37 }
38
39 public static DLClause removeNominalConcept(DLClause clause) {
40 boolean hasNominals = false;
41 Map<Variable, String> nom2iri = new HashMap<Variable, String>();
42 DLPredicate predicate;
43 Collection<Atom> remainingBodyAtoms = new LinkedList<Atom>();
44 for (Atom atom: clause.getBodyAtoms()) {
45 predicate = atom.getDLPredicate();
46 if (predicate instanceof AtomicConcept && predicate.toString().startsWith("<internal:nom#")) {
47 nom2iri.put(atom.getArgumentVariable(0), getIRI4Nominal(predicate));
48 hasNominals = true;
49 }
50 else remainingBodyAtoms.add(atom);
51 }
52
53 if (!hasNominals) return clause;
54
55 Atom[] newHeadAtoms = new Atom[clause.getHeadLength()];
56 int i = 0;
57 for (Atom atom: clause.getHeadAtoms()) {
58 newHeadAtoms[i++] = getNewAtom(atom, nom2iri);
59 }
60
61 Atom[] newBodyAtoms = new Atom[remainingBodyAtoms.size()];
62 i = 0;
63 for (Atom atom: remainingBodyAtoms) {
64 newBodyAtoms[i++] = getNewAtom(atom, nom2iri);
65 }
66
67 return DLClause.create(newHeadAtoms, newBodyAtoms);
68 }
69
70 public static Atom getNewAtom(Atom atom, Map<Variable, String> nom2iri) {
71 String iri;
72 DLPredicate predicate = atom.getDLPredicate();
73 if (predicate instanceof AtomicRole) {
74 boolean updated = false;
75 Term newArg0 = atom.getArgument(0), newArg1 = atom.getArgument(1);
76 if (newArg0 instanceof Variable && ((iri = nom2iri.get((Variable) newArg0)) != null)) {
77 newArg0 = Individual.create(iri);
78 updated = true;
79 }
80 if (newArg1 instanceof Variable && ((iri = nom2iri.get((Variable) newArg1)) != null)) {
81 newArg1 = Individual.create(iri);
82 updated = true;
83 }
84 if (updated) {
85 return Atom.create(atom.getDLPredicate(), newArg0, newArg1);
86 }
87 }
88 else if (predicate instanceof Equality || predicate instanceof AnnotatedEquality) {
89// System.out.println("To be removed ... \n" + atom);
90 Term two[] = new Term[] { atom.getArgument(0), atom.getArgument(1) };
91 Term t;
92 for (int i = 0; i < 2; ++i) {
93 t = atom.getArgument(i);
94 if (t != null && t instanceof Variable && (iri = nom2iri.get((Variable) t)) != null) {
95 two[i] = Individual.create(iri);
96 }
97 }
98 return Atom.create(Equality.INSTANCE, two);
99 }
100
101 return atom;
102 }
103
104 /**
105 * This is a preprocess for StatOil:
106 *
107 * if (AtomicNegationDataRange o (ConstantEnumerate (value))) (Z)
108 * appears the head, then replace all Z in the clause by value.
109 *
110 *
111 * @param clause
112 */
113 public static DLClause replaceWithDataValue(DLClause clause) {
114 Map<Variable, Constant> var2dataValue = new HashMap<Variable, Constant>();
115
116 boolean update = false;
117 LinkedList<Atom> newHeadAtoms = new LinkedList<Atom>();
118 for (Atom cAtom: clause.getHeadAtoms()) {
119 DLPredicate dlPredicate = cAtom.getDLPredicate();
120 if (dlPredicate instanceof AtomicNegationDataRange) {
121 AtomicDataRange atomicDataRange = ((AtomicNegationDataRange) dlPredicate).getNegatedDataRange();
122 if (atomicDataRange instanceof ConstantEnumeration) {
123 ConstantEnumeration enumeration = (ConstantEnumeration) atomicDataRange;
124 if (enumeration.getNumberOfConstants() == 1) {
125 Constant constant = enumeration.getConstant(0);
126 //TODO replace unsupported datatypes
127// if (constant.getDatatypeURI().endsWith("boolean"))
128// constant = Constant.create(constant.getLexicalForm(), constant.getDatatypeURI().replace("boolean", "string"));
129 var2dataValue.put(cAtom.getArgumentVariable(0), constant);
130 }
131 }
132 }
133 else if (dlPredicate instanceof ConstantEnumeration) {
134 ConstantEnumeration enu = (ConstantEnumeration) dlPredicate;
135 for (int i = 0; i < enu.getNumberOfConstants(); ++i)
136 newHeadAtoms.add(Atom.create(Equality.INSTANCE, cAtom.getArgument(0), enu.getConstant(i)));
137 update = true;
138 }
139 else if (dlPredicate instanceof AtLeastDataRange && ((AtLeastDataRange) dlPredicate).getToDataRange() instanceof ConstantEnumeration) {
140 AtLeastDataRange atLeast = (AtLeastDataRange) dlPredicate;
141 ConstantEnumeration enu = (ConstantEnumeration) atLeast.getToDataRange();
142 for (int i = 0; i < enu.getNumberOfConstants(); ++i)
143 newHeadAtoms.add(Atom.create((AtomicRole) atLeast.getOnRole(), cAtom.getArgument(0), enu.getConstant(i)));
144 update = true;
145 }
146 else
147 newHeadAtoms.add(cAtom);
148 }
149
150 if (var2dataValue.isEmpty()) return update ? DLClause.create(newHeadAtoms.toArray(new Atom[0]), clause.getBodyAtoms()) : clause;
151
152 Atom[] newBodyAtoms = new Atom[clause.getBodyLength()];
153 Term[] newArgs;
154 int index = 0;
155 boolean atomUpdated;
156 for (Atom bodyAtom: clause.getBodyAtoms()) {
157 newBodyAtoms[index] = bodyAtom;
158 atomUpdated = false;
159 newArgs = new Term[bodyAtom.getArity()];
160 for (int i = 0; i < newArgs.length; ++i) {
161 newArgs[i] = bodyAtom.getArgument(i);
162 if (newArgs[i] instanceof Variable && var2dataValue.containsKey(newArgs[i])) {
163 newArgs[i] = var2dataValue.get(newArgs[i]);
164 atomUpdated = true;
165 }
166 }
167 if (atomUpdated)
168 newBodyAtoms[index] = Atom.create(bodyAtom.getDLPredicate(), newArgs);
169 ++index;
170 }
171
172 return DLClause.create(newHeadAtoms.toArray(new Atom[0]), newBodyAtoms);
173 }
174
175 public static DLClause simplified(DLClause clause) {
176 TermGraph termGraph = new TermGraph(clause);
177 return termGraph.simplify();
178 }
179
180 public static DLClause contructor_differentFrom(Individual u, Individual v) {
181 Atom equalityAtom = Atom.create(AtomicRole.create(Namespace.EQUALITY), u, v);
182 return DLClause.create(new Atom[0], new Atom[] {equalityAtom});
183 }
184
185 public static String toString(Collection<DLClause> clauses) {
186 StringBuilder buf = new StringBuilder();
187 for (DLClause cls: clauses) {
188 buf.append(RuleHelper.getText(cls));
189 buf.append(Utility.LINE_SEPARATOR);
190 }
191 return buf.toString();
192 }
193
194 public static DLClause getInstance(DLClause queryClause, Map<Variable, Term> assignment) {
195 Atom[] newBodyAtoms = new Atom[queryClause.getBodyLength()];
196 int index = 0;
197 for (Atom atom: queryClause.getBodyAtoms()) {
198 newBodyAtoms[index++] = getInstance(atom, assignment);
199 }
200 return DLClause.create(queryClause.getHeadAtoms(), newBodyAtoms);
201 }
202
203 public static Atom getInstance(Atom atom, Map<Variable, Term> assignment) {
204 Term[] args = getArguments(atom);
205 for (int i = 0; i < args.length; ++i)
206 args[i] = getInstance(args[i], assignment);
207 return Atom.create(atom.getDLPredicate(), args);
208 }
209
210 private static Term getInstance(Term t, Map<Variable, Term> assignment) {
211 if (t instanceof Variable && assignment.containsKey((Variable) t))
212 return assignment.get(t);
213 return t;
214 }
215
216 public static Term[] getArguments(Atom atom) {
217 int len = atom.getArity();
218 if (len >= 2) len = 2;
219 Term[] args = new Term[len];
220 for (int i = 0; i < len; ++i)
221 args[i] = atom.getArgument(i);
222 return args;
223 }
224
225 public static DLClause getQuery(String queryText, Collection<String> answerVariables) {
226 Collection<Atom> bodyAtoms = new LinkedList<Atom>();
227 SparqlHelper.parse(queryText.replace("_:", "?"), answerVariables, bodyAtoms);
228 return DLClause.create(new Atom[0], bodyAtoms.toArray(new Atom[0]));
229 }
230
231 public static DLClause getQuery_old(String queryText, Collection<String> answerVariables) {
232 String key, value;
233 Prefixes prefixes = new Prefixes();
234 if (answerVariables != null)
235 answerVariables.clear();
236 String[] temp;
237 Term subject, object;
238 LinkedList<Atom> bodyAtoms = new LinkedList<Atom>();
239
240 for (String line: queryText.split("\n")) {
241 line = line.trim();
242 if (line.startsWith("PREFIX")) {
243 key = line.substring(7, line.indexOf(':') + 1);
244 value = line.substring(line.indexOf('<') + 1, line.length() - 1);
245 prefixes.declarePrefix(key, value);
246 }
247 else if (line.startsWith("SELECT")) {
248 if (answerVariables == null)
249 continue;
250 temp = line.split(" ");
251 for (int i = 1; i < temp.length; ++i)
252 answerVariables.add(temp[i].substring(1));
253 }
254 else if (line.startsWith("WHERE"))
255 ;
256 else if (line.startsWith("}"))
257 ;
258 else {
259 temp = line.split(" ");
260 subject = getTerm(getAbsoluteIRI(temp[0], prefixes));
261 temp[1] = getAbsoluteIRI(temp[1], prefixes);
262 temp[2] = getAbsoluteIRI(temp[2], prefixes);
263 if (temp[1].equals(Namespace.RDF_TYPE)) {
264 temp[2] = getAbsoluteIRI(temp[2], prefixes);
265 bodyAtoms.add(Atom.create(AtomicConcept.create(temp[2]), subject));
266 } else {
267 object = getTerm(temp[2]);
268 Term[] args = {subject, object};
269 bodyAtoms.add(Atom.create(AtomicRole.create(temp[1]), args));
270 }
271 }
272 }
273
274 return DLClause.create(new Atom[0], bodyAtoms.toArray(new Atom[0]));
275 }
276
277 private static String getAbsoluteIRI(String iri, Prefixes prefixes) {
278 if (prefixes.canBeExpanded(iri))
279 return prefixes.expandAbbreviatedIRI(iri);
280 if (iri.startsWith("<"))
281 return OWLHelper.removeAngles(iri);
282 return iri;
283 }
284
285 private static Term getTerm(String iri) {
286 if (iri.startsWith("?"))
287 return Variable.create(iri.substring(1));
288 else if (iri.contains("http"))
289 return Individual.create(iri);
290 else
291 return getConstant(iri);
292 }
293
294 private static Constant getConstant(String iri) {
295 String lexicalForm, datatypeIRI;
296 int index = iri.indexOf("^^");
297 if (index == -1) {
298 lexicalForm = iri;
299 int atPos = iri.indexOf("@");
300 datatypeIRI = atPos == -1 ? Namespace.XSD_STRING : Namespace.RDF_PLAIN_LITERAL;
301 }
302 else {
303 if (iri.charAt(index + 2) == '<')
304 datatypeIRI = iri.substring(index + 3, iri.length() - 1);
305 else
306 datatypeIRI = iri.substring(index + 2);
307 lexicalForm = iri.substring(1, index - 1);
308 }
309 return Constant.create(lexicalForm, datatypeIRI);
310 }
311
312 public static boolean isFunctionalDataPropertyAxioms(DLClause dlClause) {
313 if (dlClause.getBodyLength()==2 && dlClause.getHeadLength()==1) {
314 DLPredicate atomicRole=dlClause.getBodyAtom(0).getDLPredicate();
315 if (atomicRole instanceof AtomicRole) {
316 if (dlClause.getBodyAtom(1).getDLPredicate().equals(atomicRole) &&
317 (dlClause.getHeadAtom(0).getDLPredicate() instanceof Equality ||
318 dlClause.getHeadAtom(0).getDLPredicate() instanceof AnnotatedEquality)) {
319 Variable x=dlClause.getBodyAtom(0).getArgumentVariable(0);
320 if (x!=null && x.equals(dlClause.getBodyAtom(1).getArgument(0))) {
321 Variable y1=dlClause.getBodyAtom(0).getArgumentVariable(1);
322 Variable y2=dlClause.getBodyAtom(1).getArgumentVariable(1);
323 Variable headY1=dlClause.getHeadAtom(0).getArgumentVariable(0);
324 Variable headY2=dlClause.getHeadAtom(0).getArgumentVariable(1);
325 if (y1!=null && y2!=null && !y1.equals(y2) && headY1!=null && headY2!=null && ((y1.equals(headY1) && y2.equals(headY2)) || (y1.equals(headY2) && y2.equals(headY1))))
326 return true;
327 }
328 }
329 }
330 }
331 return false;
332 }
333
334 /**
335 *
336 * @param dlClause
337 * @return 000 -> 111 R \circ S \sqsubseteq T if R, S, T is inverse. -1 if it is not a role composition axiom.
338 */
339 public static int isRoleCompositionAxioms(DLClause dlClause) {
340 if (dlClause.getBodyLength()==2 && dlClause.getHeadLength()==1) {
341 Atom body1 = dlClause.getBodyAtom(0), body2 = dlClause.getBodyAtom(1);
342 Atom head = dlClause.getHeadAtom(0);
343 if (!(head.getDLPredicate() instanceof AtomicRole)) return -1;
344 if (!(body1.getDLPredicate() instanceof AtomicRole)) return -1;
345 if (!(body2.getDLPredicate() instanceof AtomicRole)) return -1;
346 if (!(head.getArgument(0) instanceof Variable)) return -1;
347 if (!(head.getArgument(1) instanceof Variable)) return -1;
348 if (!(body1.getArgument(0) instanceof Variable)) return -1;
349 if (!(body1.getArgument(1) instanceof Variable)) return -1;
350 if (!(body2.getArgument(0) instanceof Variable)) return -1;
351 if (!(body2.getArgument(1) instanceof Variable)) return -1;
352 Variable rx, ry, sx, sy, tx, ty;
353 tx = head.getArgumentVariable(0); ty = head.getArgumentVariable(1);
354 rx = body1.getArgumentVariable(0); ry = body1.getArgumentVariable(1);
355 sx = body2.getArgumentVariable(0); sy = body2.getArgumentVariable(1);
356
357 if (rx.equals(tx))
358 if (ry.equals(sx))
359 if (sy.equals(ty)) return 0;
360 else return -1;
361 else if (ry.equals(sy))
362 if (sx.equals(ty)) return 2;
363 else return -1;
364 else
365 return -1;
366 else if (rx.equals(ty))
367 if (ry.equals(sx))
368 if (sy.equals(tx)) return 1;
369 else return -1;
370 else if (ry.equals(sy))
371 if (sx.equals(tx)) return 3;
372 else return -1;
373 else
374 return -1;
375 else if (ry.equals(tx))
376 if (rx.equals(sx))
377 if (sy.equals(ty)) return 4;
378 else return -1;
379 else if (rx.equals(sy))
380 if (sx.equals(ty)) return 6;
381 else return -1;
382 else
383 return -1;
384 else if (ry.equals(ty))
385 if (rx.equals(sx))
386 if (sy.equals(tx)) return 5;
387 else return -1;
388 else if (rx.equals(sy))
389 if (sx.equals(tx)) return 7;
390 else return -1;
391 else return -1;
392 else
393 return -1;
394 }
395 return -1;
396 }
397
398 public static boolean isGround(Atom tHeadAtom) {
399 for (int i = 0; i < tHeadAtom.getArity(); ++i)
400 if (tHeadAtom.getArgument(i) instanceof Variable)
401 return false;
402 return true;
403 }
404 /**
405 * true if a \subseteq b
406 * @param a
407 * @param b
408 * @return
409 */
410 private static boolean hasSubsetAtoms(Atom[] a, Atom[] b) {
411 Set<String> atoms = new HashSet<String>();
412 for (int i = 0; i < b.length; ++i)
413 atoms.add(b[i].toString());
414
415 for (int i = 0; i < a.length; ++i)
416 if (!atoms.remove(a[i].toString()))
417 return false;
418
419 return true;
420 }
421
422 public static boolean hasSubsetBodyAtoms(DLClause c1, DLClause c2) {
423 return hasSubsetAtoms(c1.getBodyAtoms(), c2.getBodyAtoms());
424 }
425
426 public static DLClause replaceOtherBottom(DLClause dlClause) {
427 Atom[] newHeadAtoms = dlClause.getHeadAtoms(), newBodyAtoms = dlClause.getBodyAtoms();
428 if (containsOtherBottom(newHeadAtoms))
429 newHeadAtoms = replaceOtherBottom(newHeadAtoms);
430 if (containsOtherBottom(newBodyAtoms))
431 newBodyAtoms = replaceOtherBottom(newBodyAtoms);
432
433 if (newHeadAtoms == dlClause.getHeadAtoms() && newBodyAtoms == dlClause.getBodyAtoms())
434 return dlClause;
435
436 return DLClause.create(newHeadAtoms, newBodyAtoms);
437 }
438
439 private static Atom[] replaceOtherBottom(Atom[] atoms) {
440 Atom[] newAtoms = new Atom[atoms.length];
441 int index = 0;
442 for (Atom atom: atoms)
443 if (isOtherBottom(atom.getDLPredicate()))
444 newAtoms[index++] = Atom.create(AtomicConcept.NOTHING, atom.getArgument(0));
445 else
446 newAtoms[index++] = atom;
447 return newAtoms;
448 }
449
450 private static boolean isOtherBottom(DLPredicate p) {
451 if (!(p instanceof AtomicConcept)) return false;
452
453 String name = p.toString();
454 int index;
455 char ch;
456 if ((index = name.indexOf("owl:Nothing")) != -1) {
457 index += 11;
458 if (name.length() <= index) return true;
459 if ((ch = name.charAt(index)) == '_') return true;
460 if (ch >= '0' && ch <= '9') return true;
461 }
462 return false;
463 }
464
465 private static boolean containsOtherBottom(Atom[] atoms) {
466 for (Atom atom: atoms)
467 if (isOtherBottom(atom.getDLPredicate()))
468 return true;
469 return false;
470 }
471
472 public static boolean isTautologyAboutDifferentFrom(DLClause clause) {
473 if (clause.getHeadLength() > 1 || clause.getBodyLength() != 1) return false;
474 if (clause.getHeadLength() == 1 && !clause.getHeadAtom(0).getDLPredicate().toString().contains(AtomicConcept.NOTHING.toString()))
475 return false;
476 Atom bodyAtom = clause.getBodyAtom(0);
477 return (bodyAtom.getDLPredicate() instanceof Inequality) && bodyAtom.getArgument(0).equals(bodyAtom.getArgument(1));
478 }
479
480}
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-05 19:28:12 +0000