001    /**
002     * Copyright (C) 2007-2011, Jens Lehmann
003     *
004     * This file is part of DL-Learner.
005     *
006     * DL-Learner is free software; you can redistribute it and/or modify
007     * it under the terms of the GNU General Public License as published by
008     * the Free Software Foundation; either version 3 of the License, or
009     * (at your option) any later version.
010     *
011     * DL-Learner is distributed in the hope that it will be useful,
012     * but WITHOUT ANY WARRANTY; without even the implied warranty of
013     * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
014     * GNU General Public License for more details.
015     *
016     * You should have received a copy of the GNU General Public License
017     * along with this program.  If not, see <http://www.gnu.org/licenses/>.
018     */
019    
020    package org.dllearner.utilities.owl;
021    
022    import java.util.Collections;
023    import java.util.Comparator;
024    import java.util.Iterator;
025    import java.util.LinkedList;
026    import java.util.List;
027    import java.util.Set;
028    import java.util.SortedSet;
029    import java.util.TreeSet;
030    
031    import org.dllearner.core.AbstractReasonerComponent;
032    import org.dllearner.core.owl.ObjectAllRestriction;
033    import org.dllearner.core.owl.NamedClass;
034    import org.dllearner.core.owl.Nothing;
035    import org.dllearner.core.owl.Description;
036    import org.dllearner.core.owl.ObjectCardinalityRestriction;
037    import org.dllearner.core.owl.ObjectMaxCardinalityRestriction;
038    import org.dllearner.core.owl.ObjectMinCardinalityRestriction;
039    import org.dllearner.core.owl.ObjectProperty;
040    import org.dllearner.core.owl.ObjectSomeRestriction;
041    import org.dllearner.core.owl.Intersection;
042    import org.dllearner.core.owl.Property;
043    import org.dllearner.core.owl.Restriction;
044    import org.dllearner.core.owl.Union;
045    import org.dllearner.core.owl.Negation;
046    import org.dllearner.core.owl.ObjectPropertyExpression;
047    import org.dllearner.core.owl.ObjectQuantorRestriction;
048    import org.dllearner.core.owl.Thing;
049    
050    /**
051     * Concept transformation and concept checking methods.
052     * 
053     * @author Jens Lehmann
054     */
055    public class ConceptTransformation {
056    
057            public static long cleaningTimeNs = 0;
058            private static long cleaningTimeNsStart = 0;    
059            public static long onnfTimeNs = 0;
060            private static long onnfTimeNsStart = 0;
061            public static long shorteningTimeNs = 0;
062            private static long shorteningTimeNsStart = 0;
063            
064            private static ConceptComparator descComp = new ConceptComparator();
065            
066            public static void cleanConceptNonRecursive(Description concept) {
067                    // cleaningTimeNsStart = System.nanoTime();
068                    
069                    if(concept instanceof Intersection || concept instanceof Union) {
070    
071                            List<Description> deleteChilds = new LinkedList<Description>();
072                            
073                            for(Description child : concept.getChildren()) {
074                                    if((concept instanceof Intersection && child instanceof Intersection)
075                                                    || (concept instanceof Union && child instanceof Union)) {
076                                            deleteChilds.add(child);
077                                    }
078                            }
079                            
080                            for(Description dc : deleteChilds) {
081                                    // alle Kinder des zu löschenden Konzeptes hinzufügen
082                                    for(Description dcChild : dc.getChildren()) {
083                                            concept.addChild(dcChild);
084                                    }
085                                    // Konzept selber löschen
086                                    concept.removeChild(dc);
087                            }
088                            
089                    }
090                    
091                    // cleaningTimeNs += System.nanoTime() - cleaningTimeNsStart;
092            }
093            
094            
095    
096            // eliminiert Disjunktionen in Disjunktionen bzw. Konjunktionen in Konjunktionen
097            public static void cleanConcept(Description concept) {
098                    
099                    // Rekursion (verändert Eingabekonzept)
100                    for(Description child : concept.getChildren()) {
101                            cleanConcept(child);
102                    }
103                    
104                    cleaningTimeNsStart = System.nanoTime();
105                    /*
106                    if(concept instanceof Bottom || concept instanceof Top || concept instanceof AtomicConcept)
107                            return concept;
108                    else if(concept instanceof Negation)
109                            return new Negation(concept.getChild(0));
110                    else if(concept instanceof Exists)
111                            return new Exists(((Quantification)concept).getRole(),cleanConcept(concept.getChild(0)));
112                    else if(concept instanceof All)
113                            return new All(((Quantification)concept).getRole(),cleanConcept(concept.getChild(0)));
114                    */
115                    if(concept instanceof Intersection || concept instanceof Union) {
116    
117                            List<Description> deleteChilds = new LinkedList<Description>();
118                            
119                            for(Description child : concept.getChildren()) {
120                                    if((concept instanceof Intersection && child instanceof Intersection)
121                                                    || (concept instanceof Union && child instanceof Union)) {
122                                            deleteChilds.add(child);
123                                    }
124                            }
125                            
126                            for(Description dc : deleteChilds) {
127                                    // alle Kinder des zu löschenden Konzeptes hinzufügen
128                                    for(Description dcChild : dc.getChildren()) {
129                                            concept.addChild(dcChild);
130                                    }
131                                    // Konzept selber löschen
132                                    concept.removeChild(dc);
133                            }
134                            
135                    }
136                    cleaningTimeNs += System.nanoTime() - cleaningTimeNsStart;
137                            
138            }
139            
140            // wandelt ein Konzept in Negationsnormalform um
141            public static Description transformToNegationNormalForm(Description concept) {
142                    if(concept instanceof Negation) {
143                            Description child = concept.getChild(0);
144                            
145                            if(child.getChildren().size()==0) {
146                                    // NOT TOP = BOTTOM
147                                    if(child instanceof Thing)
148                                            return new Nothing();
149                                    // NOT BOTTOM = TOP
150                                    else if(child instanceof Nothing)
151                                            return new Thing();
152                                    // atomares Konzept: NOT A wird zurückgegeben
153                                    else if(child instanceof NamedClass)
154                                            return concept;
155                                    else
156                                            throw new RuntimeException("Conversion to negation normal form not supported for " + concept);
157                            } else {
158                                    if(child instanceof Negation) {
159                                            // doppelte Negation hebt sich auf
160                                            return transformToNegationNormalForm(child.getChild(0));
161                                    } else if(child instanceof ObjectQuantorRestriction) {
162                                            ObjectPropertyExpression r = ((ObjectQuantorRestriction)child).getRole();
163                                            // Negation nach innen
164                                            Description c = new Negation(child.getChild(0));
165                                            // Exists
166                                            if(child instanceof ObjectSomeRestriction)
167                                                    return new ObjectAllRestriction(r,transformToNegationNormalForm(c));
168                                            // All
169                                            else
170                                                    return new ObjectSomeRestriction(r,transformToNegationNormalForm(c));                                   
171                                    } else if(child instanceof ObjectCardinalityRestriction) {
172                                            ObjectCardinalityRestriction card = (ObjectCardinalityRestriction)child;
173                                            ObjectPropertyExpression r = card.getRole();
174                                            int number = card.getCardinality();
175                                            // Negation nach innen
176                                            Description c = new Negation(child.getChild(0));
177                                            // <= n is transformed to >= n+1 
178                                            if(child instanceof ObjectMaxCardinalityRestriction)
179                                                    return new ObjectMinCardinalityRestriction(number+1,r,transformToNegationNormalForm(c));
180                                            // >= n is transformed to <= n-1
181                                            else if(child instanceof ObjectMinCardinalityRestriction)
182                                                    return new ObjectMinCardinalityRestriction(number+1,r,transformToNegationNormalForm(c));
183                                            // >= n is transformed to <= n-1
184                                            else
185                                                    throw new RuntimeException("Conversion to negation normal form not supported for " + concept);                  
186                                    } else if(child instanceof Intersection) {
187                                            // wg. Negation wird Konjunktion zu Disjunktion
188                                            Union md = new Union();
189                                            for(Description c : child.getChildren()) {
190                                                    md.addChild(transformToNegationNormalForm(new Negation(c)));
191                                            }
192                                            return md;
193                                    } else if(child instanceof Union) {
194                                            Intersection mc = new Intersection();
195                                            for(Description c : child.getChildren()) {
196                                                    mc.addChild(transformToNegationNormalForm(new Negation(c)));
197                                            }                       
198                                            return mc;
199                                    } else
200                                            throw new RuntimeException("Conversion to negation normal form not supported for " + concept);
201                            }
202                    // keine Negation
203                    } else {
204    
205                            Description conceptClone = (Description) concept.clone();
206                            conceptClone.getChildren().clear();
207                            
208                            for(Description c : concept.getChildren()) {
209                                    conceptClone.addChild(transformToNegationNormalForm(c));
210                            }               
211                            
212                            return conceptClone;
213                    }
214            }
215            
216    
217            @SuppressWarnings("unused")
218            private boolean containsTop(Description concept) {
219                    for(Description c : concept.getChildren()) {
220                            if(c instanceof Thing)
221                                    return true;
222                    }
223                    return false;
224            }
225            
226            @SuppressWarnings("unused")
227            private boolean containsBottom(Description concept) {
228                    for(Description c : concept.getChildren()) {
229                            if(c instanceof Nothing)
230                                    return true;
231                    }
232                    return false;
233            }       
234            
235            // nimmt Konzept in Negationsnormalform und wendet äquivalenzerhaltende
236            // Regeln an, die TOP und BOTTOM aus Disjunktion/Konjunktion entfernen
237            public static Description applyEquivalenceRules(Description concept) {
238                    
239                    Description conceptClone = (Description) concept.clone();
240                    conceptClone.getChildren().clear();
241                    
242                    for(Description c : concept.getChildren()) {
243                            conceptClone.addChild(applyEquivalenceRules(c));
244                    }               
245                    
246                    // return conceptClone;         
247                    
248                    // TOP, BOTTOM in Disjunktion entfernen
249                    if(concept instanceof Union) {
250                            Iterator<Description> it = conceptClone.getChildren().iterator();
251                            while(it.hasNext()) {
252                                    Description c = it.next();
253                            // for(Concept c : concept.getChildren()) {
254                                    // TOP in Disjunktion => ganze Disjunktion äquivalent zu Top
255                                    if(c instanceof Thing)
256                                            return new Thing();
257                                    // BOTTOM in Disjunktion => entfernen
258                                    else if(c instanceof Nothing)
259                                            it.remove();
260                                            
261                            }
262                            
263                            // falls nur noch ein Kind übrig bleibt, dann entfällt
264                            // MultiDisjunction
265                            if(conceptClone.getChildren().size()==1)
266                                    return conceptClone.getChild(0);
267                            
268                            // falls keine Kinder übrig bleiben, dann war das letzte Kind
269                            // BOTTOM
270                            if(conceptClone.getChildren().size()==0)
271                                    return new Nothing();
272                            
273                    } else if(concept instanceof Intersection) {
274                            Iterator<Description> it = conceptClone.getChildren().iterator();
275                            while(it.hasNext()) {
276                                    Description c = it.next();
277                                    // TOP in Konjunktion => entfernen
278                                    if(c instanceof Thing)
279                                            it.remove();
280                                    // BOTTOM in Konjunktion => alles äquivalent zu BOTTOM
281                                    else if(c instanceof Nothing)
282                                            return new Nothing();                                                   
283                            }
284                            
285                            if(conceptClone.getChildren().size()==1)
286                                    return conceptClone.getChild(0);
287                            
288                            // falls keine Kinder übrig bleiben, dann war das letzte Kind
289                            // TOP
290                            if(conceptClone.getChildren().size()==0)
291                                    return new Thing();                                     
292                    }               
293                    
294                    return conceptClone;
295            }
296            
297            // TODO: aus Effizienzgründen könnte man noch eine nicht-rekursive Methode entwickeln, die
298            // nur die obere Ebene umwandelt
299            public static void transformToOrderedNegationNormalFormNonRecursive(Description concept, Comparator<Description> conceptComparator) {
300                    // onnfTimeNsStart = System.nanoTime();
301                    
302                    // Liste der Kinder sortieren
303                    Collections.sort(concept.getChildren(), conceptComparator);
304                    
305                    // onnfTimeNs += System.nanoTime() - onnfTimeNsStart;
306            }
307            
308            // wandelt ein Konzept in geordnete Negationsnormalform um;
309            // es wird angenommen, dass das Eingabekonzept in Negationsnormalform und
310            // "sauber" ist
311            public static void transformToOrderedForm(Description concept, Comparator<Description> conceptComparator) {
312                    
313                    // alle Kinderkonzepte in geordnete Negationsnormalform bringen
314                    for(Description child : concept.getChildren()) {
315                            transformToOrderedForm(child, conceptComparator);
316                    }
317                    
318                    onnfTimeNsStart = System.nanoTime();
319                    // Liste der Kinder sortieren
320                    Collections.sort(concept.getChildren(), conceptComparator);
321                    
322                    // Konvertierung von Liste in Array => Array sortieren => Rekonvertierung in Liste
323                    // List<Concept> childList = concept.getChildren();
324                    // Concept[] childArray = (Concept[]) childList.toArray(); 
325                    // Arrays.sort(childArray, conceptComparator);
326                    // childList = Arrays.asList(childArray);
327                    onnfTimeNs += System.nanoTime() - onnfTimeNsStart;
328            }
329            /*
330            public static Description transformToMultiClean(Description concept) {
331                    concept = transformToMulti(concept);
332                    cleanConcept(concept);
333                    return concept;
334            }
335            
336            // ersetzt einfache Disjunktionen/Konjunktionen durch Multi
337            public static Description transformToMulti(Description concept) {
338                    // alle Kinderkonzepte in geordnete Negationsnormalform bringen
339                    List<Description> multiChildren = new LinkedList<Description>();
340                    
341                    // es müssen veränderte Kinder entfernt und neu hinzugefügt werden
342                    // (einfache Zuweisung mit = funktioniert nicht, da die Pointer die gleichen
343                    // bleiben)
344                    Iterator<Description> it = concept.getChildren().iterator();
345                    while(it.hasNext()) {
346                            Description child = it.next();
347                            multiChildren.add(transformToMulti(child));
348                            it.remove();
349                    }
350                    
351                    for(Description multiChild : multiChildren)
352                            concept.addChild(multiChild);
353                            
354                    if(concept instanceof Disjunction)
355                            return new MultiDisjunction(concept.getChildren());
356                    
357                    if(concept instanceof Conjunction)
358                            return new MultiConjunction(concept.getChildren());
359                    
360                    return concept;
361            }
362            */
363            // liefert ein ev. verkürztes Konzept, wenn in Disjunktionen bzw.
364            // Konjunktionen Elemente mehrfach vorkommen
365            // (erstmal nicht-rekursiv implementiert)
366            public static Description getShortConceptNonRecursive(Description concept, ConceptComparator conceptComparator) {
367                    if(concept instanceof Union || concept instanceof Intersection) {
368                            // Verkürzung geschieht einfach durch einfügen in eine geordnete Menge
369                            Set<Description> newChildren = new TreeSet<Description>(conceptComparator);
370                            newChildren.addAll(concept.getChildren());
371                            // ev. geht das noch effizienter, wenn man keine neue Liste erstellen 
372                            // muss(?) => Listen erstellen dürfte allerdings sehr schnell gehen
373                            if(concept instanceof Intersection)
374                                    return new Intersection(new LinkedList<Description>(newChildren));
375                            else
376                                    return new Union(new LinkedList<Description>(newChildren));
377                    } else
378                            return concept;
379            }
380            
381            /**
382             * Tries to shorten a concept, e.g. male AND male is shortened to male. 
383             * @param concept The input concepts.
384             * @param conceptComparator A comparator for concepts.
385             * @return A shortened version of the concept (equal to the input concept if it cannot be shortened).
386             */
387            public static Description getShortConcept(Description concept, ConceptComparator conceptComparator) {
388                    shorteningTimeNsStart = System.nanoTime();
389                    // deep copy des Konzepts, da es nicht verändert werden darf
390                    // (Nachteil ist, dass auch Konzepte kopiert werden, bei denen sich gar
391                    // nichts ändert)
392                    Description clone = (Description) concept.clone();
393                    clone = getShortConcept(clone, conceptComparator, 0);
394                    // return getShortConcept(concept, conceptComparator, 0);
395                    shorteningTimeNs += System.nanoTime() - shorteningTimeNsStart;
396                    return clone;
397            }
398            
399            // das Eingabekonzept darf nicht modifiziert werden
400            private static Description getShortConcept(Description concept, ConceptComparator conceptComparator, int recDepth) {
401                    
402                    //if(recDepth==0)
403                    //      System.out.println(concept);
404                    
405                    // Kinder schrittweise ersetzen
406                    // TODO: effizienter wäre nur zu ersetzen, wenn sich etwas geändert hat
407                    List<Description> tmp = new LinkedList<Description>(); 
408                    Iterator<Description> it = concept.getChildren().iterator();
409                    while(it.hasNext()) {
410                            Description c = it.next();
411                            // concept.addChild(getShortConcept(c, conceptComparator));
412                            Description newChild = getShortConcept(c, conceptComparator,recDepth+1);
413                            // Vergleich, ob es sich genau um die gleichen Objekte handelt
414                            // (es wird explizit == statt equals verwendet)
415                            if(c != newChild) {
416                                    tmp.add(newChild);
417                                    it.remove();    
418                            }
419                    }
420                    for(Description child : tmp)
421                            concept.addChild(child);
422                    
423                    if(concept instanceof Union || concept instanceof Intersection) {
424                            // Verkürzung geschieht einfach durch einfügen in eine geordnete Menge
425                            SortedSet<Description> newChildren = new TreeSet<Description>(conceptComparator);
426                            newChildren.addAll(concept.getChildren());
427                            // falls sich Kinderliste auf ein Element reduziert hat, dann gebe nur
428                            // dieses Element zurück (umschließende Konjunktion/Disjunktion entfällt)
429                            if(newChildren.size()==1)
430                                    return newChildren.first();
431                            // ev. geht das noch effizienter, wenn man keine neue Liste erstellen 
432                            // muss(?) => Listen erstellen dürfte allerdings sehr schnell gehen
433                            if(concept instanceof Intersection)
434                                    return new Intersection(new LinkedList<Description>(newChildren));
435                            else
436                                    return new Union(new LinkedList<Description>(newChildren));
437                    } else
438                            return concept;
439            }       
440            
441            /**
442             * Method to determine, whether a class description is minimal,
443             * e.g. \forall r.\top (\equiv \top) or male \sqcup male are not
444             * minimal.     This method performs heuristic sanity checks (it will
445             * not try to find semantically equivalent shorter descriptions).
446             * @param description Input description.
447             * @return True if a superfluous construct has been found.
448             */
449            public static boolean isDescriptionMinimal(Description description) {
450                    ConceptComparator cc = new ConceptComparator();
451                    int length = description.getLength();
452                    int length2 = ConceptTransformation.getShortConcept(description, cc).getLength();
453                    if(length2 < length)
454                            return false;
455                    if(ConceptTransformation.findEquivalences(description))
456                            return false;
457                    return true;
458            }       
459     
460            private static boolean findEquivalences(Description description) {
461                    // \exists r.\bot \equiv \bot
462                    if(description instanceof ObjectSomeRestriction && description.getChild(0) instanceof Nothing)
463                            return true;
464                    // \forall r.\top \equiv \top
465                    if(description instanceof ObjectAllRestriction && description.getChild(0) instanceof Thing)
466                            return true;
467                    // check children
468                    for(Description child : description.getChildren()) {
469                            if(findEquivalences(child))
470                                    return true;
471                    }
472                    // false if none of the checks was successful
473                    return false;
474            }
475            
476            // replaces EXISTS hasChild.TOP with EXISTS hasChild.Person, 
477            // i.e. TOP is replaced by the range of the property; 
478            // this is semantically equivalent, but easier to read for some people
479            public static void replaceRange(Description description, AbstractReasonerComponent rs) {
480                    if(description instanceof ObjectSomeRestriction && description.getChild(0) instanceof Thing) {
481                            ObjectPropertyExpression p = ((ObjectSomeRestriction)description).getRole();
482                            if(p instanceof ObjectProperty) {
483                                    // replace TOP with range of propery
484                                    description.removeChild(description.getChild(0));
485                                    description.addChild(rs.getRange((ObjectProperty)p));
486                            }
487                    }
488                    
489                    for(Description child : description.getChildren()) {
490                            replaceRange(child, rs);
491                    }
492            }
493            
494            /**
495             * Tests whether a description is a subdescription in the sense that when
496             * parts of <code>description</code> can be removed to yield <code>subdescription</code>.
497             * 
498             * @param description A description.
499             * @param subDescription A potential subdescription.
500             * @return True if <code>subdescription</code> is indeed a sub description and false
501             * otherwise.
502             */
503            public static boolean isSubdescription(Description description, Description subDescription) {
504    //              if(description instanceof Thing) {
505    //                      return (subDescription instanceof Thing);
506    //              } else if(description instanceof Nothing) {
507    //                      return (subDescription instanceof Thing);
508    //              } else if(description instanceof NamedClass) {
509    //                      return ((subDescription instanceof NamedClass) && (((NamedClass)description).getName().equals(((NamedClass)subDescription).getName())));
510    //              }
511                    
512                    List<Description> children = description.getChildren();
513                    List<Description> subChildren = subDescription.getChildren();
514    
515                    // no children: both have to be equal
516                    if(children.size()==0) {
517                            return (descComp.compare(description, subDescription)==0);
518                    // one child: both have to be of the same class, type, and the first
519                    // child has to be sub description of the other child
520                    } else if(children.size()==1) {
521                            return (subChildren.size() == 1) && description.getClass().equals(subDescription.getClass()) && isSubdescription(children.get(0), subChildren.get(0));
522                    // intersection or union
523                    } else {
524                            // test whether subdescription corresponds to an element of the 
525                            // intersection/union
526                            if(subChildren.size()<2) {
527                                    for(Description child : children) {
528                                            if(isSubdescription(child, subDescription)) {
529                                                    return true;
530                                            }
531                                    }
532                                    return false;
533                            }
534                            
535                            // make sure that both are of the same type and subdescription actually has fewer children
536                            if(!description.getClass().equals(subDescription.getClass()) || subChildren.size() > children.size()) {
537                                    return false;
538                            }
539                            
540                            // comparing everything is quadratic; the faster linear variant (below)
541                            // using 
542                            
543                            for(Description subChild : subChildren) {
544                                    boolean foundMatch = false;
545                                    for(Description child : children) {
546                                            if(isSubdescription(child, subChild)) {
547                                                    foundMatch = true;
548                                                    break;
549                                            }
550                                    }
551                                    if(!foundMatch) {
552                                            return false;
553                                    }
554                            }
555                            
556                            return true;
557                            
558    //                      // method core; traverse the descriptions in linear time using ordered
559    //                      // normal form (TODO: does not always work e.g. A2 \sqcap (A1 \sqcup A3)
560                            // and A1 \sqcap A2 -> it won't find the A2 match because it has advanced
561                            // beyond it already)
562    //                      int j = 0;
563    //                      for(Description child : children) {
564    //                              if(isSubdescription(child, subChildren.get(j))) {
565    //                                      j++;
566    //                              }
567    //                              if(j == subChildren.size()) {
568    //                                      return true;
569    //                              }
570    //                      }
571    //                      // there is at least one child we could not match
572    //                      return false;
573                    }
574            }
575            
576            /**
577             * Counts occurrences of \forall in description.
578             * @param description A description.
579             * @return Number of \forall occurrences.
580             */
581            public static int getForallOccurences(Description description) {
582                    int count = 0;
583                    if(description instanceof ObjectAllRestriction) {
584                            count++;
585                    }
586                    for(Description child : description.getChildren()) {
587                            count += getForallOccurences(child);
588                    }
589                    return count;
590            }
591            
592            /**
593             * Gets the "contexts" of all \forall occurrences in a description. A context
594             * is a set of properties, i.e. in \exists hasChild.\exists hasBrother.\forall hasChild.male,
595             * the context of the only \forall occurrence is [hasChild, hasBrother, hasChild]. 
596             * @param description A description.
597             * @return Set of property contexts.
598             */
599            public static SortedSet<PropertyContext> getForallContexts(Description description) {
600                    return getForallContexts(description, new PropertyContext());
601            }
602            
603            private static SortedSet<PropertyContext> getForallContexts(Description description, PropertyContext currentContext) {
604                    // the context changes if we have a restriction
605                    if(description instanceof Restriction) {
606                            Property op = (Property) ((Restriction)description).getRestrictedPropertyExpression();
607                            // object restrictions
608                            if(op instanceof ObjectProperty) {
609                                    PropertyContext currentContextCopy = (PropertyContext) currentContext.clone();
610                                    // if we have an all-restriction, we return it; otherwise we call the child
611                                    // (if it exists)
612                                    if(description instanceof ObjectAllRestriction) {
613                                            currentContextCopy.add((ObjectProperty)op);
614    //                                      System.out.println("cc: " + currentContext);
615                                            TreeSet<PropertyContext> contexts = new TreeSet<PropertyContext>();
616                                            contexts.add(currentContextCopy);
617                                            contexts.addAll(getForallContexts(description.getChild(0), currentContextCopy));
618                                            return contexts;
619                                    // restriction with one child
620                                    } else if(description.getChildren().size()>0) {
621                                            currentContextCopy.add((ObjectProperty)op);
622                                            return getForallContexts(description.getChild(0), currentContextCopy);
623                                    // restrictions without a child (has value)
624                                    } else {
625                                            return new TreeSet<PropertyContext>();
626                                    }
627                            // we have a data restriction => no \forall can occur in those
628                            } else {
629                                    return new TreeSet<PropertyContext>();
630                            }
631                    // for non-restrictions, we collect contexts over all children
632                    } else {
633                            TreeSet<PropertyContext> contexts = new TreeSet<PropertyContext>();
634                            for(Description child : description.getChildren()) {
635    //                              System.out.println("testing child " + child + " " + currentContext);
636                                    contexts.addAll(getForallContexts(child, currentContext));
637                            }
638                            return contexts;
639                    }
640            }
641    }